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.

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

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

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

• h : d.mid ⟶ e.mid

  The morphism between the midpoints of the factorizations.

• ι_h : CategoryTheory.CategoryStruct.comp d.ι self.h = e.ι

  The left commuting triangle of the factorization morphism.

• h_π : CategoryTheory.CategoryStruct.comp self.h e.π = d.π

  The right commuting triangle of the factorization morphism.

@[simp]

theorem CategoryTheory.Factorisation.Hom.id_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} (d : CategoryTheory.Factorisation f) : (CategoryTheory.Factorisation.Hom.id d).h = CategoryTheory.CategoryStruct.id d.mid

def CategoryTheory.Factorisation.Hom.id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} (d : CategoryTheory.Factorisation f) : CategoryTheory.Factorisation.Hom d d

The identity morphism of Factorisation f.

Equations

• CategoryTheory.Factorisation.Hom.id d = CategoryTheory.Factorisation.Hom.mk (CategoryTheory.CategoryStruct.id d.mid)

@[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 : CategoryTheory.Factorisation.Hom d₁ d₂) (g : CategoryTheory.Factorisation.Hom d₂ d₃) : (CategoryTheory.Factorisation.Hom.comp f g).h = CategoryTheory.CategoryStruct.comp f.h g.h

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 : CategoryTheory.Factorisation.Hom d₁ d₂) (g : CategoryTheory.Factorisation.Hom d₂ d₃) : CategoryTheory.Factorisation.Hom d₁ d₃

Composition of morphisms in Factorisation f.

Equations

• CategoryTheory.Factorisation.Hom.comp f g = CategoryTheory.Factorisation.Hom.mk (CategoryTheory.CategoryStruct.comp f.h g.h)

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

Equations

• CategoryTheory.Factorisation.instCategoryFactorisation = CategoryTheory.Category.mk

@[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

def CategoryTheory.Factorisation.initial {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.Factorisation f

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

Equations

• CategoryTheory.Factorisation.initial = CategoryTheory.Factorisation.mk X (CategoryTheory.CategoryStruct.id X) f

@[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) : (CategoryTheory.Factorisation.initialHom d).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.Hom CategoryTheory.Factorisation.initial d

The unique morphism out of Factorisation.initial f.

Equations

• CategoryTheory.Factorisation.initialHom d = CategoryTheory.Factorisation.Hom.mk d.ι

instance CategoryTheory.Factorisation.instUniqueHomFactorisationToQuiverToCategoryStructInstCategoryFactorisationInitial {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

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

@[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

def CategoryTheory.Factorisation.terminal {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.Factorisation f

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

Equations

• CategoryTheory.Factorisation.terminal = CategoryTheory.Factorisation.mk Y f (CategoryTheory.CategoryStruct.id Y)

@[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) : (CategoryTheory.Factorisation.terminalHom d).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) : CategoryTheory.Factorisation.Hom d CategoryTheory.Factorisation.terminal

The unique morphism into Factorisation.terminal f.

Equations

• CategoryTheory.Factorisation.terminalHom d = CategoryTheory.Factorisation.Hom.mk d.π

instance CategoryTheory.Factorisation.instUniqueHomFactorisationToQuiverToCategoryStructInstCategoryFactorisationTerminal {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

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

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

• CategoryTheory.Factorisation.IsInitial_initial = CategoryTheory.Limits.IsInitial.ofUnique CategoryTheory.Factorisation.initial

instance CategoryTheory.Factorisation.instHasInitialFactorisationInstCategoryFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.Limits.HasInitial (CategoryTheory.Factorisation f)

Equations

• (_ : CategoryTheory.Limits.HasInitial (CategoryTheory.Factorisation f)) = (_ : CategoryTheory.Limits.HasInitial (CategoryTheory.Factorisation f))

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

• CategoryTheory.Factorisation.IsTerminal_terminal = CategoryTheory.Limits.IsTerminal.ofUnique CategoryTheory.Factorisation.terminal

instance CategoryTheory.Factorisation.instHasTerminalFactorisationInstCategoryFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.Limits.HasTerminal (CategoryTheory.Factorisation f)

Equations

• (_ : CategoryTheory.Limits.HasTerminal (CategoryTheory.Factorisation f)) = (_ : CategoryTheory.Limits.HasTerminal (CategoryTheory.Factorisation f))

@[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.toPrefunctor.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.toPrefunctor.map f_1 = f_1.h

def CategoryTheory.Factorisation.forget {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.Functor (CategoryTheory.Factorisation f) C

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

Equations

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