The category of additive commutative groups is preadditive.

@[implicit_reducible]

instance AddCommGrpCat.instAddHom {M N : AddCommGrpCat} : Add (M ⟶ N)

Equations

• AddCommGrpCat.instAddHom = { add := fun (f g : M ⟶ N) => AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f + AddCommGrpCat.Hom.hom g) }

@[simp]

theorem AddCommGrpCat.hom_add {M N : AddCommGrpCat} (f g : M ⟶ N) : Hom.hom (f + g) = Hom.hom f + Hom.hom g

theorem AddCommGrpCat.hom_add_apply {P Q : AddCommGrpCat} (f g : P ⟶ Q) (x : ↑P) : (CategoryTheory.ConcreteCategory.hom (f + g)) x = (CategoryTheory.ConcreteCategory.hom f) x + (CategoryTheory.ConcreteCategory.hom g) x

@[implicit_reducible]

instance AddCommGrpCat.instZeroHom_1 {M N : AddCommGrpCat} : Zero (M ⟶ N)

Equations

• AddCommGrpCat.instZeroHom_1 = { zero := AddCommGrpCat.ofHom 0 }

@[simp]

theorem AddCommGrpCat.hom_zero {M N : AddCommGrpCat} : Hom.hom 0 = 0

@[implicit_reducible]

instance AddCommGrpCat.instSMulNatHom {M N : AddCommGrpCat} : SMul ℕ (M ⟶ N)

Equations

• AddCommGrpCat.instSMulNatHom = { smul := fun (n : ℕ) (f : M ⟶ N) => AddCommGrpCat.ofHom (n • AddCommGrpCat.Hom.hom f) }

@[simp]

theorem AddCommGrpCat.hom_nsmul {M N : AddCommGrpCat} (n : ℕ) (f : M ⟶ N) : Hom.hom (n • f) = n • Hom.hom f

@[implicit_reducible]

instance AddCommGrpCat.instNegHom {M N : AddCommGrpCat} : Neg (M ⟶ N)

Equations

• AddCommGrpCat.instNegHom = { neg := fun (f : M ⟶ N) => AddCommGrpCat.ofHom (-AddCommGrpCat.Hom.hom f) }

@[simp]

theorem AddCommGrpCat.hom_neg {M N : AddCommGrpCat} (f : M ⟶ N) : Hom.hom (-f) = -Hom.hom f

@[implicit_reducible]

instance AddCommGrpCat.instSubHom {M N : AddCommGrpCat} : Sub (M ⟶ N)

Equations

• AddCommGrpCat.instSubHom = { sub := fun (f g : M ⟶ N) => AddCommGrpCat.ofHom (AddCommGrpCat.Hom.hom f - AddCommGrpCat.Hom.hom g) }

@[simp]

theorem AddCommGrpCat.hom_sub {M N : AddCommGrpCat} (f g : M ⟶ N) : Hom.hom (f - g) = Hom.hom f - Hom.hom g

@[implicit_reducible]

instance AddCommGrpCat.instSMulIntHom {M N : AddCommGrpCat} : SMul ℤ (M ⟶ N)

Equations

• AddCommGrpCat.instSMulIntHom = { smul := fun (n : ℤ) (f : M ⟶ N) => AddCommGrpCat.ofHom (n • AddCommGrpCat.Hom.hom f) }

@[simp]

theorem AddCommGrpCat.hom_zsmul {M N : AddCommGrpCat} (n : ℤ) (f : M ⟶ N) : Hom.hom (n • f) = n • Hom.hom f

@[implicit_reducible]

instance AddCommGrpCat.instAddCommGroupHom (P Q : AddCommGrpCat) : AddCommGroup (P ⟶ Q)

Equations

• P.instAddCommGroupHom Q = Function.Injective.addCommGroup AddCommGrpCat.Hom.hom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance AddCommGrpCat.instPreadditive : CategoryTheory.Preadditive AddCommGrpCat

Equations

• AddCommGrpCat.instPreadditive = { homGroup := inferInstance, add_comp := AddCommGrpCat.instPreadditive._proof_2, comp_add := AddCommGrpCat.instPreadditive._proof_3 }

def AddCommGrpCat.homAddEquiv {M N : AddCommGrpCat} : (M ⟶ N) ≃+ (↑M →+ ↑N)

AddCommGrpCat.Hom.hom bundled as an additive equivalence.

Equations

• AddCommGrpCat.homAddEquiv = { toEquiv := CategoryTheory.ConcreteCategory.homEquiv, map_add' := ⋯ }

@[simp]

theorem AddCommGrpCat.homAddEquiv_apply {M N : AddCommGrpCat} (a✝ : M ⟶ N) : homAddEquiv a✝ = CategoryTheory.ConcreteCategory.hom a✝

@[simp]

theorem AddCommGrpCat.homAddEquiv_symm_apply_hom {M N : AddCommGrpCat} (a✝ : CategoryTheory.ToHom M N) : Hom.hom (homAddEquiv.symm a✝) = a✝