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)
  • mid : C

    The midpoint of the factorisation.

  • ι : X s.mid

    The morphism into the factorisation midpoint.

  • π : s.mid Y

    The morphism out of the factorisation midpoint.

  • The factorisation condition.

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

Instances For
    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 : CategoryTheory.Factorisation.Hom d e), x.h = y.hx = y

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

    Instances For

      The identity morphism of Factorisation f.

      Instances For
        @[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.

        Instances For
          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.Hom CategoryTheory.Factorisation.initial d

          The unique morphism out of Factorisation.initial f.

          Instances For
            @[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
            @[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_π {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} :
            CategoryTheory.Factorisation.terminal = CategoryTheory.CategoryStruct.id Y

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

            Instances For
              def CategoryTheory.Factorisation.terminalHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (d : CategoryTheory.Factorisation f) :
              CategoryTheory.Factorisation.Hom d CategoryTheory.Factorisation.terminal

              The unique morphism into Factorisation.terminal f.

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

                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

                  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 Y : CategoryTheory.Factorisation f} (f : X Y), CategoryTheory.Factorisation.forget.map f = f.h

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

                    Instances For