Documentation

Mathlib.CategoryTheory.MorphismProperty.Factorization

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 ip 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 ip 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

  • hi : W₁ self.i
  • hp : W₂ self.p
Instances For
    @[reducible, inline]

    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₂.

      • nonempty_mapFactorizationData : ∀ {X Y : C} (f : X Y), Nonempty (W₁.MapFactorizationData W₂ f)
      Instances
        noncomputable def CategoryTheory.MorphismProperty.factorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFactorization W₂] :
        W₁.FactorizationData W₂

        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 ip with W₁ i and W₂ p.

          Equations
          • W₁.comp W₂ f = Nonempty (W₁.MapFactorizationData W₂ f)
          Instances For
            theorem CategoryTheory.MorphismProperty.comp_eq_top_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) :
            W₁.comp W₂ = W₁.HasFactorization W₂

            The data of a functorial factorization of any morphism in C as a morphism in W₁ followed by a morphism in W₂.

            Instances For
              @[simp]
              theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (self : W₁.FunctorialFactorizationData W₂) {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C} (h : CategoryTheory.Arrow.rightFunc Z) :
              @[simp]
              theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {f : CategoryTheory.Arrow C} :
              CategoryTheory.CategoryStruct.comp (data.i.app f) (data.p.app f) = f.hom
              @[simp]
              theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {f : CategoryTheory.Arrow C} {Z : C} (h : CategoryTheory.Arrow.rightFunc.obj f Z) :
              def CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {W₁' W₂' : CategoryTheory.MorphismProperty C} (le₁ : W₁ W₁') (le₂ : W₂ W₂') :
              W₁'.FunctorialFactorizationData W₂'

              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
                def CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) :
                W₁.FactorizationData W₂

                The term in FactorizationData W₁ W₂ that is deduced from a functorial factorization.

                Equations
                Instances For
                  def CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) :
                  (data.factorizationData f).Z (data.factorizationData g).Z

                  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
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) :
                    CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (data.mapZ φ) = CategoryTheory.CategoryStruct.comp φ.left (data.factorizationData g).i
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) {Z : C} (h : (data.factorizationData g).Z Z) :
                    CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (CategoryTheory.CategoryStruct.comp (data.mapZ φ) h) = CategoryTheory.CategoryStruct.comp φ.left (CategoryTheory.CategoryStruct.comp (data.factorizationData g).i h)
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) :
                    CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.factorizationData g).p = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p φ.right
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) {Z : C} (h : Y' Z) :
                    CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.factorizationData g).p h) = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p (CategoryTheory.CategoryStruct.comp φ.right h)
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y : C} (f : X Y) :
                    @[simp]
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) {X'' Y'' : C} {h : X'' Y''} (ψ : CategoryTheory.Arrow.mk g CategoryTheory.Arrow.mk h) :
                    data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.mapZ ψ)
                    theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X Y} {g : X' Y'} (φ : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) {X'' Y'' : C} {h : X'' Y''} (ψ : CategoryTheory.Arrow.mk g CategoryTheory.Arrow.mk h) {Z : C} (h✝ : (data.factorizationData h).Z Z) :

                    Auxiliary definition for FunctorialFactorizationData.functorCategory.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_map_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Functor J C)} (τ : X✝ Y✝) (j : J) :
                      ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).map τ).app j = data.mapZ { left := τ.left.app j, right := τ.right.app j, w := }
                      @[simp]
                      theorem CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] (f : CategoryTheory.Arrow (CategoryTheory.Functor J C)) {X✝ Y✝ : J} (φ : X✝ Y✝) :
                      ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).map φ = data.mapZ { left := f.left.map φ, right := f.right.map φ, w := }
                      def CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} (data : W₁.FunctorialFactorizationData W₂) (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] :
                      (W₁.functorCategory J).FunctorialFactorizationData (W₂.functorCategory J)

                      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
                          noncomputable def CategoryTheory.MorphismProperty.functorialFactorizationData {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] :
                          W₁.FunctorialFactorizationData W₂

                          A chosen term in FunctorialFactorizationData W₁ W₂ when the functorial factorization axiom HasFunctorialFactorization W₁ W₂ holds.

                          Equations
                          • W₁.functorialFactorizationData W₂ = .some
                          Instances For
                            theorem CategoryTheory.MorphismProperty.instHasFactorizationOfHasFunctorialFactorization {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] :
                            W₁.HasFactorization W₂
                            theorem CategoryTheory.MorphismProperty.instHasFunctorialFactorizationFunctorFunctorCategory {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.HasFunctorialFactorization W₂] (J : Type u_2) [CategoryTheory.Category.{u_4, u_2} J] :
                            (W₁.functorCategory J).HasFunctorialFactorization (W₂.functorCategory J)