Theorems · Definition · category theory
MonCat.ofHom
{X Y : Type u} → [inst : Monoid X] → [inst_1 : Monoid Y] → (X →* Y) → (MonCat.of X ⟶ MonCat.of Y)Typecheck a MonoidHom as a morphism in MonCat.
- Defined in
- Mathlib.Algebra.Category.MonCat.Basic
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
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.
- Quiver.Homstatement · cited by 32,603
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- MonCatstatement · cited by 127
- MonCat.ofstatement · cited by 22
- CategoryTheory.ConcreteCategory.ofHomproof · cited by 18
Cited by44
Results whose statement or proof uses this declaration.
- CategoryTheory.yonedaMonObjproof · cited by 12
- CategoryTheory.yonedaMonproof · cited by 10
- CategoryTheory.SubmonoidFunctor.toFunctorproof · cited by 8
- MonCat.shrinkFunctorproof · cited by 6
- AddMonCat.equivalenceproof · cited by 6
- CategoryTheory.SubmonoidFunctor.ιproof · cited by 4
- CategoryTheory.SubmonoidFunctor.liftproof · cited by 4
- MonCat.shrinkFunctorMapproof · cited by 2
- MonCat.uliftFunctorproof · cited by 2
- MonCat.Colimits.coconeMorphismproof · cited by 2
- MulEquiv.toMonCatIsoproof · cited by 2
- MonCat.adjoinOneproof · cited by 2