# Documentation

Mathlib.CategoryTheory.Localization.CalculusOfFractions

# Calculus of fractions #

Following the definitions by [Gabriel and Zisman][gabriel-zisman-1967], given a morphism property W : MorphismProperty C on a category C, we introduce the class W.HasLeftCalculusOfFractions. The main result (TODO) is that if L : C ⥤ D is a localization functor for W, then for any morphism L.obj X ⟶ L.obj Y in D, there exists an auxiliary object Y' : C and morphisms g : X ⟶ Y' and s : Y ⟶ Y', with W s, such that the given morphism is a sort of fraction g / s, or more precisely of the form L.map g ≫ (Localization.isoOfHom L W s hs).inv.

## References #

• [P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory][gabriel-zisman-1967]
structure CategoryTheory.MorphismProperty.LeftFraction {C : Type u_1} [] (X : C) (Y : C) :
Type (max u_1 u_2)

A left fraction from X : C to Y : C for W : MorphismProperty C consists of the datum of an object Y' : C and maps f : X ⟶ Y' and s : Y ⟶ Y' such that W s.

• Y' : C

the auxiliary object of a left fraction

• f : X s.Y'

the numerator of a left fraction

• s : Y s.Y'

the denominator of a left fraction

• hs : W s.s

the condition that the denominator belongs to the given morphism property

Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.ofHom_Y' {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.ofHom_f {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.ofHom_s {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
def CategoryTheory.MorphismProperty.LeftFraction.ofHom {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :

The left fraction from X to Y given by a morphism f : X ⟶ Y.

Equations
Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.ofInv_s {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.ofInv_f {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.ofInv_Y' {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :
def CategoryTheory.MorphismProperty.LeftFraction.ofInv {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :

The left fraction from X to Y given by a morphism s : Y ⟶ X such that W s.

Equations
Instances For
noncomputable def CategoryTheory.MorphismProperty.LeftFraction.map {C : Type u_1} {D : Type u_2} [] [] {X : C} {Y : C} (φ : ) (L : ) :
L.obj X L.obj Y

If φ : W.LeftFraction X Y and L is a functor which inverts W, this is the induced morphism L.obj X ⟶ L.obj Y

Equations
Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc {C : Type u_1} {D : Type u_4} [] [] {X : C} {Y : C} (φ : ) (L : ) {Z : D} (h : L.obj φ.Y' Z) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s {C : Type u_1} {D : Type u_4} [] [] {X : C} {Y : C} (φ : ) (L : ) :
= L.map φ.f
theorem CategoryTheory.MorphismProperty.LeftFraction.map_ofHom {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (f : X Y) (L : ) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id_assoc {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) {Z : D} (h : L.obj X Z) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) :
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id_assoc {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) {Z : D} (h : L.obj Y Z) :
= h
@[simp]
theorem CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) :
theorem CategoryTheory.MorphismProperty.LeftFraction.cases {C : Type u_1} [] {X : C} {Y : C} (α : ) :
∃ (Y' : C) (f : X Y') (s : Y Y') (hs : W s),
structure CategoryTheory.MorphismProperty.RightFraction {C : Type u_1} [] (X : C) (Y : C) :
Type (max u_1 u_2)

A right fraction from X : C to Y : C for W : MorphismProperty C consists of the datum of an object X' : C and maps s : X' ⟶ X and f : X' ⟶ Y such that W s.

• X' : C

the auxiliary object of a right fraction

• s : s.X' X

the denominator of a right fraction

• hs : W s.s

the condition that the denominator belongs to the given morphism property

• f : s.X' Y

the numerator of a right fraction

Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.ofHom_s {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.ofHom_X' {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.ofHom_f {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :
def CategoryTheory.MorphismProperty.RightFraction.ofHom {C : Type u_1} [] {X : C} {Y : C} (f : X Y) :

The right fraction from X to Y given by a morphism f : X ⟶ Y.

Equations
Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.ofInv_s {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.ofInv_X' {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.ofInv_f {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :
def CategoryTheory.MorphismProperty.RightFraction.ofInv {C : Type u_1} [] {X : C} {Y : C} (s : Y X) (hs : W s) :

The right fraction from X to Y given by a morphism s : Y ⟶ X such that W s.

Equations
Instances For
noncomputable def CategoryTheory.MorphismProperty.RightFraction.map {C : Type u_1} {D : Type u_2} [] [] {X : C} {Y : C} (L : ) :
L.obj X L.obj Y

If φ : W.RightFraction X Y and L is a functor which inverts W, this is the induced morphism L.obj X ⟶ L.obj Y

Equations
Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map_assoc {C : Type u_1} {D : Type u_4} [] [] {X : C} {Y : C} (L : ) {Z : D} (h : L.obj Y Z) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map {C : Type u_1} {D : Type u_4} [] [] {X : C} {Y : C} (L : ) :
= L.map φ.f
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_ofHom {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (f : X Y) (L : ) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id_assoc {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) {Z : D} (h : L.obj X Z) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id_assoc {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) {Z : D} (h : L.obj Y Z) :
@[simp]
theorem CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id {C : Type u_2} {D : Type u_4} [] [] {X : C} {Y : C} (s : Y X) (hs : W s) (L : ) :
theorem CategoryTheory.MorphismProperty.RightFraction.cases {C : Type u_1} [] {X : C} {Y : C} :
∃ (X' : C) (s : X' X) (hs : W s) (f : X' Y),

A multiplicative morphism property W has left calculus of fractions if any right fraction can be turned into a left fraction and that two morphisms that can be equalized by precomposition with a morphism in W can also be equalized by postcomposition with a morphism in W.

• id_mem' : ∀ (X : C),
• stableUnderComposition :
• exists_leftFraction : ∀ ⦃X Y : C⦄ (φ : ), ∃ (ψ : ),
• ext : ∀ ⦃X' X Y : C⦄ (f₁ f₂ : X Y) (s : X' X), W s∃ (Y' : C) (t : Y Y') (_ : W t),
Instances

A multiplicative morphism property W has right calculus of fractions if any left fraction can be turned into a right fraction and that two morphisms that can be equalized by postcomposition with a morphism in W can also be equalized by precomposition with a morphism in W.

• id_mem' : ∀ (X : C),
• stableUnderComposition :
• exists_rightFraction : ∀ ⦃X Y : C⦄ (φ : ), ∃ (ψ : ),
• ext : ∀ ⦃X Y Y' : C⦄ (f₁ f₂ : X Y) (s : Y Y'), W s∃ (X' : C) (t : X' X) (_ : W t),
Instances
theorem CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction {C : Type u_1} [] {X : C} {Y : C} :
∃ (ψ : ),
noncomputable def CategoryTheory.MorphismProperty.RightFraction.leftFraction {C : Type u_1} [] {X : C} {Y : C} :

A choice of a left fraction deduced from a right fraction for a morphism property W when W has left calculus of fractions.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction {C : Type u_1} [] {X : C} {Y : C} (φ : ) :
∃ (ψ : ),
noncomputable def CategoryTheory.MorphismProperty.LeftFraction.rightFraction {C : Type u_1} [] {X : C} {Y : C} (φ : ) :

A choice of a right fraction deduced from a left fraction for a morphism property W when W has right calculus of fractions.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc {C : Type u_1} [] {X : C} {Y : C} (φ : ) {Z : C} (h : φ.Y' Z) :
def CategoryTheory.MorphismProperty.LeftFractionRel {C : Type u_1} [] {X : C} {Y : C} (z₁ : ) (z₂ : ) :

The equivalence relation on left fractions for a morphism property W.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.MorphismProperty.LeftFractionRel.refl {C : Type u_1} [] {X : C} {Y : C} (z : ) :
theorem CategoryTheory.MorphismProperty.LeftFractionRel.symm {C : Type u_1} [] {X : C} {Y : C} {z₁ : } {z₂ : } :
theorem CategoryTheory.MorphismProperty.LeftFractionRel.trans {C : Type u_1} [] {X : C} {Y : C} {z₁ : } {z₂ : } {z₃ : } (h₁₂ : ) (h₂₃ : ) :
theorem CategoryTheory.MorphismProperty.equivalenceLeftFractionRel {C : Type u_1} [] (X : C) (Y : C) :
Equivalence CategoryTheory.MorphismProperty.LeftFractionRel
def CategoryTheory.MorphismProperty.LeftFraction.comp₀ {C : Type u_1} [] {X : C} {Y : C} {Z : C} (z₁ : ) (z₂ : ) (z₃ : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y') :

Auxiliary definition for the composition of left fractions.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel {C : Type u_1} [] {X : C} {Y : C} {Z : C} (z₁ : ) (z₂ : ) (z₃ : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y') (z₃' : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y') (h₃ : = ) (h₃' : CategoryTheory.CategoryStruct.comp z₂.f z₃'.s = CategoryTheory.CategoryStruct.comp z₁.s z₃'.f) :

The equivalence class of z₁.comp₀ z₂ z₃ does not depend on the choice of z₃ provided they satisfy the compatibility z₂.f ≫ z₃.s = z₁.s ≫ z₃.f.

def CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom {C : Type u_1} [] (X : C) (Y : C) :
Type (max u_1 u_2)

The morphisms in the constructed localized category for a morphism property W that has left calculus of fractions are equivalence classes of left fractions.

Equations
• = Quot CategoryTheory.MorphismProperty.LeftFractionRel
Instances For

The morphism in the constructed localized category that is induced by a left fraction.

Equations
Instances For
noncomputable def CategoryTheory.MorphismProperty.LeftFraction.comp {C : Type u_1} [] {X : C} {Y : C} {Z : C} (z₁ : ) (z₂ : ) :

Auxiliary definition towards the definition of the composition of morphisms in the constructed localized category for a morphism property that has left calculus of fractions.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.MorphismProperty.LeftFraction.comp_eq {C : Type u_1} [] {X : C} {Y : C} {Z : C} (z₁ : ) (z₂ : ) (z₃ : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y') (h₃ : = ) :