The category of additive commutative groups is preadditive. #
Equations
@[simp]
Equations
- AddCommGrp.instZeroHom_1 = { zero := AddCommGrp.ofHom 0 }
Equations
- AddCommGrp.instSMulNatHom = { smul := fun (n : ℕ) (f : M ⟶ N) => AddCommGrp.ofHom (n • AddCommGrp.Hom.hom f) }
@[simp]
Equations
- AddCommGrp.instNegHom = { neg := fun (f : M ⟶ N) => AddCommGrp.ofHom (-AddCommGrp.Hom.hom f) }
Equations
@[simp]
Equations
- AddCommGrp.instSMulIntHom = { smul := fun (n : ℤ) (f : M ⟶ N) => AddCommGrp.ofHom (n • AddCommGrp.Hom.hom f) }
@[simp]
Equations
- AddCommGrp.instPreadditive = { homGroup := inferInstance, add_comp := AddCommGrp.instPreadditive.proof_1, comp_add := AddCommGrp.instPreadditive.proof_2 }
AddCommGrp.Hom.hom
bundled as an additive equivalence.
Equations
- AddCommGrp.homAddEquiv = { toEquiv := CategoryTheory.ConcreteCategory.homEquiv, map_add' := ⋯ }
Instances For
@[simp]