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
.
- 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
- 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
The identity morphism of Factorisation f
.
Instances For
Composition of morphisms in Factorisation f
.
Instances For
The initial object in Factorisation f
, with the domain of f
as its midpoint.
Instances For
The unique morphism out of Factorisation.initial f
.
Instances For
The terminal object in Factorisation f
, with the codomain of f
as its midpoint.
Instances For
The unique morphism into Factorisation.terminal f
.
Instances For
The initial factorisation is an initial object
Instances For
The terminal factorisation is a terminal object
Instances For
The forgetful functor from Factorisation f
to the underlying category C
.