Cofibrations and fibrations in the category of simplicial sets

We endow SSet with CategoryWithCofibrations and CategoryWithFibrations instances. Cofibrations are monomorphisms, and fibrations are morphisms having the right lifting property with respect to horn inclusions.

We have an instance mono_of_cofibration (but only a lemma cofibration_of_mono). Then, when stating lemmas about cofibrations of simplicial sets, it is advisable to use the assumption [Mono f] instead of [Cofibration f].

def SSet.modelCategoryQuillen.I : CategoryTheory.MorphismProperty SSet

The generating cofibrations: this is the family of morphisms in SSet which consists of boundary inclusions ∂Δ[n].ι : ∂Δ[n] ⟶ Δ[n].

Equations

• SSet.modelCategoryQuillen.I = CategoryTheory.MorphismProperty.ofHoms fun (n : ℕ) => (SSet.boundary n).ι

theorem SSet.modelCategoryQuillen.boundary_ι_mem_I (n : ℕ) : I (boundary n).ι

def SSet.modelCategoryQuillen.J : CategoryTheory.MorphismProperty SSet

The generating trivial cofibrations: this is the family of morphisms in SSet which consists of horn inclusions Λ[n, i].ι : Λ[n, i] ⟶ Δ[n] (for positive n).

Equations

• SSet.modelCategoryQuillen.J = ⨆ (n : ℕ), CategoryTheory.MorphismProperty.ofHoms fun (i : Fin (n + 2)) => (SSet.horn (n + 1) i).ι

theorem SSet.modelCategoryQuillen.horn_ι_mem_J (n : ℕ) [NeZero n] (i : Fin (n + 1)) : J (horn n i).ι

theorem SSet.modelCategoryQuillen.I_le_monomorphisms : I ≤ CategoryTheory.MorphismProperty.monomorphisms SSet

theorem SSet.modelCategoryQuillen.J_le_monomorphisms : J ≤ CategoryTheory.MorphismProperty.monomorphisms SSet

@[implicit_reducible]

def SSet.modelCategoryQuillen.instCategoryWithCofibrations : HomotopicalAlgebra.CategoryWithCofibrations SSet

The cofibrations for the Quillen model category structure (TODO) on SSet are monomorphisms.

Equations

• SSet.modelCategoryQuillen.instCategoryWithCofibrations = { cofibrations := CategoryTheory.MorphismProperty.monomorphisms SSet }

@[implicit_reducible]

def SSet.modelCategoryQuillen.instCategoryWithFibrations : HomotopicalAlgebra.CategoryWithFibrations SSet

The fibrations for the Quillen model category structure (TODO) on SSet are the morphisms which have the right lifting property with respect to horn inclusions.

Equations

• SSet.modelCategoryQuillen.instCategoryWithFibrations = { fibrations := SSet.modelCategoryQuillen.J.rlp }

theorem SSet.modelCategoryQuillen.cofibrations_eq : HomotopicalAlgebra.cofibrations SSet = CategoryTheory.MorphismProperty.monomorphisms SSet

theorem SSet.modelCategoryQuillen.fibrations_eq : HomotopicalAlgebra.fibrations SSet = J.rlp

theorem SSet.modelCategoryQuillen.cofibration_iff {X Y : SSet} (f : X ⟶ Y) : HomotopicalAlgebra.Cofibration f ↔ CategoryTheory.Mono f

theorem SSet.modelCategoryQuillen.fibration_iff {X Y : SSet} (f : X ⟶ Y) : HomotopicalAlgebra.Fibration f ↔ J.rlp f

instance SSet.modelCategoryQuillen.mono_of_cofibration {X Y : SSet} (f : X ⟶ Y) [HomotopicalAlgebra.Cofibration f] : CategoryTheory.Mono f

theorem SSet.modelCategoryQuillen.cofibration_of_mono {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] : HomotopicalAlgebra.Cofibration f

instance SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration {X Y : SSet} (f : X ⟶ Y) [hf : HomotopicalAlgebra.Fibration f] {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.HasLiftingProperty (horn (n + 1) i).ι f

theorem SSet.horn.IsCompatible.exists_lift {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : stdSimplex.obj { len := n + 1 } ⟶ Y) (comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) : ∃ (φ : stdSimplex.obj { len := n + 1 } ⟶ X), (∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) φ = f j hj) ∧ CategoryTheory.CategoryStruct.comp φ p = b

noncomputable def SSet.horn.IsCompatible.lift {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : stdSimplex.obj { len := n + 1 } ⟶ Y) (comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) : stdSimplex.obj { len := n + 1 } ⟶ X

If f : ∀ (j : Fin (n + 2)) (_ : j ≠ i), Δ[n] ⟶ X is a compatible family of morphisms (which defines a morphism Λ[n + 1, i] ⟶ X), p : X ⟶ Y a Kan fibration and b : Δ[n + 1] ⟶ Y such that for all j ≠ i, f j _ ≫ p = stdSimplex.δ j ≫ b, then this is a lifting Δ[n + 1] ⟶ X.

Equations

• hf.lift p b comm = ⋯.choose

theorem SSet.horn.IsCompatible.δ_lift {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : stdSimplex.obj { len := n + 1 } ⟶ Y) (comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) (j : Fin (n + 2)) (hj : j ≠ i := by grind) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (hf.lift p b comm) = f j hj

theorem SSet.horn.IsCompatible.δ_lift_assoc {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : stdSimplex.obj { len := n + 1 } ⟶ Y) (comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) (j : Fin (n + 2)) (hj : j ≠ i := by grind) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp (hf.lift p b comm) h) = CategoryTheory.CategoryStruct.comp (f j hj) h

@[simp]

theorem SSet.horn.IsCompatible.lift_comp {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : stdSimplex.obj { len := n + 1 } ⟶ Y) (comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) : CategoryTheory.CategoryStruct.comp (hf.lift p b comm) p = b

@[simp]

theorem SSet.horn.IsCompatible.lift_comp_assoc {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)} (hf : horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [HomotopicalAlgebra.Fibration p] (b : stdSimplex.obj { len := n + 1 } ⟶ Y) (comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) b) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (hf.lift p b comm) (CategoryTheory.CategoryStruct.comp p h) = CategoryTheory.CategoryStruct.comp b h