Documentation

Mathlib.CategoryTheory.Localization.CalculusOfFractions

Calculus of fractions #

Following the definitions by [Gabriel and Zisman][gabriel-zisman-1967], given a morphism property W : MorphismProperty C on a category C, we introduce the class W.HasLeftCalculusOfFractions. The main result Localization.exists_leftFraction is that if L : C ⥤ D is a localization functor for W, then for any morphism L.obj X ⟶ L.obj Y in D, there exists an auxiliary object Y' : C and morphisms g : X ⟶ Y' and s : Y ⟶ Y', with W s, such that the given morphism is a sort of fraction g / s, or more precisely of the form L.map g ≫ (Localization.isoOfHom L W s hs).inv. We also show that the functor L.mapArrow : Arrow C ⥤ Arrow D is essentially surjective.

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

References #

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

    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
      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
        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) :
          @[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.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

          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

            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
              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
                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) :
                  @[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] :
                  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

                  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.

                  Instances
                    theorem CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [self : W.HasLeftCalculusOfFractions] ⦃X : C ⦃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} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [self : W.HasLeftCalculusOfFractions] ⦃X' : C ⦃X : C ⦃Y : C (f₁ : X Y) (f₂ : X Y) (s : X' X) :

                    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.

                    Instances
                      theorem CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [self : W.HasRightCalculusOfFractions] ⦃X : C ⦃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} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} [self : W.HasRightCalculusOfFractions] ⦃X : C ⦃Y : C ⦃Y' : C (f₁ : X Y) (f₂ : X Y) (s : Y Y') :
                      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) :
                        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) :
                          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.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
                            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.

                              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
                              Instances For

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

                                Equations
                                Instances For
                                  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
                                  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) :

                                    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) :

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

                                      Equations
                                      Instances For

                                        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

                                          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

                                            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
                                            Instances For

                                              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

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  theorem CategoryTheory.MorphismProperty.LeftFraction.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] :
                                                  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] :
                                                  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_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
                                                  @[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'
                                                  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
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.MorphismProperty.RightFraction.op_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : W.RightFraction X Y) :
                                                    φ.op.f = φ.f.op
                                                    @[simp]
                                                    theorem CategoryTheory.MorphismProperty.RightFraction.op_Y' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : W.RightFraction X Y) :
                                                    φ.op.Y' = Opposite.op φ.X'
                                                    @[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
                                                    Instances For
                                                      @[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

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

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

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

                                                        Equations
                                                        Instances For
                                                          theorem CategoryTheory.MorphismProperty.RightFraction.op_map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {W : CategoryTheory.MorphismProperty C} {X : C} {Y : C} (φ : 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
                                                          Equations
                                                          • =
                                                          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.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) :
                                                            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₂