Documentation

Mathlib.CategoryTheory.Category.Factorisation

The Factorisation Category of a Category #

Factorisation f is the category containing as objects all factorisations of a morphism f.

We show that Factorisation f always has an initial and a terminal object.

TODO: Show that Factorisation f is isomorphic to a comma category in two ways.

TODO: Make MonoFactorisation f a special case of a Factorisation f.

structure CategoryTheory.Factorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :
Type (max u v)

Factorisations of a morphism f as a structure, containing, one object, two morphisms, and the condition that their composition equals f.

  • mid : C

    The midpoint of the factorisation.

  • ι : X self.mid

    The morphism into the factorisation midpoint.

  • π : self.mid Y

    The morphism out of the factorisation midpoint.

  • ι_π : CategoryTheory.CategoryStruct.comp self self = f

    The factorisation condition.

Instances For
    @[simp]

    The factorisation condition.

    theorem CategoryTheory.Factorisation.Hom.ext_iff {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X Y} {d e : CategoryTheory.Factorisation f} (x y : d.Hom e), x = y x.h = y.h
    theorem CategoryTheory.Factorisation.Hom.ext {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X Y} {d e : CategoryTheory.Factorisation f} (x y : d.Hom e), x.h = y.hx = y

    Morphisms of Factorisation f consist of morphism between their midpoints and the obvious commutativity conditions.

    Instances For
      @[simp]

      The left commuting triangle of the factorization morphism.

      @[simp]

      The right commuting triangle of the factorization morphism.

      The identity morphism of Factorisation f.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Factorisation.Hom.comp_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {d₁ : CategoryTheory.Factorisation f✝} {d₂ : CategoryTheory.Factorisation f✝} {d₃ : CategoryTheory.Factorisation f✝} (f : d₁.Hom d₂) (g : d₂.Hom d₃) :
        def CategoryTheory.Factorisation.Hom.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {d₁ : CategoryTheory.Factorisation f✝} {d₂ : CategoryTheory.Factorisation f✝} {d₃ : CategoryTheory.Factorisation f✝} (f : d₁.Hom d₂) (g : d₂.Hom d₃) :
        d₁.Hom d₃

        Composition of morphisms in Factorisation f.

        Equations
        Instances For
          Equations
          @[simp]
          theorem CategoryTheory.Factorisation.initial_mid {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
          CategoryTheory.Factorisation.initial.mid = X
          @[simp]
          theorem CategoryTheory.Factorisation.initial_π {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
          CategoryTheory.Factorisation.initial = f
          @[simp]
          theorem CategoryTheory.Factorisation.initial_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
          CategoryTheory.Factorisation.initial = CategoryTheory.CategoryStruct.id X

          The initial object in Factorisation f, with the domain of f as its midpoint.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Factorisation.initialHom_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
            d.initialHom.h = d
            def CategoryTheory.Factorisation.initialHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
            CategoryTheory.Factorisation.initial.Hom d

            The unique morphism out of Factorisation.initial f.

            Equations
            • d.initialHom = { h := d, ι_h := , h_π := }
            Instances For
              instance CategoryTheory.Factorisation.instUniqueHomInitial {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
              Unique (CategoryTheory.Factorisation.initial d)
              Equations
              • d.instUniqueHomInitial = { default := d.initialHom, uniq := }
              @[simp]
              theorem CategoryTheory.Factorisation.terminal_π {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
              CategoryTheory.Factorisation.terminal = CategoryTheory.CategoryStruct.id Y
              @[simp]
              theorem CategoryTheory.Factorisation.terminal_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
              CategoryTheory.Factorisation.terminal = f
              @[simp]
              theorem CategoryTheory.Factorisation.terminal_mid {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
              CategoryTheory.Factorisation.terminal.mid = Y

              The terminal object in Factorisation f, with the codomain of f as its midpoint.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Factorisation.terminalHom_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
                d.terminalHom.h = d
                def CategoryTheory.Factorisation.terminalHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
                d.Hom CategoryTheory.Factorisation.terminal

                The unique morphism into Factorisation.terminal f.

                Equations
                • d.terminalHom = { h := d, ι_h := , h_π := }
                Instances For
                  instance CategoryTheory.Factorisation.instUniqueHomTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
                  Unique (d CategoryTheory.Factorisation.terminal)
                  Equations
                  • d.instUniqueHomTerminal = { default := d.terminalHom, uniq := }
                  def CategoryTheory.Factorisation.IsInitial_initial {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
                  CategoryTheory.Limits.IsInitial CategoryTheory.Factorisation.initial

                  The initial factorisation is an initial object

                  Equations
                  Instances For
                    def CategoryTheory.Factorisation.IsTerminal_terminal {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
                    CategoryTheory.Limits.IsTerminal CategoryTheory.Factorisation.terminal

                    The terminal factorisation is a terminal object

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Factorisation.forget_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (self : CategoryTheory.Factorisation f) :
                      CategoryTheory.Factorisation.forget.obj self = self.mid
                      @[simp]
                      theorem CategoryTheory.Factorisation.forget_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
                      ∀ {X_1 Y_1 : CategoryTheory.Factorisation f} (f_1 : X_1 Y_1), CategoryTheory.Factorisation.forget.map f_1 = f_1.h

                      The forgetful functor from Factorisation f to the underlying category C.

                      Equations
                      • CategoryTheory.Factorisation.forget = { obj := CategoryTheory.Factorisation.mid, map := fun {X_1 Y_1 : CategoryTheory.Factorisation f} (f_1 : X_1 Y_1) => f_1.h, map_id := , map_comp := }
                      Instances For