Skip to content

Commit c8d7ba9

Browse files
jcreinholdjcreinhold
committed
feat(AlgebraicTopology/SimplicialSet): single-cell boundary and horn attachments
1 parent d9874e4 commit c8d7ba9

4 files changed

Lines changed: 403 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1529,6 +1529,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
15291529
public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
15301530
public import Mathlib.AlgebraicTopology.SimplicialSet.Basic
15311531
public import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
1532+
public import Mathlib.AlgebraicTopology.SimplicialSet.BoundaryAttach
15321533
public import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
15331534
public import Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
15341535
public import Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
@@ -1545,6 +1546,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvarianc
15451546
public import Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
15461547
public import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
15471548
public import Mathlib.AlgebraicTopology.SimplicialSet.Horn
1549+
public import Mathlib.AlgebraicTopology.SimplicialSet.HornAttach
15481550
public import Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
15491551
public import Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
15501552
public import Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
@@ -1572,6 +1574,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
15721574
public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
15731575
public import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
15741576
public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
1577+
public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexAttach
15751578
public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
15761579
public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
15771580
public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp

‎Mathlib/AlgebraicTopology/SimplicialSet/BoundaryAttach.lean‎

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
/-
2+
Copyright (c) 2026 Jacob Reinhold. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jacob Reinhold
5+
-/
6+
module
7+
8+
public import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
9+
public import Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
10+
public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexAttach
11+
12+
/-!
13+
# Single-cell boundary attachment to a subcomplex
14+
15+
`Skeleton.lean` attaches all nondegenerate `n`-simplices of a simplicial set
16+
in one step, dimension by dimension. This file refines that picture to a
17+
single cell along its boundary: for a nondegenerate `n`-simplex `x : X _⦋n⦌`
18+
with `x ∉ A` and boundary already in `A`, the square
19+
```
20+
∂Δ[n] ──→ A
21+
│ │
22+
↓ ↓
23+
Δ[n] ──→ A ⊔ ofSimplex x
24+
```
25+
is a pushout in `SSet`
26+
(`Subcomplex.boundaryAttach_isPushout_of_nonDegenerate`).
27+
28+
The map `yonedaEquiv.symm x` need not be monic; injectivity off the
29+
boundary is enough, and that follows from nondegeneracy by an
30+
Eilenberg–Zilber argument
31+
(`Subcomplex.injOn_compl_boundary_yonedaEquiv_symm`). The pushout then
32+
follows from `Subcomplex.attachingMap_isPushout_of_injOn_compl` once the
33+
preimage of `A` along `yonedaEquiv.symm x` is identified with `∂Δ[n]`
34+
(`Subcomplex.preimage_yonedaEquiv_symm_eq_boundary`).
35+
36+
## References
37+
38+
* [E. Riehl and D. Verity, *Elements of ∞-Category Theory*][RiehlVerity2022],
39+
Section 1.1 (cellular structure of simplicial sets, Remark 1.1.27).
40+
-/
41+
42+
@[expose] public section
43+
44+
universe u
45+
46+
noncomputable section
47+
48+
open CategoryTheory Limits Opposite
49+
open scoped Simplicial
50+
51+
namespace SSet
52+
namespace Subcomplex
53+
54+
/-- If the boundary of a nondegenerate `n`-simplex `x` already lies in `A` and
55+
`x` itself does not, the preimage of `A` along the classifier of `x` is exactly
56+
the boundary `∂Δ[n]`. -/
57+
lemma preimage_yonedaEquiv_symm_eq_boundary {X : SSet.{u}} {n : ℕ}
58+
(A : X.Subcomplex) {x : X _⦋n⦌} (_hx : x ∈ X.nonDegenerate n)
59+
(hxA : x ∉ A.obj (op ⦋n⦌))
60+
(hboundary :
61+
(∂Δ[n] : (Δ[n] : SSet.{u}).Subcomplex).image (yonedaEquiv.symm x) ≤ A) :
62+
A.preimage (yonedaEquiv.symm x) = (∂Δ[n] : (Δ[n] : SSet.{u}).Subcomplex) := by
63+
classical
64+
ext ⟨⟨d⟩⟩ y
65+
refine ⟨fun hyA ↦ ?_, fun hybdry ↦ hboundary _ ⟨y, hybdry, rfl⟩⟩
66+
by_contra hybdry
67+
have hsurj : Function.Surjective (stdSimplex.asOrderHom y) := not_not.mp hybdry
68+
let f := stdSimplex.objEquiv y
69+
haveI : Epi f := by
70+
rw [SimplexCategory.epi_iff_surjective]
71+
simpa [f, stdSimplex.asOrderHom] using hsurj
72+
obtain ⟨⟨hsplit⟩⟩ := isSplitEpi_of_epi f
73+
apply hxA
74+
have hxA' :
75+
X.map hsplit.section_.op ((yonedaEquiv.symm x).app (op ⦋d⦌) y) ∈
76+
A.obj (op ⦋n⦌) :=
77+
A.map hsplit.section_.op hyA
78+
convert hxA' using 1
79+
calc
80+
x = X.map (𝟙 (op ⦋n⦌)) x := by simp
81+
_ = X.map (f.op ≫ hsplit.section_.op) x := by
82+
rw [← op_comp, hsplit.id]; simp
83+
_ = X.map hsplit.section_.op (X.map f.op x) := by simp [Functor.map_comp]
84+
_ = X.map hsplit.section_.op ((yonedaEquiv.symm x).app (op ⦋d⦌) y) := by
85+
rw [stdSimplex.map_objEquiv_op_apply]
86+
87+
/-- The classifier of a nondegenerate simplex is injective off the boundary,
88+
even when it is not monic. This is the Eilenberg–Zilber input to single-cell
89+
boundary attachment. -/
90+
lemma injOn_compl_boundary_yonedaEquiv_symm {X : SSet.{u}} {n : ℕ}
91+
{x : X _⦋n⦌} (hx : x ∈ X.nonDegenerate n) (d : SimplexCategoryᵒᵖ) :
92+
Set.InjOn ((yonedaEquiv.symm x).app d)
93+
((∂Δ[n] : (Δ[n] : SSet.{u}).Subcomplex).obj d)ᶜ := by
94+
classical
95+
obtain ⟨⟨d⟩⟩ := d
96+
intro y₁ hy₁ y₂ hy₂ h
97+
rw [Set.mem_compl_iff] at hy₁ hy₂
98+
let f₁ := stdSimplex.objEquiv y₁
99+
let f₂ := stdSimplex.objEquiv y₂
100+
have hsurj₁ : Function.Surjective (stdSimplex.asOrderHom y₁) := not_not.mp hy₁
101+
have hsurj₂ : Function.Surjective (stdSimplex.asOrderHom y₂) := not_not.mp hy₂
102+
haveI : Epi f₁ := by
103+
rw [SimplexCategory.epi_iff_surjective]
104+
simpa [f₁, stdSimplex.asOrderHom] using hsurj₁
105+
haveI : Epi f₂ := by
106+
rw [SimplexCategory.epi_iff_surjective]
107+
simpa [f₂, stdSimplex.asOrderHom] using hsurj₂
108+
have hf : f₁ = f₂ := by
109+
refine X.unique_nonDegenerate_map ((yonedaEquiv.symm x).app (op ⦋d⦌) y₁)
110+
f₁ ⟨x, hx⟩ ?_ f₂ ⟨x, hx⟩ ?_
111+
· simpa [f₁] using (stdSimplex.map_objEquiv_op_apply (X := X) x y₁).symm
112+
· calc
113+
(yonedaEquiv.symm x).app (op ⦋d⦌) y₁ =
114+
(yonedaEquiv.symm x).app (op ⦋d⦌) y₂ := h
115+
_ = X.map f₂.op x := by
116+
simpa [f₂] using (stdSimplex.map_objEquiv_op_apply (X := X) x y₂).symm
117+
exact stdSimplex.objEquiv.injective hf
118+
119+
/-- Single-cell boundary attachment as a pushout. If `x : X _⦋n⦌` is
120+
nondegenerate with `x ∉ A` and its boundary already in `A`, then
121+
`A ⊔ ofSimplex x` is the pushout of `∂Δ[n] ↪ Δ[n]` along the attaching map.
122+
This is the per-cell counterpart to the `skeletonOfMono` filtration in
123+
`Skeleton.lean`. -/
124+
lemma boundaryAttach_isPushout_of_nonDegenerate {X : SSet.{u}} {n : ℕ}
125+
(A : X.Subcomplex) {x : X _⦋n⦌} (hx : x ∈ X.nonDegenerate n)
126+
(hxA : x ∉ A.obj (op ⦋n⦌))
127+
(hboundary :
128+
(∂Δ[n] : (Δ[n] : SSet.{u}).Subcomplex).image (yonedaEquiv.symm x) ≤ A) :
129+
IsPushout
130+
(attachingMap A (yonedaEquiv.symm x)
131+
(preimage_yonedaEquiv_symm_eq_boundary A hx hxA hboundary))
132+
(∂Δ[n] : (Δ[n] : SSet.{u}).Subcomplex).ι
133+
(homOfLE (show A ≤ A ⊔ ofSimplex x by simp))
134+
(lift (yonedaEquiv.symm x) (show range (yonedaEquiv.symm x) ≤ A ⊔ ofSimplex x by
135+
simp [Subcomplex.range_eq_ofSimplex])) := by
136+
have h := attachingMap_isPushout_of_injOn_compl A (yonedaEquiv.symm x)
137+
(preimage_yonedaEquiv_symm_eq_boundary A hx hxA hboundary)
138+
(injOn_compl_boundary_yonedaEquiv_symm hx)
139+
convert h using 2
140+
all_goals simp [Subcomplex.range_eq_ofSimplex]
141+
142+
end Subcomplex
143+
end SSet

‎Mathlib/AlgebraicTopology/SimplicialSet/HornAttach.lean‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
/-
2+
Copyright (c) 2026 Jacob Reinhold. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jacob Reinhold
5+
-/
6+
module
7+
8+
public import Mathlib.AlgebraicTopology.SimplicialSet.Horn
9+
public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexAttach
10+
11+
/-!
12+
# Single-cell horn attachment to a subcomplex
13+
14+
For a monic `σ : Δ[n + 1] ⟶ X` whose preimage of `A` equals `Λ[n + 1, i]`,
15+
the square
16+
```
17+
Λ[n+1, i] ──→ A
18+
│ │
19+
↓ ↓
20+
Δ[n+1] ──→ A ⊔ range σ
21+
```
22+
is a pushout in `SSet` (`Subcomplex.hornAttach_isPushout_of_mono`).
23+
Injectivity off `Λ[n + 1, i]` is automatic from `Mono σ`
24+
(`Subcomplex.injOn_compl_horn_of_mono`), so the pushout follows from
25+
`Subcomplex.attachingMap_isPushout_of_injOn_compl`. This is the horn
26+
analogue of single-cell boundary attachment in
27+
`Mathlib/AlgebraicTopology/SimplicialSet/BoundaryAttach.lean`.
28+
29+
Two preimage characterizations identify when `A.preimage σ` equals a horn:
30+
a basic form in terms of faces lying in `A.preimage σ`
31+
(`Subcomplex.preimage_eq_horn_of_face_le_of_omitted_not_le`), and an
32+
image-form variant convenient for cellular filtrations
33+
(`Subcomplex.preimage_eq_horn_of_face_image_le_of_omitted_not_le`).
34+
35+
## References
36+
37+
* [E. Riehl and D. Verity, *Elements of ∞-Category Theory*][RiehlVerity2022],
38+
Section 1.1 (cellular generation by inner horn inclusions,
39+
Proposition 1.1.29).
40+
-/
41+
42+
@[expose] public section
43+
44+
universe u
45+
46+
noncomputable section
47+
48+
open CategoryTheory Limits Opposite
49+
open scoped Simplicial
50+
51+
namespace SSet
52+
namespace Subcomplex
53+
54+
/-- If every codimension-one face except the `i`-th lands in `A` and the
55+
omitted face does not, the preimage of `A` along `σ : Δ[n + 1] ⟶ X` is exactly
56+
the horn `Λ[n + 1, i]`. -/
57+
lemma preimage_eq_horn_of_face_le_of_omitted_not_le {X : SSet.{u}} {n : ℕ}
58+
(A : X.Subcomplex) (σ : Δ[n + 1] ⟶ X) (i : Fin (n + 2))
59+
(hfaces : ∀ j : Fin (n + 2), j ≠ i →
60+
stdSimplex.face.{u} ({j}ᶜ : Finset (Fin (n + 2))) ≤ A.preimage σ)
61+
(homit :
62+
¬ stdSimplex.face.{u} ({i}ᶜ : Finset (Fin (n + 2))) ≤ A.preimage σ) :
63+
A.preimage σ = (Λ[n + 1, i] : (Δ[n + 1] : SSet.{u}).Subcomplex) := by
64+
apply le_antisymm
65+
· rw [subcomplex_le_horn_iff]; exact homit
66+
· rw [horn_eq_iSup, iSup_le_iff]; exact fun j ↦ hfaces j.1 j.2
67+
68+
/-- Image-form variant of `preimage_eq_horn_of_face_le_of_omitted_not_le`:
69+
the hypotheses ask that face images lie in `A` rather than that the faces
70+
themselves lie in `A.preimage σ`. -/
71+
lemma preimage_eq_horn_of_face_image_le_of_omitted_not_le {X : SSet.{u}} {n : ℕ}
72+
(A : X.Subcomplex) (σ : Δ[n + 1] ⟶ X) (i : Fin (n + 2))
73+
(hfaces : ∀ j : Fin (n + 2), j ≠ i →
74+
(stdSimplex.face.{u} ({j}ᶜ : Finset (Fin (n + 2)))).image σ ≤ A)
75+
(homit :
76+
¬ (stdSimplex.face.{u} ({i}ᶜ : Finset (Fin (n + 2)))).image σ ≤ A) :
77+
A.preimage σ = (Λ[n + 1, i] : (Δ[n + 1] : SSet.{u}).Subcomplex) := by
78+
apply preimage_eq_horn_of_face_le_of_omitted_not_le A σ i
79+
· intro j hj; rw [← image_le_iff]; exact hfaces j hj
80+
· intro hle; apply homit; rwa [image_le_iff]
81+
82+
/-- A monic classifier `σ : Δ[n] ⟶ X` is injective at every dimension on the
83+
complement of the horn `Λ[n, i]`. -/
84+
lemma injOn_compl_horn_of_mono {X : SSet.{u}} {n : ℕ} (σ : Δ[n] ⟶ X) [Mono σ]
85+
(i : Fin (n + 1)) (d : SimplexCategoryᵒᵖ) :
86+
Set.InjOn (σ.app d) ((Λ[n, i] : (Δ[n] : SSet.{u}).Subcomplex).obj d)ᶜ := by
87+
have hmono_app : Mono (σ.app d) :=
88+
(NatTrans.mono_iff_mono_app σ).mp inferInstance d
89+
exact fun _ _ _ _ h ↦ (mono_iff_injective (σ.app d)).mp hmono_app h
90+
91+
/-- Single-cell horn attachment as a pushout for a monic classifier. If
92+
`σ : Δ[n + 1] ⟶ X` is monic with preimage of `A` equal to `Λ[n + 1, i]`, then
93+
`A ⊔ range σ` is the pushout of `Λ[n + 1, i] ↪ Δ[n + 1]` along the attaching
94+
map. -/
95+
lemma hornAttach_isPushout_of_mono {X : SSet.{u}} {n : ℕ} (i : Fin (n + 2))
96+
(A : X.Subcomplex) (σ : Δ[n + 1] ⟶ X) [Mono σ]
97+
(hhorn : A.preimage σ = (Λ[n + 1, i] : (Δ[n + 1] : SSet.{u}).Subcomplex)) :
98+
IsPushout (attachingMap A σ hhorn)
99+
(Λ[n + 1, i] : (Δ[n + 1] : SSet.{u}).Subcomplex).ι
100+
(homOfLE (show A ≤ A ⊔ range σ from le_sup_left))
101+
(lift σ (show range σ ≤ A ⊔ range σ from le_sup_right)) :=
102+
attachingMap_isPushout_of_injOn_compl A σ hhorn (injOn_compl_horn_of_mono σ i)
103+
104+
end Subcomplex
105+
end SSet

0 commit comments

Comments
 (0)