Anodyne extensions and pushout-products, fibrations and pullbacks

The main result in this file is that if i : X₁ ⟶ Y₁ is a monomorphism in SSet and j : X₂ ⟶ Y₂ is an anodyne extension, then the map from the pushout-product of i and j into Y₁ ⊗ Y₂ is an anodyne extension (SSet.anodyneExtensions_pushoutObjObjι). This is closely related to the lemma SSet.fibration_pullbackObjObjπ which says that if i : X₁ ⟶ Y₁ is a monomorphism and p : E ⟶ B is a fibration, then the canonical morphism from Y₁ ⟶[SSet] E to the pullback of X₁ ⟶[SSet] E and Y₁ ⟶[SSet] B over X₁ ⟶[SSet] B is also a fibration. In particular, if A : SSet and X is a Kan complex, then the internal hom A ⟶[SSet] X is also a Kan complex.

Besides abstract arguments involving parametrized adjunctions and lifting properties, the proof relies on two facts:

• the case i : ∂Δ[n] ⟶ Δ[n] and j : Λ[m, k] ⟶ Δ[m] which was obtained in the file Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean
• the fact that a morphism has the right lifting property with respect to all monomorphisms iff it has the right lifting property with respect to morphisms of the form ∂Δ[n] ⟶ Δ[n] (see SSet.rlp_monomorphisms in the file Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean), which follows from the fact that any monomorphism is a relative cell complex with basic cells of the form ∂Δ[n] ⟶ Δ[n], see the file Mathlib/AlgebraicTopology/SimplicialSet/Skeleton.lean).

theorem SSet.prodStdSimplex.strongAnodyneExtensions_unionProd_ι {m : ℕ} (k : Fin (m + 2)) (n : ℕ) : strongAnodyneExtensions ((horn (m + 1) k).unionProd (boundary n)).ι

theorem SSet.prodStdSimplex.anodyneExtensions_unionProd_ι {m : ℕ} (k : Fin (m + 2)) (n : ℕ) : anodyneExtensions ((horn (m + 1) k).unionProd (boundary n)).ι

theorem SSet.fibration_pullbackObjObjπ {X₁ Y₁ E B : SSet} {i : X₁ ⟶ Y₁} {p : E ⟶ B} [CategoryTheory.Mono i] [HomotopicalAlgebra.Fibration p] (sq₁₃ : CategoryTheory.MonoidalClosed.internalHom.PullbackObjObj i p) : HomotopicalAlgebra.Fibration sq₁₃.π

theorem SSet.anodyneExtensions_pushoutObjObjι {X₁ X₂ Y₁ Y₂ : SSet} {i : X₁ ⟶ Y₁} {j : X₂ ⟶ Y₂} (sq₁₂ : (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj i j) [CategoryTheory.Mono i] (hj : anodyneExtensions j) : anodyneExtensions sq₁₂.ι

theorem SSet.anodyneExtensions_pushoutObjObjι' {X₁ X₂ Y₁ Y₂ : SSet} {i : X₁ ⟶ Y₁} {j : X₂ ⟶ Y₂} (sq₁₂ : (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj i j) [CategoryTheory.Mono j] (hi : anodyneExtensions i) : anodyneExtensions sq₁₂.ι

theorem SSet.anodyneExtensions_unionProd_ι {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) (hB : anodyneExtensions B.ι) : anodyneExtensions (A.unionProd B).ι

theorem SSet.anodyneExtensions_unionProd_ι' {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex) (hA : anodyneExtensions A.ι) : anodyneExtensions (A.unionProd B).ι

theorem SSet.anodyneExtensions.whiskerRight {X Y : SSet} {f : X ⟶ Y} (hf : anodyneExtensions f) (Z : SSet) : anodyneExtensions (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)

theorem SSet.anodyneExtensions.whiskerLeft {X Y : SSet} {f : X ⟶ Y} (hf : anodyneExtensions f) (Z : SSet) : anodyneExtensions (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)

instance SSet.instFibrationMapIhom {E B X : SSet} (p : E ⟶ B) [HomotopicalAlgebra.Fibration p] : HomotopicalAlgebra.Fibration ((CategoryTheory.ihom X).map p)

instance SSet.instFibrationAppPreOfMonoOfKanComplex {A B : SSet} (i : A ⟶ B) [CategoryTheory.Mono i] (X : SSet) [X.KanComplex] : HomotopicalAlgebra.Fibration ((CategoryTheory.MonoidalClosed.pre i).app X)

instance SSet.instKanComplexObjIhomTerminal (A : SSet) : (A ⟹ ⊤_ SSet).KanComplex

instance SSet.instKanComplexObjIhom {A X : SSet} [X.KanComplex] : (A ⟹ X).KanComplex