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
• Finite pi functions: Pi.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

def RingTheory.LinearMap.termε : Lean.ParserDescr

The counit of the coalgebra

def RingTheory.LinearMap.termδ : Lean.ParserDescr

The comultiplication 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.

def Coalgebra.termℛ : Lean.ParserDescr

An arbitrarily chosen representation.

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 : ↑(_root_.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) : (_root_.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) : (_root_.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] : ↑(_root_.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))

theorem Coalgebra.sum_counit_smul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] {a : A} (𝓡 : Repr R a) : ∑ x ∈ 𝓡.index, counit (𝓡.left x) • 𝓡.right x = a

theorem Coalgebra.lift_lsmul_comp_counit_comp_comul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id

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

@[implicit_reducible]

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

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

@[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

@[implicit_reducible]

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)

@[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

@[implicit_reducible]

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)

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)

@[implicit_reducible]

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

@[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 : ι) → CoalgebraStruct R (A i)] (i : ι) (a : A i) : (CoalgebraStruct.comul fun₀ | 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 : ι) → CoalgebraStruct R (A i)] (i : ι) (a : A i) : (CoalgebraStruct.counit fun₀ | 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 : ι) → CoalgebraStruct 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 : ι) → CoalgebraStruct 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 : ι) → CoalgebraStruct R (A i)] (i : ι) : CoalgebraStruct.counit ∘ₗ lsingle i = CoalgebraStruct.counit

@[implicit_reducible]

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.

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)

@[implicit_reducible]

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

@[simp]

theorem Finsupp.comul_single (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (i : ι) (a : A) : (CoalgebraStruct.comul fun₀ | 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] [CoalgebraStruct R A] (i : ι) (a : A) : (CoalgebraStruct.counit fun₀ | 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] [CoalgebraStruct 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] [CoalgebraStruct 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] [CoalgebraStruct R A] (i : ι) : CoalgebraStruct.counit ∘ₗ lsingle i = CoalgebraStruct.counit

@[implicit_reducible]

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.

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)

@[implicit_reducible]

instance Pi.instCoalgebraStruct {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] : CoalgebraStruct R ((i : n) → A i)

@[simp]

theorem Pi.comul_single {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (i : n) (a : A i) : CoalgebraStruct.comul (single i a) = (TensorProduct.map (LinearMap.single R A i) (LinearMap.single R A i)) (CoalgebraStruct.comul a)

@[simp]

theorem Pi.counit_single {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (i : n) (a : A i) : CoalgebraStruct.counit (single i a) = CoalgebraStruct.counit a

theorem Pi.comul_comp_single {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (i : n) : CoalgebraStruct.comul ∘ₗ LinearMap.single R A i = TensorProduct.map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ CoalgebraStruct.comul

theorem Pi.comul_comp_proj {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (i : n) : CoalgebraStruct.comul ∘ₗ LinearMap.proj i = TensorProduct.map (LinearMap.proj i) (LinearMap.proj i) ∘ₗ CoalgebraStruct.comul

@[simp]

theorem Pi.counit_comp_single {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (i : n) : CoalgebraStruct.counit ∘ₗ LinearMap.single R A i = CoalgebraStruct.counit

theorem Pi.counit_comp_dFinsuppCoeFnLinearMap {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] : CoalgebraStruct.counit ∘ₗ DFinsupp.coeFnLinearMap R = CoalgebraStruct.counit

@[simp]

theorem Pi.counit_coe_dFinsupp {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (x : Π₀ (i : n), A i) : CoalgebraStruct.counit ⇑x = CoalgebraStruct.counit x

theorem Pi.comul_comp_dFinsuppCoeFnLinearMap {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] : CoalgebraStruct.comul ∘ₗ DFinsupp.coeFnLinearMap R = TensorProduct.map (DFinsupp.coeFnLinearMap R) (DFinsupp.coeFnLinearMap R) ∘ₗ CoalgebraStruct.comul

@[simp]

theorem Pi.comul_coe_dFinsupp {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → CoalgebraStruct R (A i)] (x : Π₀ (i : n), A i) : CoalgebraStruct.comul ⇑x = (TensorProduct.map (DFinsupp.coeFnLinearMap R) (DFinsupp.coeFnLinearMap R)) (CoalgebraStruct.comul x)

theorem Pi.counit_comp_finsuppLcoeFun {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {M : Type u_4} [AddCommMonoid M] [Module R M] [CoalgebraStruct R M] : CoalgebraStruct.counit ∘ₗ Finsupp.lcoeFun = CoalgebraStruct.counit

@[simp]

theorem Pi.counit_coe_finsupp {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {M : Type u_4} [AddCommMonoid M] [Module R M] [CoalgebraStruct R M] (x : n →₀ M) : CoalgebraStruct.counit ⇑x = CoalgebraStruct.counit x

theorem Pi.comul_comp_finsuppLcoeFun {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {M : Type u_4} [AddCommMonoid M] [Module R M] [CoalgebraStruct R M] : CoalgebraStruct.comul ∘ₗ Finsupp.lcoeFun = TensorProduct.map Finsupp.lcoeFun Finsupp.lcoeFun ∘ₗ CoalgebraStruct.comul

@[simp]

theorem Pi.comul_coe_finsupp {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {M : Type u_4} [AddCommMonoid M] [Module R M] [CoalgebraStruct R M] (x : n →₀ M) : CoalgebraStruct.comul ⇑x = (TensorProduct.map Finsupp.lcoeFun Finsupp.lcoeFun) (CoalgebraStruct.comul x)

@[implicit_reducible]

instance Pi.instCoalgebra {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → Coalgebra R (A i)] : Coalgebra R ((i : n) → A i)

The R-module whose elements are functions Π i, A i for finite n 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.

instance Pi.instIsCocomm {R : Type u_1} {n : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] {A : n → Type u_3} [(i : n) → AddCommMonoid (A i)] [(i : n) → Module R (A i)] [(i : n) → Coalgebra R (A i)] [∀ (i : n), Coalgebra.IsCocomm R (A i)] : Coalgebra.IsCocomm R ((i : n) → A i)

@[reducible, inline]

abbrev Equiv.coalgebraStruct (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid B] [Module R B] [CoalgebraStruct R B] (e : A ≃ B) : CoalgebraStruct R A

Transfer CoalgebraStruct across an Equiv.

@[reducible, inline]

abbrev Equiv.coalgebra (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid B] [Module R B] [Coalgebra R B] (e : A ≃ B) : Coalgebra R A

Transfer Coalgebra across an Equiv.

theorem Equiv.coalgebraIsCocomm (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid B] [Module R B] [Coalgebra R B] [Coalgebra.IsCocomm R B] (e : A ≃ B) : Coalgebra.IsCocomm R A

Transfer Coalgebra.IsCocomm across an Equiv.