Theorems · Theorem · category theory
CoalgCat.ofComonObjCoalgebraStruct_counit
∀ {R : Type u} [inst : CommRing R] (X : ModuleCat R) [inst_1 : CategoryTheory.ComonObj X],
CoalgebraStruct.counit = ModuleCat.Hom.hom CategoryTheory.ComonObj.counit- Cited by
- 3 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapstatement · cited by 10,215
- ModuleCatstatement and proof · cited by 1,429
- CategoryTheory.MonoidalCategoryStruct.tensorUnitstatement · cited by 1,384
- ModuleCat.carrierstatement · cited by 997
- ModuleCat.Hom.homstatement · cited by 341
- CoalgebraStruct.counitstatement and proof · cited by 108
- CategoryTheory.ComonObj.counitstatement · cited by 67
- CategoryTheory.ComonObjstatement and proof · cited by 48
Cited by3
Results whose statement or proof uses this declaration.
- 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