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} [Category.{v, u} C] {X 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.
ι_π : CategoryStruct.comp self.ι self.π = f
The factorisation condition.

Instances For

source

@[simp]

theorem CategoryTheory.Factorisation.ι_π_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : Factorisation f) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp self.ι (CategoryStruct.comp self.π h) = CategoryStruct.comp f h

The factorisation condition.

source

structure CategoryTheory.Factorisation.Hom {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (d e : 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 : CategoryStruct.comp d.ι self.h = e.ι
The left commuting triangle of the factorization morphism.
h_π : CategoryStruct.comp self.h e.π = d.π
The right commuting triangle of the factorization morphism.

Instances For

source

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

x = y

source

theorem CategoryTheory.Factorisation.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {X Y : C} {f : X ⟶ Y} {d e : Factorisation f} {x y : d.Hom e} :

x = y ↔ x.h = y.h

source

@[simp]

theorem CategoryTheory.Factorisation.Hom.ι_h_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : Factorisation f} (self : d.Hom e) {Z : C} (h : e.mid ⟶ Z) :

CategoryStruct.comp d.ι (CategoryStruct.comp self.h h) = CategoryStruct.comp e.ι h

The left commuting triangle of the factorization morphism.

source

@[simp]

theorem CategoryTheory.Factorisation.Hom.h_π_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : Factorisation f} (self : d.Hom e) {Z : C} (h : Y ⟶ Z) :

CategoryStruct.comp self.h (CategoryStruct.comp e.π h) = CategoryStruct.comp d.π h

The right commuting triangle of the factorization morphism.

source

@[implicit_reducible]

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

Quiver (Factorisation f)

Equations

CategoryTheory.Factorisation.instQuiver = { Hom := fun (d e : CategoryTheory.Factorisation f) => d.Hom e }

source

@[implicit_reducible]

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

Category.{max u v, max u v} (Factorisation f)

Equations

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

source

@[simp]

theorem CategoryTheory.Factorisation.comp_h {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X✝ Y✝ Z✝ : Factorisation f} (f✝ : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) :

(CategoryStruct.comp f✝ g).h = CategoryStruct.comp f✝.h g.h

source

@[simp]

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

(CategoryStruct.id d).h = CategoryStruct.id d.mid

source

theorem CategoryTheory.Factorisation.comp_h_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X✝ Y✝ Z✝ : Factorisation f} (f✝ : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) {Z : C} (h : Z✝.mid ⟶ Z) :

CategoryStruct.comp (CategoryStruct.comp f✝ g).h h = CategoryStruct.comp f✝.h (CategoryStruct.comp g.h h)

source

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

Factorisation f

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

Equations

CategoryTheory.Factorisation.initial = { mid := X, ι := CategoryTheory.CategoryStruct.id X, π := f, ι_π := ⋯ }

Instances For

source

@[simp]

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

Factorisation.initial.mid = X

source

@[simp]

theorem CategoryTheory.Factorisation.initial_π {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} :

Factorisation.initial.π = f

source

@[simp]

theorem CategoryTheory.Factorisation.initial_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} :

Factorisation.initial.ι = CategoryStruct.id X

source

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

Factorisation.initial.Hom d

The unique morphism out of Factorisation.initial f.

Equations

d.initialHom = { h := d.ι, ι_h := ⋯, h_π := ⋯ }

Instances For

source

@[simp]

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

d.initialHom.h = d.ι

source

@[implicit_reducible]

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

Unique (Factorisation.initial ⟶ d)

Equations

d.instUniqueHomInitial = { default := d.initialHom, uniq := ⋯ }

source

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

Factorisation f

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

Equations

CategoryTheory.Factorisation.terminal = { mid := Y, ι := f, π := CategoryTheory.CategoryStruct.id Y, ι_π := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Factorisation.terminal_ι {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} :

Factorisation.terminal.ι = f

source

@[simp]

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

Factorisation.terminal.mid = Y

source

@[simp]

theorem CategoryTheory.Factorisation.terminal_π {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} :

Factorisation.terminal.π = CategoryStruct.id Y

source

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

d.Hom Factorisation.terminal

The unique morphism into Factorisation.terminal f.

Equations

d.terminalHom = { h := d.π, ι_h := ⋯, h_π := ⋯ }

Instances For

source

@[simp]

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

d.terminalHom.h = d.π

source

@[implicit_reducible]

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

Unique (d ⟶ Factorisation.terminal)

Equations

d.instUniqueHomTerminal = { default := d.terminalHom, uniq := ⋯ }

source

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

Limits.IsInitial Factorisation.initial

The initial factorisation is an initial object

Equations

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

Instances For

source

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

Limits.HasInitial (Factorisation f)

source

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

Limits.IsTerminal Factorisation.terminal

The terminal factorisation is a terminal object

Equations

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

Instances For

source

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

Limits.HasTerminal (Factorisation f)

source

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

Functor (Factorisation f) C

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

source

@[simp]

theorem CategoryTheory.Factorisation.forget_map {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X✝ Y✝ : Factorisation f} (f✝ : X✝ ⟶ Y✝) :

forget.map f✝ = f✝.h

source

@[simp]

theorem CategoryTheory.Factorisation.forget_obj {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : Factorisation f) :

forget.obj self = self.mid

Documentation

Mathlib.CategoryTheory.Category.Factorisation

The Factorisation Category of a Category #