F-coalgebras

An F-coalgebra for an endofunctor F on Type is a type S together with a structure map out : S → F S.

This is the categorical dual of MonadAlgebra: where an algebra collapses a functor layer, a coalgebra observes one layer of structure from a state.

Main definitions

• Coalg F S: typeclass packaging out : S → F S.
• Coalg.Hom S₁ S₂: a function S₁ → S₂ that commutes with the structure maps (Functor.map f ∘ out = out ∘ f). Equipped with coercion, id, comp.

Relationship to Mathlib and Poly

CategoryTheory.Endofunctor.Coalgebra in Mathlib defines coalgebras for endofunctors on an arbitrary category. This file instead provides a Lean-native typeclass for Type-endofunctors, following the style of MonadAlgebra. The Type-level definition suffices for the interaction framework, where the step functors (StepOver Γ, Machine.StepFun) are polynomial endofunctors on Type in the sense of the Poly book (Spivak, 2022).

class Coalg (F : Type u → Type v) (S : Type u) : Type (max u v)

An F-coalgebra on S is a structure map out : S → F S.

Named Coalg to avoid collision with Mathlib.RingTheory.Coalgebra. This is the dual of MonadAlgebra. No [Functor F] constraint is imposed on the class itself so that the definition applies to arbitrary type-level maps.

• out : S → F S

Coalg morphisms

structure Coalg.Hom (F : Type u → Type v) [Functor F] (S₁ S₂ : Type u) [Coalg F S₁] [Coalg F S₂] : Type u

A coalgebra morphism between F-coalgebras on S₁ and S₂ is a function that commutes with the structure maps:

      out
  S₁ -----> F S₁
  |          |
  f        F f
  |          |
  v          v
  S₂ -----> F S₂
      out

In the interaction framework, coalgebra morphisms between processes correspond to forward simulations that preserve step structure.

• toFun : S₁ → S₂

  The underlying function between state spaces.

• comm : Functor.map self.toFun ∘ out = out ∘ self.toFun

  The commutativity condition: F.map f ∘ out = out ∘ f.

@[implicit_reducible]

instance Coalg.Hom.instFunLike {F : Type u → Type v} [Functor F] {S₁ S₂ : Type u} [Coalg F S₁] [Coalg F S₂] : FunLike (Hom F S₁ S₂) S₁ S₂

theorem Coalg.Hom.ext {F : Type u → Type v} [Functor F] {S₁ S₂ : Type u} [Coalg F S₁] [Coalg F S₂] {f g : Hom F S₁ S₂} (h : ∀ (x : S₁), f x = g x) : f = g

theorem Coalg.Hom.ext_iff {F : Type u → Type v} [Functor F] {S₁ S₂ : Type u} [Coalg F S₁] [Coalg F S₂] {f g : Hom F S₁ S₂} : f = g ↔ ∀ (x : S₁), f x = g x

def Coalg.Hom.id {F : Type u → Type v} [Functor F] {S₁ : Type u} [Coalg F S₁] [LawfulFunctor F] : Hom F S₁ S₁

The identity coalgebra morphism.

def Coalg.Hom.comp {F : Type u → Type v} [Functor F] {S₁ S₂ S₃ : Type u} [Coalg F S₁] [Coalg F S₂] [Coalg F S₃] [LawfulFunctor F] (g : Hom F S₂ S₃) (f : Hom F S₁ S₂) : Hom F S₁ S₃

Composition of coalgebra morphisms.

@[simp]

theorem Coalg.Hom.id_apply {F : Type u → Type v} [Functor F] {S₁ : Type u} [Coalg F S₁] [LawfulFunctor F] (x : S₁) : id x = x

@[simp]

theorem Coalg.Hom.comp_apply {F : Type u → Type v} [Functor F] {S₁ S₂ S₃ : Type u} [Coalg F S₁] [Coalg F S₂] [Coalg F S₃] [LawfulFunctor F] (g : Hom F S₂ S₃) (f : Hom F S₁ S₂) (x : S₁) : (g.comp f) x = g (f x)