Calculus of fractions #
Following the definitions by [Gabriel and Zisman][gabriel-zisman-1967],
given a morphism property W : MorphismProperty C on a category C,
we introduce the class W.HasLeftCalculusOfFractions. The main
result (TODO) is that if L : C ⥤ D is a localization functor for W,
then for any morphism L.obj X ⟶ L.obj Y in D, there exists an auxiliary
object Y' : C and morphisms g : X ⟶ Y' and s : Y ⟶ Y', with W s, such
that the given morphism is a sort of fraction g / s, or more precisely of
the form L.map g ≫ (Localization.isoOfHom L W s hs).inv.
References #
- [P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory][gabriel-zisman-1967]
structure
CategoryTheory.MorphismProperty.LeftFraction
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W : CategoryTheory.MorphismProperty C)
(X : C)
(Y : C)
:
Type (max u_1 u_2)
A left fraction from X : C to Y : C for W : MorphismProperty C consists of the
datum of an object Y' : C and maps f : X ⟶ Y' and s : Y ⟶ Y' such that W s.
- Y' : C
the auxiliary object of a left fraction
- f : X ⟶ 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_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofHom_Y'
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.ofInv_s
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
def
CategoryTheory.MorphismProperty.LeftFraction.ofInv
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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.toPrefunctor.obj X ⟶ L.toPrefunctor.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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
{C : Type u_1}
{D : Type u_4}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.obj φ.Y' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.map φ L hL)
(CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map φ.s) h) = CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map φ.f) h
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s
{C : Type u_1}
{D : Type u_4}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.map φ.s) = L.toPrefunctor.map φ.f
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_ofHom
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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]
:
CategoryTheory.MorphismProperty.LeftFraction.map (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f) L hL = L.toPrefunctor.map f
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id_assoc
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MorphismProperty.LeftFraction.map (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs) L hL)
(CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map s) h) = h
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MorphismProperty.LeftFraction.map (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs) L hL)
(L.toPrefunctor.map s) = CategoryTheory.CategoryStruct.id (L.toPrefunctor.obj X)
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id_assoc
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map s)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MorphismProperty.LeftFraction.map (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs) L hL)
h) = h
@[simp]
theorem
CategoryTheory.MorphismProperty.LeftFraction.map_hom_ofInv_id
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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)
:
CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map s)
(CategoryTheory.MorphismProperty.LeftFraction.map (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs) L hL) = CategoryTheory.CategoryStruct.id (L.toPrefunctor.obj Y)
theorem
CategoryTheory.MorphismProperty.LeftFraction.cases
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, u_1} C]
(W : CategoryTheory.MorphismProperty C)
(X : C)
(Y : C)
:
Type (max u_1 u_2)
A right fraction from X : C to Y : C for W : MorphismProperty C consists of the
datum of an object X' : C and maps s : X' ⟶ X and f : X' ⟶ Y such that W s.
- X' : C
the auxiliary object of a right fraction
- s : 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_X'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.MorphismProperty.ContainsIdentities W]
:
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofHom_s
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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_X'
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_s
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
(s : Y ⟶ X)
(hs : W s)
:
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.ofInv_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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.toPrefunctor.obj X ⟶ L.toPrefunctor.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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map_assoc
{C : Type u_1}
{D : Type u_4}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map φ.s)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.RightFraction.map φ L hL) h) = CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map φ.f) h
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map
{C : Type u_1}
{D : Type u_4}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.map φ.s) (CategoryTheory.MorphismProperty.RightFraction.map φ L hL) = L.toPrefunctor.map φ.f
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_ofHom
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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]
:
CategoryTheory.MorphismProperty.RightFraction.map (CategoryTheory.MorphismProperty.RightFraction.ofHom W f) L hL = L.toPrefunctor.map f
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id_assoc
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MorphismProperty.RightFraction.map (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs) L hL)
(CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map s) h) = h
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_ofInv_hom_id
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MorphismProperty.RightFraction.map (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs) L hL)
(L.toPrefunctor.map s) = CategoryTheory.CategoryStruct.id (L.toPrefunctor.obj X)
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id_assoc
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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.toPrefunctor.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map s)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MorphismProperty.RightFraction.map (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs) L
hL)
h) = h
@[simp]
theorem
CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id
{C : Type u_2}
{D : Type u_4}
[CategoryTheory.Category.{u_1, u_2} C]
[CategoryTheory.Category.{u_3, u_4} 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)
:
CategoryTheory.CategoryStruct.comp (L.toPrefunctor.map s)
(CategoryTheory.MorphismProperty.RightFraction.map (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs) L
hL) = CategoryTheory.CategoryStruct.id (L.toPrefunctor.obj Y)
theorem
CategoryTheory.MorphismProperty.RightFraction.cases
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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)
- stableUnderComposition : CategoryTheory.MorphismProperty.StableUnderComposition W
- 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_2, 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)
- stableUnderComposition : CategoryTheory.MorphismProperty.StableUnderComposition W
- 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_2, 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_2, 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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_2, 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, u_1} C]
(W : CategoryTheory.MorphismProperty C)
(X : C)
(Y : C)
:
Type (max u_1 u_2)
The morphisms in the constructed localized category for a morphism property W
that has left calculus of fractions are equivalence classes of left fractions.
Equations
- 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, 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_2, u_1} C]
(W : CategoryTheory.MorphismProperty C)
[CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions W]
(X : C)
:
(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).toPrefunctor.obj X = X
def
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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.