Documentation

Mathlib.Algebra.Category.Grp.Preadditive

The category of additive commutative groups is preadditive. #

source
@[instance_reducible]
instance AddCommGrpCat.instAddHom {M N : AddCommGrpCat} :
Add (M ⟶ N)
source
@[simp]
theorem AddCommGrpCat.hom_add {M N : AddCommGrpCat} (f g : M ⟶ N) :
Hom.hom (f + g) = Hom.hom f + Hom.hom g
source
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
source
@[instance_reducible]
instance AddCommGrpCat.instZeroHom_1 {M N : AddCommGrpCat} :
Zero (M ⟶ N)
source
@[simp]
theorem AddCommGrpCat.hom_zero {M N : AddCommGrpCat} :
Hom.hom 0 = 0
source
@[instance_reducible]
instance AddCommGrpCat.instSMulNatHom {M N : AddCommGrpCat} :
SMul ℕ (M ⟶ N)
source
@[simp]
theorem AddCommGrpCat.hom_nsmul {M N : AddCommGrpCat} (n : ℕ) (f : M ⟶ N) :
Hom.hom (n • f) = n • Hom.hom f
source
@[instance_reducible]
instance AddCommGrpCat.instNegHom {M N : AddCommGrpCat} :
Neg (M ⟶ N)
source
@[simp]
theorem AddCommGrpCat.hom_neg {M N : AddCommGrpCat} (f : M ⟶ N) :
Hom.hom (-f) = -Hom.hom f
source
@[instance_reducible]
instance AddCommGrpCat.instSubHom {M N : AddCommGrpCat} :
Sub (M ⟶ N)
source
@[simp]
theorem AddCommGrpCat.hom_sub {M N : AddCommGrpCat} (f g : M ⟶ N) :
Hom.hom (f - g) = Hom.hom f - Hom.hom g
source
@[instance_reducible]
instance AddCommGrpCat.instSMulIntHom {M N : AddCommGrpCat} :
SMul ℤ (M ⟶ N)
source
@[simp]
theorem AddCommGrpCat.hom_zsmul {M N : AddCommGrpCat} (n : ℤ) (f : M ⟶ N) :
Hom.hom (n • f) = n • Hom.hom f
source
@[instance_reducible]
instance AddCommGrpCat.instAddCommGroupHom (P Q : AddCommGrpCat) :
AddCommGroup (P ⟶ Q)
source
@[instance_reducible]
instance AddCommGrpCat.instPreadditive :
CategoryTheory.Preadditive AddCommGrpCat
source
def AddCommGrpCat.homAddEquiv {M N : AddCommGrpCat} :
(M ⟶ N) ≃+ (↑M →+ ↑N)

AddCommGrpCat.Hom.hom bundled as an additive equivalence.

Instances For
    source
    @[simp]
    theorem AddCommGrpCat.homAddEquiv_apply {M N : AddCommGrpCat} (a✝ : M ⟶ N) :
    homAddEquiv a✝ = CategoryTheory.ConcreteCategory.hom a✝
    source
    @[simp]
    theorem AddCommGrpCat.homAddEquiv_symm_apply_hom {M N : AddCommGrpCat} (a✝ : CategoryTheory.ToHom M N) :
    Hom.hom (homAddEquiv.symm a✝) = a✝