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
theorem
CategoryTheory.MorphismProperty.LeftFraction.hs
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(self : W.LeftFraction X Y)
:
W self.s
the condition that the denominator belongs to the given morphism property
@[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)
[W.ContainsIdentities]
:
@[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)
[W.ContainsIdentities]
:
@[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)
[W.ContainsIdentities]
:
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)
[W.ContainsIdentities]
:
W.LeftFraction X Y
The left fraction from X to Y given by a morphism f : X ⟶ Y.
Equations
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofInv_s
{C : Type u_1}
[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)
:
W.LeftFraction X Y
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}
(φ : 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))
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}
(φ : 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
@[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}
(φ : 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
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 : 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_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 : 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_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 : 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_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 : 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
@[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 : W.IsInvertedBy L)
:
CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) = CategoryTheory.CategoryStruct.id (L.obj Y)
theorem
CategoryTheory.MorphismProperty.LeftFraction.cases
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{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 : 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
theorem
CategoryTheory.MorphismProperty.RightFraction.hs
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(self : W.RightFraction X Y)
:
W self.s
the condition that the denominator belongs to the given morphism property
@[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)
[W.ContainsIdentities]
:
@[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)
[W.ContainsIdentities]
:
@[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)
[W.ContainsIdentities]
:
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)
[W.ContainsIdentities]
:
W.RightFraction X Y
The right fraction from X to Y given by a morphism f : X ⟶ Y.
Equations
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofInv_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.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
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)
:
W.RightFraction X Y
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}
(φ : 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)
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}
(φ : 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_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}
(φ : 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_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 : 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_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 : 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_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 : 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_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 : 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
@[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 : W.IsInvertedBy L)
:
CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) = CategoryTheory.CategoryStruct.id (L.obj Y)
theorem
CategoryTheory.MorphismProperty.RightFraction.cases
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{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
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⦄ (φ : 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
theorem
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {W : CategoryTheory.MorphismProperty C}
[self : W.HasLeftCalculusOfFractions] ⦃X Y : C⦄ (φ : W.RightFraction X Y),
∃ (ψ : W.LeftFraction X Y), CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f
theorem
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {W : CategoryTheory.MorphismProperty C}
[self : W.HasLeftCalculusOfFractions] ⦃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
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⦄ (φ : 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.HasRightCalculusOfFractions.exists_rightFraction
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {W : CategoryTheory.MorphismProperty C}
[self : W.HasRightCalculusOfFractions] ⦃X Y : C⦄ (φ : W.LeftFraction X Y),
∃ (ψ : W.RightFraction X Y), CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s
theorem
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.ext
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {W : CategoryTheory.MorphismProperty C}
[self : W.HasRightCalculusOfFractions] ⦃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₂
theorem
CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
{X : C}
{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 : C}
{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
Instances For
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 : C}
{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.RightFraction.leftFraction_fac
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
(φ : W.RightFraction X Y)
:
CategoryTheory.CategoryStruct.comp φ.f φ.leftFraction.s = CategoryTheory.CategoryStruct.comp φ.s φ.leftFraction.f
theorem
CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasRightCalculusOfFractions]
{X : C}
{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 : C}
{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
Instances For
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 : C}
{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)
theorem
CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasRightCalculusOfFractions]
{X : C}
{Y : C}
(φ : W.LeftFraction X Y)
:
CategoryTheory.CategoryStruct.comp φ.rightFraction.s φ.f = CategoryTheory.CategoryStruct.comp φ.rightFraction.f φ.s
def
CategoryTheory.MorphismProperty.LeftFractionRel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(z₁ : W.LeftFraction X Y)
(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.
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 : W.LeftFraction 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₁ : W.LeftFraction X Y}
{z₂ : W.LeftFraction 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₁ : W.LeftFraction X Y}
{z₂ : W.LeftFraction X Y}
{z₃ : W.LeftFraction X Y}
[W.HasLeftCalculusOfFractions]
(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)
[W.HasLeftCalculusOfFractions]
(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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
{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) ⋯
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
{Z : C}
(z₁ : W.LeftFraction X Y)
(z₂ : W.LeftFraction Y Z)
(z₃ : W.LeftFraction z₁.Y' z₂.Y')
(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 : 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 : W.LeftFraction 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)
:
∃ (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 : C}
{Y : C}
{Z : C}
(z₁ : W.LeftFraction X Y)
(z₂ : W.LeftFraction 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
- z₁.comp z₂ = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk (z₁.comp₀ z₂ (CategoryTheory.MorphismProperty.RightFraction.mk z₁.s ⋯ z₂.f).leftFraction)
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.comp_eq
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
{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 : 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
- z₁.comp z₂ = Quot.lift₂ (fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) => a.comp b) ⋯ ⋯ z₁ z₂
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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
{Z : C}
(z₁ : W.LeftFraction X Y)
(z₂ : W.LeftFraction 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.instCategory
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
:
Equations
- CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory = 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)
[W.HasLeftCalculusOfFractions]
(X : C)
:
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W : CategoryTheory.MorphismProperty C)
[W.HasLeftCalculusOfFractions]
:
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
@[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 : C}
{Y : C}
(f : W.LeftFraction 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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
(f : W.LeftFraction X Y)
:
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 : 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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
{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)
:
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 : C}
{Y : C}
(z₁ : W.LeftFraction X Y)
(z₂ : W.LeftFraction 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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
(z₁ : W.LeftFraction X Y)
(z₂ : W.LeftFraction X Y)
:
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
{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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
{Y' : C}
(f : X ⟶ Y')
(s : Y ⟶ 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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
(s : X ⟶ 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}
[W.HasLeftCalculusOfFractions]
{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}
[W.HasLeftCalculusOfFractions]
{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}
[W.HasLeftCalculusOfFractions]
{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}
[W.HasLeftCalculusOfFractions]
{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}
[W.HasLeftCalculusOfFractions]
{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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
(s : X ⟶ Y)
(hs : W s)
:
instance
CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsIsoQinv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
[W.HasLeftCalculusOfFractions]
{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 : W.IsInvertedBy F)
:
F.obj X ⟶ F.obj Y
The image by a functor which inverts W of an equivalence class of left fractions.
Instances For
@[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 : C}
{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)
:
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}
[W.HasLeftCalculusOfFractions]
{E : Type u_3}
[CategoryTheory.Category.{u_5, u_3} E]
(F : CategoryTheory.Functor C E)
(hF : W.IsInvertedBy 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₁ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E)
(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]
:
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
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 : C}
{Y : C}
(f : W.LeftFraction 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}
[W.HasLeftCalculusOfFractions]
{X : C}
{Y : C}
(f : W.LeftFraction X Y)
(g : W.LeftFraction 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}
(φ : 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 : C}
{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 : C}
{Y : C}
(φ₁ : W.LeftFraction X Y)
(φ₂ : 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 : C}
{Y : C}
{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 : C}
{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 : C}
{Y : C}
(φ : W.LeftFraction X Y)
(ψ : 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 : 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
{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
@[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}
(φ : W.LeftFraction X Y)
:
φ.op.X' = Opposite.op φ.Y'
@[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}
(φ : W.LeftFraction X Y)
:
φ.op.s = φ.s.op
@[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}
(φ : W.LeftFraction X Y)
:
φ.op.f = φ.f.op
def
CategoryTheory.MorphismProperty.LeftFraction.op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{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
Instances For
@[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}
(φ : 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 : C}
{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 : C}
{Y : C}
(φ : W.RightFraction X Y)
:
φ.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}
(φ : 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 ⋯
Instances For
@[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ᵒᵖ}
(φ : W.LeftFraction X Y)
:
φ.unop.X' = Opposite.unop φ.Y'
@[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ᵒᵖ}
(φ : W.LeftFraction X Y)
:
φ.unop.f = φ.f.unop
@[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ᵒᵖ}
(φ : W.LeftFraction X Y)
:
φ.unop.s = φ.s.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ᵒᵖ}
(φ : 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
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ᵒᵖ}
(φ : 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 : Cᵒᵖ}
{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 : Cᵒᵖ}
{Y : Cᵒᵖ}
(φ : W.RightFraction X Y)
:
φ.unop.s = φ.s.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ᵒᵖ}
(φ : 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 ⋯
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}
(φ : 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 : C}
{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 : C}
{Y : C}
(z₁ : W.RightFraction X Y)
(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.
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₁ : W.RightFraction X Y}
{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 : Cᵒᵖ}
{Y : Cᵒᵖ}
{z₁ : W.RightFraction X Y}
{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 : C}
{Y : C}
{z₁ : W.LeftFraction X Y}
{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 : Cᵒᵖ}
{Y : Cᵒᵖ}
{z₁ : W.LeftFraction X Y}
{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 : C}
{Y : C}
(z₁ : W.RightFraction X Y)
(z₂ : W.RightFraction 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₁ : W.LeftFraction X Y)
(z₂ : W.LeftFraction 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 : W.RightFraction 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₁ : W.RightFraction X Y}
{z₂ : W.RightFraction 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₁ : W.RightFraction X Y}
{z₂ : W.RightFraction X Y}
{z₃ : W.RightFraction X Y}
[W.HasRightCalculusOfFractions]
(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)
[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 : C}
{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 : C}
{Y : C}
(φ : W.RightFraction X Y)
(ψ : 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 : 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)
[L.IsLocalization W]
[W.HasRightCalculusOfFractions]
:
L.mapArrow.EssSurj