Coalgebras

In this file we define Coalgebra, and provide instances for:

• Commutative semirings: CommSemiring.toCoalgebra
• Binary products: Prod.instCoalgebra
• Finitely supported functions: DFinsupp.instCoalgebra, Finsupp.instCoalgebra

References

• https://en.wikipedia.org/wiki/Coalgebra

class CoalgebraStruct (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] : Type (max u v)

Data fields for Coalgebra, to allow API to be constructed before proving Coalgebra.coassoc.

See Coalgebra for documentation.

• comul : A →ₗ[R] TensorProduct R A A

  The comultiplication of the coalgebra

• counit : A →ₗ[R] R

  The counit of the coalgebra

structure Coalgebra.Repr (R : Type u) {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (a : A) : Type (max (u_1 + 1) v)

A representation of an element a of a coalgebra A is a finite sum of pure tensors ∑ xᵢ ⊗ yᵢ that is equal to comul a.

• ι : Type u_1

  the indexing type of a representation of comul a

• index : Finset self.ι

  the finite indexing set of a representation of comul a

• left : self.ι → A

  the first coordinate of a representation of comul a

• right : self.ι → A

  the second coordinate of a representation of comul a

• eq : ∑ i ∈ self.index, self.left i ⊗ₜ[R] self.right i = comul a

  comul a is equal to a finite sum of some pure tensors

noncomputable def Coalgebra.Repr.arbitrary (R : Type u) {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (a : A) : Repr R a

An arbitrarily chosen representation.

Equations

• Coalgebra.Repr.arbitrary R a = { ι := A × A, index := ⋯.choose, left := Prod.fst, right := Prod.snd, eq := ⋯ }

def Coalgebra.termℛ : Lean.ParserDescr

An arbitrarily chosen representation.

Equations

• Coalgebra.termℛ = Lean.ParserDescr.node `Coalgebra.termℛ 1024 (Lean.ParserDescr.symbol "ℛ")

class Coalgebra (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] extends CoalgebraStruct R A : Type (max u v)

A coalgebra over a commutative (semi)ring R is an R-module equipped with a coassociative comultiplication Δ and a counit ε obeying the left and right counitality laws.

• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul

  The comultiplication is coassociative

• rTensor_counit_comp_comul : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1

  The counit satisfies the left counitality law

• lTensor_counit_comp_comul : LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1

  The counit satisfies the right counitality law

@[simp]

theorem Coalgebra.coassoc_apply {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (a : A) : (TensorProduct.assoc R A A A) ((LinearMap.rTensor A comul) (comul a)) = (LinearMap.lTensor A comul) (comul a)

@[simp]

theorem Coalgebra.coassoc_symm_apply {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (a : A) : (TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A comul) (comul a)) = (LinearMap.rTensor A comul) (comul a)

@[simp]

theorem Coalgebra.coassoc_symm {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A comul ∘ₗ comul = LinearMap.rTensor A comul ∘ₗ comul

@[simp]

theorem Coalgebra.rTensor_counit_comul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (a : A) : (LinearMap.rTensor A counit) (comul a) = 1 ⊗ₜ[R] a

@[simp]

theorem Coalgebra.lTensor_counit_comul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (a : A) : (LinearMap.lTensor A counit) (comul a) = a ⊗ₜ[R] 1

@[simp]

theorem Coalgebra.sum_counit_tmul_eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a : A} (repr : Repr R a) : ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a

@[simp]

theorem Coalgebra.sum_tmul_counit_eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a : A} (repr : Repr R a) : ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1

theorem Coalgebra.sum_tmul_tmul_eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a : A} (repr : Repr R a) (a₁ : (i : repr.ι) → Repr R (repr.left i)) (a₂ : (i : repr.ι) → Repr R (repr.right i)) : ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i = ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j

@[simp]

theorem Coalgebra.sum_counit_tmul_map_eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {B : Type u_1} [AddCommMonoid B] [Module R B] {F : Type u_2} [FunLike F A B] [LinearMapClass F R A B] (f : F) (a : A) {repr : Repr R a} : ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

@[simp]

theorem Coalgebra.sum_map_tmul_counit_eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {B : Type u_1} [AddCommMonoid B] [Module R B] {F : Type u_2} [FunLike F A B] [LinearMapClass F R A B] (f : F) (a : A) {repr : Repr R a} : ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1

theorem Coalgebra.sum_map_tmul_tmul_eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {B : Type u_1} [AddCommMonoid B] [Module R B] {F : Type u_2} [FunLike F A B] [LinearMapClass F R A B] (f g h : F) (a : A) {repr : Repr R a} {a₁ : (i : repr.ι) → Repr R (repr.left i)} {a₂ : (i : repr.ι) → Repr R (repr.right i)} : ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j) = ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)

class Coalgebra.IsCocomm (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : Prop

A coalgebra A is cocommutative if its comultiplication δ : A → A ⊗ A commutes with the swapping β : A ⊗ A ≃ A ⊗ A of the factors in the tensor product.

• comm_comp_comul : ↑(TensorProduct.comm R A A) ∘ₗ comul = comul

@[simp]

theorem Coalgebra.comm_comp_comul (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] [IsCocomm R A] : ↑(TensorProduct.comm R A A) ∘ₗ comul = comul

@[simp]

theorem Coalgebra.comm_comul (R : Type u) {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] [IsCocomm R A] (a : A) : (TensorProduct.comm R A A) (comul a) = comul a

noncomputable instance CommSemiring.toCoalgebra (R : Type u) [CommSemiring R] : Coalgebra R R

Every commutative (semi)ring is a coalgebra over itself, with Δ r = 1 ⊗ₜ r.

Equations

• CommSemiring.toCoalgebra R = { comul := (TensorProduct.mk R R R) 1, counit := LinearMap.id, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

@[simp]

theorem CommSemiring.comul_apply (R : Type u) [CommSemiring R] (r : R) : CoalgebraStruct.comul r = 1 ⊗ₜ[R] r

@[simp]

theorem CommSemiring.counit_apply (R : Type u) [CommSemiring R] (r : R) : CoalgebraStruct.counit r = r

instance CommSemiring.instIsCocomm (R : Type u) [CommSemiring R] : Coalgebra.IsCocomm R R

noncomputable instance Prod.instCoalgebraStruct (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct R (A × B)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Prod.comul_apply (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (r : A × B) : CoalgebraStruct.comul r = (TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B)) (CoalgebraStruct.comul r.1) + (TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B)) (CoalgebraStruct.comul r.2)

@[simp]

theorem Prod.counit_apply (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (r : A × B) : CoalgebraStruct.counit r = CoalgebraStruct.counit r.1 + CoalgebraStruct.counit r.2

theorem Prod.comul_comp_inl (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.inl R A B = TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B) ∘ₗ CoalgebraStruct.comul

theorem Prod.comul_comp_inr (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.inr R A B = TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B) ∘ₗ CoalgebraStruct.comul

theorem Prod.comul_comp_fst (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ CoalgebraStruct.comul

theorem Prod.comul_comp_snd (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ CoalgebraStruct.comul

@[simp]

theorem Prod.counit_comp_inr (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.counit ∘ₗ LinearMap.inr R A B = CoalgebraStruct.counit

@[simp]

theorem Prod.counit_comp_inl (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.counit ∘ₗ LinearMap.inl R A B = CoalgebraStruct.counit

noncomputable instance Prod.instCoalgebra (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : Coalgebra R (A × B)

Equations

• Prod.instCoalgebra R A B = { toCoalgebraStruct := Prod.instCoalgebraStruct R A B, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

instance Prod.instIsCocomm (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] [Coalgebra.IsCocomm R A] [Coalgebra.IsCocomm R B] : Coalgebra.IsCocomm R (A × B)

noncomputable instance DFinsupp.instCoalgebraStruct (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] : CoalgebraStruct R (Π₀ (i : ι), A i)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DFinsupp.comul_single (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) (a : A i) : CoalgebraStruct.comul (single i a) = (TensorProduct.map (lsingle i) (lsingle i)) (CoalgebraStruct.comul a)

@[simp]

theorem DFinsupp.counit_single (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) (a : A i) : CoalgebraStruct.counit (single i a) = CoalgebraStruct.counit a

theorem DFinsupp.comul_comp_lsingle (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) : CoalgebraStruct.comul ∘ₗ lsingle i = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ CoalgebraStruct.comul

theorem DFinsupp.comul_comp_lapply (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) : CoalgebraStruct.comul ∘ₗ lapply i = TensorProduct.map (lapply i) (lapply i) ∘ₗ CoalgebraStruct.comul

@[simp]

theorem DFinsupp.counit_comp_lsingle (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) : CoalgebraStruct.counit ∘ₗ lsingle i = CoalgebraStruct.counit

noncomputable instance DFinsupp.instCoalgebra (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] : Coalgebra R (Π₀ (i : ι), A i)

The R-module whose elements are dependent functions (i : ι) → A i which are zero on all but finitely many elements of ι has a coalgebra structure.

The coproduct Δ is given by Δ(fᵢ a) = fᵢ a₁ ⊗ fᵢ a₂ where Δ(a) = a₁ ⊗ a₂ and the counit ε by ε(fᵢ a) = ε(a), where fᵢ a is the function sending i to a and all other elements of ι to zero.

Equations

• DFinsupp.instCoalgebra R ι A = { toCoalgebraStruct := DFinsupp.instCoalgebraStruct R ι A, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

instance DFinsupp.instIsCocomm (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] [∀ (i : ι), Coalgebra.IsCocomm R (A i)] : Coalgebra.IsCocomm R (Π₀ (i : ι), A i)

noncomputable instance Finsupp.instCoalgebraStruct (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : CoalgebraStruct R (ι →₀ A)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.comul_single (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) (a : A) : CoalgebraStruct.comul (single i a) = (TensorProduct.map (lsingle i) (lsingle i)) (CoalgebraStruct.comul a)

@[simp]

theorem Finsupp.counit_single (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) (a : A) : CoalgebraStruct.counit (single i a) = CoalgebraStruct.counit a

theorem Finsupp.comul_comp_lsingle (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) : CoalgebraStruct.comul ∘ₗ lsingle i = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ CoalgebraStruct.comul

theorem Finsupp.comul_comp_lapply (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) : CoalgebraStruct.comul ∘ₗ lapply i = TensorProduct.map (lapply i) (lapply i) ∘ₗ CoalgebraStruct.comul

@[simp]

theorem Finsupp.counit_comp_lsingle (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) : CoalgebraStruct.counit ∘ₗ lsingle i = CoalgebraStruct.counit

noncomputable instance Finsupp.instCoalgebra (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : Coalgebra R (ι →₀ A)

The R-module whose elements are functions ι → A which are zero on all but finitely many elements of ι has a coalgebra structure. The coproduct Δ is given by Δ(fᵢ a) = fᵢ a₁ ⊗ fᵢ a₂ where Δ(a) = a₁ ⊗ a₂ and the counit ε by ε(fᵢ a) = ε(a), where fᵢ a is the function sending i to a and all other elements of ι to zero.

Equations

• Finsupp.instCoalgebra R ι A = { toCoalgebraStruct := Finsupp.instCoalgebraStruct R ι A, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

instance Finsupp.instIsCocomm (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] [Coalgebra.IsCocomm R A] : Coalgebra.IsCocomm R (ι →₀ A)