Mathlib.CategoryTheory.MorphismProperty.Factorization

Module docstring

{"# 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).

CategoryTheory.MorphismProperty.MapFactorizationData structure

{X Y : C} (f : X ⟶ Y)

Full source

/-- 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`. -/
structure MapFactorizationData {X Y : C} (f : X ⟶ Y) where
  /-- the intermediate object in the factorization -/
  Z : C
  /-- the first morphism in the factorization -/
  i : X ⟶ Z
  /-- the second morphism in the factorization -/
  p : Z ⟶ Y
  fac : i ≫ p = f := by aesop_cat
  hi : W₁ i
  hp : W₂ p

Factorization data of a morphism into $ W_1 $ followed by $ W_2 $

Informal description

Given two classes of morphisms $ W_1 $ and $ W_2 $ in a category $ \mathcal{C} $, a `MapFactorizationData` for a morphism $ f: X \to Y $ consists of a factorization of $ f $ as $ i \circ p $, where $ i $ is in $ W_1 $ and $ p $ is in $ W_2 $.

CategoryTheory.MorphismProperty.FactorizationData abbrev

Full source

/-- The data of a term in `MapFactorizationData W₁ W₂ f` for any morphism `f`. -/
abbrev FactorizationData := ∀ {X Y : C} (f : X ⟶ Y), MapFactorizationData W₁ W₂ f

Factorization Data for Morphism Classes $W_1$ and $W_2$

Informal description

Given a category $\mathcal{C}$ and two classes of morphisms $W_1$ and $W_2$ in $\mathcal{C}$, a `FactorizationData` for $W_1$ and $W_2$ consists of, for every morphism $f: X \to Y$ in $\mathcal{C}$, a factorization of $f$ as $f = i \circ p$ where $i$ is in $W_1$ and $p$ is in $W_2$.

CategoryTheory.MorphismProperty.HasFactorization structure

Full source

/-- 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₂`. -/
class HasFactorization : Prop where
  nonempty_mapFactorizationData {X Y : C} (f : X ⟶ Y) : Nonempty (MapFactorizationData W₁ W₂ f)

Factorization axiom for morphism classes $W_1$ and $W_2$

Informal description

Given a category $\mathcal{C}$ and two classes of morphisms $W_1$ and $W_2$ in $\mathcal{C}$, the structure `HasFactorization W₁ W₂` asserts that every morphism $f: X \to Y$ in $\mathcal{C}$ can be factored as $f = i \circ p$, where $i$ belongs to $W_1$ and $p$ belongs to $W_2$.

CategoryTheory.MorphismProperty.factorizationData definition

[HasFactorization W₁ W₂] : FactorizationData W₁ W₂

Full source

/-- A chosen term in `FactorizationData W₁ W₂` when `HasFactorization W₁ W₂` holds. -/
noncomputable def factorizationData [HasFactorization W₁ W₂] : FactorizationData W₁ W₂ :=
  fun _ => Nonempty.some (HasFactorization.nonempty_mapFactorizationData _)

Factorization data for morphisms in $W_1$ followed by $W_2$

Informal description

Given a category $\mathcal{C}$ and two classes of morphisms $W_1$ and $W_2$ in $\mathcal{C}$, the term `factorizationData` provides, for any morphism $f: X \to Y$ in $\mathcal{C}$, a factorization of $f$ as $f = i \circ p$ where $i$ is in $W_1$ and $p$ is in $W_2$. This term exists when the category satisfies the `HasFactorization W₁ W₂` property.

CategoryTheory.MorphismProperty.comp definition

: MorphismProperty C

Full source

/-- The class of morphisms that are of the form `i ≫ p` with `W₁ i` and `W₂ p`. -/
def comp : MorphismProperty C := fun _ _ f => Nonempty (MapFactorizationData W₁ W₂ f)

Composition class of morphisms $W_1$ followed by $W_2$

Informal description

The class of morphisms in a category $\mathcal{C}$ that can be written as a composition $i \circ p$ where $i$ belongs to a class of morphisms $W_1$ and $p$ belongs to a class of morphisms $W_2$.

CategoryTheory.MorphismProperty.comp_eq_top_iff theorem

: W₁.comp W₂ = ⊤ ↔ HasFactorization W₁ W₂

Full source

lemma comp_eq_top_iff : W₁.comp W₂ = ⊤ ↔ HasFactorization W₁ W₂ := by
  constructor
  · intro h
    refine ⟨fun f => ?_⟩
    have : W₁.comp W₂ f := by simp only [h, top_apply]
    exact ⟨this.some⟩
  · intro
    ext X Y f
    simp only [top_apply, iff_true]
    exact ⟨factorizationData W₁ W₂ f⟩

Characterization of Factorization Axiom via Composition Class Equality: $W_1 \circ W_2 = \top$ iff $\mathcal{C}$ has $W_1$-then-$W_2$ factorizations

Informal description

For any two classes of morphisms $W_1$ and $W_2$ in a category $\mathcal{C}$, the composition class $W_1 \circ W_2$ (consisting of all morphisms that can be written as $i \circ p$ with $i \in W_1$ and $p \in W_2$) equals the class of all morphisms in $\mathcal{C}$ if and only if $\mathcal{C}$ satisfies the factorization property for $W_1$ followed by $W_2$ (i.e., every morphism in $\mathcal{C}$ can be factored as a morphism in $W_1$ followed by a morphism in $W_2$).

CategoryTheory.MorphismProperty.FunctorialFactorizationData structure

Full source

/-- The data of a functorial factorization of any morphism in `C` as a morphism in `W₁`
followed by a morphism in `W₂`. -/
structure FunctorialFactorizationData where
  /-- the intermediate objects in the factorizations -/
  Z : ArrowArrow C ⥤ C
  /-- the first morphism in the factorizations -/
  i : Arrow.leftFuncArrow.leftFunc ⟶ Z
  /-- the second morphism in the factorizations -/
  p : Z ⟶ Arrow.rightFunc
  fac : i ≫ p = Arrow.leftToRight := by aesop_cat
  hi (f : Arrow C) : W₁ (i.app f)
  hp (f : Arrow C) : W₂ (p.app f)

Functorial Factorization Data

Informal description

The structure `FunctorialFactorizationData W₁ W₂` provides the data of a functorial factorization for any morphism in a category `C` as a composition of a morphism in `W₁$ followed by a morphism in `W₂`. This means that for any morphism $f$ in `C`, there exists a factorization $f = i \circ p$ where $i \in W₁$ and $p \in W₂$, and this factorization is functorial in $f$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app theorem

{f : Arrow C} : data.i.app f ≫ data.p.app f = f.hom

Full source

@[reassoc (attr := simp)]
lemma fac_app {f : Arrow C} : data.i.app f ≫ data.p.app f = f.hom := by
  rw [← NatTrans.comp_app, fac,Arrow.leftToRight_app]

Functorial Factorization Composition Property: $i_f \circ p_f = f$

Informal description

For any morphism $f$ in the category $\mathcal{C}$, the composition of the morphisms $i_f$ (in $W_1$) and $p_f$ (in $W_2$) obtained from the functorial factorization data equals $f$, i.e., $i_f \circ p_f = f$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLE definition

 {W₁' W₂' : MorphismProperty C} (le₁ : W₁ ≤ W₁') (le₂ : W₂ ≤ W₂') : FunctorialFactorizationData W₁' W₂'

Full source

/-- If `W₁ ≤ W₁'` and `W₂ ≤ W₂'`, then a functorial factorization for `W₁` and `W₂` induces
a functorial factorization for `W₁'` and `W₂'`. -/
def ofLE {W₁' W₂' : MorphismProperty C} (le₁ : W₁ ≤ W₁') (le₂ : W₂ ≤ W₂') :
    FunctorialFactorizationData W₁' W₂' where
  Z := data.Z
  i := data.i
  p := data.p
  hi f := le₁ _ (data.hi f)
  hp f := le₂ _ (data.hp f)

Induced Functorial Factorization via Morphism Property Inclusion

Informal description

Given two morphism properties $ W_1' $ and $ W_2' $ in a category $ C $ such that $ W_1 \leq W_1' $ and $ W_2 \leq W_2' $, any functorial factorization data for $ W_1 $ and $ W_2 $ induces functorial factorization data for $ W_1' $ and $ W_2' $. This means that if every morphism in $ C $ can be functorially factored as a morphism in $ W_1 $ followed by a morphism in $ W_2 $, then the same holds for $ W_1' $ and $ W_2' $.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData definition

: FactorizationData W₁ W₂

Full source

/-- The term in `FactorizationData W₁ W₂` that is deduced from a functorial factorization. -/
def factorizationData : FactorizationData W₁ W₂ := fun f =>
  { Z := data.Z.obj (Arrow.mk f)
    i := data.i.app (Arrow.mk f)
    p := data.p.app (Arrow.mk f)
    hi := data.hi _
    hp := data.hp _ }

Factorization data induced by functorial factorization

Informal description

Given a functorial factorization data for morphism classes $ W_1 $ and $ W_2 $ in a category $ \mathcal{C} $, this function associates to each morphism $ f $ in $ \mathcal{C} $ a factorization $ f = i \circ p $ where $ i $ is in $ W_1 $ and $ p $ is in $ W_2 $. Specifically, for a morphism $ f $, the factorization consists of an intermediate object $ Z $, a morphism $ i $ from the domain of $ f $ to $ Z $ in $ W_1 $, and a morphism $ p $ from $ Z $ to the codomain of $ f $ in $ W_2 $.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ definition

: (data.factorizationData f).Z ⟶ (data.factorizationData g).Z

Full source

/-- 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`. -/
def mapZ : (data.factorizationData f).Z ⟶ (data.factorizationData g).Z := data.Z.map φ

Functorial map between intermediate objects in factorization

Informal description

Given a functorial factorization data for morphism classes $ W_1 $ and $ W_2 $ in a category $ \mathcal{C} $, and given a morphism $ \phi $ between two morphisms $ f $ and $ g $ in $ \mathcal{C} $, this function returns the induced morphism between the intermediate objects $ Z_f $ and $ Z_g $ of the factorizations of $ f $ and $ g $, respectively. This morphism $ Z_f \to Z_g $ expresses the functoriality of the factorization process.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ theorem

: (data.factorizationData f).i ≫ data.mapZ φ = φ.left ≫ (data.factorizationData g).i

Full source

@[reassoc (attr := simp)]
lemma i_mapZ :
    (data.factorizationData f).i ≫ data.mapZ φ = φ.left ≫ (data.factorizationData g).i :=
  (data.i.naturality φ).symm

Functoriality of Factorization: Commutativity of $ i $ with Induced Map

Informal description

Given a functorial factorization data for morphism classes $ W_1 $ and $ W_2 $ in a category $ \mathcal{C} $, and given a morphism $ \phi $ between two morphisms $ f $ and $ g $ in $ \mathcal{C} $, the composition of the morphism $ i_f $ (from the factorization of $ f $) with the induced morphism $ Z_f \to Z_g $ equals the composition of the left component of $ \phi $ with the morphism $ i_g $ (from the factorization of $ g $). In other words, the following diagram commutes: \[ i_f \circ \text{mapZ}(\phi) = \phi_{\text{left}} \circ i_g \] where $ i_f $ and $ i_g $ are the $ W_1 $-morphisms in the factorizations of $ f $ and $ g $ respectively, and $ \text{mapZ}(\phi) $ is the induced morphism between the intermediate objects $ Z_f $ and $ Z_g $.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p theorem

: data.mapZ φ ≫ (data.factorizationData g).p = (data.factorizationData f).p ≫ φ.right

Full source

@[reassoc (attr := simp)]
lemma mapZ_p :
    data.mapZ φ ≫ (data.factorizationData g).p = (data.factorizationData f).p ≫ φ.right :=
  data.p.naturality φ

Commutativity of Functorial Factorization with Respect to Right Component

Informal description

Given a functorial factorization data for morphism classes $ W_1 $ and $ W_2 $ in a category $ \mathcal{C} $, and given a morphism $ \phi $ between two morphisms $ f $ and $ g $ in $ \mathcal{C} $, the induced morphism $ \text{mapZ}(\phi) $ between the intermediate objects $ Z_f $ and $ Z_g $ satisfies the commutativity condition: \[ \text{mapZ}(\phi) \circ p_g = p_f \circ \phi_{\text{right}}, \] where $ p_f $ and $ p_g $ are the morphisms in $ W_2 $ from the factorizations of $ f $ and $ g $, respectively, and $ \phi_{\text{right}} $ is the right component of $ \phi $.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id theorem

: data.mapZ (𝟙 (Arrow.mk f)) = 𝟙 _

Full source

@[simp]
lemma mapZ_id : data.mapZ (𝟙 (Arrow.mk f)) = 𝟙 _ :=
  data.Z.map_id _

Identity Morphism Preserves Intermediate Object in Functorial Factorization

Informal description

For any morphism $f$ in a category $\mathcal{C}$ with functorial factorization data, the induced morphism between the intermediate objects $Z_f$ and $Z_f$ of the factorization of $f$ is the identity morphism, i.e., $\text{mapZ}(\text{id}_f) = \text{id}_{Z_f}$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp theorem

 {X'' Y'' : C} {h : X'' ⟶ Y''} (ψ : Arrow.mk g ⟶ Arrow.mk h) : data.mapZ (φ ≫ ψ) = data.mapZ φ ≫ data.mapZ ψ

Full source

@[reassoc, simp]
lemma mapZ_comp {X'' Y'' : C} {h : X'' ⟶ Y''} (ψ : Arrow.mkArrow.mk g ⟶ Arrow.mk h) :
    data.mapZ (φ ≫ ψ) = data.mapZ φ ≫ data.mapZ ψ :=
  data.Z.map_comp _ _

Functoriality of Intermediate Object Maps in Factorization: $Z(\phi \circ \psi) = Z(\phi) \circ Z(\psi)$

Informal description

Given a functorial factorization data for morphism classes $W_1$ and $W_2$ in a category $\mathcal{C}$, and morphisms $\phi \colon f \to g$ and $\psi \colon g \to h$ in $\mathcal{C}$, the induced morphism on the intermediate objects satisfies $Z(\phi \circ \psi) = Z(\phi) \circ Z(\psi)$, where $Z(\phi)$ denotes the map between the intermediate objects of the factorizations of $f$ and $g$, and similarly for $Z(\psi)$ and $Z(\phi \circ \psi)$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z definition

: Arrow (J ⥤ C) ⥤ J ⥤ C

Full source

/-- Auxiliary definition for `FunctorialFactorizationData.functorCategory`. -/
@[simps]
def functorCategory.Z : ArrowArrow (J ⥤ C) ⥤ J ⥤ C where
  obj f :=
    { obj := fun j => (data.factorizationData (f.hom.app j)).Z
      map := fun φ => data.mapZ
        { left := f.left.map φ
          right := f.right.map φ }
      map_id := fun j => by
        dsimp
        rw [← data.mapZ_id (f.hom.app j)]
        congr <;> simp
      map_comp := fun _ _ => by
        dsimp
        rw [← data.mapZ_comp]
        congr <;> simp }
  map τ :=
    { app := fun j => data.mapZ
        { left := τ.left.app j
          right := τ.right.app j
          w := congr_app τ.w j }
      naturality := fun _ _ α => by
        dsimp
        rw [← data.mapZ_comp, ← data.mapZ_comp]
        congr 1
        ext <;> simp }
  map_id f := by
    ext j
    dsimp
    rw [← data.mapZ_id]
    congr 1
  map_comp f g := by
    ext j
    dsimp
    rw [← data.mapZ_comp]
    congr 1

Intermediate object functor in functorial factorization

Informal description

The functor that assigns to each morphism $f$ in the functor category $J \to C$ the intermediate object $Z$ in the factorization of $f$ as a composition of a morphism in $W_1$ followed by a morphism in $W_2$. This functor is constructed by applying the factorization data pointwise for each object in $J$, ensuring that the factorization is functorial across the category $J$.

CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory definition

: FunctorialFactorizationData (W₁.functorCategory J) (W₂.functorCategory J)

Full source

/-- A functorial factorization in the category `C` extends to the functor category `J ⥤ C`. -/
def functorCategory :
    FunctorialFactorizationData (W₁.functorCategory J) (W₂.functorCategory J) where
  Z := functorCategory.Z data J
  i := { app := fun f => { app := fun j => (data.factorizationData (f.hom.app j)).i } }
  p := { app := fun f => { app := fun j => (data.factorizationData (f.hom.app j)).p } }
  hi _ _ := data.hi _
  hp _ _ := data.hp _

Functorial factorization in functor categories

Informal description

Given a functorial factorization data for morphism classes $ W_1 $ and $ W_2 $ in a category $ \mathcal{C} $, this construction extends the factorization to the functor category $ J \to \mathcal{C} $. Specifically, for any morphism $ f $ in the functor category, it provides a factorization $ f = i \circ p $ where $ i $ is in $ W_1 $ and $ p $ is in $ W_2 $, with the intermediate object $ Z $ and morphisms $ i $ and $ p $ defined pointwise for each object in $ J $.

CategoryTheory.MorphismProperty.HasFunctorialFactorization structure

Full source

/-- 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₂`. -/
class HasFunctorialFactorization : Prop where
  nonempty_functorialFactorizationData : Nonempty (FunctorialFactorizationData W₁ W₂)

Functorial Factorization Property for Morphism Classes W₁ and W₂

Informal description

The structure `HasFunctorialFactorization W₁ W₂` asserts that in a category `C`, any morphism can be factored in a functorial way as a composition of a morphism from class `W₁` followed by a morphism from class `W₂`. This means there exists a systematic (functorial) method to decompose any morphism into such a factorization.

CategoryTheory.MorphismProperty.functorialFactorizationData definition

[HasFunctorialFactorization W₁ W₂] : FunctorialFactorizationData W₁ W₂

Full source

/-- A chosen term in `FunctorialFactorizationData W₁ W₂` when the functorial factorization
axiom `HasFunctorialFactorization W₁ W₂` holds. -/
noncomputable def functorialFactorizationData [HasFunctorialFactorization W₁ W₂] :
    FunctorialFactorizationData W₁ W₂ :=
  Nonempty.some (HasFunctorialFactorization.nonempty_functorialFactorizationData)

Functorial factorization data for morphism classes W₁ and W₂

Informal description

Given a category `C` with classes of morphisms `W₁` and `W₂`, the term `functorialFactorizationData` provides a chosen functorial factorization for any morphism in `C` as a composition of a morphism in `W₁` followed by a morphism in `W₂`, when the category satisfies the `HasFunctorialFactorization W₁ W₂` property.

CategoryTheory.MorphismProperty.instHasFactorizationOfHasFunctorialFactorization instance

[HasFunctorialFactorization W₁ W₂] : HasFactorization W₁ W₂

Full source

instance [HasFunctorialFactorization W₁ W₂] : HasFactorization W₁ W₂ where
  nonempty_mapFactorizationData f := ⟨(functorialFactorizationData W₁ W₂).factorizationData f⟩

Functorial Factorization Implies Factorization Axiom

Informal description

For any category $\mathcal{C}$ with classes of morphisms $W_1$ and $W_2$, if $\mathcal{C}$ has a functorial factorization of morphisms into $W_1$ followed by $W_2$, then $\mathcal{C}$ satisfies the factorization axiom for $W_1$ and $W_2$. That is, every morphism in $\mathcal{C}$ can be factored as a morphism in $W_1$ followed by a morphism in $W_2$.

CategoryTheory.MorphismProperty.instHasFunctorialFactorizationFunctorFunctorCategory instance

 [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category J] :
  HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J)

Full source

instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category J] :
    HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) :=
  ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩

Functorial Factorization in Functor Categories

Informal description

For any category $\mathcal{C}$ with classes of morphisms $W_1$ and $W_2$ that admits a functorial factorization into $W_1$ followed by $W_2$, and for any small category $J$, the functor category $J \to \mathcal{C}$ also admits a functorial factorization into $W_1$-morphisms followed by $W_2$-morphisms in the functor category.