Theorems · Definition · category theory
CoalgCat.comonEquivalence
(R : Type u) → [inst : CommRing R] → CoalgCat R ≌ CategoryTheory.Comon (ModuleCat R)
The natural category equivalence between R-coalgebras and comonoid objects in the
category of R-modules.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functor.compproof · cited by 6,529
- CategoryTheory.Functor.idproof · cited by 3,333
- ModuleCatstatement and proof · cited by 1,429
- CategoryTheory.Iso.reflproof · cited by 727
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.NatIso.ofComponentsproof · cited by 178
- CategoryTheory.Comonstatement and proof · cited by 125
- CoalgCatstatement and proof · cited by 63
- CoalgCat.toComonproof · cited by 5
Cited by13
Results whose statement or proof uses this declaration.
- CoalgCat.MonoidalCategoryAux.tensorObj_comulproof · cited by 0
- CoalgCat.comonEquivalence_counitIsostatement and proof · cited by 0
- CoalgCat.comonEquivalence_functorstatement and proof · cited by 0
- CoalgCat.comonEquivalence_inversestatement and proof · cited by 0
- CoalgCat.comonEquivalence_unitIsostatement and proof · cited by 0
- CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMapproof · cited by 0
- CoalgCat.MonoidalCategoryAux.comul_tensorObjproof · cited by 0
- CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_rightproof · cited by 0
- CoalgCat.MonoidalCategoryAux.counit_tensorObjproof · cited by 0
- CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_leftproof · cited by 0
- CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_rightproof · cited by 0
- CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMapproof · cited by 0