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 : C)
(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
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofHom_Y'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofHom_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofHom_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
def
CategoryTheory.MorphismProperty.LeftFraction.ofHom
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
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}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofInv_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofInv_Y'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).Y' = X
def
CategoryTheory.MorphismProperty.LeftFraction.ofInv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{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}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W 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
- CategoryTheory.MorphismProperty.LeftFraction.map φ L hL = let_fun this := ⋯; CategoryTheory.CategoryStruct.comp (L.map φ.f) (CategoryTheory.inv (L.map φ.s))
Instances For
@[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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
{Z : D}
(h : L.obj φ.Y' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.map φ L hL)
(CategoryTheory.CategoryStruct.comp (L.map φ.s) h) = CategoryTheory.CategoryStruct.comp (L.map φ.f) h
@[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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.map φ L hL) (L.map φ.s) = L.map φ.f
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 : C}
{Y : C}
(f : X ⟶ Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
{Z : D}
(h : L.obj X ⟶ Z)
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
{Z : D}
(h : L.obj Y ⟶ Z)
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.cases
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(α : CategoryTheory.MorphismProperty.LeftFraction W 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 : C)
(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
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofHom_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofHom_X'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofHom_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
def
CategoryTheory.MorphismProperty.RightFraction.ofHom
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
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}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofInv_X'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).X' = Y
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofInv_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
def
CategoryTheory.MorphismProperty.RightFraction.ofInv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{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}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W 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
- CategoryTheory.MorphismProperty.RightFraction.map φ L hL = let_fun this := ⋯; CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (L.map φ.s)) (L.map φ.f)
Instances For
@[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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
{Z : D}
(h : L.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (L.map φ.s)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.RightFraction.map φ L hL) h) = CategoryTheory.CategoryStruct.comp (L.map φ.f) h
@[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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
CategoryTheory.CategoryStruct.comp (L.map φ.s) (CategoryTheory.MorphismProperty.RightFraction.map φ L hL) = L.map φ.f
@[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 : C}
{Y : C}
(f : X ⟶ Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
{Z : D}
(h : L.obj X ⟶ Z)
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
{Z : D}
(h : L.obj Y ⟶ Z)
:
@[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 : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
theorem
CategoryTheory.MorphismProperty.RightFraction.cases
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(α : CategoryTheory.MorphismProperty.RightFraction W 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
CategoryTheory.MorphismProperty.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⦄ (φ : CategoryTheory.MorphismProperty.RightFraction W X Y), ∃ (ψ : CategoryTheory.MorphismProperty.LeftFraction W 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
CategoryTheory.MorphismProperty.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⦄ (φ : CategoryTheory.MorphismProperty.LeftFraction W X Y), ∃ (ψ : CategoryTheory.MorphismProperty.RightFraction W 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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
∃ (ψ : CategoryTheory.MorphismProperty.LeftFraction W 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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W 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.
Instances For
theorem
CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
{Z : C}
(h : (CategoryTheory.MorphismProperty.RightFraction.leftFraction φ).Y' ⟶ Z)
:
theorem
CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
∃ (ψ : CategoryTheory.MorphismProperty.RightFraction W 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}
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W 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.
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
{Z : C}
(h : φ.Y' ⟶ Z)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
def
CategoryTheory.MorphismProperty.LeftFractionRel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W 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.
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFractionRel.refl
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.LeftFractionRel.symm
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
(h : 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 : C}
{Y : C}
{z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
{z₃ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
(h₁₂ : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂)
(h₂₃ : CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₃)
:
theorem
CategoryTheory.MorphismProperty.equivalenceLeftFractionRel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
(X : C)
(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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y 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}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y Z)
(z₃ : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y')
(z₃' : CategoryTheory.MorphismProperty.LeftFraction W 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)
:
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 : C)
(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
Instances For
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z : CategoryTheory.MorphismProperty.LeftFraction 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
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y)
:
noncomputable def
CategoryTheory.MorphismProperty.LeftFraction.comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y 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}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y Z)
(z₃ : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y')
(h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f)
:
noncomputable def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W Y Z)
:
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.Localization.Hom.comp_eq
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y 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.
Instances For
noncomputable instance
CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategoryLocalization
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
:
Equations
- CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategoryLocalization = CategoryTheory.Category.mk ⋯ ⋯ ⋯
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_obj
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
(X : C)
:
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions 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.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
The morphism on Localization W that is induced by a left fraction.
Equations
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y Z)
(z₃ : CategoryTheory.MorphismProperty.LeftFraction W 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
(CategoryTheory.MorphismProperty.LeftFraction.comp₀ z₁ 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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ 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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
The morphism in Localization W that is the formal inverse of a morphism
which belongs to W.
Equations
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Y' : C}
(f : X ⟶ Y')
(s : Y ⟶ Y')
(hs : W s)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
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.
Instances For
@[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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
{Z : CategoryTheory.MorphismProperty.LeftFraction.Localization W}
(h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ⟶ Z)
:
@[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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
@[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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
{Z : CategoryTheory.MorphismProperty.LeftFraction.Localization W}
(h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y ⟶ Z)
:
@[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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
instance
CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsIsoLocalizationInstCategoryLocalizationObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorQQinv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
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 : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y)
(F : CategoryTheory.Functor C E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy W F)
:
F.obj X ⟶ F.obj Y
The image by a functor which inverts W of an equivalence class of left fractions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk
{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 : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(F : CategoryTheory.Functor C E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy W F)
:
noncomputable def
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(F : CategoryTheory.Functor C E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy W F)
:
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.
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.fac
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(F : CategoryTheory.Functor C E)
(hF : CategoryTheory.MorphismProperty.IsInvertedBy W F)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.uniq
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(F₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E)
(F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E)
(h : CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) F₁ = CategoryTheory.Functor.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) 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)
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
(E : Type u_4)
[CategoryTheory.Category.{u_6, u_4} 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.
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.LeftFraction.Localization.map_eq_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(g : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(L : CategoryTheory.Functor C D)
[CategoryTheory.Functor.IsLocalization L W]
:
CategoryTheory.MorphismProperty.LeftFraction.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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(L₁ : CategoryTheory.Functor C D)
(L₂ : CategoryTheory.Functor C E)
[CategoryTheory.Functor.IsLocalization L₁ W]
[CategoryTheory.Functor.IsLocalization L₂ W]
:
(CategoryTheory.Localization.uniq L₁ L₂ W).functor.map (CategoryTheory.MorphismProperty.LeftFraction.map φ L₁ ⋯) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.compUniqFunctor L₁ L₂ W).hom.app X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.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 : C}
{Y : C}
(φ₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(φ₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(L₁ : CategoryTheory.Functor C D)
(L₂ : CategoryTheory.Functor C E)
[CategoryTheory.Functor.IsLocalization L₁ W]
[CategoryTheory.Functor.IsLocalization L₂ W]
(h : CategoryTheory.MorphismProperty.LeftFraction.map φ₁ L₁ ⋯ = CategoryTheory.MorphismProperty.LeftFraction.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}
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
{Z : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W Y Z)
(z₃ : CategoryTheory.MorphismProperty.LeftFraction W z₁.Y' z₂.Y')
(h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f)
(L : CategoryTheory.Functor C D)
[CategoryTheory.Functor.IsLocalization L W]
:
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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f : L.obj X ⟶ L.obj Y)
:
∃ (φ : CategoryTheory.MorphismProperty.LeftFraction W X Y), f = CategoryTheory.MorphismProperty.LeftFraction.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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(ψ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
{X : C}
{Y : C}
(f₁ : X ⟶ Y)
(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_of_hasLeftCalculusofFractions
{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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.op_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
(CategoryTheory.MorphismProperty.LeftFraction.op φ).f = φ.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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
(CategoryTheory.MorphismProperty.LeftFraction.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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
def
CategoryTheory.MorphismProperty.LeftFraction.op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
The right fraction in the opposite category corresponding to a left fraction.
Equations
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.op_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
(CategoryTheory.MorphismProperty.RightFraction.op φ).f = φ.f.op
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.op_Y'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.op_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
(CategoryTheory.MorphismProperty.RightFraction.op φ).s = φ.s.op
def
CategoryTheory.MorphismProperty.RightFraction.op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
The left fraction in the opposite category corresponding to a right fraction.
Equations
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.unop_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
(CategoryTheory.MorphismProperty.LeftFraction.unop φ).s = φ.s.unop
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.unop_X'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
(CategoryTheory.MorphismProperty.LeftFraction.unop φ).X' = φ.Y'.unop
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.unop_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
(CategoryTheory.MorphismProperty.LeftFraction.unop φ).f = φ.f.unop
def
CategoryTheory.MorphismProperty.LeftFraction.unop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
The right fraction corresponding to a left fraction in the opposite category.
Equations
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.unop_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
(CategoryTheory.MorphismProperty.RightFraction.unop φ).f = φ.f.unop
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.unop_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
(CategoryTheory.MorphismProperty.RightFraction.unop φ).s = φ.s.unop
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.unop_Y'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
(CategoryTheory.MorphismProperty.RightFraction.unop φ).Y' = φ.X'.unop
def
CategoryTheory.MorphismProperty.RightFraction.unop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
The left fraction corresponding to a right fraction in the opposite category.
Equations
Instances For
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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
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 : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(L : CategoryTheory.Functor C D)
(hL : CategoryTheory.MorphismProperty.IsInvertedBy W L)
:
instance
CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsOppositeOppositeOp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[h : CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOppositeOp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[h : CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsUnop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty Cᵒᵖ)
[h : CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsUnop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty Cᵒᵖ)
[h : CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.MorphismProperty.RightFractionRel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z₁ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.RightFraction W 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.
Instances For
theorem
CategoryTheory.MorphismProperty.RightFractionRel.op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{z₁ : CategoryTheory.MorphismProperty.RightFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.RightFraction W X Y}
(h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂)
:
theorem
CategoryTheory.MorphismProperty.RightFractionRel.unop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{z₁ : CategoryTheory.MorphismProperty.RightFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.RightFraction W X Y}
(h : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂)
:
theorem
CategoryTheory.MorphismProperty.LeftFractionRel.op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
(h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂)
:
theorem
CategoryTheory.MorphismProperty.LeftFractionRel.unop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y}
(h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂)
:
theorem
CategoryTheory.MorphismProperty.leftFractionRel_op_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z₁ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.rightFractionRel_op_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z₁ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
(z₂ : CategoryTheory.MorphismProperty.LeftFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.RightFractionRel.refl
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
theorem
CategoryTheory.MorphismProperty.RightFractionRel.symm
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{z₁ : CategoryTheory.MorphismProperty.RightFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.RightFraction W X Y}
(h : 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 : C}
{Y : C}
{z₁ : CategoryTheory.MorphismProperty.RightFraction W X Y}
{z₂ : CategoryTheory.MorphismProperty.RightFraction W X Y}
{z₃ : CategoryTheory.MorphismProperty.RightFraction W X Y}
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
(h₁₂ : CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂)
(h₂₃ : 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 : C)
(Y : C)
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
:
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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{X : C}
{Y : C}
(f : L.obj X ⟶ L.obj Y)
:
∃ (φ : CategoryTheory.MorphismProperty.RightFraction W X Y), f = CategoryTheory.MorphismProperty.RightFraction.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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{X : C}
{Y : C}
(φ : CategoryTheory.MorphismProperty.RightFraction W X Y)
(ψ : CategoryTheory.MorphismProperty.RightFraction W X Y)
:
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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
{Y : C}
{Z : C}
(f₁ : Y ⟶ Z)
(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)
[CategoryTheory.Functor.IsLocalization L W]
[CategoryTheory.MorphismProperty.HasRightCalculusOfFractions W]
: