Inner anodyne extensions and pushout-products, inner fibrations and pullbacks

This file is mirrored from SSet/AnodyneExtensions/PushoutProduct.

The main result in this file is that if i : X₁ ⟶ Y₁ is a monomorphism in SSet and j : X₂ ⟶ Y₂ is an inner anodyne extension, then the pushout-product of i and j is an inner anodyne extension (SSet.innerAnodyneExtensions_pushoutObjObjι). This is closely related to the lemma SSet.innerFibration_pullbackObjObjπ which says that if i : X₁ ⟶ Y₁ is a monomorphism and p : E ⟶ B is an inner 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 an inner fibration. In particular, if A : SSet and X is a quasi-category, then the internal hom A ⟶[SSet] X is also a quasi-category.

For implementation details, see SSet/AnodyneExtensions/PushoutProduct.

References

• Jack McKoen, A Formalization of Functor Quasi-Categories in Lean 4

Note

The result that the internal hom into a quasi-category is also a quasi-category was first formalized by Jack McKoen for his master's thesis, following an approach outlined on Kerodon (https://kerodon.net/tag/0066). Specifically, this approach hinges on the lemma https://kerodon.net/tag/0079 which is avoided in the mathlib implementation.

theorem SSet.prodStdSimplex.innerAnodyneExtensions_unionProd_ι {m : ℕ} (k : Fin (m + 2)) (h0 : 0 < k) (hn : k < Fin.last (m + 1)) (n : ℕ) : innerAnodyneExtensions ((horn (m + 1) k).unionProd (boundary n)).ι

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

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

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

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

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

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

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

instance SSet.instInnerFibrationMapIhom {E B X : SSet} (p : E ⟶ B) [InnerFibration p] : InnerFibration ((CategoryTheory.ihom X).map p)

instance SSet.instInnerFibrationAppPreOfMonoOfQuasicategory {A B : SSet} (i : A ⟶ B) [CategoryTheory.Mono i] (X : SSet) [X.Quasicategory] : InnerFibration ((CategoryTheory.MonoidalClosed.pre i).app X)

instance SSet.instQuasicategoryObjIhomTerminal (A : SSet) : (A ⟹ ⊤_ SSet).Quasicategory

instance SSet.instQuasicategoryObjIhom {A X : SSet} [X.Quasicategory] : (A ⟹ X).Quasicategory