Theorems · Theorem · category theory

HomotopicalAlgebra.CofibrantBrownFactorization.mk.inj

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : HomotopicalAlgebra.ModelCategory C} {X Y : C}
  {f : X ⟶ Y}
  {toMapFactorizationData :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f}
  {s : Y ⟶ toMapFactorizationData.Z}
  {s_p :
    autoParam (CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam}
  {cofibration_s :
    autoParam (HomotopicalAlgebra.Cofibration s)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam}
  {toMapFactorizationData_1 :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f}
  {s_1 : Y ⟶ toMapFactorizationData_1.Z}
  {s_p_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 toMapFactorizationData_1.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam}
  {cofibration_s_1 :
    autoParam (HomotopicalAlgebra.Cofibration s_1)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam},
  { toMapFactorizationData := toMapFactorizationData, s := s, s_p := s_p, cofibration_s := cofibration_s } =
      { toMapFactorizationData := toMapFactorizationData_1, s := s_1, s_p := s_p_1, cofibration_s := cofibration_s_1 } →
    toMapFactorizationData = toMapFactorizationData_1 ∧ s ≍ s_1

Defined in

Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Cited by

1 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound