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 Localization.exists_leftFraction 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. We also show that the functor L.mapArrow : Arrow C ⥤ Arrow D is essentially surjective.

Similar results are obtained when W has a right calculus of fractions.

References #

[P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory][gabriel-zisman-1967]

structure CategoryTheory.MorphismProperty.LeftFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) (X Y : C) :

Type (max u_1 u_3)

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 ⟶ self.Y'
the numerator of a left fraction
s : Y ⟶ self.Y'
the denominator of a left fraction
hs : W self.s
the condition that the denominator belongs to the given morphism property

def CategoryTheory.MorphismProperty.LeftFraction.ofHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

W.LeftFraction X Y

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

Equations

CategoryTheory.MorphismProperty.LeftFraction.ofHom W f = CategoryTheory.MorphismProperty.LeftFraction.mk f (CategoryTheory.CategoryStruct.id Y) ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.ofHom_Y' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).Y' = Y

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.ofHom_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).f = f

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.ofHom_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).s = CategoryTheory.CategoryStruct.id Y

def CategoryTheory.MorphismProperty.LeftFraction.ofInv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

W.LeftFraction X Y

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

Equations

CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs = CategoryTheory.MorphismProperty.LeftFraction.mk (CategoryTheory.CategoryStruct.id X) s hs

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.ofInv_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).s = s

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.ofInv_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).f = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.ofInv_Y' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).Y' = X

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy 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

φ.map L hL = CategoryTheory.CategoryStruct.comp (L.map φ.f) (CategoryTheory.inv (L.map φ.s))

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

CategoryTheory.CategoryStruct.comp (φ.map L hL) (L.map φ.s) = L.map φ.f

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj φ.Y' ⟶ Z) :

CategoryTheory.CategoryStruct.comp (φ.map L hL) (CategoryTheory.CategoryStruct.comp (L.map φ.s) h) = CategoryTheory.CategoryStruct.comp (L.map φ.f) h

theorem CategoryTheory.MorphismProperty.LeftFraction.map_ofHom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).map L hL = L.map f

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) (L.map s) = CategoryTheory.CategoryStruct.id (L.obj X)

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) (CategoryTheory.CategoryStruct.comp (L.map s) h) = h

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) = CategoryTheory.CategoryStruct.id (L.obj Y)

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (L.map s) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) h) = h

theorem CategoryTheory.MorphismProperty.LeftFraction.cases {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (α : W.LeftFraction X Y) :

∃ (Y' : C) (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s), α = CategoryTheory.MorphismProperty.LeftFraction.mk f s hs

structure CategoryTheory.MorphismProperty.RightFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) (X Y : C) :

Type (max u_1 u_3)

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 : self.X' ⟶ X
the denominator of a right fraction
hs : W self.s
the condition that the denominator belongs to the given morphism property
f : self.X' ⟶ Y
the numerator of a right fraction

def CategoryTheory.MorphismProperty.RightFraction.ofHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

W.RightFraction X Y

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

Equations

CategoryTheory.MorphismProperty.RightFraction.ofHom W f = CategoryTheory.MorphismProperty.RightFraction.mk (CategoryTheory.CategoryStruct.id X) ⋯ f

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.ofHom_X' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).X' = X

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.ofHom_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).f = f

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.ofHom_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).s = CategoryTheory.CategoryStruct.id X

def CategoryTheory.MorphismProperty.RightFraction.ofInv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

W.RightFraction X Y

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

Equations

CategoryTheory.MorphismProperty.RightFraction.ofInv s hs = CategoryTheory.MorphismProperty.RightFraction.mk s hs (CategoryTheory.CategoryStruct.id Y)

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.ofInv_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).f = CategoryTheory.CategoryStruct.id Y

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.ofInv_X' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).X' = Y

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.ofInv_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (s : Y ⟶ X) (hs : W s) :

(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).s = s

noncomputable def CategoryTheory.MorphismProperty.RightFraction.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy 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

φ.map L hL = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (L.map φ.s)) (L.map φ.f)

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

CategoryTheory.CategoryStruct.comp (L.map φ.s) (φ.map L hL) = L.map φ.f

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (L.map φ.s) (CategoryTheory.CategoryStruct.comp (φ.map L hL) h) = CategoryTheory.CategoryStruct.comp (L.map φ.f) h

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_ofHom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) [W.ContainsIdentities] :

(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).map L hL = L.map f

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) (L.map s) = CategoryTheory.CategoryStruct.id (L.obj X)

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) (CategoryTheory.CategoryStruct.comp (L.map s) h) = h

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) = CategoryTheory.CategoryStruct.id (L.obj Y)

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X) (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (L.map s) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) h) = h

theorem CategoryTheory.MorphismProperty.RightFraction.cases {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (α : W.RightFraction X Y) :

∃ (X' : C) (s : X' ⟶ X) (hs : W s) (f : X' ⟶ Y), α = CategoryTheory.MorphismProperty.RightFraction.mk s hs f

class CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) extends W.IsMultiplicative :

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), W (CategoryTheory.CategoryStruct.id X)
comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
exists_leftFraction : ∀ ⦃X Y : C⦄ (φ : W.RightFraction X Y), ∃ (ψ : W.LeftFraction X Y), CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f
ext : ∀ ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X), W s → CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂ → ∃ (Y' : C) (t : Y ⟶ Y') (_ : W t), CategoryTheory.CategoryStruct.comp f₁ t = CategoryTheory.CategoryStruct.comp f₂ t

Instances

class CategoryTheory.MorphismProperty.HasRightCalculusOfFractions {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) extends W.IsMultiplicative :

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), W (CategoryTheory.CategoryStruct.id X)
comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
exists_rightFraction : ∀ ⦃X Y : C⦄ (φ : W.LeftFraction X Y), ∃ (ψ : W.RightFraction X Y), CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s
ext : ∀ ⦃X Y Y' : C⦄ (f₁ f₂ : X ⟶ Y) (s : Y ⟶ Y'), W s → CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s → ∃ (X' : C) (t : X' ⟶ X) (_ : W t), CategoryTheory.CategoryStruct.comp t f₁ = CategoryTheory.CategoryStruct.comp t f₂

Instances

theorem CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) :

∃ (ψ : W.LeftFraction X Y), CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f

noncomputable def CategoryTheory.MorphismProperty.RightFraction.leftFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) :

W.LeftFraction X Y

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

Equations

φ.leftFraction = ⋯.choose

theorem CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) :

CategoryTheory.CategoryStruct.comp φ.f φ.leftFraction.s = CategoryTheory.CategoryStruct.comp φ.s φ.leftFraction.f

theorem CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) {Z : C} (h : φ.leftFraction.Y' ⟶ Z) :

CategoryTheory.CategoryStruct.comp φ.f (CategoryTheory.CategoryStruct.comp φ.leftFraction.s h) = CategoryTheory.CategoryStruct.comp φ.s (CategoryTheory.CategoryStruct.comp φ.leftFraction.f h)

theorem CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) :

∃ (ψ : W.RightFraction X Y), CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.rightFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) :

W.RightFraction X Y

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

Equations

φ.rightFraction = ⋯.choose

theorem CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) :

CategoryTheory.CategoryStruct.comp φ.rightFraction.s φ.f = CategoryTheory.CategoryStruct.comp φ.rightFraction.f φ.s

theorem CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) {Z : C} (h : φ.Y' ⟶ Z) :

CategoryTheory.CategoryStruct.comp φ.rightFraction.s (CategoryTheory.CategoryStruct.comp φ.f h) = CategoryTheory.CategoryStruct.comp φ.rightFraction.f (CategoryTheory.CategoryStruct.comp φ.s h)

def CategoryTheory.MorphismProperty.LeftFractionRel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z₁ z₂ : W.LeftFraction X Y) :

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

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.MorphismProperty.LeftFractionRel.refl {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z : W.LeftFraction X Y) :

CategoryTheory.MorphismProperty.LeftFractionRel z z

theorem CategoryTheory.MorphismProperty.LeftFractionRel.symm {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} {z₁ z₂ : W.LeftFraction X Y} (h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₁

theorem CategoryTheory.MorphismProperty.LeftFractionRel.trans {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} {z₁ z₂ z₃ : W.LeftFraction X Y} [W.HasLeftCalculusOfFractions] (h₁₂ : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂) (h₂₃ : CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₃) :

CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₃

theorem CategoryTheory.MorphismProperty.equivalenceLeftFractionRel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] (X Y : C) :

Equivalence CategoryTheory.MorphismProperty.LeftFractionRel

def CategoryTheory.MorphismProperty.LeftFraction.comp₀ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) (z₃ : W.LeftFraction z₁.Y' z₂.Y') :

W.LeftFraction X Z

Auxiliary definition for the composition of left fractions.

Equations

z₁.comp₀ z₂ z₃ = CategoryTheory.MorphismProperty.LeftFraction.mk (CategoryTheory.CategoryStruct.comp z₁.f z₃.f) (CategoryTheory.CategoryStruct.comp z₂.s z₃.s) ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) (z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y') (h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f) (h₃' : CategoryTheory.CategoryStruct.comp z₂.f z₃'.s = CategoryTheory.CategoryStruct.comp z₁.s z₃'.f) :

CategoryTheory.MorphismProperty.LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')

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} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) (X Y : C) :

Type (max u_1 u_3)

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

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y = Quot CategoryTheory.MorphismProperty.LeftFractionRel

def CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z : W.LeftFraction X Y) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y

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

Equations

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z = Quot.mk CategoryTheory.MorphismProperty.LeftFractionRel z

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (f : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y) :

∃ (z : W.LeftFraction X Y), f = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X 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

z₁.comp z₂ = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk (z₁.comp₀ z₂ (CategoryTheory.MorphismProperty.RightFraction.mk z₁.s ⋯ z₂.f).leftFraction)

theorem CategoryTheory.MorphismProperty.LeftFraction.comp_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f) :

z₁.comp z₂ = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk (z₁.comp₀ z₂ z₃)

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y) (z₂ : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W Y Z) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Z

Composition of morphisms in the constructed localized category for a morphism property that has left calculus of fractions.

Equations

z₁.comp z₂ = Quot.lift₂ (fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) => a.comp b) ⋯ ⋯ z₁ z₂

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₁).comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₂) = z₁.comp z₂

def CategoryTheory.MorphismProperty.LeftFraction.Localization {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] :

CategoryTheory.MorphismProperty C → Type u_1

The constructed localized category for a morphism property that has left calculus of fractions.

Equations

CategoryTheory.MorphismProperty.LeftFraction.Localization x = C

noncomputable instance CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] :

CategoryTheory.Category.{max u_3 u_1, u_1} (CategoryTheory.MorphismProperty.LeftFraction.Localization W)

Equations

CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.MorphismProperty.LeftFraction.Localization.Q {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] :

CategoryTheory.Functor C (CategoryTheory.MorphismProperty.LeftFraction.Localization W)

The localization functor to 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.

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] (X : C) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X = X

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (f : W.LeftFraction X Y) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ⟶ (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y

The morphism on Localization W that is induced by a left fraction.

Equations

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (f : W.LeftFraction X Y) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] {X Y : C} (f : X ⟶ Y) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map f = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f)

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁) (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂) = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (z₁.comp₀ z₂ z₃)

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_of_leftFractionRel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (z₁ z₂ : W.LeftFraction X Y) (h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁ = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_iff_leftFractionRel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (z₁ z₂ : W.LeftFraction X Y) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁ = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂ ↔ CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂

def CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y ⟶ (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X

The morphism in Localization W that is the formal inverse of a morphism which belongs to W.

Equations

CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs)

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Y' : C} (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map f) (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (CategoryTheory.MorphismProperty.LeftFraction.mk f s hs)

def CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ≅ (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y

The isomorphism in Localization W that is induced by a morphism in W.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso s hs).hom = (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso s hs).inv = CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X)

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) {Z : CategoryTheory.MorphismProperty.LeftFraction.Localization W} (h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) h) = h

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y)

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) {Z : CategoryTheory.MorphismProperty.LeftFraction.Localization W} (h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) h) = h

instance CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsIsoQinv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) :

CategoryTheory.IsIso (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs)

Equations

⋯ = ⋯

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] {X Y : C} (f : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y) (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F) :

F.obj X ⟶ F.obj Y

The image by a functor which inverts W of an equivalence class of left fractions.

Equations

f.map F hF = Quot.lift (fun (f : W.LeftFraction X Y) => f.map F hF) ⋯ f

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] {W : CategoryTheory.MorphismProperty C} {X Y : C} (f : W.LeftFraction X Y) (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f).map F hF = f.map F hF

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] :

W.IsInvertedBy (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W)

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F) :

CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E

The functor Localization W ⥤ E that is induced by a functor C ⥤ E which inverts W, when W has a left calculus of fractions.

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.fac {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F) :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift F hF) = F

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.uniq {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E) (h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp F₁ = (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp F₂) :

F₁ = F₂

noncomputable def CategoryTheory.MorphismProperty.LeftFraction.Localization.strictUniversalPropertyFixedTarget {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] (E : Type u_4) [CategoryTheory.Category.{u_6, u_4} E] :

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) W E

The universal property of the localization for the constructed localized category when there is a left calculus of fractions.

Equations

One or more equations did not get rendered due to their size.

instance CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsLocalizationQ {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] :

(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).IsLocalization W

Equations

⋯ = ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (f : W.LeftFraction X Y) :

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f = f.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.map_eq_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (f g : W.LeftFraction X Y) :

f.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯ = g.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯ ↔ CategoryTheory.MorphismProperty.LeftFractionRel f g

theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) [L.IsLocalization W] :

φ.map L ⋯ = CategoryTheory.CategoryStruct.comp (L.map φ.f) (CategoryTheory.Localization.isoOfHom L W φ.s ⋯).inv

theorem CategoryTheory.MorphismProperty.LeftFraction.map_compatibility {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] (L₁ : CategoryTheory.Functor C D) (L₂ : CategoryTheory.Functor C E) [L₁.IsLocalization W] [L₂.IsLocalization W] :

(CategoryTheory.Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).hom.app X) (CategoryTheory.CategoryStruct.comp (φ.map L₂ ⋯) ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).inv.app Y))

theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq_of_map_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ₁ φ₂ : W.LeftFraction X Y) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] (L₁ : CategoryTheory.Functor C D) (L₂ : CategoryTheory.Functor C E) [L₁.IsLocalization W] [L₂.IsLocalization W] (h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯) :

φ₁.map L₂ ⋯ = φ₂.map L₂ ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f) (L : CategoryTheory.Functor C D) [L.IsLocalization W] :

CategoryTheory.CategoryStruct.comp (z₁.map L ⋯) (z₂.map L ⋯) = (z₁.comp₀ z₂ z₃).map L ⋯

theorem CategoryTheory.Localization.exists_leftFraction {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (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), f = φ.map L ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff {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) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (φ ψ : W.LeftFraction X Y) :

φ.map L ⋯ = ψ.map L ⋯ ↔ CategoryTheory.MorphismProperty.LeftFractionRel φ ψ

theorem CategoryTheory.MorphismProperty.map_eq_iff_postcomp {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) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y) :

L.map f₁ = L.map f₂ ↔ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s

theorem CategoryTheory.Localization.essSurj_mapArrow {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) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] :

L.mapArrow.EssSurj

def CategoryTheory.MorphismProperty.LeftFraction.op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) :

W.op.RightFraction (Opposite.op Y) (Opposite.op X)

The right fraction in the opposite category corresponding to a left fraction.

Equations

φ.op = CategoryTheory.MorphismProperty.RightFraction.mk φ.s.op ⋯ φ.f.op

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.op_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) :

φ.op.s = φ.s.op

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.op_X' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) :

φ.op.X' = Opposite.op φ.Y'

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.op_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) :

φ.op.f = φ.f.op

def CategoryTheory.MorphismProperty.RightFraction.op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) :

W.op.LeftFraction (Opposite.op Y) (Opposite.op X)

The left fraction in the opposite category corresponding to a right fraction.

Equations

φ.op = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f.op φ.s.op ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.op_Y' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) :

φ.op.Y' = Opposite.op φ.X'

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.op_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) :

φ.op.f = φ.f.op

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.op_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) :

φ.op.s = φ.s.op

def CategoryTheory.MorphismProperty.LeftFraction.unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.LeftFraction X Y) :

W.unop.RightFraction (Opposite.unop Y) (Opposite.unop X)

The right fraction corresponding to a left fraction in the opposite category.

Equations

φ.unop = CategoryTheory.MorphismProperty.RightFraction.mk φ.s.unop ⋯ φ.f.unop

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.unop_X' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.LeftFraction X Y) :

φ.unop.X' = Opposite.unop φ.Y'

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.unop_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.LeftFraction X Y) :

φ.unop.s = φ.s.unop

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.unop_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.LeftFraction X Y) :

φ.unop.f = φ.f.unop

def CategoryTheory.MorphismProperty.RightFraction.unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.RightFraction X Y) :

W.unop.LeftFraction (Opposite.unop Y) (Opposite.unop X)

The left fraction corresponding to a right fraction in the opposite category.

Equations

φ.unop = CategoryTheory.MorphismProperty.LeftFraction.mk φ.f.unop φ.s.unop ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.unop_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.RightFraction X Y) :

φ.unop.f = φ.f.unop

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.unop_Y' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.RightFraction X Y) :

φ.unop.Y' = Opposite.unop φ.X'

@[simp]

theorem CategoryTheory.MorphismProperty.RightFraction.unop_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} (φ : W.RightFraction X Y) :

φ.unop.s = φ.s.unop

theorem CategoryTheory.MorphismProperty.RightFraction.op_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

(φ.map L hL).op = φ.op.map L.op ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.op_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) :

(φ.map L hL).op = φ.op.map L.op ⋯

instance CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [h : W.HasLeftCalculusOfFractions] :

W.op.HasRightCalculusOfFractions

Equations

⋯ = ⋯

instance CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [h : W.HasRightCalculusOfFractions] :

W.op.HasLeftCalculusOfFractions

Equations

⋯ = ⋯

instance CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [h : W.HasLeftCalculusOfFractions] :

W.unop.HasRightCalculusOfFractions

Equations

⋯ = ⋯

instance CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [h : W.HasRightCalculusOfFractions] :

W.unop.HasLeftCalculusOfFractions

Equations

⋯ = ⋯

def CategoryTheory.MorphismProperty.RightFractionRel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z₁ z₂ : W.RightFraction X Y) :

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

Equations

One or more equations did not get rendered due to their size.

theorem CategoryTheory.MorphismProperty.RightFractionRel.op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} {z₁ z₂ : W.RightFraction X Y} (h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.LeftFractionRel z₁.op z₂.op

theorem CategoryTheory.MorphismProperty.RightFractionRel.unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} {z₁ z₂ : W.RightFraction X Y} (h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.LeftFractionRel z₁.unop z₂.unop

theorem CategoryTheory.MorphismProperty.LeftFractionRel.op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} {z₁ z₂ : W.LeftFraction X Y} (h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.RightFractionRel z₁.op z₂.op

theorem CategoryTheory.MorphismProperty.LeftFractionRel.unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ} {z₁ z₂ : W.LeftFraction X Y} (h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.RightFractionRel z₁.unop z₂.unop

theorem CategoryTheory.MorphismProperty.leftFractionRel_op_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z₁ z₂ : W.RightFraction X Y) :

CategoryTheory.MorphismProperty.LeftFractionRel z₁.op z₂.op ↔ CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂

theorem CategoryTheory.MorphismProperty.rightFractionRel_op_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z₁ z₂ : W.LeftFraction X Y) :

CategoryTheory.MorphismProperty.RightFractionRel z₁.op z₂.op ↔ CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂

theorem CategoryTheory.MorphismProperty.RightFractionRel.refl {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} (z : W.RightFraction X Y) :

CategoryTheory.MorphismProperty.RightFractionRel z z

theorem CategoryTheory.MorphismProperty.RightFractionRel.symm {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} {z₁ z₂ : W.RightFraction X Y} (h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂) :

CategoryTheory.MorphismProperty.RightFractionRel z₂ z₁

theorem CategoryTheory.MorphismProperty.RightFractionRel.trans {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C} {z₁ z₂ z₃ : W.RightFraction X Y} [W.HasRightCalculusOfFractions] (h₁₂ : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂) (h₂₃ : CategoryTheory.MorphismProperty.RightFractionRel z₂ z₃) :

CategoryTheory.MorphismProperty.RightFractionRel z₁ z₃

theorem CategoryTheory.MorphismProperty.equivalenceRightFractionRel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} (X Y : C) [W.HasRightCalculusOfFractions] :

Equivalence CategoryTheory.MorphismProperty.RightFractionRel

theorem CategoryTheory.Localization.exists_rightFraction {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) :

∃ (φ : W.RightFraction X Y), f = φ.map L ⋯

theorem CategoryTheory.MorphismProperty.RightFraction.map_eq_iff {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) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {X Y : C} (φ ψ : W.RightFraction X Y) :

φ.map L ⋯ = ψ.map L ⋯ ↔ CategoryTheory.MorphismProperty.RightFractionRel φ ψ

theorem CategoryTheory.MorphismProperty.map_eq_iff_precomp {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) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {Y Z : C} (f₁ f₂ : Y ⟶ Z) :

L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂

theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions {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) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] :

L.mapArrow.EssSurj