Structures · Algebra
Submodule.IsCoideal
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.
- Defined in
- Mathlib.RingTheory.Coalgebra.Quotient
- Shape
- One type argument · adds counit_eq_zero, map_mkQ_comul_eq_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- Bialgebra.Quotient.comulAlgHom
- Bialgebra.Quotient.counitAlgHom
- Bialgebra.Quotient.mkBialgHom
- Coalgebra.Quotient.mkQCoalgHom
- Bialgebra.Quotient.counitAlgHom.congr_simp
- Bialgebra.Quotient.instQuotientIdeal
- Coalgebra.Quotient.comul_mk
- Bialgebra.Quotient.comul_mk
- Bialgebra.Quotient.counit_mk
- Bialgebra.Quotient.mkBialgHom_apply
- Coalgebra.Quotient.mkQCoalgHom_apply
- Coalgebra.Quotient.counit_comp_mkQ
- Bialgebra.Quotient.comul_comp_mkₐ
- Coalgebra.Quotient.comul_comp_mkQ
- Coalgebra.Quotient.counit_mk
- Submodule.IsCoideal.counit_eq_zero
- Coalgebra.Quotient.instCoalgebraStructQuotientSubmodule
- Bialgebra.Quotient.comulAlgHom.congr_simp
- Submodule.IsCoideal.map_mkQ_comul_eq_zero
- Bialgebra.Quotient.counit_comp_mkₐ
- Coalgebra.Quotient.instQuotientSubmodule
Ancestors0
No ancestors.