Coalgebra structure on the quotient by a coideal

Main definitions

• Submodule.IsCoideal I : the submodule I : Submodule R C is a coideal.
• Coalgebra.Quotient.mkQCoalgHom : Submodule.mkQ as a coalgebra homomorphism.

Main results

• Coalgebra instance on C ⧸ I when [I.IsCoideal].

class Submodule.IsCoideal {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) : Prop

An R-submodule I of an R-coalgebra C is a coideal if the counit vanishes on I and the comultiplication descends through the module quotient C ⧸ I.

• counit_eq_zero ⦃x : C⦄ : x ∈ I → CoalgebraStruct.counit x = 0
• map_mkQ_comul_eq_zero ⦃x : C⦄ : x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (CoalgebraStruct.comul x) = 0

theorem Submodule.isCoideal_iff {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) : I.IsCoideal ↔ (∀ ⦃x : C⦄, x ∈ I → CoalgebraStruct.counit x = 0) ∧ ∀ ⦃x : C⦄, x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (CoalgebraStruct.comul x) = 0

theorem Submodule.isCoideal_iff_comul_mem {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) : I.IsCoideal ↔ (∀ x ∈ I, CoalgebraStruct.counit x = 0) ∧ ∀ x ∈ I, CoalgebraStruct.comul x ∈ (LinearMap.lTensor C I.subtype).range ⊔ (LinearMap.rTensor C I.subtype).range

A submodule is a coideal iff the counit vanishes on it and its comultiplication image lies in I ⊗ C + C ⊗ I, the textbook form of the coideal condition.

@[implicit_reducible]

instance Coalgebra.Quotient.instCoalgebraStructQuotientSubmodule {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] : CoalgebraStruct R (C ⧸ I)

Equations

• Coalgebra.Quotient.instCoalgebraStructQuotientSubmodule I = { comul := I.liftQ (TensorProduct.map I.mkQ I.mkQ ∘ₗ CoalgebraStruct.comul) ⋯, counit := I.liftQ CoalgebraStruct.counit ⋯ }

theorem Coalgebra.Quotient.comul_comp_mkQ {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] : comul ∘ₗ I.mkQ = TensorProduct.map I.mkQ I.mkQ ∘ₗ comul

theorem Coalgebra.Quotient.counit_comp_mkQ {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] : counit ∘ₗ I.mkQ = counit

@[simp]

theorem Coalgebra.Quotient.counit_mk {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] (x : C) : counit (Submodule.Quotient.mk x) = counit x

@[simp]

theorem Coalgebra.Quotient.comul_mk {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] (x : C) : comul (Submodule.Quotient.mk x) = (TensorProduct.map I.mkQ I.mkQ) (comul x)

def Coalgebra.Quotient.mkQCoalgHom {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] : C →ₗc[R] C ⧸ I

Submodule.mkQ as a coalgebra homomorphism.

Equations

• Coalgebra.Quotient.mkQCoalgHom I = { toLinearMap := I.mkQ, counit_comp := ⋯, map_comp_comul := ⋯ }

@[simp]

theorem Coalgebra.Quotient.mkQCoalgHom_apply {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [CoalgebraStruct R C] (I : Submodule R C) [I.IsCoideal] (x : C) : (mkQCoalgHom I) x = Submodule.Quotient.mk x

@[implicit_reducible]

instance Coalgebra.Quotient.instQuotientSubmodule {R : Type u_1} {C : Type u_2} [CommRing R] [AddCommGroup C] [Module R C] [Coalgebra R C] (I : Submodule R C) [I.IsCoideal] : Coalgebra R (C ⧸ I)

Equations

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