Theorems · Definition · category theory
AddCommGrpCat.ofHom
{X Y : Type u} →
[inst : AddCommGroup X] → [inst_1 : AddCommGroup Y] → (X →+ Y) → (AddCommGrpCat.of X ⟶ AddCommGrpCat.of Y)Typecheck an AddMonoidHom as a morphism in AddCommGrpCat.
- Defined in
- Mathlib.Algebra.Category.Grp.Basic
- Cited by
- 72 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommGroupAddCommGroup
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
- AddCommGroupstatement and proof · cited by 12,871
- AddMonoidHomstatement and proof · cited by 3,230
- AddCommGrpCatstatement · cited by 462
- AddCommGrpCat.ofstatement · cited by 97
- CategoryTheory.ConcreteCategory.ofHomproof · cited by 18
Cited by121
Results whose statement or proof uses this declaration.
- PresheafOfModules.presheafproof · cited by 85
- PresheafOfModules.toPresheafproof · cited by 24
- CategoryTheory.preadditiveYonedaproof · cited by 17
- ModuleCat.smulproof · cited by 13
- AddCommGrpCat.freeproof · cited by 12
- CochainComplex.HomComplexproof · cited by 10
- CategoryTheory.preadditiveCoyonedaproof · cited by 10
- AddCommGrpCat.uliftFunctorproof · cited by 7
- CategoryTheory.ShortComplex.abLeftHomologyDataproof · cited by 7
- AddCommGrpCat.binaryProductLimitConeproof · cited by 6
- AddCommGrpCat.coyonedaproof · cited by 5
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δproof · cited by 5