From 72aa268ad9878ef02927dca10a19f8519caceff6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 29 Mar 2026 10:20:53 +0200 Subject: [PATCH] feat(AlgebraicTopology/SimplicialSet): more on nondegenerate simplices of the standard simplex --- .../SimplicialSet/Boundary.lean | 5 + .../SimplicialSet/Simplices.lean | 8 ++ .../SimplicialSet/StdSimplex.lean | 132 ++++++++++++++++++ Mathlib/Data/Finset/BooleanAlgebra.lean | 4 + Mathlib/Order/Fin/Basic.lean | 5 + 5 files changed, 154 insertions(+) diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean index 35bedd2a8f0fe6..5da3ed26d0fc91 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean +++ b/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 diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean index 0613fbdce2c72e..ce08c8c892f20a 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean +++ b/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 diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean index 99a3791f741ea2..dbf6a1ced7fe03 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean +++ b/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 diff --git a/Mathlib/Data/Finset/BooleanAlgebra.lean b/Mathlib/Data/Finset/BooleanAlgebra.lean index 938b4d68a37d10..4ab53df9e7d5de 100644 --- a/Mathlib/Data/Finset/BooleanAlgebra.lean +++ b/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 diff --git a/Mathlib/Order/Fin/Basic.lean b/Mathlib/Order/Fin/Basic.lean index 1e8583c8c1c5d2..d948b85721966c 100644 --- a/Mathlib/Order/Fin/Basic.lean +++ b/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 α]