feat(AlgebraicTopology/SimplicialSet): more on nondegenerate simplices of the standard simplex

Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean

@@ -48,4 +48,9 @@ lemma boundary_eq_iSup (n : ℕ) :
   simp [stdSimplex.face_obj, boundary, Function.Surjective]
   tauto
 
+instance {n : ℕ} : HasDimensionLT (boundary n) n := by
+  rw [boundary_eq_iSup, hasDimensionLT_iSup_iff]
+  intro i
+  exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])
+
 end SSet

Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean

@@ -102,6 +102,14 @@ lemma ext_iff {n : ℕ} (x y : X _⦋n⦌) :
 /-- The subcomplex generated by a simplex. -/
 abbrev subcomplex (s : X.S) : X.Subcomplex := Subcomplex.ofSimplex s.simplex
 
+lemma ofSimplex_eq_subcomplex_mk {n : ℕ} (x : X _⦋n⦌) :
+    Subcomplex.ofSimplex x = (S.mk x).subcomplex := rfl
+
+@[simp]
+lemma subcomplex_cast (s : X.S) {d : ℕ} (hd : s.dim = d) :
+    (s.cast hd).subcomplex = s.subcomplex := by
+  rw [cast_eq_self]
+
 /-- If `s : X.S` and `t : X.S` are simplices of a simplicial set, `s ≤ t` means
 that the subcomplex generated by `s` is contained in the subcomplex generated by `t`,
 see `SSet.S.le_def` and `SSet.S.le_iff`. Note that the

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -162,6 +162,12 @@ lemma yonedaEquiv_map {n m : SimplexCategory} (f : n ⟶ m) :
     yonedaEquiv.{u} (stdSimplex.map f) = objEquiv.symm f :=
   yonedaEquiv.symm.injective rfl
 
+lemma map_objEquiv_op_apply
+    {X : SSet.{u}} {n : SimplexCategory} (x : X.obj (op n))
+    {m : SimplexCategoryᵒᵖ} (y : (stdSimplex.obj n).obj m) :
+    dsimp% X.map (stdSimplex.objEquiv y).op x = (yonedaEquiv.symm x).app m y := by
+  rfl
+
 lemma yonedaEquiv_symm_app_objEquiv_symm {X : SSet.{u}} {n : SimplexCategory}
     (x : X.obj (op n)) {m : SimplexCategoryᵒᵖ} (f : unop m ⟶ n) :
     dsimp% (yonedaEquiv.symm x).app _ (stdSimplex.objEquiv.symm f) =
@@ -237,12 +243,32 @@ lemma face_inter_face {n : ℕ} (S₁ S₂ : Finset (Fin (n + 1))) :
     face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂) := by
   aesop
 
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma face_bot (n : ℕ) :
+    face.{u} (∅ : Finset (Fin (n + 1))) = ⊥ := by
+  ext
+  simpa using Finset.univ_neq_empty _
+
+@[simp]
+lemma face_univ (n : ℕ) :
+    face.{u} (.univ : Finset (Fin (n + 1))) = ⊤ := by
+  ext
+  dsimp
+  simp only [Set.mem_univ, iff_true]
+  apply Finset.subset_univ
+
 end stdSimplex
 
 lemma yonedaEquiv_comp {X Y : SSet.{u}} {n : SimplexCategory}
     (f : stdSimplex.obj n ⟶ X) (g : X ⟶ Y) :
     yonedaEquiv (f ≫ g) = g.app _ (yonedaEquiv f) := rfl
 
+@[simp]
+lemma yonedaEquiv_symm_app_id {X : SSet.{u}} {n : ℕ} (x : X _⦋n⦌) :
+    (yonedaEquiv.symm x).app _ (yonedaEquiv (𝟙 _)) = x :=
+  yonedaEquiv.symm.injective (by simp [← yonedaEquiv_symm_comp])
+
 namespace Subcomplex
 
 variable {X : SSet.{u}}
@@ -447,6 +473,100 @@ noncomputable def facePairIso {n : ℕ} (i j : Fin (n + 1)) (hij : i < j) :
   stdSimplex.isoOfRepresentableBy
     (stdSimplex.faceRepresentableBy.{u} _ _ (Fin.orderIsoPair i j hij))
 
+set_option backward.isDefEq.respectTransparency false in
+variable (n) in
+lemma bijective_image_objEquiv_toOrderHom_univ (m : ℕ) :
+    Function.Bijective (fun (⟨x, hx⟩ : (Δ[n] : SSet.{u}).nonDegenerate m) ↦
+      (⟨Finset.image (objEquiv x).toOrderHom .univ, by
+        dsimp
+        rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective] at hx
+        rw [Finset.card_image_of_injective _ (by exact hx), Finset.card_univ,
+          Fintype.card_fin]⟩ : { S : Finset (Fin (n + 1)) | S.card = m + 1 })) := by
+  constructor
+  · rintro ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h₃
+    obtain ⟨f₁, rfl⟩ := objEquiv.symm.surjective x₁
+    obtain ⟨f₂, rfl⟩ := objEquiv.symm.surjective x₂
+    simp only [mem_nonDegenerate_iff_mono, Equiv.apply_symm_apply,
+      SimplexCategory.mono_iff_injective, SimplexCategory.len_mk] at h₁ h₂
+    simp only [Set.mem_setOf_eq, SimplexCategory.len_mk, Equiv.apply_symm_apply,
+      Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq] at h₃ ⊢
+    apply SimplexCategory.Hom.ext
+    rw [← OrderHom.range_eq_iff h₁ h₂]
+    ext x
+    simpa using congr_fun (congrArg Membership.mem h₃) x
+  · intro ⟨S, hS⟩
+    dsimp at hS
+    let e := monoEquivOfFin S (k := m + 1) (by simpa using hS)
+    refine ⟨⟨objMk ((OrderHom.Subtype.val _).comp (e.toOrderEmbedding.toOrderHom)), ?_⟩, ?_⟩
+    · rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective]
+      intro a b h
+      apply e.injective
+      ext : 1
+      exact h
+    · simp [e, ← Finset.image_image, Finset.image_univ_of_surjective e.surjective]
+
+/-- Nondegenerate `d`-dimensional simplices of the standard simplex `Δ[n]`
+identify to subsets of `Fin (n + 1)` of cardinality `d + 1`. -/
+noncomputable def nonDegenerateEquiv' {n d : ℕ} : (Δ[n] : SSet.{u}).nonDegenerate d ≃
+    { S : Finset (Fin (n + 1)) | S.card = d + 1 } :=
+  Equiv.ofBijective _ (bijective_image_objEquiv_toOrderHom_univ n d)
+
+set_option backward.isDefEq.respectTransparency false in
+lemma nonDegenerateEquiv'_iff {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) (j : Fin (n + 1)) :
+    j ∈ (nonDegenerateEquiv' x).1 ↔ ∃ (i : Fin (d + 1)), x.1 i = j := by
+  simp only [Set.mem_setOf_eq, Set.coe_setOf]
+  dsimp [nonDegenerateEquiv']
+  aesop
+
+set_option backward.isDefEq.respectTransparency false in
+/-- If `x` is a nondegenerate `d`-simplex of `Δ[n]`, this is the order isomorphism
+between `Fin (d + 1)` and the corresponding subset of `Fin (n + 1)` of cardinality `d + 1`. -/
+noncomputable def orderIsoOfNonDegenerate {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) :
+    Fin (d + 1) ≃o (nonDegenerateEquiv' x).1 where
+  toEquiv := Equiv.ofBijective (fun i ↦ ⟨x.1 i, Finset.mem_image_of_mem _ (by simp)⟩) (by
+    constructor
+    · have := (mem_nonDegenerate_iff_mono x.1).1 x.2
+      rw [SimplexCategory.mono_iff_injective] at this
+      exact fun _ _ h ↦ this (by simpa using h)
+    · rintro ⟨j, hj⟩
+      rw [nonDegenerateEquiv'_iff] at hj
+      aesop)
+  map_rel_iff' := by
+    have := (mem_nonDegenerate_iff_mono x.1).1 x.2
+    rw [SimplexCategory.mono_iff_injective] at this
+    intro a b
+    dsimp
+    simp only [Subtype.mk_le_mk]
+    constructor
+    · rw [← not_lt, ← not_lt]
+      intro h h'
+      apply h
+      obtain h'' | h'' := (monotone_apply x.1 h'.le).lt_or_eq
+      · assumption
+      · simp only [this h'', lt_self_iff_false] at h'
+    · intro h
+      exact monotone_apply _ h
+
+lemma face_nonDegenerateEquiv' {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) :
+    face (nonDegenerateEquiv' x).1 = Subcomplex.ofSimplex x.1 :=
+  face_eq_ofSimplex.{u} _ _ (orderIsoOfNonDegenerate x)
+
+set_option backward.isDefEq.respectTransparency false in
+lemma nonDegenerateEquiv'_symm_apply_mem {n d : ℕ}
+    (S : { S : Finset (Fin (n + 1)) | S.card = d + 1 }) (i : Fin (d + 1)) :
+      (nonDegenerateEquiv'.{u}.symm S).1 i ∈ S.1 := by
+  obtain ⟨f, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S
+  dsimp [nonDegenerateEquiv']
+  simp only [Equiv.ofBijective_symm_apply_apply, Finset.mem_image, Finset.mem_univ, true_and]
+  exact ⟨i, rfl⟩
+
+lemma nonDegenerateEquiv'_symm_mem_iff_face_le {n d : ℕ}
+    (S : { S : Finset (Fin (n + 1)) | S.card = d + 1 })
+    (A : (Δ[n] : SSet.{u}).Subcomplex) :
+    (nonDegenerateEquiv'.symm S).1 ∈ A.obj _ ↔ face S ≤ A := by
+  obtain ⟨x, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S
+  rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]
+
 instance (n : SimplexCategory) (d : SimplexCategoryᵒᵖ) :
     Finite ((stdSimplex.{u}.obj n).obj d) := by
   rw [objEquiv.finite_iff]
@@ -462,6 +582,18 @@ instance {X : SSet.{u}} {n : ℕ} (x : X _⦋n⦌) :
   rw [← Subcomplex.range_eq_ofSimplex]
   infer_instance
 
+lemma hasDimensionLT_face {n : ℕ} (S : Finset (Fin (n + 1)))
+    (d : ℕ) (hd : S.card ≤ d) :
+    HasDimensionLT (face.{u} S) d := by
+  generalize hm : S.card = m
+  obtain _ | m := m
+  · obtain rfl : S = ∅ := by rwa [← Finset.card_eq_zero]
+    rw [face_bot]
+    infer_instance
+  · rw [← hasDimensionLT_iff_of_iso
+      (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))]
+    exact hasDimensionLT_of_le _ (m + 1) _
+
 end stdSimplex
 
 section Examples

Mathlib/Data/Finset/BooleanAlgebra.lean

@@ -59,6 +59,10 @@ theorem univ_nontrivial_iff :
     (Finset.univ : Finset α).Nontrivial ↔ Nontrivial α := by
   rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]
 
+lemma univ_neq_empty (α : Type*) [Fintype α] [Nonempty α] :
+    (Finset.univ : Finset α) ≠ ∅ :=
+  fun h ↦ (Finset.univ_eq_empty_iff.1 h).elim (Classical.arbitrary _)
+
 theorem univ_nontrivial [h : Nontrivial α] :
     (Finset.univ : Finset α).Nontrivial :=
   univ_nontrivial_iff.mpr h

Mathlib/Order/Fin/Basic.lean

@@ -378,6 +378,11 @@ def natAddOrderEmb (n) : Fin m ↪o Fin (n + m) := .ofStrictMono (natAdd n) (str
 def succAboveOrderEmb (p : Fin (n + 1)) : Fin n ↪o Fin (n + 1) :=
   OrderEmbedding.ofStrictMono (succAbove p) (strictMono_succAbove p)
 
+@[simp]
+lemma range_succAboveOrderEmb {n : ℕ} (i : Fin (n + 1)) :
+    Set.range (Fin.succAboveOrderEmb i) = {i}ᶜ := by
+  aesop
+
 /-! ### Uniqueness of order isomorphisms -/
 
 variable {α : Type*} [Preorder α]