Skip to content

Commit 9123595

Browse files
joelrioujoelriou
committed
feat(AlgebraicTopology/SimplicialSet): pairings of non degenerate simplices, following Sean Moss (#28332)
In this PR, we introduce the notion of pairing for a subcomplex of a simplicial set. Following the work of Sean Moss, *Another approach to the Kan-Quillen model structure*, this is an essential tool in the study of (inner) anodyne extensions.
1 parent 53655df commit 9123595

File tree

5 files changed

+217
-0
lines changed

5 files changed

+217
-0
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1368,6 +1368,8 @@ import Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
13681368
import Mathlib.AlgebraicTopology.SimplicialObject.II
13691369
import Mathlib.AlgebraicTopology.SimplicialObject.Op
13701370
import Mathlib.AlgebraicTopology.SimplicialObject.Split
1371+
import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
1372+
import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
13711373
import Mathlib.AlgebraicTopology.SimplicialSet.Basic
13721374
import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
13731375
import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

‎Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
/-
2+
Copyright (c) 2025 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
import Mathlib.AlgebraicTopology.SimplicialSet.Simplices
7+
8+
/-!
9+
# Simplices that are uniquely codimensional one faces
10+
11+
Let `X` be a simplicial set. If `x : X _⦋d⦌` and `y : X _⦋d + 1⦌`,
12+
we say that `x` is uniquely a `1`-codimensional face of `y` if there
13+
exists a unique `i : Fin (d + 2)` such that `X.δ i y = x`. In this file,
14+
we extend this to a predicate `IsUniquelyCodimOneFace` involving two terms
15+
in the type `X.S` of simplices of `X`. This is used in the
16+
file `AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing` for the
17+
study of strong (inner) anodyne extensions.
18+
19+
## References
20+
* [Sean Moss, *Another approach to the Kan-Quillen model structure*][moss-2020]
21+
22+
-/
23+
24+
universe u
25+
26+
open CategoryTheory Simplicial
27+
28+
namespace SSet.S
29+
30+
variable {X : SSet.{u}} (x y : X.S)
31+
32+
/-- The property that a simplex is uniquely a `1`-codimensional face of another simplex -/
33+
def IsUniquelyCodimOneFace : Prop :=
34+
y.dim = x.dim + 1 ∧ ∃! (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌), Mono f ∧ X.map f.op y.simplex = x.simplex
35+
36+
namespace IsUniquelyCodimOneFace
37+
38+
lemma iff {d : ℕ} (x : X _⦋d⦌) (y : X _⦋d + 1⦌) :
39+
IsUniquelyCodimOneFace (S.mk x) (S.mk y) ↔
40+
∃! (i : Fin (d + 2)), X.δ i y = x := by
41+
constructor
42+
· rintro ⟨_, ⟨f, ⟨_, h₁⟩, h₂⟩⟩
43+
obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f
44+
exact ⟨i, h₁, fun j hj ↦ SimplexCategory.δ_injective (h₂ _ ⟨inferInstance, hj⟩)⟩
45+
· rintro ⟨i, h₁, h₂⟩
46+
refine ⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩
47+
obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f
48+
obtain rfl : j = i := h₂ _ h₄
49+
rfl
50+
51+
variable {x y} (hxy : IsUniquelyCodimOneFace x y)
52+
53+
include hxy in
54+
lemma dim_eq : y.dim = x.dim + 1 := hxy.1
55+
56+
section
57+
58+
variable {d : ℕ} (hd : x.dim = d)
59+
60+
lemma cast : IsUniquelyCodimOneFace (x.cast hd) (y.cast (by rw [hxy.dim_eq, hd])) := by
61+
simpa only [cast_eq_self]
62+
63+
lemma existsUnique_δ_cast_simplex :
64+
∃! (i : Fin (d + 2)), X.δ i (y.cast (by rw [hxy.dim_eq, hd])).simplex =
65+
(x.cast hd).simplex := by
66+
simpa only [S.cast, iff] using hxy.cast hd
67+
68+
include hxy in
69+
/-- When a `d`-dimensional simplex `x` is a `1`-codimensional face of `y`, this is
70+
the only `i : Fin (d + 2)`, such that `X.δ i y = x` (with an abuse of notation:
71+
see `δ_index` and `δ_eq_iff` for well typed statements). -/
72+
noncomputable def index : Fin (d + 2) :=
73+
(hxy.existsUnique_δ_cast_simplex hd).exists.choose
74+
75+
lemma δ_index :
76+
X.δ (hxy.index hd) (y.cast (by rw [hxy.dim_eq, hd])).simplex = (x.cast hd).simplex :=
77+
(hxy.existsUnique_δ_cast_simplex hd).exists.choose_spec
78+
79+
lemma δ_eq_iff (i : Fin (d + 2)) :
80+
X.δ i (y.cast (by rw [hxy.dim_eq, hd])).simplex = (x.cast hd).simplex ↔
81+
i = hxy.index hd :=
82+
⟨fun h ↦ (hxy.existsUnique_δ_cast_simplex hd).unique h (hxy.δ_index hd),
83+
by rintro rfl; apply δ_index⟩
84+
85+
end
86+
87+
end IsUniquelyCodimOneFace
88+
89+
end SSet.S

‎Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
/-
2+
Copyright (c) 2025 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
7+
import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
8+
9+
/-!
10+
# Pairings
11+
12+
In this file, we introduce the definition of a pairing for a subcomplex `A`
13+
of a simplicial set `X`, following the ideas by Sean Moss,
14+
*Another approach to the Kan-Quillen model structure*, who gave a
15+
complete combinatorial characterization of strong (inner) anodyne extensions.
16+
Strong (inner) anodyne extensions are transfinite compositions of pushouts of coproducts
17+
of (inner) horn inclusions, i.e. this is similar to (inner) anodyne extensions but
18+
without the stability property under retracts.
19+
20+
A pairing for `A` consists in the data of a partition of the nondegenerate
21+
simplices of `X` not in `A` into type (I) simplices and type (II) simplices,
22+
and of a bijection between the types of type (I) and type (II) simplices.
23+
Indeed, the main observation is that when we attach a simplex along a horn
24+
inclusion, exactly two nondegenerate simplices are added: this simplex,
25+
and the unique face which is not in the image of the horn. The former shall be
26+
considered as of type (I) and the latter as type (II).
27+
28+
We say that a pairing is *regular* (typeclass `Pairing.IsRegular`) when
29+
- it is proper (`Pairing.IsProper`), i.e. any type (II) simplex is uniquely
30+
a face of the corresponding type (I) simplex.
31+
- a certain ancestrality relation is well founded.
32+
When these conditions are satisfied, the inclusion `A.ι : A ⟶ X` is
33+
a strong anodyne extension (TODO @joelriou), and the converse is also true
34+
(if `A.ι` is a strong anodyne extension, then there is a regular pairing for `A` (TODO)).
35+
36+
## References
37+
* [Sean Moss, *Another approach to the Kan-Quillen model structure*][moss-2020]
38+
39+
-/
40+
41+
universe u
42+
43+
namespace SSet.Subcomplex
44+
45+
variable {X : SSet.{u}} (A : X.Subcomplex)
46+
47+
/-- A pairing for a subcomplex `A` of a simplicial set `X` consists of a partition
48+
of the nondegenerate simplices of `X` not in `A` in two types (I) and (II) of simplices,
49+
and a bijection between the type (II) simplices and the type (I) simplices.
50+
See the introduction of the file `AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing`. -/
51+
structure Pairing where
52+
/-- the set of type (I) simplices -/
53+
I : Set A.N
54+
/-- the set of type (II) simplices -/
55+
II : Set A.N
56+
inter : I ∩ II = ∅
57+
union : I ∪ II = Set.univ
58+
/-- a bijection from the type (II) simplices to the type (I) simplices -/
59+
p : II ≃ I
60+
61+
namespace Pairing
62+
63+
variable {A} (P : A.Pairing)
64+
65+
/-- A pairing is regular when each type (II) simplex
66+
is uniquely a `1`-codimensional face of the corresponding (I)
67+
simplex. -/
68+
class IsProper where
69+
isUniquelyCodimOneFace (x : P.II) :
70+
S.IsUniquelyCodimOneFace x.1.toS (P.p x).1.toS
71+
72+
lemma isUniquelyCodimOneFace [P.IsProper] (x : P.II) :
73+
S.IsUniquelyCodimOneFace x.1.toS (P.p x).1.toS :=
74+
IsProper.isUniquelyCodimOneFace x
75+
76+
/-- The condition that a pairing only involves inner horns. -/
77+
class IsInner [P.IsProper] : Prop where
78+
ne_zero (x : P.II) {d : ℕ} (hd : x.1.dim = d) :
79+
(P.isUniquelyCodimOneFace x).index hd ≠ 0
80+
ne_last (x : P.II) {d : ℕ} (hd : x.1.dim = d) :
81+
(P.isUniquelyCodimOneFace x).index hd ≠ Fin.last _
82+
83+
/-- The ancestrality relation on type (II) simplices. -/
84+
def AncestralRel (x y : P.II) : Prop :=
85+
x ≠ y ∧ x.1 < (P.p y).1
86+
87+
/-- A proper pairing is regular when the ancestrality relation
88+
is well founded. -/
89+
class IsRegular extends P.IsProper where
90+
wf : WellFounded P.AncestralRel
91+
92+
section
93+
94+
variable [P.IsRegular]
95+
96+
lemma wf : WellFounded P.AncestralRel := IsRegular.wf
97+
98+
instance : IsWellFounded _ P.AncestralRel where
99+
wf := P.wf
100+
101+
end
102+
103+
end Pairing
104+
105+
end SSet.Subcomplex

‎Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplicesSubcomplex.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,11 @@ lemma ext_iff (x y : A.N) :
5353
x = y ↔ x.toN = y.toN := by
5454
grind [cases SSet.Subcomplex.N]
5555

56+
instance : PartialOrder A.N :=
57+
PartialOrder.lift toN (fun _ _ ↦ by simp [ext_iff])
58+
59+
lemma le_iff {x y : A.N} : x ≤ y ↔ x.toN ≤ y.toN :=
60+
Iff.rfl
5661
section
5762

5863
variable (s : A.N) {d : ℕ} (hd : s.dim = d)

‎docs/references.bib‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3451,6 +3451,22 @@ @Article{ morrison-penney-enriched
34513451
eprint = {https://academic.oup.com/imrn/article-pdf/2019/11/3527/28757603/rnx217.pdf}
34523452
}
34533453

3454+
@Article{ moss-2020,
3455+
author = {Moss, Sean},
3456+
title = {Another approach to the {K}an-{Q}uillen model structure},
3457+
journal = {J. Homotopy Relat. Struct.},
3458+
fjournal = {Journal of Homotopy and Related Structures},
3459+
volume = {15},
3460+
year = {2020},
3461+
number = {1},
3462+
pages = {143--165},
3463+
issn = {2193-8407,1512-2891},
3464+
mrclass = {55U35 (55U10)},
3465+
mrnumber = {4062882},
3466+
doi = {10.1007/s40062-019-00247-y},
3467+
url = {https://doi.org/10.1007/s40062-019-00247-y}
3468+
}
3469+
34543470
@Article{ MR0236876,
34553471
title = {A new proof that metric spaces are paracompact},
34563472
author = {Mary Ellen Rudin},

0 commit comments

Comments
 (0)