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!)

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

The opposite of a left fraction.

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

      The sum of two left fractions with the same denominator.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.LeftFraction₂.symm_add {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y) :
          φ.symm.add = φ.add
          source
          @[simp]
          theorem CategoryTheory.MorphismProperty.LeftFraction₂.map_add {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y) (F : Functor C D) (hF : W.IsInvertedBy F) [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.

          source
          noncomputable def CategoryTheory.Localization.Preadditive.neg' {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X 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
              source
              theorem CategoryTheory.Localization.Preadditive.neg'_eq {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction X Y) (hφ : f = φ.map L ⋯) :
              neg' W f = φ.neg.map L ⋯
              source
              noncomputable def CategoryTheory.Localization.Preadditive.add' {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ 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
                  source
                  theorem CategoryTheory.Localization.Preadditive.add'_eq {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction₂ X Y) (hφ₁ : f₁ = φ.fst.map L ⋯) (hφ₂ : f₂ = φ.snd.map L ⋯) :
                  add' W f₁ f₂ = φ.add.map L ⋯
                  source
                  theorem CategoryTheory.Localization.Preadditive.add'_comm {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) :
                  add' W f₁ f₂ = add' W f₂ f₁
                  source
                  theorem CategoryTheory.Localization.Preadditive.add'_zero {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) :
                  add' W f (L.map 0) = f
                  source
                  theorem CategoryTheory.Localization.Preadditive.zero_add' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) :
                  add' W (L.map 0) f = f
                  source
                  theorem CategoryTheory.Localization.Preadditive.neg'_add'_self {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) :
                  add' W (neg' W f) f = L.map 0
                  source
                  theorem CategoryTheory.Localization.Preadditive.add'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ f₃ : L.obj X ⟶ L.obj Y) :
                  add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
                  source
                  @[simp]
                  theorem CategoryTheory.Localization.Preadditive.add'_comp {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z) :
                  CategoryStruct.comp (add' W f₁ f₂) g = add' W (CategoryStruct.comp f₁ g) (CategoryStruct.comp f₂ g)
                  source
                  @[simp]
                  theorem CategoryTheory.Localization.Preadditive.add'_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z) {Z✝ : D} (h : L.obj Z ⟶ Z✝) :
                  CategoryStruct.comp (add' W f₁ f₂) (CategoryStruct.comp g h) = CategoryStruct.comp (add' W (CategoryStruct.comp f₁ g) (CategoryStruct.comp f₂ g)) h
                  source
                  @[simp]
                  theorem CategoryTheory.Localization.Preadditive.comp_add' {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} (f : L.obj X ⟶ L.obj Y) (g₁ g₂ : L.obj Y ⟶ L.obj Z) :
                  CategoryStruct.comp f (add' W g₁ g₂) = add' W (CategoryStruct.comp f g₁) (CategoryStruct.comp f g₂)
                  source
                  @[simp]
                  theorem CategoryTheory.Localization.Preadditive.comp_add'_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} (f : L.obj X ⟶ L.obj Y) (g₁ g₂ : L.obj Y ⟶ L.obj Z) {Z✝ : D} (h : L.obj Z ⟶ Z✝) :
                  CategoryStruct.comp f (CategoryStruct.comp (add' W g₁ g₂) h) = CategoryStruct.comp (add' W (CategoryStruct.comp f g₁) (CategoryStruct.comp f g₂)) h
                  source
                  @[simp]
                  theorem CategoryTheory.Localization.Preadditive.add'_map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y) :
                  add' W (L.map f₁) (L.map f₂) = L.map (f₁ + f₂)
                  source
                  noncomputable def CategoryTheory.Localization.Preadditive.addCommGroup' {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] (X 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
                      source
                      def CategoryTheory.Localization.Preadditive.homEquiv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {L : Functor C D} {X Y : C} {X' 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
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Localization.Preadditive.homEquiv_symm_apply {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {L : Functor C D} {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (g : L.obj X ⟶ L.obj Y) :
                          (homEquiv eX eY).symm g = CategoryStruct.comp eX.inv (CategoryStruct.comp g eY.hom)
                          source
                          @[simp]
                          theorem CategoryTheory.Localization.Preadditive.homEquiv_apply {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {L : Functor C D} {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (f : X' ⟶ Y') :
                          (homEquiv eX eY) f = CategoryStruct.comp eX.hom (CategoryStruct.comp f eY.inv)
                          source
                          noncomputable def CategoryTheory.Localization.Preadditive.add {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (f₁ 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
                            Instances For
                              source
                              theorem CategoryTheory.Localization.Preadditive.add_comp {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (eZ : L.obj Z ≅ Z') (f₁ f₂ : X' ⟶ Y') (g : Y' ⟶ Z') :
                              CategoryStruct.comp (add W eX eY f₁ f₂) g = add W eX eZ (CategoryStruct.comp f₁ g) (CategoryStruct.comp f₂ g)
                              source
                              theorem CategoryTheory.Localization.Preadditive.add_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (eZ : L.obj Z ≅ Z') (f₁ f₂ : X' ⟶ Y') (g : Y' ⟶ Z') {Z✝ : D} (h : Z' ⟶ Z✝) :
                              CategoryStruct.comp (add W eX eY f₁ f₂) (CategoryStruct.comp g h) = CategoryStruct.comp (add W eX eZ (CategoryStruct.comp f₁ g) (CategoryStruct.comp f₂ g)) h
                              source
                              theorem CategoryTheory.Localization.Preadditive.comp_add {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (eZ : L.obj Z ≅ Z') (f : X' ⟶ Y') (g₁ g₂ : Y' ⟶ Z') :
                              CategoryStruct.comp f (add W eY eZ g₁ g₂) = add W eX eZ (CategoryStruct.comp f g₁) (CategoryStruct.comp f g₂)
                              source
                              theorem CategoryTheory.Localization.Preadditive.comp_add_assoc {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (eZ : L.obj Z ≅ Z') (f : X' ⟶ Y') (g₁ g₂ : Y' ⟶ Z') {Z✝ : D} (h : Z' ⟶ Z✝) :
                              CategoryStruct.comp f (CategoryStruct.comp (add W eY eZ g₁ g₂) h) = CategoryStruct.comp (add W eX eZ (CategoryStruct.comp f g₁) (CategoryStruct.comp f g₂)) h
                              source
                              theorem CategoryTheory.Localization.Preadditive.add_eq_add {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') {X'' Y'' : C} (eX' : L.obj X'' ≅ X') (eY' : L.obj Y'' ≅ Y') (f₁ f₂ : X' ⟶ Y') :
                              add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
                              source
                              noncomputable def CategoryTheory.Localization.Preadditive.addCommGroup {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] (X' Y' : D) :
                              AddCommGroup (X' ⟶ Y')

                              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
                                Instances For
                                  source
                                  theorem CategoryTheory.Localization.Preadditive.add_eq {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive C] {L : Functor C D} (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') (f₁ f₂ : X' ⟶ Y') :
                                  f₁ + f₂ = add W eX eY f₁ f₂
                                  source
                                  theorem CategoryTheory.Localization.Preadditive.map_add {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y) :
                                  L.map (f₁ + f₂) = L.map f₁ + L.map f₂
                                  source
                                  @[irreducible]
                                  noncomputable def CategoryTheory.Localization.preadditive {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] :
                                  Preadditive D

                                  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
                                      source
                                      theorem CategoryTheory.Localization.functor_additive {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] :
                                      L.Additive
                                      source
                                      theorem CategoryTheory.Localization.functor_additive_iff {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_5, u_2} D] [Preadditive C] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {E : Type u_3} [Category.{u_4, u_3} E] [Preadditive E] [Preadditive D] [L.Additive] (G : Functor D E) :
                                      G.Additive ↔ (L.comp G).Additive
                                      source
                                      noncomputable instance CategoryTheory.Localization.instPreadditiveLocalization {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] :
                                      Preadditive W.Localization
                                      Equations
                                        source
                                        instance CategoryTheory.Localization.instAdditiveLocalizationQ {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] :
                                        W.Q.Additive
                                        source
                                        instance CategoryTheory.Localization.instHasZeroObjectLocalization {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [Limits.HasZeroObject C] :
                                        Limits.HasZeroObject W.Localization
                                        source
                                        noncomputable instance CategoryTheory.Localization.instPreadditiveLocalization' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.HasLocalization] :
                                        Preadditive W.Localization'
                                        Equations
                                          source
                                          instance CategoryTheory.Localization.instAdditiveLocalization'Q' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.HasLocalization] :
                                          W.Q'.Additive
                                          source
                                          instance CategoryTheory.Localization.instHasZeroObjectLocalization' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (W : MorphismProperty C) [W.HasLeftCalculusOfFractions] [W.HasLocalization] [Limits.HasZeroObject C] :
                                          Limits.HasZeroObject W.Localization'