Documentation

Mathlib.Algebra.Category.Grp.Preadditive

The category of additive commutative groups is preadditive. #

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

                  AddCommGrpCat.Hom.hom bundled as an additive equivalence.

                  Equations
                    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✝