refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API

Mathlib.lean

@@ -1135,6 +1135,7 @@ import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
 import Mathlib.AlgebraicTopology.SimplicialSet.Path
 import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
 import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
+import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
 import Mathlib.AlgebraicTopology.SingularSet
 import Mathlib.AlgebraicTopology.TopologicalSimplex
 import Mathlib.Analysis.Analytic.Basic
@@ -4243,6 +4244,7 @@ import Mathlib.Order.Filter.Ultrafilter.Defs
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 import Mathlib.Order.Fin.Basic
 import Mathlib.Order.Fin.Finset
+import Mathlib.Order.Fin.SuccAboveOrderIso
 import Mathlib.Order.Fin.Tuple
 import Mathlib.Order.FixedPoints
 import Mathlib.Order.GaloisConnection.Basic

Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

@@ -181,29 +181,28 @@ open SSet.stdSimplex in
 protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
     SimplicialObject.Augmented.ExtraDegeneracy (stdSimplex.obj Δ) where
   s' _ := objMk (OrderHom.const _ 0)
-  s  _ f := (objEquiv _ _).symm
-    (shift (objEquiv _ _ f))
+  s  _ f := objEquiv.symm (shift (objEquiv f))
   s'_comp_ε := by
     dsimp
     subsingleton
   s₀_comp_δ₁ := by
     dsimp
     ext1 x
-    apply (objEquiv _ _).injective
+    apply objEquiv.injective
     ext j
     fin_cases j
     rfl
   s_comp_δ₀ n := by
     ext1 φ
-    apply (objEquiv _ _).injective
+    apply objEquiv.injective
     apply SimplexCategory.Hom.ext
     ext i : 2
     dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex,
       objEquiv, Equiv.ulift, uliftFunctor]
     simp only [shiftFun_succ]
   s_comp_δ n i := by
     ext1 φ
-    apply (objEquiv _ _).injective
+    apply objEquiv.injective
     apply SimplexCategory.Hom.ext
     ext j : 2
     dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex,
@@ -216,7 +215,7 @@ protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
         Fin.succAboveOrderEmb_apply]
   s_comp_σ n i := by
     ext1 φ
-    apply (objEquiv _ _).injective
+    apply objEquiv.injective
     apply SimplexCategory.Hom.ext
     ext j : 2
     dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.stdSimplex,

Mathlib/AlgebraicTopology/Quasicategory/Basic.lean

@@ -34,13 +34,13 @@ every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `
 -/
 @[kerodon 003A]
 class Quasicategory (S : SSet) : Prop where
-  hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : Λ[n+2, i] ⟶ S)
+  hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : (Λ[n+2, i] : SSet) ⟶ S)
     (_h0 : 0 < i) (_hn : i < Fin.last (n+2)),
-      ∃ σ : Δ[n+2] ⟶ S, σ₀ = hornInclusion (n+2) i ≫ σ
+      ∃ σ : Δ[n+2] ⟶ S, σ₀ = Λ[n + 2, i].ι ≫ σ
 
 lemma Quasicategory.hornFilling {S : SSet} [Quasicategory S] ⦃n : ℕ⦄ ⦃i : Fin (n+1)⦄
     (h0 : 0 < i) (hn : i < Fin.last n)
-    (σ₀ : Λ[n, i] ⟶ S) : ∃ σ : Δ[n] ⟶ S, σ₀ = hornInclusion n i ≫ σ := by
+    (σ₀ : (Λ[n, i] : SSet) ⟶ S) : ∃ σ : Δ[n] ⟶ S, σ₀ = Λ[n, i].ι ≫ σ := by
   cases n using Nat.casesAuxOn with
   | zero => simp [Fin.lt_iff_val_lt_val] at hn
   | succ n =>
@@ -56,13 +56,13 @@ instance (S : SSet) [KanComplex S] : Quasicategory S where
   hornFilling' _ _ σ₀ _ _ := KanComplex.hornFilling σ₀
 
 lemma quasicategory_of_filler (S : SSet)
-    (filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : Λ[n+2, i] ⟶ S)
+    (filler : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : (Λ[n+2, i] : SSet) ⟶ S)
       (_h0 : 0 < i) (_hn : i < Fin.last (n+2)),
       ∃ σ : S _[n+2], ∀ (j) (h : j ≠ i), S.δ j σ = σ₀.app _ (horn.face i j h)) :
     Quasicategory S where
   hornFilling' n i σ₀ h₀ hₙ := by
     obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ
-    refine ⟨(S.yonedaEquiv _).symm σ, ?_⟩
+    refine ⟨yonedaEquiv.symm σ, ?_⟩
     apply horn.hom_ext
     intro j hj
     rw [← h j hj, NatTrans.comp_app]

Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean

@@ -28,7 +28,7 @@ namespace SSet.StrictSegal
 instance quasicategory {X : SSet.{u}} [StrictSegal X] : Quasicategory X := by
   apply quasicategory_of_filler X
   intro n i σ₀ h₀ hₙ
-  use spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
+  use spineToSimplex <| Path.map (subcomplexHorn.spineId i h₀ hₙ) σ₀
   intro j hj
   apply spineInjective
   ext k
@@ -39,64 +39,54 @@ instance quasicategory {X : SSet.{u}} [StrictSegal X] : Quasicategory X := by
   · rw [← spine_arrow, spine_δ_arrow_lt _ hlt]
     dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
     apply congr_arg
-    simp only [horn, horn.spineId, stdSimplex, uliftFunctor, Functor.comp_obj,
-      yoneda_obj_obj, whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map,
-      stdSimplex.objEquiv, Equiv.ulift, Equiv.coe_fn_symm_mk,
-      Quiver.Hom.unop_op, horn.face_coe, Subtype.mk.injEq]
-    rw [mkOfSucc_δ_lt hlt]
+    apply Subtype.ext
+    dsimp [horn.face, CosimplicialObject.δ]
+    rw [Subcomplex.yonedaEquiv_coe, Subpresheaf.lift_ι, stdSimplex.map_apply,
+      Quiver.Hom.unop_op, stdSimplex.yonedaEquiv_map, Equiv.apply_symm_apply,
+      mkOfSucc_δ_lt hlt]
     rfl
   · rw [← spine_arrow, spine_δ_arrow_gt _ hgt]
     dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
     apply congr_arg
-    simp only [horn, horn.spineId, stdSimplex, uliftFunctor, Functor.comp_obj,
-      yoneda_obj_obj, whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map,
-      stdSimplex.objEquiv, Equiv.ulift, Equiv.coe_fn_symm_mk,
-      Quiver.Hom.unop_op, horn.face_coe, Subtype.mk.injEq]
-    rw [mkOfSucc_δ_gt hgt]
+    apply Subtype.ext
+    dsimp [horn.face, CosimplicialObject.δ]
+    rw [Subcomplex.yonedaEquiv_coe, Subpresheaf.lift_ι, stdSimplex.map_apply,
+      Quiver.Hom.unop_op, stdSimplex.yonedaEquiv_map, Equiv.apply_symm_apply,
+      mkOfSucc_δ_gt hgt]
     rfl
-  · /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
-    have hn0 : n ≠ 0 := by
-      rintro rfl
+  · obtain _ | n := n
+    · /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
       obtain rfl : k = 0 := by omega
       fin_cases i <;> contradiction
-    /- We construct the triangle in the standard simplex as a 2-simplex in
-    the horn. While the triangle is not contained in the inner horn `Λ[2, 1]`,
-    we can inhabit `Λ[n + 2, i] _[2]` by induction on `n`. -/
-    let triangle : Λ[n + 2, i] _[2] := by
-      cases n with
-      | zero => contradiction
-      | succ _ => exact horn.primitiveTriangle i h₀ hₙ k (by omega)
-    /- The interval spanning from `k` to `k + 2` is equivalently the spine
-    of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
-    have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by omega) =
-        X.spine 2 (σ₀.app _ triangle) := by
-      ext m
-      dsimp [spine_arrow, Path.interval, Path.map]
-      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
+    · /- We construct the triangle in the standard simplex as a 2-simplex in
+      the horn. While the triangle is not contained in the inner horn `Λ[2, 1]`,
+      it suffices to inhabit `Λ[n + 3, i] _[2]`. -/
+      let triangle : (Λ[n + 3, i] : SSet.{u}) _[2] :=
+        horn.primitiveTriangle i h₀ hₙ k (by omega)
+      /- The interval spanning from `k` to `k + 2` is equivalently the spine
+      of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
+      have hi : ((subcomplexHorn.spineId i h₀ hₙ).map σ₀).interval k 2 (by omega) =
+          X.spine 2 (σ₀.app _ triangle) := by
+        ext m
+        dsimp [spine_arrow, Path.interval, Path.map]
+        rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
+        apply congr_arg
+        apply Subtype.ext
+        ext a : 1
+        fin_cases a <;> fin_cases m <;> rfl
+      rw [← spine_arrow, spine_δ_arrow_eq _ heq, hi]
+      simp only [spineToDiagonal, diagonal, spineToSimplex_spine]
+      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
       apply congr_arg
-      simp only [horn, stdSimplex, uliftFunctor, Functor.comp_obj,
-        whiskering_obj_obj_obj, yoneda_obj_obj, uliftFunctor_obj, ne_eq,
-        whiskering_obj_obj_map, uliftFunctor_map, yoneda_obj_map, len_mk,
-        Nat.reduceAdd, Quiver.Hom.unop_op]
-      cases n with
-      | zero => contradiction
-      | succ _ => ext x; fin_cases x <;> fin_cases m <;> rfl
-    rw [← spine_arrow, spine_δ_arrow_eq _ heq, hi]
-    simp only [spineToDiagonal, diagonal, spineToSimplex_spine]
-    rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
-    apply congr_arg
-    simp only [horn, stdSimplex, uliftFunctor, Functor.comp_obj,
-      whiskering_obj_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
-      uliftFunctor_map, whiskering_obj_obj_map, yoneda_obj_map, horn.face_coe,
-      len_mk, Nat.reduceAdd, Quiver.Hom.unop_op, Subtype.mk.injEq, ULift.up_inj]
-    ext z
-    cases n with
-    | zero => contradiction
-    | succ _ =>
-      fin_cases z <;>
-      · simp only [stdSimplex.objEquiv, uliftFunctor_map, yoneda_obj_map,
-          Quiver.Hom.unop_op, Equiv.ulift_symm_down]
-        rw [mkOfSucc_δ_eq heq]
-        rfl
+      apply Subtype.ext
+      ext z : 1
+      dsimp [horn.face]
+      rw [Subcomplex.yonedaEquiv_coe, Subpresheaf.lift_ι, stdSimplex.map_apply,
+        Quiver.Hom.unop_op, stdSimplex.map_apply, Quiver.Hom.unop_op]
+      dsimp [CosimplicialObject.δ]
+      rw [stdSimplex.yonedaEquiv_map]
+      simp only [Fin.isValue, Equiv.apply_symm_apply, triangle]
+      rw [mkOfSucc_δ_eq heq]
+      fin_cases z <;> rfl
 
 end SSet.StrictSegal

Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

@@ -53,6 +53,26 @@ lemma hom_ext {X Y : SSet} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f =
 lemma comp_app {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ) :
     (f ≫ g).app n = f.app n ≫ g.app n := NatTrans.comp_app _ _ _
 
+/-- The constant map of simplicial sets `X ⟶ Y` induced by a simplex `y : Y _[0]`. -/
+@[simps]
+def const {X Y : SSet.{u}} (y : Y _[0]) : X ⟶ Y where
+  app n _ := Y.map (n.unop.const _ 0).op y
+  naturality n m f := by
+    ext
+    dsimp
+    rw [← FunctorToTypes.map_comp_apply]
+    rfl
+
+@[simp]
+lemma comp_const {X Y Z : SSet.{u}} (f : X ⟶ Y) (z : Z _[0]) :
+    f ≫ const z = const z := rfl
+
+@[simp]
+lemma const_comp {X Y Z : SSet.{u}} (y : Y _[0]) (g : Y ⟶ Z) :
+    const (X := X) y ≫ g = const (g.app _ y) := by
+  ext m x
+  simp [FunctorToTypes.naturality]
+
 /-- The ulift functor `SSet.{u} ⥤ SSet.{max u v}` on simplicial sets. -/
 def uliftFunctor : SSet.{u} ⥤ SSet.{max u v} :=
   (SimplicialObject.whiskering _ _).obj CategoryTheory.uliftFunctor.{v, u}

Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean

@@ -30,18 +30,24 @@ namespace SSet
 /-- The boundary `∂Δ[n]` of the `n`-th standard simplex consists of
 all `m`-simplices of `stdSimplex n` that are not surjective
 (when viewed as monotone function `m → n`). -/
-def boundary (n : ℕ) : SSet.{u} where
-  obj m := { α : Δ[n].obj m // ¬Function.Surjective (asOrderHom α) }
-  map {m₁ m₂} f α :=
-    ⟨Δ[n].map f α.1, by
-      intro h
-      apply α.property
-      exact Function.Surjective.of_comp h⟩
+def subcomplexBoundary (n : ℕ) : (Δ[n] : SSet.{u}).Subcomplex where
+  obj _ := setOf (fun s ↦ ¬Function.Surjective (stdSimplex.asOrderHom s))
+  map _ _ hs h := hs (Function.Surjective.of_comp h)
 
 /-- The boundary `∂Δ[n]` of the `n`-th standard simplex -/
-scoped[Simplicial] notation3 "∂Δ[" n "]" => SSet.boundary n
+scoped[Simplicial] notation3 "∂Δ[" n "]" => SSet.subcomplexBoundary n
+
+lemma subcomplexBoundary_eq_iSup (n : ℕ) :
+    subcomplexBoundary.{u} n = ⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ := by
+  ext
+  simp [stdSimplex.face_obj, subcomplexBoundary, Function.Surjective]
+  tauto
+
+@[deprecated (since := "2025-01-26")]
+alias boundary := subcomplexBoundary
 
 /-- The inclusion of the boundary of the `n`-th standard simplex into that standard simplex. -/
-def boundaryInclusion (n : ℕ) : ∂Δ[n] ⟶ Δ[n] where app m (α : { α : Δ[n].obj m // _ }) := α
+@[deprecated subcomplexBoundary (since := "2025-01-26")]
+abbrev boundaryInclusion (n : ℕ) : (∂Δ[n] : SSet.{u}) ⟶ Δ[n] := ∂Δ[n].ι
 
 end SSet