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
the first morphism in the factorization
the second morphism in the factorization
- hi : W₁ self.i
- hp : W₂ self.p
Instances For
The data of a term in MapFactorizationData W₁ W₂ f for any morphism f.
Equations
- W₁.FactorizationData W₂ = ({X Y : C} → (f : X ⟶ Y) → W₁.MapFactorizationData W₂ 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.
Equations
- W₁.comp W₂ f = Nonempty (W₁.MapFactorizationData W₂ f)
Instances For
The data of a functorial factorization of any morphism in C as a morphism in W₁
followed by a morphism in W₂.
the intermediate objects in the factorizations
the first morphism in the factorizations
the second morphism in the factorizations
Instances For
If W₁ ≤ W₁' and W₂ ≤ W₂', then a functorial factorization for W₁ and W₂ induces
a functorial factorization for W₁' and W₂'.
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.
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