Structures · Category theory
CategoryTheory.ComonObj
A comonoid object internal to a monoidal category. When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".
- Defined in
- Mathlib.CategoryTheory.Monoidal.Comon_
- Shape
- One type argument · adds counit, comul, counit_comul, comul_counit, comul_assoc
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances3
- ModuleCat
- CategoryTheory.WideSubcategory
- SFinKer
How is a type an instance?
Loading the hierarchy index…
Assumed by51
- CategoryTheory.ComonObj.comul
- CategoryTheory.ComonObj.counit
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj
- CategoryTheory.ComonObj.counit_comul
- CategoryTheory.Conv.mul_eq
- CoalgCat.ofComonObjCoalgebraStruct_comul
- CategoryTheory.Conv.one_eq
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj
- CategoryTheory.ComonObj.comul_counit
- CoalgCat.ofComonObjCoalgebraStruct_counit
- CategoryTheory.ComonObj.comul_assoc
- CategoryTheory.ComonObj.comul_counit_assoc
- CategoryTheory.ComonObj.comul_assoc_flip
- CategoryTheory.Functor.obj.ε_def
- CategoryTheory.ComonObj.counit_comul_hom
- CategoryTheory.Comon.tensorObj_comul'
- CategoryTheory.ComonObj.comul_assoc_assoc
- CategoryTheory.counit_eq_toUnit
- CategoryTheory.ComonObj.comul_assoc_flip_assoc
- CategoryTheory.Functor.obj.Δ_def
- CategoryTheory.Comon.tensorObj_comul
- CategoryTheory.ComonObj.counit_comul_assoc
- CategoryTheory.ComonObj.comul_counit_hom
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_X
- CategoryTheory.Functor.obj.Δ_def_assoc
- CategoryTheory.ComonObj.comul_counit_hom_assoc
- CategoryTheory.Conv.instMonoid
- CategoryTheory.Functor.obj.ε_def_assoc
- CategoryTheory.Comon.tensorObj_counit
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_counit
- CategoryTheory.instIsComonHomComp
- CategoryTheory.instIsComonHomId
- CategoryTheory.Comon.instComonObjTensorObj
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom
- CategoryTheory.MorphismProperty.comul_hom
- CoalgCat.ofComonObj
- CategoryTheory.instIsComonHomInvOfHom
- CategoryTheory.ComonObj.counit_comul_hom_assoc
- CoalgCat.ofComonObjCoalgebraStruct
- CategoryTheory.Conv.instMul
- CategoryTheory.instIsComonHomInv
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_comul
- CategoryTheory.MorphismProperty.instComonObjWideSubcategoryOfIsStableUnderComonoidObj
- CategoryTheory.comul_eq_lift
- CategoryTheory.MorphismProperty.instIsCommComonObjWideSubcategoryOfObj
- CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj
- CategoryTheory.Functor.map.instIsComon_Hom
- CategoryTheory.instIsCommComonObjTensorObj
- CategoryTheory.Functor.obj.instComonObj
- CategoryTheory.MorphismProperty.counit_hom
Ancestors0
No ancestors.