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.
- ι_π : CategoryTheory.CategoryStruct.comp s.ι s.π = 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 : 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)
- h : d.mid ⟶ e.mid
The morphism between the midpoints of the factorizations.
- ι_h : CategoryTheory.CategoryStruct.comp d.ι s.h = e.ι
The left commuting triangle of the factorization morphism.
- h_π : CategoryTheory.CategoryStruct.comp s.h e.π = 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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
def
CategoryTheory.Factorisation.Hom.id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
The identity morphism of Factorisation f.
Instances For
@[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₃)
:
Composition of morphisms in Factorisation f.
Instances For
instance
CategoryTheory.Factorisation.instCategoryFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
:
@[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}
:
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}
[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.
Instances For
instance
CategoryTheory.Factorisation.instUniqueHomFactorisationToQuiverToCategoryStructInstCategoryFactorisationInitial
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
@[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}
:
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}
[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.
Instances For
instance
CategoryTheory.Factorisation.instUniqueHomFactorisationToQuiverToCategoryStructInstCategoryFactorisationTerminal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(d : CategoryTheory.Factorisation f)
:
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
instance
CategoryTheory.Factorisation.instHasInitialFactorisationInstCategoryFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
:
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
instance
CategoryTheory.Factorisation.instHasTerminalFactorisationInstCategoryFactorisation
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
:
@[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
def
CategoryTheory.Factorisation.forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{f : X ⟶ Y}
:
The forgetful functor from Factorisation f to the underlying category C.