Theorems · Definition · category theory
CategoryTheory.Comonad.Coalgebra.A
{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {G : CategoryTheory.Comonad C} → G.Coalgebra → CThe underlying object associated to a coalgebra.
- Defined in
- Mathlib.CategoryTheory.Monad.Algebra
- Cited by
- 75 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Comonadstatement and proof · cited by 125
- CategoryTheory.Comonad.Coalgebrastatement and proof · cited by 114
Cited by101
Results whose statement or proof uses this declaration.
- CategoryTheory.Comonad.Coalgebra.astatement · cited by 48
- CategoryTheory.Comonad.Coalgebra.Hom.fstatement · cited by 46
- CategoryTheory.Comonad.forgetproof · cited by 29
- CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalenceproof · cited by 13
- CategoryTheory.Comonad.Coalgebra.isoMkstatement and proof · cited by 6
- CategoryTheory.Comonad.CofreeEqualizer.bottomMapstatement and proof · cited by 4
- CategoryTheory.Comonad.CofreeEqualizer.topMapstatement · cited by 4
- CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunctionstatement and proof · cited by 4
- CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquivstatement and proof · cited by 4
- CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObjstatement and proof · cited by 4
- CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparisonstatement and proof · cited by 4
- CategoryTheory.coalgebraEquivOverproof · cited by 4