The factorization axiom #
In this file, we introduce a type-class HasFactorization W₁ W₂
, which, given
two classes of morphisms W₁
and W₂
in a category C
, asserts that any morphism
in C
can be factored as a morphism in W₁
followed by a morphism in W₂
. The data
of such factorizations can be packaged in the type FactorizationData W₁ W₂
.
This shall be used in the formalization of model categories for which the CM5 axiom asserts that any morphism can be factored as a cofibration followed by a trivial fibration (or a trivial cofibration followed by a fibration).
We also provide a structure FunctorialFactorizationData W₁ W₂
which contains
the data of a functorial factorization as above. With this design, when we
formalize certain constructions (e.g. cylinder objects in model categories),
we may first construct them using using data : FactorizationData W₁ W₂
.
Without duplication of code, it shall be possible to show these cylinders
are functorial when a term data : FunctorialFactorizationData W₁ W₂
is available,
the existence of which is asserted in the type-class HasFunctorialFactorization W₁ W₂
.
We also introduce the class W₁.comp W₂
of morphisms of the form i ≫ p
with W₁ i
and W₂ p
and show that W₁.comp W₂ = ⊤
iff HasFactorization W₁ W₂
holds (this
is MorphismProperty.comp_eq_top_iff
).
Given two classes of morphisms W₁
and W₂
on a category C
, this is
the data of the factorization of a morphism f : X ⟶ Y
as i ≫ p
with
W₁ i
and W₂ p
.
- Z : C
the intermediate object in the factorization
- i : X ⟶ self.Z
the first morphism in the factorization
- p : self.Z ⟶ Y
the second morphism in the factorization
- fac : CategoryTheory.CategoryStruct.comp self.i self.p = f
- hi : W₁ self.i
- hp : W₂ self.p
Instances For
The data of a term in MapFactorizationData W₁ W₂ f
for any morphism f
.
Instances For
The factorization axiom for two classes of morphisms W₁
and W₂
in a category C
. It
asserts that any morphism can be factored as a morphism in W₁
followed by a morphism
in W₂
.
Instances
A chosen term in FactorizationData W₁ W₂
when HasFactorization W₁ W₂
holds.
Equations
- W₁.factorizationData W₂ x = ⋯.some
Instances For
The class of morphisms that are of the form i ≫ p
with W₁ i
and W₂ p
.
Instances For
The data of a functorial factorization of any morphism in C
as a morphism in W₁
followed by a morphism in W₂
.
- Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C
the intermediate objects in the factorizations
- i : CategoryTheory.Arrow.leftFunc ⟶ self.Z
the first morphism in the factorizations
- p : self.Z ⟶ CategoryTheory.Arrow.rightFunc
the second morphism in the factorizations
- fac : CategoryTheory.CategoryStruct.comp self.i self.p = CategoryTheory.Arrow.leftToRight
- hi : ∀ (f : CategoryTheory.Arrow C), W₁ (self.i.app f)
- hp : ∀ (f : CategoryTheory.Arrow C), W₂ (self.p.app f)
Instances For
If W₁ ≤ W₁'
and W₂ ≤ W₂'
, then a functorial factorization for W₁
and W₂
induces
a functorial factorization for W₁'
and W₂'
.
Equations
- data.ofLE le₁ le₂ = { Z := data.Z, i := data.i, p := data.p, fac := ⋯, hi := ⋯, hp := ⋯ }
Instances For
The term in FactorizationData W₁ W₂
that is deduced from a functorial factorization.
Equations
- data.factorizationData f = { Z := data.Z.obj (CategoryTheory.Arrow.mk f), i := data.i.app (CategoryTheory.Arrow.mk f), p := data.p.app (CategoryTheory.Arrow.mk f), fac := ⋯, hi := ⋯, hp := ⋯ }
Instances For
When data : FunctorialFactorizationData W₁ W₂
, this is the
morphism (data.factorizationData f).Z ⟶ (data.factorizationData g).Z
expressing the
functoriality of the intermediate objects of the factorizations
for φ : Arrow.mk f ⟶ Arrow.mk g
.
Equations
- data.mapZ φ = data.Z.map φ
Instances For
Auxiliary definition for FunctorialFactorizationData.functorCategory
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functorial factorization in the category C
extends to the functor category J ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functorial factorization axiom for two classes of morphisms W₁
and W₂
in a
category C
. It asserts that any morphism can be factored in a functorial manner
as a morphism in W₁
followed by a morphism in W₂
.
- nonempty_functorialFactorizationData : Nonempty (W₁.FunctorialFactorizationData W₂)
Instances
A chosen term in FunctorialFactorizationData W₁ W₂
when the functorial factorization
axiom HasFunctorialFactorization W₁ W₂
holds.
Equations
- W₁.functorialFactorizationData W₂ = ⋯.some