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

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

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

Instances For

source

theorem Coalgebra.Repr.eq {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] {a : A} (self : Coalgebra.Repr R a) :

∑ 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

source

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 ⋯

Instances For

source

def Coalgebra.termℛ :

Lean.ParserDescr

An arbitrarily chosen representation.

Equations

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

Instances For

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} :

∀ {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : 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} :

∀ {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : 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} :

∀ {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : 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

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

source

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

source

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

source

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

source

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

source

@[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 : F) (g : F) (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)

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

source

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

source

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

source

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

source

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

source

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

source

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

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)

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

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 #