Documentation

Mathlib.Algebra.Category.Grp.Preadditive

The category of additive commutative groups is preadditive. #

instance AddCommGrp.instAddHom {M N : AddCommGrp} :

Add (M ⟶ N)

Equations

@[simp]

theorem AddCommGrp.hom_add {M N : AddCommGrp} (f g : M ⟶ N) :

Hom.hom (f + g) = Hom.hom f + Hom.hom g

theorem AddCommGrp.hom_add_apply {P Q : AddCommGrp} (f g : P ⟶ Q) (x : ↑P) :

(CategoryTheory.ConcreteCategory.hom (f + g)) x = (CategoryTheory.ConcreteCategory.hom f) x + (CategoryTheory.ConcreteCategory.hom g) x

instance AddCommGrp.instZeroHom_1 {M N : AddCommGrp} :

Zero (M ⟶ N)

Equations

@[simp]

theorem AddCommGrp.hom_zero {M N : AddCommGrp} :

instance AddCommGrp.instSMulNatHom {M N : AddCommGrp} :

SMul ℕ (M ⟶ N)

Equations

@[simp]

theorem AddCommGrp.hom_nsmul {M N : AddCommGrp} (n : ℕ) (f : M ⟶ N) :

Hom.hom (n • f) = n • Hom.hom f

instance AddCommGrp.instNegHom {M N : AddCommGrp} :

Neg (M ⟶ N)

Equations

@[simp]

theorem AddCommGrp.hom_neg {M N : AddCommGrp} (f : M ⟶ N) :

Hom.hom (-f) = -Hom.hom f

instance AddCommGrp.instSubHom {M N : AddCommGrp} :

Sub (M ⟶ N)

Equations

@[simp]

theorem AddCommGrp.hom_sub {M N : AddCommGrp} (f g : M ⟶ N) :

Hom.hom (f - g) = Hom.hom f - Hom.hom g

instance AddCommGrp.instSMulIntHom {M N : AddCommGrp} :

SMul ℤ (M ⟶ N)

Equations

@[simp]

theorem AddCommGrp.hom_zsmul {M N : AddCommGrp} (n : ℕ) (f : M ⟶ N) :

Hom.hom (n • f) = n • Hom.hom f

instance AddCommGrp.instAddCommGroupHom (P Q : AddCommGrp) :

AddCommGroup (P ⟶ Q)

Equations

instance AddCommGrp.instPreadditive :

CategoryTheory.Preadditive AddCommGrp

Equations

def AddCommGrp.homAddEquiv {M N : AddCommGrp} :

(M ⟶ N) ≃+ (↑M →+ ↑N)

AddCommGrp.Hom.hom bundled as an additive equivalence.

Equations

Instances For

@[simp]

theorem AddCommGrp.homAddEquiv_symm_apply_hom {M N : AddCommGrp} (a✝ : CategoryTheory.ToHom M N) :

Hom.hom (homAddEquiv.symm a✝) = a✝

@[simp]

theorem AddCommGrp.homAddEquiv_apply {M N : AddCommGrp} (a✝ : M ⟶ N) :

homAddEquiv a✝ = CategoryTheory.ConcreteCategory.hom a✝