Coalgebras #

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

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

References #

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

source

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

Instances

source

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

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

Instances

source

theorem Coalgebra.coassoc {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [self : Coalgebra R A] :

↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul

The comultiplication is coassociative

source

theorem Coalgebra.rTensor_counit_comp_comul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [self : Coalgebra R A] :

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

The counit satisfies the left counitality law

source

theorem Coalgebra.lTensor_counit_comp_comul {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [self : Coalgebra R A] :

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

The counit satisfies the right counitality law

source

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

source

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

source

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

source

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

source

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

source

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 ⋯ ⋯ ⋯

source

@[simp]

theorem CommSemiring.comul_apply (R : Type u) [CommSemiring R] (r : R) :

Coalgebra.comul r = 1 ⊗ₜ[R] r

source

@[simp]

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

Coalgebra.counit r = r

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 ⋯ ⋯ ⋯

source

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.

source

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

source

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

source

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

source

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

source

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

source

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 ⋯ ⋯ ⋯

source

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)

The coalgebra instance will be defined in #11975, in Mathlib.RingTheory.Coalgebra.TensorProduct.

Equations

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

source

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

source

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

Documentation

Mathlib.RingTheory.Coalgebra.Basic

Coalgebras #

References #