module Cat.Morphism.Factorisation where
Factorisations🔗
module _ {o ℓ ℓl ℓr} (C : Precategory o ℓ) (L : Arrows C ℓl) (R : Arrows C ℓr) where private module C = Cat.Reasoning C
Let be two classes of morphisms of An factorisation of a morphism consists of an object and a pair of morphisms such that and
record Factorisation {a b} (f : C.Hom a b) : Type (o ⊔ ℓ ⊔ ℓl ⊔ ℓr) where field mid : C.Ob left : C.Hom a mid right : C.Hom mid b left∈L : left ∈ L right∈R : right ∈ R factors : f ≡ right C.∘ left
module _ {o ℓ ℓl ℓr} {C : Precategory o ℓ} {L : Arrows C ℓl} {R : Arrows C ℓr} where private module C = Cat.Reasoning C open Factorisation
Properties of factorisations🔗
If is monic and factors as then must also be monic.
factor-monic→left-monic : ∀ {x y} {f : C.Hom x y} → (f-fac : Factorisation C L R f) → C.is-monic f → C.is-monic (f-fac .left) factor-monic→left-monic {f = f} f-fac f-monic = C.monic-cancell $ C.subst-is-monic (f-fac .factors) f-monic
If is epic and factors as then must also be epic.
factor-epic→right-epic : ∀ {x y} {f : C.Hom x y} → (f-fac : Factorisation C L R f) → C.is-epic f → C.is-epic (f-fac .right) factor-epic→right-epic {f = f} f-fac f-epic = C.epic-cancelr $ C.subst-is-epic (f-fac .factors) f-epic