The factorization lemma by K. S. Brown

In a model category, any morphism f : X ⟶ Y between cofibrant objects can be factored as i ≫ p with i a cofibration and p a trivial fibration which has a section s that is a cofibration. In order to state this, we introduce a structure CofibrantBrownFactorization f with the data of such morphisms i, p and s with the expected properties, and show it is nonempty. Moreover, if f is a weak equivalence, then all the morphisms i, p and s are weak equivalences. (We also obtain the dual results about morphisms between fibrant objects.)

References

• [Brown, Kenneth S., Abstract homotopy theory and generalized sheaf cohomology, §I.1][brown-1973]

structure HomotopicalAlgebra.CofibrantBrownFactorization {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) extends (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f : Type (max u_1 v_1)

Given a morphism f : X ⟶ Y in a model category, this structure contains the data of a factorization i ≫ p = f with i a cofibration, p a trivial fibration which has a section s that is a cofibration. That this structure is nonempty when X and Y are cofibrant is Ken Brown's factorization lemma.

• Z : C
• i : X ⟶ self.Z
• p : self.Z ⟶ Y
• fac : CategoryStruct.comp self.i self.p = f
• hi : HomotopicalAlgebra.cofibrations C self.i
• hp : HomotopicalAlgebra.trivialFibrations C self.p
• s : Y ⟶ self.Z

  a cofibration that is a section of p

• s_p : CategoryTheory.CategoryStruct.comp self.s self.p = CategoryTheory.CategoryStruct.id Y
• cofibration_s : Cofibration self.s

@[simp]

theorem HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : CofibrantBrownFactorization f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp self.p h) = h

instance HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : CofibrantBrownFactorization f) [WeakEquivalence f] : WeakEquivalence h.i

instance HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : CofibrantBrownFactorization f) : WeakEquivalence h.s

noncomputable def HomotopicalAlgebra.CofibrantBrownFactorization.mk' {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : CofibrantBrownFactorization f

The term in CofibrantBrownFactorization f that is deduced from a factorization of coprod.desc f (𝟙 Y) : X ⨿ Y ⟶ Y as a cofibration followed by a trivial fibration.

@[simp]

theorem HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (mk' f h).s = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h.i

@[simp]

theorem HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (mk' f h).Z = h.Z

@[simp]

theorem HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (mk' f h).p = h.p

@[simp]

theorem HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))) : (mk' f h).i = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h.i

instance HomotopicalAlgebra.CofibrantBrownFactorization.instNonemptyOfIsCofibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] : Nonempty (CofibrantBrownFactorization f)

structure HomotopicalAlgebra.FibrantBrownFactorization {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) extends (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f : Type (max u_1 v_1)

Given a morphism f : X ⟶ Y in a model category, this structure contains the data of a factorization i ≫ p = f with p a fibration, i a trivial cofibration which has a retraction r that is a fibration. That this structure is nonempty when X and Y are fibrant is Ken Brown's factorization lemma.

• Z : C
• i : X ⟶ self.Z
• p : self.Z ⟶ Y
• fac : CategoryStruct.comp self.i self.p = f
• hi : HomotopicalAlgebra.trivialCofibrations C self.i
• hp : HomotopicalAlgebra.fibrations C self.p
• r : self.Z ⟶ X

  a fibration that is a retraction of i

• i_r : CategoryTheory.CategoryStruct.comp self.i self.r = CategoryTheory.CategoryStruct.id X
• fibration_r : Fibration self.r

@[simp]

theorem HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} {f : X ⟶ Y} (self : FibrantBrownFactorization f) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.r h) = h

instance HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : FibrantBrownFactorization f) [WeakEquivalence f] : WeakEquivalence h.p

instance HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) (h : FibrantBrownFactorization f) : WeakEquivalence h.r

noncomputable def HomotopicalAlgebra.FibrantBrownFactorization.mk' {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsFibrant X] [IsFibrant Y] (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : FibrantBrownFactorization f

The term in CofibrantBrownFactorization f that is deduced from a factorization of prod.lift f (𝟙 X) : X ⟶ Y ⨯ X as a cofibration followed by a trivial fibration.

@[simp]

theorem HomotopicalAlgebra.FibrantBrownFactorization.mk'_i {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsFibrant X] [IsFibrant Y] (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (mk' f h).i = h.i

@[simp]

theorem HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsFibrant X] [IsFibrant Y] (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (mk' f h).Z = h.Z

@[simp]

theorem HomotopicalAlgebra.FibrantBrownFactorization.mk'_r {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsFibrant X] [IsFibrant Y] (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (mk' f h).r = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.snd

@[simp]

theorem HomotopicalAlgebra.FibrantBrownFactorization.mk'_p {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsFibrant X] [IsFibrant Y] (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X))) : (mk' f h).p = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst

instance HomotopicalAlgebra.FibrantBrownFactorization.instNonemptyOfIsFibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) [IsFibrant X] [IsFibrant Y] : Nonempty (FibrantBrownFactorization f)