[Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): induction principles for nondegenerate simplices

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean

@@ -53,6 +53,19 @@ lemma mk_surjective (x : X.N) :
     ∃ (n : ℕ) (y : X.nonDegenerate n), x = N.mk _ y.prop :=
   ⟨x.dim, ⟨_, x.nonDegenerate⟩, rfl⟩
 
+/-- Induction principle for the type `X.N` of nondegenerate simplices of
+a simplicial set `X`. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
+def induction {motive : X.N → Sort*}
+    (mk : ∀ (n : ℕ) (x : X.nonDegenerate n), motive (mk x.val x.property)) (s : X.N) :
+    motive s :=
+  mk s.dim ⟨_, s.nonDegenerate⟩
+
+@[simp]
+lemma induction_mk {motive : X.N → Sort*}
+    (mk : ∀ (n : ℕ) (x : X.nonDegenerate n), motive (mk x.1 x.2)) {n : ℕ} (s : X.nonDegenerate n) :
+  induction (motive := motive) mk (N.mk s.val s.property) = mk n s := rfl
+
 lemma ext_iff (x y : X.N) :
     x = y ↔ x.toS = y.toS := by
   grind [cases SSet.N]
@@ -62,6 +75,9 @@ instance : Preorder X.N := Preorder.lift toS
 lemma le_iff {x y : X.N} : x ≤ y ↔ x.subcomplex ≤ y.subcomplex :=
   Iff.rfl
 
+lemma lt_iff {x y : X.N} : x < y ↔ x.subcomplex < y.subcomplex :=
+  Iff.rfl
+
 lemma le_iff_exists_mono {x y : X.N} :
     x ≤ y ↔ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f), X.map f.op y.simplex = x.simplex := by
   simp only [le_iff, CategoryTheory.Subfunctor.ofSection_le_iff,
@@ -136,6 +152,17 @@ lemma iSup_subcomplex_eq_top :
     rintro ⟨d, s, hs⟩
     exact le_trans (by rfl) (le_iSup _ (N.mk _ hs)))
 
+lemma subcomplex_le_iff {A B : X.Subcomplex} :
+    A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B := by
+  rw [Subcomplex.le_iff_contains_nonDegenerate]
+  refine ⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩
+  · induction s using N.induction with
+    | mk n x =>
+      intro hx
+      simp only [Subfunctor.ofSection_le_iff, mk_dim, mk_simplex] at hx ⊢
+      exact h _ _ hx
+  · simpa using h (N.mk _ x.prop) (by simpa)
+
 end N
 
 /-- The map which sends a non degenerate simplex of a simplicial set to
@@ -152,6 +179,28 @@ namespace S
 
 variable {X}
 
+lemma eq_iff_ofSimplex_eq {X : SSet.{u}} {n m : ℕ} (x : X _⦋n⦌) (y : X _⦋m⦌)
+    (hx : x ∈ X.nonDegenerate _) (hy : y ∈ X.nonDegenerate _) :
+    S.mk x = S.mk y ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y := by
+  trans N.mk x hx = N.mk y hy
+  · exact (N.ext_iff (N.mk x hx) (N.mk y hy)).symm
+  · simp only [le_antisymm_iff]
+    rfl
+
+lemma subcomplex_map_le (x y : X.S) (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌)
+    (hf : X.map f.op y.simplex = x.simplex) :
+    x.subcomplex ≤ y.subcomplex := by
+  simp only [Subcomplex.ofSimplex_le_iff]
+  exact ⟨_, hf⟩
+
+lemma subcomplex_eq_of_epi (x y : X.S) (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) [Epi f]
+    (hf : X.map f.op y.simplex = x.simplex) :
+    x.subcomplex = y.subcomplex := by
+  refine le_antisymm (subcomplex_map_le x y f hf) ?_
+  simp only [Subcomplex.ofSimplex_le_iff]
+  have := isSplitEpi_of_epi f
+  exact ⟨(section_ f).op, by simp [← hf, ← FunctorToTypes.map_comp_apply, ← op_comp]⟩
+
 lemma existsUnique_n (x : X.S) : ∃! (y : X.N), y.subcomplex = x.subcomplex :=
   existsUnique_of_exists_of_unique (by
     obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
@@ -182,6 +231,35 @@ lemma toN_eq_iff {x : X.S} {y : X.N} :
     x.toN = y ↔ y.subcomplex = x.subcomplex :=
   ⟨by rintro rfl; simp, fun h ↦ x.existsUnique_n.unique (by simp) h⟩
 
+set_option backward.isDefEq.respectTransparency false in
+lemma existsUnique_toNπ {x : X.S} {y : X.N} (hy : x.toN = y) :
+    ∃! (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌), Epi f ∧ X.map f.op y.simplex = x.simplex := by
+  obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
+  obtain ⟨m, f, _, z, rfl⟩ := X.exists_nonDegenerate x
+  obtain rfl : y = N.mk _ z.2 := by
+    rw [toN_eq_iff] at hy
+    rw [← N.subcomplex_injective_iff, hy]
+    exact subcomplex_eq_of_epi _ _ f rfl
+  refine existsUnique_of_exists_of_unique ⟨f, inferInstance, rfl⟩
+    (fun f₁ f₂ ⟨_, hf₁⟩ ⟨_, hf₂⟩ ↦ unique_nonDegenerate_map _ _ _ _ hf₁.symm _ _ hf₂.symm)
+
+/-- Given a simplex `x : X.S` of a simplicial set `X`, this is the unique
+(epi)morphism `f : ⦋x.dim⦌ ⟶ ⦋x.toN.dim⦌` such that `x.simplex` is
+`X.map f.op x.toN.simplex` where `x.toN : X.N` is the unique nondegenerate
+simplex of `X` which generates the same subcomplex as `x`. -/
+@[no_expose] noncomputable def toNπ (x : X.S) : ⦋x.dim⦌ ⟶ ⦋x.toN.dim⦌ :=
+  (existsUnique_toNπ rfl).exists.choose
+
+instance (x : X.S) : Epi x.toNπ := (existsUnique_toNπ rfl).exists.choose_spec.1
+
+@[simp]
+lemma map_toNπ_op_apply (x : X.S) :
+    X.map x.toNπ.op x.toN.simplex = x.simplex := (existsUnique_toNπ rfl).exists.choose_spec.2
+
+lemma dim_toN_le (x : X.S) :
+    x.toN.dim ≤ x.dim :=
+  SimplexCategory.le_of_epi x.toNπ
+
 end S
 
 end SSet

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean

@@ -57,11 +57,30 @@ lemma ext_iff (x y : A.N) :
     x = y ↔ x.toN = y.toN := by
   grind [cases SSet.Subcomplex.N]
 
+variable (A) in
+@[elab_as_elim]
+lemma cases {motive : X.N → Prop}
+    (mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s)
+    (notMem : ∀ (s : A.N), motive s.toN)
+    (s : X.N) :
+    motive s := by
+  by_cases hs : s.subcomplex ≤ A
+  · exact mem s hs
+  · exact notMem (.mk' s (by simpa using hs))
+
+lemma eq_iff_sMk_eq {X : SSet.{u}} {A : X.Subcomplex} (x y : A.N) :
+    x = y ↔ S.mk x.simplex = S.mk y.simplex := by
+  rw [N.ext_iff, SSet.N.ext_iff]
+
 instance : PartialOrder A.N :=
   PartialOrder.lift toN (fun _ _ ↦ by simp [ext_iff])
 
 lemma le_iff {x y : A.N} : x ≤ y ↔ x.toN ≤ y.toN :=
   Iff.rfl
+
+lemma lt_iff {x y : A.N} : x < y ↔ x.toN < y.toN :=
+  Iff.rfl
+
 section
 
 variable (s : A.N) {d : ℕ} (hd : s.dim = d)
@@ -81,4 +100,11 @@ end
 
 end N
 
+lemma existsN {X : SSet.{u}} {n : ℕ} (s : X _⦋n⦌) {A : X.Subcomplex}
+    (hs : s ∉ A.obj _) :
+    ∃ (x : A.N) (f : ⦋n⦌ ⟶ ⦋x.dim⦌), Epi f ∧ X.map f.op x.simplex = s := by
+  refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, by simp⟩⟩
+  simp only [← ofSimplex_le_iff] at h ⊢
+  simpa using h
+
 end SSet.Subcomplex

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