Coalgebra structures on flat subcoalgebras

A flat subcoalgebra of a flat coalgebra inherits comultiplication and counit from the ambient coalgebra: flatness makes the inclusion of its tensor square injective. The induced structure is supplied as a definition, with formulas relating its operations to those of the ambient coalgebra. This construction supplies the coalgebra underlying a flat Hopf subalgebra.

For D : TauCeti.Subcoalgebra R C, the induced coalgebra has carrier D.toSubmodule; use D.coalgebra for the structure and D.comul_apply and D.counit_apply for its operations.

References

• M. E. Sweedler, Hopf Algebras (1969), Chapter 2.

noncomputable def TauCeti.Subcoalgebra.comulLinearMap {R : Type u_1} {C : Type u_2} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Flat R C] [Module.Flat R ↥D.toSubmodule] : ↥D.toSubmodule →ₗ[R] TensorProduct R ↥D.toSubmodule ↥D.toSubmodule

The comultiplication of a flat subcoalgebra, valued in its own tensor square.

Equations

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

@[simp]

theorem TauCeti.Subcoalgebra.map_subtype_comulLinearMap {R : Type u_1} {C : Type u_2} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Flat R C] [Module.Flat R ↥D.toSubmodule] (x : ↥D.toSubmodule) : (TensorProduct.map D.toSubmodule.subtype D.toSubmodule.subtype) (D.comulLinearMap x) = CoalgebraStruct.comul ↑x

Including the comultiplication of a subcoalgebra recovers the ambient comultiplication.

@[instance_reducible]

noncomputable def TauCeti.Subcoalgebra.coalgebra {R : Type u_1} {C : Type u_2} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Flat R C] [Module.Flat R ↥D.toSubmodule] : Coalgebra R ↥D.toSubmodule

A flat subcoalgebra of a flat coalgebra inherits a coalgebra structure. This is a definition rather than a global instance, so its carrier remains a submodule.

Equations

• D.coalgebra = { comul := D.comulLinearMap, counit := CoalgebraStruct.counit ∘ₗ D.toSubmodule.subtype, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

@[simp]

theorem TauCeti.Subcoalgebra.comul_apply {R : Type u_1} {C : Type u_2} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Flat R C] [Module.Flat R ↥D.toSubmodule] (x : ↥D.toSubmodule) : CoalgebraStruct.comul x = D.comulLinearMap x

The comultiplication of the induced coalgebra is the restricted linear map.

@[simp]

theorem TauCeti.Subcoalgebra.counit_apply {R : Type u_1} {C : Type u_2} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] (D : Subcoalgebra R C) [Module.Flat R C] [Module.Flat R ↥D.toSubmodule] (x : ↥D.toSubmodule) : CoalgebraStruct.counit x = CoalgebraStruct.counit ↑x

The counit of the induced coalgebra is the ambient counit.