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 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
structure
CategoryTheory.Factorisation.Hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d 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.
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 : d.Hom e}
(h : x.h = y.h)
:
x = y
def
CategoryTheory.Factorisation.Hom.id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
d.Hom d
The identity morphism of Factorisation f.
Equations
- CategoryTheory.Factorisation.Hom.id d = { h := CategoryTheory.CategoryStruct.id d.mid, ι_h := ⋯, h_π := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Factorisation.Hom.id_h
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
def
CategoryTheory.Factorisation.Hom.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
{d₁ d₂ d₃ : CategoryTheory.Factorisation f}
:
d₁.Hom d₂ → (g : d₂.Hom d₃) → d₁.Hom d₃
Composition of morphisms in Factorisation f.
Equations
- f.comp g = { h := CategoryTheory.CategoryStruct.comp f.h g.h, ι_h := ⋯, h_π := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Factorisation.Hom.comp_h
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
{d₁ d₂ d₃ : CategoryTheory.Factorisation f}
(f✝ : d₁.Hom d₂)
(g : d₂.Hom d₃)
:
(f✝.comp g).h = CategoryTheory.CategoryStruct.comp f✝.h g.h
instance
CategoryTheory.Factorisation.instCategory
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
Equations
def
CategoryTheory.Factorisation.initial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
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
@[simp]
theorem
CategoryTheory.Factorisation.initial_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.Factorisation.initial_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.Factorisation.initial_mid
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
def
CategoryTheory.Factorisation.initialHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
The unique morphism out of Factorisation.initial f.
Equations
- d.initialHom = { h := d.ι, ι_h := ⋯, h_π := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Factorisation.initialHom_h
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
d.initialHom.h = d.ι
instance
CategoryTheory.Factorisation.instUniqueHomInitial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
Equations
- d.instUniqueHomInitial = { default := d.initialHom, uniq := ⋯ }
def
CategoryTheory.Factorisation.terminal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
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
@[simp]
theorem
CategoryTheory.Factorisation.terminal_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.Factorisation.terminal_mid
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
@[simp]
theorem
CategoryTheory.Factorisation.terminal_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
def
CategoryTheory.Factorisation.terminalHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
The unique morphism into Factorisation.terminal f.
Equations
- d.terminalHom = { h := d.π, ι_h := ⋯, h_π := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Factorisation.terminalHom_h
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
d.terminalHom.h = d.π
instance
CategoryTheory.Factorisation.instUniqueHomTerminal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
Equations
- d.instUniqueHomTerminal = { default := d.terminalHom, uniq := ⋯ }
def
CategoryTheory.Factorisation.IsInitial_initial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
The initial factorisation is an initial object
Equations
Instances For
instance
CategoryTheory.Factorisation.instHasInitial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
def
CategoryTheory.Factorisation.IsTerminal_terminal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
The terminal factorisation is a terminal object
Equations
Instances For
instance
CategoryTheory.Factorisation.instHasTerminal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
def
CategoryTheory.Factorisation.forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X Y : C}
{f : X ⟶ Y}
:
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
@[simp]
theorem
CategoryTheory.Factorisation.forget_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X 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 Y : C}
{f : X ⟶ Y}
{X✝ Y✝ : CategoryTheory.Factorisation f}
(f✝ : X✝ ⟶ Y✝)
:
CategoryTheory.Factorisation.forget.map f✝ = f✝.h