feat(AlgebraicTopology/SimplicialSet/AnodyneExtensions): the opposite of a pairing (#38061)

Author: joelriou

Mathlib.lean

@@ -1511,6 +1511,7 @@ public import Mathlib.AlgebraicTopology.SimplicialObject.II
 public import Mathlib.AlgebraicTopology.SimplicialObject.Op
 public import Mathlib.AlgebraicTopology.SimplicialObject.Split
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
 public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
@@ -1561,6 +1562,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
 public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
 public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
+public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
 public import Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
 public import Mathlib.AlgebraicTopology.SingularHomology.Basic
 public import Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance

Mathlib/AlgebraicTopology/SimplexCategory/Rev.lean

@@ -81,4 +81,6 @@ def revEquivalence : SimplexCategory ≌ SimplexCategory where
   unitIso := revCompRevIso.symm
   counitIso := revCompRevIso
 
+instance : rev.IsEquivalence := revEquivalence.isEquivalence_functor
+
 end SimplexCategory

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

@@ -104,6 +104,16 @@ lemma unique (f : ⦋d⦌ ⟶ ⦋d + 1⦌) [Mono f]
 
 end
 
+include hxy in
+lemma op : (S.opEquiv.symm x).IsUniquelyCodimOneFace (S.opEquiv.symm y) := by
+  obtain ⟨d, x, rfl⟩ := x.mk_surjective
+  obtain ⟨d', y, rfl⟩ := y.mk_surjective
+  obtain rfl : d' = d + 1 := hxy.dim_eq
+  simp only [opEquiv_symm_apply, iff]
+  refine ⟨(hxy.index rfl).rev, by simpa using hxy.δ_index rfl, fun i hi ↦ ?_⟩
+  obtain ⟨i, rfl⟩ := i.rev_surjective
+  simpa [← hxy.δ_eq_iff rfl] using hi
+
 include hxy in
 lemma of_iso {Y : SSet.{u}} (e : X ≅ Y) :
     (S.mk (e.hom.app _ x.simplex)).IsUniquelyCodimOneFace (S.mk (e.hom.app _ y.simplex)) := by

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
+public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
+
+/-!
+# The opposite of a pairing
+
+Let `A` be a subcomplex of a simplicial set `X`. If `P` is a pairing of `A`,
+we construct a pairing `P.op` for the subcomplex `A.op` of `X.op`.
+
+-/
+
+@[expose] public section
+
+universe u
+
+namespace SSet.Subcomplex.Pairing
+
+variable {X : SSet.{u}} {A : X.Subcomplex} (P : A.Pairing)
+
+/-- If `P` is a pairing for a subcomplex `A` of a simplicial set `X`,
+this is the corresponding pairing of `A.op`. -/
+@[simps I II]
+def op : A.op.Pairing where
+  I := Subcomplex.N.opEquiv ⁻¹' P.I
+  II := Subcomplex.N.opEquiv ⁻¹' P.II
+  inter := by simp [← Set.preimage_inter, P.inter]
+  union := by simp [← Set.preimage_union, P.union]
+  p := (N.opEquiv.subtypeEquiv (by simp)).trans
+    (P.p.trans (N.opEquiv.symm.subtypeEquiv (by simp)))
+
+@[simp]
+lemma op_p (x : P.II) :
+    dsimp% P.op.p ⟨Subcomplex.N.opEquiv.symm x.1, x.2⟩ =
+      ⟨Subcomplex.N.opEquiv.symm (P.p x), by simp⟩ := rfl
+
+lemma op_ancestralRel_iff (x y : P.II) :
+    P.op.AncestralRel ⟨Subcomplex.N.opEquiv.symm x.1, x.2⟩
+      ⟨Subcomplex.N.opEquiv.symm y.1, y.2⟩ ↔ P.AncestralRel x y :=
+  and_congr (not_congr (by aesop)) (by simp)
+
+instance [P.IsProper] : P.op.IsProper where
+  isUniquelyCodimOneFace x := (P.isUniquelyCodimOneFace ⟨_, x.2⟩).op
+
+instance [P.IsRegular] : P.op.IsRegular where
+  wf := by
+    have hP := P.wf
+    rw [wellFounded_iff_isEmpty_descending_chain] at hP ⊢
+    by_contra!
+    obtain ⟨f, hf⟩ := this
+    refine hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩
+    simpa [← P.op_ancestralRel_iff] using hf n
+
+end SSet.Subcomplex.Pairing

Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean

@@ -5,6 +5,7 @@ Authors: Joël Riou
 -/
 module
 
+public import Mathlib.AlgebraicTopology.SimplicialSet.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
 
 /-!
@@ -75,6 +76,23 @@ lemma mem_degenerate_iff (x : X _⦋n⦌) :
   · rintro ⟨m, hm, f, hf, hx⟩
     exact ⟨m, hm, f, hx⟩
 
+set_option backward.isDefEq.respectTransparency false in
+lemma opObjEquiv_mem_degenerate_iff (x : X.op _⦋n⦌) :
+    opObjEquiv x ∈ X.degenerate n ↔ x ∈ X.op.degenerate n := by
+  simp only [mem_degenerate_iff]
+  refine exists_congr (fun m ↦ exists_congr (fun _ ↦ ?_))
+  constructor
+  · obtain ⟨x, rfl⟩ := opObjEquiv.symm.surjective x
+    rintro ⟨f, _, y, rfl⟩
+    exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv.symm y, by simp [op_map]⟩
+  · rintro ⟨f, _, y, rfl⟩
+    exact ⟨SimplexCategory.rev.map f, inferInstance, opObjEquiv y, by simp [op_map]⟩
+
+lemma opObjEquiv_mem_nonDegenerate_iff (x : X.op _⦋n⦌) :
+    opObjEquiv x ∈ X.nonDegenerate n ↔ x ∈ X.op.nonDegenerate n := by
+  simp only [mem_nonDegenerate_iff_notMem_degenerate,
+    opObjEquiv_mem_degenerate_iff]
+
 lemma degenerate_eq_iUnion_range_σ :
     X.degenerate (n + 1) = ⋃ (i : Fin (n + 1)), Set.range (X.σ i) := by
   ext x

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
 public import Mathlib.AlgebraicTopology.SimplicialSet.Simplices
+public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp
 
 /-!
 # The partially ordered type of non degenerate simplices of a simplicial set
@@ -163,6 +164,23 @@ lemma subcomplex_le_iff {A B : X.Subcomplex} :
       exact h _ _ hx
   · simpa using h (N.mk _ x.prop) (by simpa)
 
+set_option backward.isDefEq.respectTransparency false in
+/-- The bijection `X.op.N ≃ X.N`. -/
+@[simps -isSimp apply symm_apply]
+def opEquiv : X.op.N ≃o X.N where
+  toFun x := N.mk (opObjEquiv x.simplex)
+    (by simpa only [opObjEquiv_mem_nonDegenerate_iff] using x.nonDegenerate)
+  invFun y := N.mk (opObjEquiv.symm y.simplex)
+    (by simpa [← opObjEquiv_mem_nonDegenerate_iff] using y.nonDegenerate)
+  map_rel_iff' {x y} := by
+    dsimp
+    simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
+    constructor
+    · rintro ⟨f, hf⟩
+      exact ⟨SimplexCategory.rev.map f, by simp [op_map, dsimp% hf]⟩
+    · rintro ⟨f, hf⟩
+      exact ⟨SimplexCategory.rev.map f, by simp [op_map, ← hf]⟩
+
 set_option backward.isDefEq.respectTransparency false in
 /-- The bijection `X.N ≃ Y.N` on nondegenerate simplices of simplicial sets
 that is induced by an isomorphism `X ≅ Y`. -/

Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean

@@ -98,6 +98,15 @@ lemma cast_eq_self : s.cast hd = s := by
 
 end
 
+/-- The bijection `A.op.N ≃ A.N` for a subcomplex `A` of a simplicial set.. -/
+@[simps -isSimp apply symm_apply]
+def opEquiv : A.op.N ≃o A.N where
+  toFun x := N.mk' (SSet.N.opEquiv x.toN) x.notMem
+  invFun y := N.mk' (SSet.N.opEquiv.symm y.toN) y.notMem
+  left_inv _ := rfl
+  right_inv _ := rfl
+  map_rel_iff' := SSet.N.opEquiv.map_rel_iff
+
 /-- The bijection `A.N ≃ B.N` on nondegenerate simplices not belonging
 to a certain subcomplex that is induced by an isomorphism `X ≅ Y` of
 simplicial sets which maps `A : X.Subcomplex` to `B : Y.Subcomplex`. -/

Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean

@@ -6,6 +6,7 @@ Authors: Joël Riou
 module
 
 public import Mathlib.CategoryTheory.Elements
+public import Mathlib.AlgebraicTopology.SimplicialSet.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
 
 /-!
@@ -164,6 +165,12 @@ lemma le_iff_nonempty_hom (x y : X.S) :
   · rintro ⟨f, hf⟩
     exact ⟨f.unop, hf⟩
 
+/-- The bijection `X.op.S ≃ X.S`. -/
+@[simps -isSimp apply symm_apply]
+def opEquiv : X.op.S ≃ X.S where
+  toFun x := S.mk (opObjEquiv x.simplex)
+  invFun y := S.mk (opObjEquiv.symm y.simplex)
+
 /-- The bijection `X.S ≃ Y.S` on simplices of simplicial sets that
 is induced by an isomorphism `X ≅ Y`. -/
 @[simps -isSimp apply symm_apply]

Mathlib/AlgebraicTopology/SimplicialSet/SubcomplexOp.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.SimplicialSet.Op
+public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
+
+/-!
+# The opposite of a subcomplex
+
+-/
+
+@[expose] public section
+
+universe u
+
+namespace SSet.Subcomplex
+
+variable {X : SSet.{u}} (A : X.Subcomplex)
+
+/-- The opposite of subcomplex, as a subcomplex of the opposite simplicial set. -/
+protected def op : X.op.Subcomplex where
+  obj := A.obj
+  map _ := A.map _
+
+lemma mem_op_obj_iff {d : SimplexCategoryᵒᵖ} (x : X.op.obj d) :
+    x ∈ A.op.obj d ↔ X.opObjEquiv x ∈ A.obj d := Iff.rfl
+
+end SSet.Subcomplex