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 = Coalgebra.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) : Coalgebra.Repr R a

An arbitrarily chosen representation.

Equations

• Coalgebra.Repr.arbitrary R a = Coalgebra.Repr.mk ⋯.choose Prod.fst Prod.snd ⋯

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 Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul

  The comultiplication is coassociative

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

  The counit satisfies the left counitality law

• lTensor_counit_comp_comul : LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.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 Coalgebra.comul) (Coalgebra.comul a)) = (LinearMap.lTensor A Coalgebra.comul) (Coalgebra.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 Coalgebra.comul) (Coalgebra.comul a)) = (LinearMap.rTensor A Coalgebra.comul) (Coalgebra.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 Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.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 Coalgebra.counit) (Coalgebra.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 Coalgebra.counit) (Coalgebra.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 : Coalgebra.Repr R a) : ∑ i ∈ repr.index, Coalgebra.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 : Coalgebra.Repr R a) : ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] Coalgebra.counit (repr.right i) = a ⊗ₜ[R] 1

@[simp]

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 : Coalgebra.Repr R a) (a₁ : (i : repr.ι) → Coalgebra.Repr R (repr.left i)) (a₂ : (i : repr.ι) → Coalgebra.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 : Coalgebra.Repr R a} : ∑ i ∈ repr.index, Coalgebra.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 : Coalgebra.Repr R a} : ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] Coalgebra.counit (repr.right i) = f a ⊗ₜ[R] 1

@[simp]

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 : Coalgebra.Repr R a} {a₁ : (i : repr.ι) → Coalgebra.Repr R (repr.left i)} {a₂ : (i : repr.ι) → Coalgebra.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)

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 = Coalgebra.mk ⋯ ⋯ ⋯

@[simp]

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

@[simp]

theorem CommSemiring.counit_apply (R : Type u) [CommSemiring R] (r : R) : Coalgebra.counit 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) : Coalgebra.comul r = (TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B)) (Coalgebra.comul r.1) + (TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B)) (Coalgebra.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) : Coalgebra.counit r = Coalgebra.counit r.1 + Coalgebra.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] : Coalgebra.comul ∘ₗ LinearMap.inl R A B = TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B) ∘ₗ Coalgebra.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] : Coalgebra.comul ∘ₗ LinearMap.inr R A B = TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B) ∘ₗ Coalgebra.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] : Coalgebra.comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ Coalgebra.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] : Coalgebra.comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ Coalgebra.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] : Coalgebra.counit ∘ₗ LinearMap.inr R A B = Coalgebra.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] : Coalgebra.counit ∘ₗ LinearMap.inl R A B = Coalgebra.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 = Coalgebra.mk ⋯ ⋯ ⋯

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) : Coalgebra.comul (DFinsupp.single i a) = (TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i)) (Coalgebra.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) : Coalgebra.counit (DFinsupp.single i a) = Coalgebra.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 : ι) : Coalgebra.comul ∘ₗ DFinsupp.lsingle i = TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i) ∘ₗ Coalgebra.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 : ι) : Coalgebra.comul ∘ₗ DFinsupp.lapply i = TensorProduct.map (DFinsupp.lapply i) (DFinsupp.lapply i) ∘ₗ Coalgebra.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 : ι) : Coalgebra.counit ∘ₗ DFinsupp.lsingle i = Coalgebra.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 = Coalgebra.mk ⋯ ⋯ ⋯

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) : Coalgebra.comul (Finsupp.single i a) = (TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i)) (Coalgebra.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) : Coalgebra.counit (Finsupp.single i a) = Coalgebra.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 : ι) : Coalgebra.comul ∘ₗ Finsupp.lsingle i = TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i) ∘ₗ Coalgebra.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 : ι) : Coalgebra.comul ∘ₗ Finsupp.lapply i = TensorProduct.map (Finsupp.lapply i) (Finsupp.lapply i) ∘ₗ Coalgebra.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 : ι) : Coalgebra.counit ∘ₗ Finsupp.lsingle i = Coalgebra.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 = Coalgebra.mk ⋯ ⋯ ⋯

noncomputable instance TensorProduct.instCoalgebraStruct {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : CoalgebraStruct R (TensorProduct R A B)

See Mathlib.RingTheory.Coalgebra.TensorProduct for the Coalgebra instance.

Equations

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

@[simp]

theorem TensorProduct.instCoalgebraStruct_counit {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Coalgebra.counit = LinearMap.mul' R R ∘ₗ TensorProduct.map Coalgebra.counit Coalgebra.counit

@[simp]

theorem TensorProduct.instCoalgebraStruct_comul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Coalgebra.comul = ↑(TensorProduct.tensorTensorTensorComm R A A B B) ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul