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 (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 #

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 s.Y'

    the numerator of a left fraction

  • s : Y s.Y'

    the denominator of a left fraction

  • hs : W s.s

    the condition that the denominator belongs to the given morphism property

Instances For

    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

      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 : s.X' X

        the denominator of a right fraction

      • hs : W s.s

        the condition that the denominator belongs to the given morphism property

      • f : s.X' Y

        the numerator of a right fraction

      Instances For

        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

          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

            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

              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

                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

                  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

                    Auxiliary definition for the composition of left fractions.

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

                      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

                        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