# 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} {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.

• ι_π : = f

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_iff {C : Type u} :
∀ {inst : } {X Y : C} {f : X Y} {d e : } (x y : ), x = y x.h = y.h
theorem CategoryTheory.Factorisation.Hom.ext {C : Type u} :
∀ {inst : } {X Y : C} {f : X Y} {d e : } (x y : ), x.h = y.hx = y
structure CategoryTheory.Factorisation.Hom {C : Type u} {X : C} {Y : C} {f : X Y} (d : ) (e : ) :
Type (max u v)
• h : d.mid e.mid

The morphism between the midpoints of the factorizations.

• ι_h : = e

The left commuting triangle of the factorization morphism.

• h_π : = d

The right commuting triangle of the factorization morphism.

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

Instances For
@[simp]
theorem CategoryTheory.Factorisation.Hom.id_h {C : Type u} {X : C} {Y : C} {f : X Y} (d : ) :
def CategoryTheory.Factorisation.Hom.id {C : Type u} {X : C} {Y : C} {f : X Y} (d : ) :

The identity morphism of Factorisation f.

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

Composition of morphisms in Factorisation f.

Instances For
instance CategoryTheory.Factorisation.instCategoryFactorisation {C : Type u} {X : C} {Y : C} {f : X Y} :
@[simp]
theorem CategoryTheory.Factorisation.initial_mid {C : Type u} {X : C} {Y : C} {f : X Y} :
CategoryTheory.Factorisation.initial.mid = X
@[simp]
theorem CategoryTheory.Factorisation.initial_π {C : Type u} {X : C} {Y : C} {f : X Y} :
CategoryTheory.Factorisation.initial = f
@[simp]
theorem CategoryTheory.Factorisation.initial_ι {C : Type u} {X : C} {Y : C} {f : X Y} :
CategoryTheory.Factorisation.initial =
def CategoryTheory.Factorisation.initial {C : Type u} {X : C} {Y : C} {f : X Y} :

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

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

The unique morphism out of Factorisation.initial f.

Instances For
instance CategoryTheory.Factorisation.instUniqueHomFactorisationToQuiverToCategoryStructInstCategoryFactorisationInitial {C : Type u} {X : C} {Y : C} {f : X Y} (d : ) :
Unique (CategoryTheory.Factorisation.initial d)
@[simp]
theorem CategoryTheory.Factorisation.terminal_mid {C : Type u} {X : C} {Y : C} {f : X Y} :
CategoryTheory.Factorisation.terminal.mid = Y
@[simp]
theorem CategoryTheory.Factorisation.terminal_ι {C : Type u} {X : C} {Y : C} {f : X Y} :
CategoryTheory.Factorisation.terminal = f
@[simp]
theorem CategoryTheory.Factorisation.terminal_π {C : Type u} {X : C} {Y : C} {f : X Y} :
CategoryTheory.Factorisation.terminal =
def CategoryTheory.Factorisation.terminal {C : Type u} {X : C} {Y : C} {f : X Y} :

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

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

The unique morphism into Factorisation.terminal f.

Instances For
instance CategoryTheory.Factorisation.instUniqueHomFactorisationToQuiverToCategoryStructInstCategoryFactorisationTerminal {C : Type u} {X : C} {Y : C} {f : X Y} (d : ) :
Unique (d CategoryTheory.Factorisation.terminal)
def CategoryTheory.Factorisation.IsInitial_initial {C : Type u} {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} {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} {X : C} {Y : C} {f : X Y} (self : ) :
CategoryTheory.Factorisation.forget.obj self = self.mid
@[simp]
theorem CategoryTheory.Factorisation.forget_map {C : Type u} {X : C} {Y : C} {f : X Y} :
∀ {X Y : } (f : X Y), CategoryTheory.Factorisation.forget.map f = f.h
def CategoryTheory.Factorisation.forget {C : Type u} {X : C} {Y : C} {f : X Y} :

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

Instances For