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 Y : C}
(φ : W.LeftFraction X Y)
:
W.LeftFraction X Y
The opposite of a left fraction.
Equations
- φ.neg = CategoryTheory.MorphismProperty.LeftFraction.mk (-φ.f) φ.s ⋯
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 Y : C}
(φ : W.LeftFraction₂ X Y)
:
W.LeftFraction X Y
The sum of two left fractions with the same denominator.
Equations
- φ.add = CategoryTheory.MorphismProperty.LeftFraction.mk (φ.f + φ.f') φ.s ⋯
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 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 Y : C}
(φ : W.LeftFraction₂ X Y)
(F : CategoryTheory.Functor C D)
(hF : W.IsInvertedBy F)
[CategoryTheory.Preadditive D]
[F.Additive]
:
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 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
- CategoryTheory.Localization.Preadditive.neg' W f = ⋯.choose.neg.map L ⋯
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 Y : C}
(f : L.obj X ⟶ L.obj Y)
(φ : W.LeftFraction X Y)
(hφ : f = φ.map L ⋯)
:
CategoryTheory.Localization.Preadditive.neg' W f = φ.neg.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 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
- CategoryTheory.Localization.Preadditive.add' W f₁ f₂ = ⋯.choose.add.map L ⋯
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 Y : C}
(f₁ 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 Y : C}
(f₁ 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 Y : C}
(f : L.obj X ⟶ L.obj Y)
:
CategoryTheory.Localization.Preadditive.add' W f (L.map 0) = f
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 Y : C}
(f : L.obj X ⟶ L.obj Y)
:
CategoryTheory.Localization.Preadditive.add' W (L.map 0) f = f
theorem
CategoryTheory.Localization.Preadditive.neg'_add'_self
{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 Y : C}
(f : L.obj X ⟶ L.obj Y)
:
theorem
CategoryTheory.Localization.Preadditive.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 Y : C}
(f₁ f₂ f₃ : L.obj X ⟶ L.obj Y)
:
@[simp]
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 Y Z : C}
(f₁ f₂ : L.obj X ⟶ L.obj Y)
(g : L.obj Y ⟶ L.obj Z)
:
@[simp]
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 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✝)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add' W f₁ f₂)
(CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f₁ g)
(CategoryTheory.CategoryStruct.comp f₂ g))
h
@[simp]
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 Y Z : C}
(f : L.obj X ⟶ L.obj Y)
(g₁ g₂ : L.obj Y ⟶ L.obj Z)
:
@[simp]
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 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✝)
:
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add' W g₁ g₂) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f g₁)
(CategoryTheory.CategoryStruct.comp f g₂))
h
@[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 Y : C}
(f₁ 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 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 Y : C}
{X' Y' : D}
(eX : L.obj X ≅ X')
(eY : L.obj Y ≅ 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
@[simp]
theorem
CategoryTheory.Localization.Preadditive.homEquiv_symm_apply
{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 Y : C}
{X' Y' : D}
(eX : L.obj X ≅ X')
(eY : L.obj Y ≅ Y')
(g : L.obj X ⟶ L.obj Y)
:
(CategoryTheory.Localization.Preadditive.homEquiv eX eY).symm g = CategoryTheory.CategoryStruct.comp eX.inv (CategoryTheory.CategoryStruct.comp g eY.hom)
@[simp]
theorem
CategoryTheory.Localization.Preadditive.homEquiv_apply
{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 Y : C}
{X' Y' : D}
(eX : L.obj X ≅ X')
(eY : L.obj Y ≅ Y')
(f : X' ⟶ Y')
:
(CategoryTheory.Localization.Preadditive.homEquiv eX eY) f = CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.CategoryStruct.comp f eY.inv)
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 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
- One or more equations did not get rendered due to their size.
Instances For
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 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')
:
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 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✝)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂)
(CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f₁ g)
(CategoryTheory.CategoryStruct.comp f₂ g))
h
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 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')
:
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 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✝)
:
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add W eY eZ g₁ g₂) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f g₁)
(CategoryTheory.CategoryStruct.comp f g₂))
h
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 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')
:
CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂ = CategoryTheory.Localization.Preadditive.add W eX' eY' 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' 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
- CategoryTheory.Localization.Preadditive.addCommGroup L W X' Y' = (CategoryTheory.Localization.Preadditive.homEquiv (L.objObjPreimageIso X') (L.objObjPreimageIso Y')).addCommGroup
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 Y : C}
{X' Y' : D}
(eX : L.obj X ≅ X')
(eY : L.obj Y ≅ Y')
(f₁ 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 Y : C}
(f₁ f₂ : X ⟶ Y)
:
@[irreducible]
noncomputable def
CategoryTheory.Localization.preadditive
{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]
:
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
- CategoryTheory.Localization.preadditive L W = { homGroup := CategoryTheory.Localization.Preadditive.addCommGroup L W, add_comp := ⋯, comp_add := ⋯ }
Instances For
theorem
CategoryTheory.Localization.functor_additive
{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]
:
L.Additive
theorem
CategoryTheory.Localization.functor_additive_iff
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_1} C]
[CategoryTheory.Category.{u_5, u_2} D]
[CategoryTheory.Preadditive C]
(L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C)
[L.IsLocalization W]
[W.HasLeftCalculusOfFractions]
{E : Type u_3}
[CategoryTheory.Category.{u_4, u_3} E]
[CategoryTheory.Preadditive E]
[CategoryTheory.Preadditive D]
[L.Additive]
(G : CategoryTheory.Functor D E)
:
G.Additive ↔ (L.comp G).Additive
noncomputable instance
CategoryTheory.Localization.instPreadditiveLocalization
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(W : CategoryTheory.MorphismProperty C)
[W.HasLeftCalculusOfFractions]
:
CategoryTheory.Preadditive W.Localization
instance
CategoryTheory.Localization.instAdditiveLocalizationQ
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(W : CategoryTheory.MorphismProperty C)
[W.HasLeftCalculusOfFractions]
:
W.Q.Additive
Equations
- ⋯ = ⋯
instance
CategoryTheory.Localization.instHasZeroObjectLocalization
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(W : CategoryTheory.MorphismProperty C)
[W.HasLeftCalculusOfFractions]
[CategoryTheory.Limits.HasZeroObject C]
:
CategoryTheory.Limits.HasZeroObject W.Localization
Equations
- ⋯ = ⋯
noncomputable instance
CategoryTheory.Localization.instPreadditiveLocalization'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(W : CategoryTheory.MorphismProperty C)
[W.HasLeftCalculusOfFractions]
[W.HasLocalization]
:
CategoryTheory.Preadditive W.Localization'
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
- ⋯ = ⋯
instance
CategoryTheory.Localization.instHasZeroObjectLocalization'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(W : CategoryTheory.MorphismProperty C)
[W.HasLeftCalculusOfFractions]
[W.HasLocalization]
[CategoryTheory.Limits.HasZeroObject C]
:
CategoryTheory.Limits.HasZeroObject W.Localization'
Equations
- ⋯ = ⋯