feat(AlgebraicTopology/SimplicialSet): constructors for subfaces (#9363)

constructors for subfaces of the standard simplex and horn simplices

Mathlib/AlgebraicTopology/SimplicialSet.lean

@@ -7,6 +7,8 @@ import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.CategoryTheory.Limits.Presheaf
 import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.CategoryTheory.Yoneda
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Tactic.FinCases
 
 #align_import algebraic_topology.simplicial_set from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
@@ -82,6 +84,44 @@ scoped[Simplicial] notation3 "Δ[" n "]" => SSet.standardSimplex.obj (SimplexCat
 instance : Inhabited SSet :=
   ⟨Δ[0]⟩
 
+namespace standardSimplex
+
+open Finset Opposite SimplexCategory
+
+/-- The (degenerate) `m`-simplex in the standard simplex concentrated in vertex `k`. -/
+def const (n : ℕ) (k : Fin (n+1)) (m : SimplexCategoryᵒᵖ) : Δ[n].obj m :=
+  Hom.mk <| OrderHom.const _ k
+
+@[simp]
+lemma const_toOrderHom (n : ℕ) (k : Fin (n+1)) (m : SimplexCategoryᵒᵖ) :
+    (const n k m).toOrderHom = OrderHom.const _ k :=
+  rfl
+
+/-- The edge of the standard simplex with endpoints `a` and `b`. -/
+def edge (n : ℕ) (a b : Fin (n+1)) (hab : a ≤ b) : Δ[n] _[1] := by
+  refine Hom.mk ⟨![a, b], ?_⟩
+  rw [Fin.monotone_iff_le_succ]
+  simp only [unop_op, len_mk, Fin.forall_fin_one]
+  apply Fin.mk_le_mk.mpr hab
+
+lemma coe_edge_toOrderHom (n : ℕ) (a b : Fin (n+1)) (hab : a ≤ b) :
+    ↑(edge n a b hab).toOrderHom = ![a, b] :=
+  rfl
+
+/-- The triangle in the standard simplex with vertices `a`, `b`, and `c`. -/
+def triangle {n : ℕ} (a b c : Fin (n+1)) (hab : a ≤ b) (hbc : b ≤ c) : Δ[n] _[2] := by
+  refine Hom.mk ⟨![a, b, c], ?_⟩
+  rw [Fin.monotone_iff_le_succ]
+  simp only [unop_op, len_mk, Fin.forall_fin_two]
+  dsimp
+  simp only [*, Matrix.tail_cons, Matrix.head_cons, true_and]
+
+lemma coe_triangle_toOrderHom {n : ℕ} (a b c : Fin (n+1)) (hab : a ≤ b) (hbc : b ≤ c) :
+    ↑(triangle a b c hab hbc).toOrderHom = ![a, b, c] :=
+  rfl
+
+end standardSimplex
+
 section
 
 /-- The `m`-simplices of the `n`-th standard simplex are
@@ -139,6 +179,95 @@ def hornInclusion (n : ℕ) (i : Fin (n + 1)) : Λ[n, i] ⟶ Δ[n] where
 set_option linter.uppercaseLean3 false in
 #align sSet.horn_inclusion SSet.hornInclusion
 
+namespace horn
+
+open SimplexCategory Finset Opposite
+
+/-- The (degenerate) subsimplex of `Λ[n+2, i]` concentrated in vertex `k`. -/
+@[simps]
+def const (n : ℕ) (i k : Fin (n+3)) (m : SimplexCategoryᵒᵖ) : Λ[n+2, i].obj m := by
+  refine ⟨standardSimplex.const _ k _, ?_⟩
+  suffices ¬ Finset.univ ⊆ {i, k} by
+    simpa [← Set.univ_subset_iff, Set.subset_def, asOrderHom, not_or, Fin.forall_fin_one,
+      subset_iff, mem_univ, @eq_comm _ _ k]
+  intro h
+  have := (card_le_card h).trans card_le_two
+  rw [card_fin] at this
+  omega
+
+/-- The edge of `Λ[n, i]` with endpoints `a` and `b`.
+
+This edge only exists if `{i, a, b}` has cardinality less than `n`. -/
+@[simps]
+def edge (n : ℕ) (i a b : Fin (n+1)) (hab : a ≤ b) (H : Finset.card {i, a, b} ≤ n) :
+    Λ[n, i] _[1] := by
+  refine ⟨standardSimplex.edge n a b hab, ?range⟩
+  case range =>
+    suffices ∃ x, ¬i = x ∧ ¬a = x ∧ ¬b = x by
+      simpa only [unop_op, SimplexCategory.len_mk, asOrderHom, SimplexCategory.Hom.toOrderHom_mk,
+        Set.union_singleton, ne_eq, ← Set.univ_subset_iff, Set.subset_def, Set.mem_univ,
+        Set.mem_insert_iff, @eq_comm _ _ i, Set.mem_range, forall_true_left, not_forall, not_or,
+        not_exists, Fin.forall_fin_two]
+    contrapose! H
+    replace H : univ ⊆ {i, a, b} :=
+      fun x _ ↦ by simpa [or_iff_not_imp_left, eq_comm] using H x
+    replace H := card_le_card H
+    rwa [card_fin] at H
+
+/-- Alternative constructor for the edge of `Λ[n, i]` with endpoints `a` and `b`,
+assuming `3 ≤ n`. -/
+@[simps!]
+def edge₃ (n : ℕ) (i a b : Fin (n+1)) (hab : a ≤ b) (H : 3 ≤ n) :
+    Λ[n, i] _[1] :=
+  horn.edge n i a b hab <| Finset.card_le_three.trans H
+
+/-- The edge of `Λ[n, i]` with endpoints `j` and `j+1`.
+
+This constructor assumes `0 < i < n`,
+which is the type of horn that occurs in the horn-filling condition of quasicategories. -/
+@[simps!]
+def primitiveEdge {n : ℕ} {i : Fin (n+1)}
+    (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) :
+    Λ[n, i] _[1] := by
+  refine horn.edge n i j.castSucc j.succ ?_ ?_
+  · simp only [← Fin.val_fin_le, Fin.coe_castSucc, Fin.val_succ, le_add_iff_nonneg_right, zero_le]
+  simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ
+  obtain rfl|hn : n = 2 ∨ 2 < n := by
+    rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; omega
+  · revert i j; decide
+  · exact Finset.card_le_three.trans hn
+
+/-- The triangle in the standard simplex with vertices `k`, `k+1`, and `k+2`.
+
+This constructor assumes `0 < i < n`,
+which is the type of horn that occurs in the horn-filling condition of quasicategories. -/
+@[simps]
+def primitiveTriangle {n : ℕ} (i : Fin (n+4))
+    (h₀ : 0 < i) (hₙ : i < Fin.last (n+3))
+    (k : ℕ) (h : k < n+2) : Λ[n+3, i] _[2] := by
+  refine ⟨standardSimplex.triangle
+    (n := n+3) ⟨k, by omega⟩ ⟨k+1, by omega⟩ ⟨k+2, by omega⟩ ?_ ?_, ?_⟩
+  · simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]
+  · simp only [Fin.mk_le_mk, add_le_add_iff_left, one_le_two]
+  simp only [unop_op, SimplexCategory.len_mk, asOrderHom, SimplexCategory.Hom.toOrderHom_mk,
+    OrderHom.const_coe_coe, Set.union_singleton, ne_eq, ← Set.univ_subset_iff, Set.subset_def,
+    Set.mem_univ, Set.mem_insert_iff, Set.mem_range, Function.const_apply, exists_const,
+    forall_true_left, not_forall, not_or, unop_op, not_exists,
+    standardSimplex.triangle, OrderHom.coe_mk, @eq_comm _ _ i]
+  dsimp
+  by_cases hk0 : k = 0
+  · subst hk0
+    use Fin.last (n+3)
+    simp only [hₙ.ne, not_false_eq_true, Fin.zero_eta, zero_add, true_and]
+    intro j
+    fin_cases j <;> simp [Fin.ext_iff] <;> omega
+  · use 0
+    simp only [h₀.ne', not_false_eq_true, true_and]
+    intro j
+    fin_cases j <;> simp [Fin.ext_iff, hk0]
+
+end horn
+
 section Examples
 
 open Simplicial