Mathlib Map

Theorems · Definition · category theory

AddMonCat.ofHom

{X Y : Type u} → [inst : AddMonoid X] → [inst_1 : AddMonoid Y] → (X →+ Y) → (AddMonCat.of X ⟶ AddMonCat.of Y)

Typecheck an AddMonoidHom as a morphism in AddMonCat.

Defined in
Mathlib.Algebra.Category.MonCat.Basic
Cited by
17 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext, Quot.sound
Assumes
AddMonoidAddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.yonedaAddMonObj · cited by 12CategoryTheory.yonedaAddM…CategoryTheory.yonedaAddMon · cited by 8CategoryTheory.yonedaAddM…AddMonCat.equivalence · cited by 6AddMonCat.equivalenceAddEquiv.toAddMonCatIso · cited by 2AddEquiv.toAddMonCatIsoAddMonCat.adjoinZero · cited by 2AddMonCat.adjoinZeroAddMonCat.uliftFunctor · cited by 2AddMonCat.uliftFunctorAddMonCat.FilteredColimits.coconeMorphism · cited by 1FilteredColimits.coconeMo…AddCommMonCat.forget₂_map_ofHom · cited by 0AddCommMonCat.forget₂_map…AddMonCat.HasLimits.limitCone · cited by 0HasLimits.limitConeAddMonCat.HasLimits.limitConeIsLimit · cited by 0HasLimits.limitConeIsLimitAddEquiv.toAddMonCatIso_hom · cited by 0AddEquiv.toAddMonCatIso_h…AddEquiv.toAddMonCatIso_inv · cited by 0AddEquiv.toAddMonCatIso_i…AddMonCat.ofHom_apply · cited by 0AddMonCat.ofHom_applyAddMonCat.ofHom_comp · cited by 0AddMonCat.ofHom_compAddMonCat.ofHom_hom · cited by 0AddMonCat.ofHom_homQuiver.Hom · cited by 32603Quiver.HomAddMonoidHom · cited by 3230AddMonoidHomAddMonoid · cited by 2864AddMonoidAddMonCat · cited by 71AddMonCatCategoryTheory.ConcreteCategory.ofHom · cited by 18ConcreteCategory.ofHomAddMonCat.of · cited by 16AddMonCat.ofAddMonCat.ofHomCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by28

Results whose statement or proof uses this declaration.