[Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): more API for horns

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

@@ -598,6 +598,12 @@ lemma toType_apply (x : SimplexCategory) : ToType x = Fin (x.len + 1) := rfl
 @[simp]
 lemma concreteCategoryHom_id (n : SimplexCategory) : ConcreteCategory.hom (𝟙 n) = .id := rfl
 
+lemma coe_δ {n : ℕ} (i : Fin (n + 2)) :
+    dsimp% ⇑(δ i) = Fin.succAbove i := rfl
+
+lemma coe_σ {n : ℕ} (i : Fin (n + 1)) :
+    dsimp% ⇑(σ i) = Fin.predAbove i := rfl
+
 end Concrete
 
 section EpiMono

Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

@@ -39,13 +39,22 @@ def horn (n : ℕ) (i : Fin (n + 1)) : (Δ[n] : SSet.{u}).Subcomplex where
 /-- The `i`-th horn `Λ[n, i]` of the standard `n`-simplex -/
 scoped[Simplicial] notation3 "Λ[" n ", " i "]" => SSet.horn (n : ℕ) i
 
+lemma mem_horn_iff {n : ℕ} (i : Fin (n + 1)) {m : SimplexCategoryᵒᵖ} (x : Δ[n].obj m) :
+    x ∈ (horn n i).obj m ↔ Set.range (stdSimplex.asOrderHom x) ∪ {i} ≠ Set.univ := Iff.rfl
+
+set_option backward.isDefEq.respectTransparency false in
 lemma horn_eq_iSup (n : ℕ) (i : Fin (n + 1)) :
     horn.{u} n i =
       ⨆ (j : ({i}ᶜ : Set (Fin (n + 1)))), stdSimplex.face {j.1}ᶜ := by
   ext m j
   simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]
   rfl
 
+instance {n : ℕ} (i : Fin (n + 1)) : HasDimensionLT (horn.{u} n i) n := by
+  rw [horn_eq_iSup, hasDimensionLT_iSup_iff]
+  intro i
+  exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])
+
 lemma face_le_horn {n : ℕ} (i j : Fin (n + 1)) (h : i ≠ j) :
     stdSimplex.face.{u} {i}ᶜ ≤ horn n j := by
   rw [horn_eq_iSup]
@@ -73,6 +82,81 @@ lemma horn_obj_zero (n : ℕ) (i : Fin (n + 3)) :
   fin_cases a
   exact Ne.symm hk.2
 
+lemma horn_obj_eq_univ {n : ℕ} (i : Fin (n + 1)) (m : ℕ) (h : m + 1 < n := by lia) :
+    (horn.{u} n i).obj (op ⦋m⦌) = .univ := by
+  ext x
+  obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x
+  obtain ⟨j, hij, hj⟩ : ∃ (j : Fin (n + 1)), j ≠ i ∧ j ∉ Set.range f.toOrderHom := by
+    by_contra!
+    have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
+    have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
+    simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin,
+      Finset.card_singleton, add_le_add_iff_right] at this
+    have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
+    lia
+  have : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm.{u} f) i = j :=
+    ⟨j, hij, fun k hk ↦ hj ⟨k, hk⟩⟩
+  simpa [horn_eq_iSup] using this
+
+lemma subcomplex_le_horn_iff {n : ℕ}
+    (A : Δ[n + 1].Subcomplex) (i : Fin (n + 2)) :
+    A ≤ horn.{u} (n + 1) i ↔ ¬ stdSimplex.face {i}ᶜ ≤ A := by
+  refine ⟨fun hA h ↦ ?_, fun h ↦ ?_⟩
+  · replace h := h.trans hA
+    rw [stdSimplex.face_singleton_compl, Subcomplex.ofSimplex_le_iff, mem_horn_iff] at h
+    apply h
+    rw [stdSimplex.coe_asOrderHom_objEquiv_symm, SimplexCategory.coe_δ,
+      Fin.range_succAbove, Set.compl_union_self]
+  · rw [Subcomplex.le_iff_contains_nonDegenerate]
+    intro d x hx
+    by_cases! hd : d < n
+    · simp [horn_obj_eq_univ i d]
+    · obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x
+      dsimp at hS
+      simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢
+      obtain hd | rfl := hd.lt_or_eq
+      · obtain rfl : S = .univ := by
+          rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
+          exact le_antisymm (card_finset_fin_le S) (by lia)
+        exact (h (le_trans (by simp) hx)).elim
+      · replace hS : Sᶜ.card = 1 := by
+          have := S.card_compl_add_card
+          rw [Fintype.card_fin] at this
+          lia
+        obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
+          rw [Finset.card_eq_one] at hS
+          obtain ⟨j, hS⟩ := hS
+          exact ⟨j, by simp [← hS]⟩
+        exact face_le_horn _ _ (by rintro rfl; tauto)
+
+lemma face_le_horn_iff {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)) :
+    stdSimplex.face.{u} S ≤ Λ[n + 1, j] ↔ S ≠ .univ ∧ S ≠ {j}ᶜ := by
+  rw [subcomplex_le_horn_iff, stdSimplex.face_le_face_iff, ← not_iff_not]
+  simp only [Finset.le_eq_subset, Decidable.not_not, ne_eq, not_and_or]
+  refine ⟨fun h ↦ ?_, by aesop⟩
+  rw [← Finset.compl_subset_compl, compl_compl,
+    Finset.subset_singleton_iff, Finset.compl_eq_empty_iff] at h
+  grind [eq_compl_comm]
+
+lemma objEquiv_symm_notMem_horn_of_isIso {n : ℕ} (i : Fin (n + 1))
+    {d : SimplexCategory} (f : d ⟶ ⦋n⦌) [IsIso f] :
+    stdSimplex.objEquiv.symm.{u} f ∉ Λ[n, i].obj (op d) := by
+  rw [mem_horn_iff, ne_eq, not_not]
+  ext i
+  simpa using Or.inr ⟨inv f i, by simp [stdSimplex.coe_asOrderHom_objEquiv_symm.{u}]⟩
+
+lemma objEquiv_symm_δ_mem_horn_iff {n : ℕ} (i j : Fin (n + 2)) :
+    (stdSimplex.objEquiv (m := op ⦋n⦌)).symm
+      (SimplexCategory.δ i) ∈ (horn.{u} (n + 1) j).obj (op ⦋n⦌) ↔ i ≠ j := by
+  dsimp
+  rw [← Subcomplex.ofSimplex_le_iff, ← stdSimplex.face_singleton_compl, face_le_horn_iff]
+  simp
+
+lemma objEquiv_symm_δ_notMem_horn_iff {n : ℕ} (i j : Fin (n + 2)) :
+    (stdSimplex.objEquiv (m := op ⦋n⦌)).symm
+      (SimplexCategory.δ i) ∉ (horn.{u} _ j).obj (op ⦋n⦌) ↔ i = j := by
+  simp [objEquiv_symm_δ_mem_horn_iff.{u}]
+
 namespace horn
 
 open SimplexCategory Finset Opposite

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -138,6 +138,10 @@ lemma map_apply {m₁ m₂ : SimplexCategoryᵒᵖ} (f : m₁ ⟶ m₂) {n : Sim
     (stdSimplex.{u}.obj n).map f x = objEquiv.symm (f.unop ≫ objEquiv x) := by
   rfl
 
+@[simp]
+lemma coe_asOrderHom_objEquiv_symm {n m : ℕ} (α : ⦋n⦌ ⟶ ⦋m⦌) :
+    ⇑(asOrderHom (objEquiv.{u}.symm α)) = α := rfl
+
 end stdSimplex
 
 /-- The canonical bijection `(stdSimplex.obj n ⟶ X) ≃ X.obj (op n)`. -/