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

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

• Y' : C

  the auxiliary object of a left fraction

• f : X ⟶ self.Y'

  the numerator of a left fraction

• s : Y ⟶ self.Y'

  the denominator of a left fraction

• hs : W self.s

  the condition that the denominator belongs to the given morphism property

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

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

Equations

• CategoryTheory.MorphismProperty.LeftFraction.ofHom W f = { Y' := Y, f := f, s := CategoryTheory.CategoryStruct.id Y, hs := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs = { Y' := X, f := CategoryTheory.CategoryStruct.id X, s := s, hs := hs }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

• X' : C

  the auxiliary object of a right fraction

• s : self.X' ⟶ X

  the denominator of a right fraction

• hs : W self.s

  the condition that the denominator belongs to the given morphism property

• f : self.X' ⟶ Y

  the numerator of a right fraction

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

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

Equations

• CategoryTheory.MorphismProperty.RightFraction.ofHom W f = { X' := X, s := CategoryTheory.CategoryStruct.id X, hs := ⋯, f := f }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.MorphismProperty.RightFraction.ofInv s hs = { X' := Y, s := s, hs := hs, f := CategoryTheory.CategoryStruct.id Y }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) : ∃ (ψ : W.LeftFraction X Y), CategoryStruct.comp φ.f ψ.s = CategoryStruct.comp φ.s ψ.f

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

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

Equations

• φ.leftFraction = ⋯.choose

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

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

theorem CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y) : ∃ (ψ : W.RightFraction X Y), CategoryStruct.comp ψ.s φ.f = CategoryStruct.comp ψ.f φ.s

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

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

Equations

• φ.rightFraction = ⋯.choose

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

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

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

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

Equations

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

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

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

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

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

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

Auxiliary definition for the composition of left fractions.

Equations

• z₁.comp₀ z₂ z₃ = { Y' := z₃.Y', f := CategoryTheory.CategoryStruct.comp z₁.f z₃.f, s := CategoryTheory.CategoryStruct.comp z₂.s z₃.s, hs := ⋯ }

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

• z₁.comp z₂ = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk (z₁.comp₀ z₂ { X' := Y, s := z₁.s, hs := ⋯, f := z₂.f }.leftFraction)

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

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

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

Equations

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

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

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

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

Equations

• CategoryTheory.MorphismProperty.LeftFraction.Localization x✝ = C

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

Equations

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

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

The localization functor to the constructed localized category for a morphism property that has left calculus of fractions.

Equations

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

@[simp]

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

@[reducible, inline]

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

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

Equations

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

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

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

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

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

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

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

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

Equations

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) : CategoryStruct.comp ((Q W).map s) (Qinv s hs) = CategoryStruct.id ((Q W).obj X)

@[simp]

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

@[simp]

theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s) : CategoryStruct.comp (Qinv s hs) ((Q W).map s) = CategoryStruct.id ((Q W).obj Y)

@[simp]

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

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) (L : Functor C D) [L.IsLocalization W] : φ.map L ⋯ = CategoryStruct.comp (L.map φ.f) (Localization.isoOfHom L W φ.s ⋯).inv

theorem CategoryTheory.MorphismProperty.LeftFraction.map_compatibility {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] {W : MorphismProperty C} {X Y : C} (φ : W.LeftFraction X Y) {E : Type u_3} [Category.{u_5, u_3} E] (L₁ : Functor C D) (L₂ : Functor C E) [L₁.IsLocalization W] [L₂.IsLocalization W] : (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) = CategoryStruct.comp ((Localization.compUniqFunctor L₁ L₂ W).hom.app X) (CategoryStruct.comp (φ.map L₂ ⋯) ((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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] {W : MorphismProperty C} {X Y : C} (φ₁ φ₂ : W.LeftFraction X Y) {E : Type u_3} [Category.{u_5, u_3} E] (L₁ : Functor C D) (L₂ : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {W : MorphismProperty C} [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z) (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : CategoryStruct.comp z₂.f z₃.s = CategoryStruct.comp z₁.s z₃.f) (L : Functor C D) [L.IsLocalization W] : 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} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) : ∃ (φ : W.LeftFraction X Y), f = φ.map L ⋯

theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (φ ψ : W.LeftFraction X Y) : φ.map L ⋯ = ψ.map L ⋯ ↔ LeftFractionRel φ ψ

theorem CategoryTheory.MorphismProperty.map_eq_iff_postcomp {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y) : L.map f₁ = L.map f₂ ↔ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), CategoryStruct.comp f₁ s = CategoryStruct.comp f₂ s

theorem CategoryTheory.Localization.essSurj_mapArrow {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] : L.mapArrow.EssSurj

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

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

Equations

• φ.op = { X' := Opposite.op φ.Y', s := φ.s.op, hs := ⋯, f := φ.f.op }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• φ.op = { Y' := Opposite.op φ.X', f := φ.f.op, s := φ.s.op, hs := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• φ.unop = { X' := Opposite.unop φ.Y', s := φ.s.unop, hs := ⋯, f := φ.f.unop }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• φ.unop = { Y' := Opposite.unop φ.X', f := φ.f.unop, s := φ.s.unop, hs := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.MorphismProperty.RightFraction.map_eq_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {X Y : C} (φ ψ : W.RightFraction X Y) : φ.map L ⋯ = ψ.map L ⋯ ↔ RightFractionRel φ ψ

theorem CategoryTheory.MorphismProperty.map_eq_iff_precomp {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] {Y Z : C} (f₁ f₂ : Y ⟶ Z) : L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), CategoryStruct.comp s f₁ = CategoryStruct.comp s f₂

theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] : L.mapArrow.EssSurj