Theorems · Definition · category theory
AddGrpCat.ofHom
{X Y : Type u} → [inst : AddGroup X] → [inst_1 : AddGroup Y] → (X →+ Y) → (AddGrpCat.of X ⟶ AddGrpCat.of Y)Typecheck an AddMonoidHom as a morphism in AddGrpCat.
- Defined in
- Mathlib.Algebra.Category.Grp.Basic
- Cited by
- 17 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
- AddGroupstatement and proof · cited by 4,410
- AddMonoidHomstatement and proof · cited by 3,230
- AddGrpCatstatement · cited by 80
- AddGrpCat.ofstatement · cited by 23
- CategoryTheory.ConcreteCategory.ofHomproof · cited by 18
Cited by29
Results whose statement or proof uses this declaration.
- CategoryTheory.yonedaAddGrpObjproof · cited by 9
- CategoryTheory.yonedaAddGrpproof · cited by 7
- AddEquiv.toAddGrpIsoproof · cited by 4
- GrpCat.toAddGrpproof · cited by 4
- ProfiniteAddGrp.ProfiniteCompletion.etaproof · cited by 3
- AddGrpCat.uliftFunctorproof · cited by 2
- AddGrpCat.binaryProductLimitConeproof · cited by 2
- FiniteAddGrp.ofHomproof · cited by 1
- AddEquiv.toAddGrpIso_homstatement · cited by 0
- AddEquiv.toAddGrpIso_invstatement · cited by 0
- AddGrpCat.ofHom_applystatement · cited by 0
- AddGrpCat.ofHom_compstatement · cited by 0