feat(AlgebraicTopology): order relation between simplices of the nerve of a partial order

Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean

@@ -21,11 +21,11 @@ public section
 
 universe u
 
-open CategoryTheory Simplicial
+open CategoryTheory Simplicial SSet
 
 namespace PartialOrder
 
-variable {X : Type*} [PartialOrder X] {n : ℕ}
+variable {X : Type*} [PartialOrder X] {n m : ℕ}
 
 set_option backward.isDefEq.respectTransparency.types false in
 lemma mem_range_nerve_σ_iff (s : (nerve X) _⦋n + 1⦌) (i : Fin (n + 1)) :
@@ -73,4 +73,31 @@ lemma mem_nerve_nonDegenerate_iff_injective (s : (nerve X) _⦋n⦌) :
   · exact h'
   · exact ((h h').not_lt hij).elim
 
+lemma nerve_ofSimplex_le_ofSimplex_iff
+    (s : (nerve X) _⦋n⦌) (t : (nerve X) _⦋m⦌) :
+    Subcomplex.ofSimplex s ≤ Subcomplex.ofSimplex t ↔
+      Set.range s.obj ⊆ Set.range t.obj := by
+  refine ⟨?_, ?_⟩
+  · rintro hst _ ⟨i, rfl⟩
+    rw [Subcomplex.ofSimplex_le_iff] at hst
+    obtain ⟨⟨f⟩, rfl⟩ := hst
+    exact ⟨_, rfl⟩
+  · wlog ht : t ∈ (nerve X).nonDegenerate m generalizing m t
+    · intro hst
+      obtain ⟨m', f, _, ⟨t', h₁⟩, rfl⟩ := exists_nonDegenerate _ t
+      rw [Subcomplex.ofSimplex_map_of_epi]
+      refine this _ h₁ ?_
+      rintro _ ⟨i, rfl⟩
+      obtain ⟨j, hj⟩ := hst (Set.mem_range_self i)
+      aesop
+    rw [mem_nerve_nonDegenerate_iff_strictMono] at ht
+    intro hst
+    rw [Subcomplex.ofSimplex_le_iff]
+    have (i : Fin (n + 1)) : ∃ (j : Fin (m + 1)), t.obj j = s.obj i := by aesop
+    choose f hf using this
+    have hf' : Monotone f := fun i₁ i₂ hi ↦ by
+      rw [← ht.le_iff_le, hf, hf]
+      exact s.monotone hi
+    exact ⟨Quiver.Hom.op (SimplexCategory.Hom.mk ⟨f, hf'⟩), by aesop⟩
+
 end PartialOrder

Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean

@@ -92,6 +92,24 @@ lemma nonDegenerate_iff_strictMono_objEquiv {n : ℕ} (z : (Δ[p] ⊗ Δ[q] : SS
     PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]
   rfl
 
+lemma isoNerve_hom_app_obj {n : ℕ} (x : (Δ[p] ⊗ Δ[q] : SSet.{u}) _⦋n⦌) :
+    ((isoNerve p q).hom.app _ x).obj = ULift.up ∘ objEquiv x := rfl
+
+lemma range_isoNerve_hom_app_obj {n : ℕ} (x : (Δ[p] ⊗ Δ[q] : SSet.{u}) _⦋n⦌) :
+    Set.range ((isoNerve p q).hom.app _ x).obj = ULift.down ⁻¹' Set.range (objEquiv x) := by
+  rw [isoNerve_hom_app_obj]
+  refine (Equiv.ulift.eq_preimage_iff_image_eq ..).2 ?_
+  simp [Set.range_comp, ← Set.image_comp]
+
+lemma ofSimplex_le_ofSimplex_iff
+    {n m : ℕ} (s : (Δ[p] ⊗ Δ[q] : SSet.{u}) _⦋n⦌) (t : (Δ[p] ⊗ Δ[q] : SSet.{u}) _⦋m⦌) :
+    Subcomplex.ofSimplex s ≤ Subcomplex.ofSimplex t ↔
+      Set.range (objEquiv s) ⊆ Set.range (objEquiv t) := by
+  simp only [← Subcomplex.image_le_image_iff (isoNerve p q).hom,
+    Subcomplex.image_ofSimplex, PartialOrder.nerve_ofSimplex_le_ofSimplex_iff,
+    range_isoNerve_hom_app_obj]
+  exact ⟨Set.preimage_mono (f := ULift.up), Set.preimage_mono⟩
+
 /-- Given a `n`-simplex `x` in `Δ[p] ⊗ Δ[q]`, this is the order preserving
 map `Fin (n + 1) →o Fin (m + 1)` (with `p + q = m`) which corresponds to the
 sum of the two components of `objEquiv x : Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)`. -/

Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean

@@ -262,6 +262,9 @@ set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma preimage_ι (A : X.Subcomplex) : A.preimage A.ι = ⊤ := by aesop
 
+lemma preimage_monotone (f : Y ⟶ X) : Monotone (fun (S : X.Subcomplex) ↦ S.preimage f) :=
+  fun _ _ h _ _ hx ↦ h _ hx
+
 end
 
 section
@@ -342,6 +345,20 @@ lemma image_preimage_le (B : X.Subcomplex) (f : Y ⟶ X) :
     (B.preimage f).image f ≤ B := by
   rw [image_le_iff]
 
+@[simp]
+lemma preimage_image (S : X.Subcomplex) (f : X ⟶ Y) [Mono f] :
+    (S.image f).preimage f = S := by
+  refine le_antisymm ?_ (by rw [← image_le_iff])
+  intro n x ⟨y, hy, h⟩
+  rwa [← injective_of_mono (f.app n) h]
+
+@[simp]
+lemma image_le_image_iff (f : X ⟶ Y) [Mono f] {S₁ S₂ : X.Subcomplex} :
+    S₁.image f ≤ S₂.image f ↔ S₁ ≤ S₂ := by
+  refine ⟨fun h ↦ ?_, fun h ↦ image_monotone f h⟩
+  rw [← S₁.preimage_image f, ← S₂.preimage_image f]
+  exact preimage_monotone f h
+
 @[simp]
 lemma preimage_image_of_isIso (f : X ⟶ Y) (B : Y.Subcomplex) [IsIso f] :
     (B.preimage f).image f = B := by