Theorems · Definition · category theory
CategoryTheory.Mon.Hom.hom
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
[inst_1 : CategoryTheory.MonoidalCategory C] → {M N : CategoryTheory.Mon C} → M.Hom N → (M.X ⟶ N.X)The underlying morphism
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mon
- Cited by
- 200 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 11 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.MonoidalCategorystatement and proof · cited by 3,095
- CategoryTheory.Monstatement and proof · cited by 465
- CategoryTheory.Mon.Xstatement · cited by 329
- CategoryTheory.Mon.Homstatement and proof · cited by 9
Cited by216
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.mapMonproof · cited by 38
- CategoryTheory.Mon.forgetproof · cited by 33
- CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalproof · cited by 15
- MonObj.mopEquivproof · cited by 14
- CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedproof · cited by 11
- CategoryTheory.yonedaMonproof · cited by 10
- commBialgCatEquivComonCommAlgCatproof · cited by 9
- CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorproof · cited by 9
- CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseproof · cited by 9
- CategoryTheory.Monad.monToMonadproof · cited by 7
- commHopfAlgCatEquivCogrpCommAlgCatproof · cited by 6
- CategoryTheory.Mon.Hom.extstatement and proof · cited by 6
Showing the 200 most cited of 216.