Documentation

Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

The preadditive category structure on the localized category #

In this file, it is shown that if W : MorphismProperty C has a left calculus of fractions, and C is preadditive, then the localized category is preadditive, and the localization functor is additive.

Let L : C ⥤ D be a localization functor for W. We first construct an abelian group structure on L.obj X ⟶ L.obj Y for X and Y in C. The addition is defined using representatives of two morphisms in L as left fractions with the same denominator thanks to the lemmas in CategoryTheory.Localization.CalculusOfFractions.Fractions. As L is essentially surjective, we finally transport these abelian group structures to X' ⟶ Y' for all X' and Y' in D.

Preadditive category instances are defined on the categories W.Localization (and W.Localization') under the assumption the W has a left calculus of fractions. (It would be easy to deduce from the results in this file that if W has a right calculus of fractions, then the localized category can also be equipped with a preadditive structure, but only one of these two constructions can be made an instance!)

@[reducible, inline]
abbrev CategoryTheory.MorphismProperty.LeftFraction.neg {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : W.LeftFraction X Y) :
W.LeftFraction X Y

The opposite of a left fraction.

Equations
Instances For
    @[reducible, inline]
    abbrev CategoryTheory.MorphismProperty.LeftFraction₂.add {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : W.LeftFraction₂ X Y) :
    W.LeftFraction X Y

    The sum of two left fractions with the same denominator.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.MorphismProperty.LeftFraction₂.symm_add {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : W.LeftFraction₂ X Y) :
      φ.symm.add = φ.add
      @[simp]
      theorem CategoryTheory.MorphismProperty.LeftFraction₂.map_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : W.LeftFraction₂ X Y) (F : CategoryTheory.Functor C D) (hF : W.IsInvertedBy F) [CategoryTheory.Preadditive D] [F.Additive] :
      φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF

      The definitions in this section (like neg' and add') should never be used directly. These are auxiliary definitions in order to construct the preadditive structure Localization.preadditive (which is made irreducible). The user should only rely on the fact that the localization functor is additive, as this completely determines the preadditive structure on the localized category when there is a calculus of left fractions.

      noncomputable def CategoryTheory.Localization.Preadditive.neg' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f : L.obj X L.obj Y) :
      L.obj X L.obj Y

      The opposite of a map L.obj X ⟶ L.obj Y when L : C ⥤ D is a localization functor, C is preadditive and there is a left calculus of fractions.

      Equations
      Instances For
        theorem CategoryTheory.Localization.Preadditive.neg'_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f : L.obj X L.obj Y) (φ : W.LeftFraction X Y) (hφ : f = φ.map L ) :
        noncomputable def CategoryTheory.Localization.Preadditive.add' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f₁ : L.obj X L.obj Y) (f₂ : L.obj X L.obj Y) :
        L.obj X L.obj Y

        The addition of two maps L.obj X ⟶ L.obj Y when L : C ⥤ D is a localization functor, C is preadditive and there is a left calculus of fractions.

        Equations
        Instances For
          theorem CategoryTheory.Localization.Preadditive.add'_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f₁ : L.obj X L.obj Y) (f₂ : L.obj X L.obj Y) (φ : W.LeftFraction₂ X Y) (hφ₁ : f₁ = φ.fst.map L ) (hφ₂ : f₂ = φ.snd.map L ) :
          CategoryTheory.Localization.Preadditive.add' W f₁ f₂ = φ.add.map L
          theorem CategoryTheory.Localization.Preadditive.add'_comm {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f₁ : L.obj X L.obj Y) (f₂ : L.obj X L.obj Y) :
          theorem CategoryTheory.Localization.Preadditive.add'_zero {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f : L.obj X L.obj Y) :
          theorem CategoryTheory.Localization.Preadditive.zero_add' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f : L.obj X L.obj Y) :
          @[simp]
          theorem CategoryTheory.Localization.Preadditive.add'_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f₁ : X Y) (f₂ : X Y) :
          CategoryTheory.Localization.Preadditive.add' W (L.map f₁) (L.map f₂) = L.map (f₁ + f₂)
          noncomputable def CategoryTheory.Localization.Preadditive.addCommGroup' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] (X : C) (Y : C) :
          AddCommGroup (L.obj X L.obj Y)

          The abelian group structure on L.obj X ⟶ L.obj Y when L : C ⥤ D is a localization functor, C is preadditive and there is a left calculus of fractions.

          Equations
          Instances For
            def CategoryTheory.Localization.Preadditive.homEquiv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {L : CategoryTheory.Functor C D} {X : C} {Y : C} {X' : D} {Y' : D} (eX : L.obj X X') (eY : L.obj Y Y') :
            (X' Y') (L.obj X L.obj Y)

            The bijection (X' ⟶ Y') ≃ (L.obj X ⟶ L.obj Y) induced by isomorphisms eX : L.obj X ≅ X' and eY : L.obj Y ≅ Y'.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def CategoryTheory.Localization.Preadditive.add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {X' : D} {Y' : D} (eX : L.obj X X') (eY : L.obj Y Y') (f₁ : X' Y') (f₂ : X' Y') :
              X' Y'

              The addition of morphisms in D, when L : C ⥤ D is a localization functor, C is preadditive and there is a left calculus of fractions.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem CategoryTheory.Localization.Preadditive.add_comp_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {Z : C} {X' : D} {Y' : D} {Z' : D} (eX : L.obj X X') (eY : L.obj Y Y') (eZ : L.obj Z✝ Z') (f₁ : X' Y') (f₂ : X' Y') (g : Y' Z') {Z : D} (h : Z' Z) :
                theorem CategoryTheory.Localization.Preadditive.add_comp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {Z : C} {X' : D} {Y' : D} {Z' : D} (eX : L.obj X X') (eY : L.obj Y Y') (eZ : L.obj Z Z') (f₁ : X' Y') (f₂ : X' Y') (g : Y' Z') :
                theorem CategoryTheory.Localization.Preadditive.comp_add_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {Z : C} {X' : D} {Y' : D} {Z' : D} (eX : L.obj X X') (eY : L.obj Y Y') (eZ : L.obj Z✝ Z') (f : X' Y') (g₁ : Y' Z') (g₂ : Y' Z') {Z : D} (h : Z' Z) :
                theorem CategoryTheory.Localization.Preadditive.comp_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {Z : C} {X' : D} {Y' : D} {Z' : D} (eX : L.obj X X') (eY : L.obj Y Y') (eZ : L.obj Z Z') (f : X' Y') (g₁ : Y' Z') (g₂ : Y' Z') :
                theorem CategoryTheory.Localization.Preadditive.add_eq_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {X' : D} {Y' : D} (eX : L.obj X X') (eY : L.obj Y Y') {X'' : C} {Y'' : C} (eX' : L.obj X'' X') (eY' : L.obj Y'' Y') (f₁ : X' Y') (f₂ : X' Y') :
                noncomputable def CategoryTheory.Localization.Preadditive.addCommGroup {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] (X' : D) (Y' : D) :

                The abelian group structure on morphisms in D, when L : C ⥤ D is a localization functor, C is preadditive and there is a left calculus of fractions.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem CategoryTheory.Localization.Preadditive.add_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive C] {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} {X' : D} {Y' : D} (eX : L.obj X X') (eY : L.obj Y Y') (f₁ : X' Y') (f₂ : X' Y') :
                  f₁ + f₂ = CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂
                  theorem CategoryTheory.Localization.Preadditive.map_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X : C} {Y : C} (f₁ : X Y) (f₂ : X Y) :
                  L.map (f₁ + f₂) = L.map f₁ + L.map f₂
                  @[irreducible]

                  The preadditive structure on D, when L : C ⥤ D is a localization functor, C is preadditive and there is a left calculus of fractions.

                  Equations
                  Instances For
                    instance CategoryTheory.Localization.instAdditiveLocalization'Q' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.HasLocalization] :
                    W.Q'.Additive
                    Equations
                    • =