Skip to content

Commit c4848a1

Browse files
joelrioujoelriou
committed
feat(AlgebraicTopology): Edge and CompStruct for simplicial sets (#31265)
The API for `2`-truncated simplicial sets #31254 is reproduced for simplicial sets. The definitions for simplicial sets are defeq to their `2`-truncated counterparts, but an effort is made to contain abuse of defeq...
1 parent 108a53e commit c4848a1

File tree

3 files changed

+187
-1
lines changed

3 files changed

+187
-1
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1390,6 +1390,7 @@ import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
13901390
import Mathlib.AlgebraicTopology.SimplicialSet.Basic
13911391
import Mathlib.AlgebraicTopology.SimplicialSet.Boundary
13921392
import Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
1393+
import Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
13931394
import Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
13941395
import Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
13951396
import Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

‎Mathlib/AlgebraicTopology/SimplicialSet/CompStruct.lean‎

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
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.CompStructTruncated
7+
8+
/-!
9+
# Edges and "triangles" in simplicial sets
10+
11+
Given a simplicial set `X`, we introduce two types:
12+
* Given `0`-simplices `x₀` and `x₁`, we define `Edge x₀ x₁`
13+
which is the type of `1`-simplices with faces `x₁` and `x₀` respectively;
14+
* Given `0`-simplices `x₀`, `x₁`, `x₂`, edges `e₀₁ : Edge x₀ x₁`, `e₁₂ : Edge x₁ x₂`,
15+
`e₀₂ : Edge x₀ x₂`, a structure `CompStruct e₀₁ e₁₂ e₀₂` which records the
16+
data of a `2`-simplex with faces `e₁₂`, `e₀₂` and `e₀₁` respectively. This data
17+
will allow to obtain relations in the homotopy category of `X`.
18+
(This API parallels similar definitions for `2`-truncated simplicial sets.
19+
The definitions in this file are definitionally equal to their `2`-truncated
20+
counterparts.)
21+
22+
-/
23+
24+
universe v u
25+
26+
open CategoryTheory Simplicial
27+
28+
namespace SSet
29+
30+
variable {X Y : SSet.{u}} {x₀ x₁ x₂ : X _⦋0⦌}
31+
32+
variable (x₀ x₁) in
33+
/-- In a simplicial set, an edge from a vertex `x₀` to `x₁` is
34+
a `1`-simplex with prescribed `0`-dimensional faces. -/
35+
def Edge := ((truncation 2).obj X).Edge x₀ x₁
36+
37+
namespace Edge
38+
39+
/-- Constructor for `SSet.Edge` which takes as an input a term in the definitionally
40+
equal type `SSet.Truncated.Edge` for the `2`-truncation of the simplicial set.
41+
(This definition is made to contain abuse of defeq in other definitions.) -/
42+
def ofTruncated (e : ((truncation 2).obj X).Edge x₀ x₁) :
43+
Edge x₀ x₁ := e
44+
45+
/-- The edge of the `2`-truncation of a simplicial set `X` that is induced
46+
by an edge of `X`. -/
47+
def toTruncated (e : Edge x₀ x₁) :
48+
((truncation 2).obj X).Edge x₀ x₁ :=
49+
e
50+
51+
/-- In a simplicial set, an edge from a vertex `x₀` to `x₁` is
52+
a `1`-simplex with prescribed `0`-dimensional faces. -/
53+
def edge (e : Edge x₀ x₁) : X _⦋1⦌ := e.toTruncated.edge
54+
55+
@[simp]
56+
lemma ofTruncated_edge (e : ((truncation 2).obj X).Edge x₀ x₁) :
57+
(ofTruncated e).edge = e.edge := rfl
58+
59+
@[simp]
60+
lemma toTruncated_edge (e : Edge x₀ x₁) :
61+
(toTruncated e).edge = e.edge := rfl
62+
63+
@[simp]
64+
lemma src_eq (e : Edge x₀ x₁) : X.δ 1 e.edge = x₀ := Truncated.Edge.src_eq e
65+
66+
@[simp]
67+
lemma tgt_eq (e : Edge x₀ x₁) : X.δ 0 e.edge = x₁ := Truncated.Edge.tgt_eq e
68+
69+
@[ext]
70+
lemma ext {e e' : Edge x₀ x₁} (h : e.edge = e'.edge) :
71+
e = e' := Truncated.Edge.ext h
72+
73+
variable (x₀) in
74+
/-- The constant edge on a `0`-simplex. -/
75+
def id : Edge x₀ x₀ := ofTruncated (.id _)
76+
77+
variable (x₀) in
78+
@[simp]
79+
lemma id_edge : (id x₀).edge = X.σ 0 x₀ := rfl
80+
81+
/-- The image of an edge by a morphism of simplicial sets. -/
82+
def map (e : Edge x₀ x₁) (f : X ⟶ Y) : Edge (f.app _ x₀) (f.app _ x₁) :=
83+
ofTruncated (e.toTruncated.map ((truncation 2).map f))
84+
85+
variable (x₀) in
86+
@[simp]
87+
lemma map_id (f : X ⟶ Y) :
88+
(Edge.id x₀).map f = Edge.id (f.app _ x₀) :=
89+
Truncated.Edge.map_id _ _
90+
91+
/-- The edge given by a `1`-simplex. -/
92+
def mk' (s : X _⦋1⦌) : Edge (X.δ 1 s) (X.δ 0 s) :=
93+
.ofTruncated (Truncated.Edge.mk' (X := (truncation 2).obj X) s)
94+
95+
@[simp]
96+
lemma mk'_edge (s : X _⦋1⦌) : (mk' s).edge = s := rfl
97+
98+
lemma exists_of_simplex (s : X _⦋1⦌) :
99+
∃ (x₀ x₁ : X _⦋0⦌) (e : Edge x₀ x₁), e.edge = s :=
100+
⟨_, _, mk' s, rfl⟩
101+
102+
/-- Let `x₀`, `x₁`, `x₂` be `0`-simplices of a simplicial set `X`,
103+
`e₀₁` an edge from `x₀` to `x₁`, `e₁₂` an edge from `x₁` to `x₂`,
104+
`e₀₂` an edge from `x₀` to `x₂`. This is the data of a `2`-simplex whose
105+
faces are respectively `e₀₂`, `e₁₂` and `e₀₁`. Such structures shall provide
106+
relations in the homotopy category of arbitrary simplicial sets
107+
(and specialized constructions for quasicategories and Kan complexes.). -/
108+
def CompStruct (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) :=
109+
Truncated.Edge.CompStruct e₀₁.toTruncated e₁₂.toTruncated e₀₂.toTruncated
110+
111+
namespace CompStruct
112+
113+
variable {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂}
114+
115+
/-- Constructor for `SSet.Edge.CompStruct` which takes as an input a term in the
116+
definitionally equal type `SSet.Truncated.Edge.CompStruct` for the `2`-truncation of
117+
the simplicial set. (This definition is made to contain abuse of defeq in
118+
other definitions.) -/
119+
def ofTruncated (h : Truncated.Edge.CompStruct e₀₁.toTruncated e₁₂.toTruncated e₀₂.toTruncated) :
120+
CompStruct e₀₁ e₁₂ e₀₂ := h
121+
122+
/-- Conversion from `SSet.Edge.CompStruct` to `SSet.Truncated.Edge.CompStruct`. -/
123+
def toTruncated (h : CompStruct e₀₁ e₁₂ e₀₂) :
124+
Truncated.Edge.CompStruct e₀₁.toTruncated e₁₂.toTruncated e₀₂.toTruncated :=
125+
h
126+
127+
/-- The underlying `2`-simplex in a structure `SSet.Edge.CompStruct`. -/
128+
def simplex (h : CompStruct e₀₁ e₁₂ e₀₂) : X _⦋2⦌ :=
129+
h.toTruncated.simplex
130+
131+
section
132+
133+
variable (simplex : X _⦋2⦌)
134+
(d₂ : X.δ 2 simplex = e₀₁.edge := by cat_disch)
135+
(d₀ : X.δ 0 simplex = e₁₂.edge := by cat_disch)
136+
(d₁ : X.δ 1 simplex = e₀₂.edge := by cat_disch)
137+
138+
/-- Constructor for `SSet.Edge.CompStruct`. -/
139+
def mk : CompStruct e₀₁ e₁₂ e₀₂ where
140+
simplex := simplex
141+
142+
@[simp]
143+
lemma mk_simplex : (mk simplex).simplex = simplex := rfl
144+
145+
end
146+
147+
@[ext]
148+
lemma ext {h h' : CompStruct e₀₁ e₁₂ e₀₂} (eq : h.simplex = h'.simplex) :
149+
h = h' :=
150+
Truncated.Edge.CompStruct.ext eq
151+
152+
lemma exists_of_simplex (s : X _⦋2⦌) :
153+
∃ (x₀ x₁ x₂ : X _⦋0⦌) (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂)
154+
(e₀₂ : Edge x₀ x₂) (h : CompStruct e₀₁ e₁₂ e₀₂), h.simplex = s :=
155+
Truncated.Edge.CompStruct.exists_of_simplex (X := (truncation 2).obj X) s
156+
157+
/-- `e : Edge x₀ x₁` is a composition of `Edge.id x₀` with `e`. -/
158+
def idComp (e : Edge x₀ x₁) : CompStruct (.id x₀) e e :=
159+
ofTruncated (.idComp _)
160+
161+
@[simp]
162+
lemma idComp_simplex (e : Edge x₀ x₁) : (idComp e).simplex = X.σ 0 e.edge := rfl
163+
164+
/-- `e : Edge x₀ x₁` is a composition of `e` with `Edge.id x₁` -/
165+
def compId (e : Edge x₀ x₁) : CompStruct e (.id x₁) e :=
166+
ofTruncated (.compId _)
167+
168+
@[simp]
169+
lemma compId_simplex (e : Edge x₀ x₁) : (compId e).simplex = X.σ 1 e.edge := rfl
170+
171+
/-- The image of a `Edge.CompStruct` by a morphism of simplicial sets. -/
172+
def map (h : CompStruct e₀₁ e₁₂ e₀₂) (f : X ⟶ Y) :
173+
CompStruct (e₀₁.map f) (e₁₂.map f) (e₀₂.map f) :=
174+
.ofTruncated (h.toTruncated.map ((truncation 2).map f))
175+
176+
@[simp]
177+
lemma map_simplex (h : CompStruct e₀₁ e₁₂ e₀₂) (f : X ⟶ Y) :
178+
(h.map f).simplex = f.app _ h.simplex := rfl
179+
180+
end CompStruct
181+
182+
end Edge
183+
184+
end SSet

‎Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ lemma map_id (x : X _⦋0⦌₂) (f : X ⟶ Y) :
7979
faces are respectively `e₀₂`, `e₁₂` and `e₀₁`. Such structures shall provide
8080
relations in the homotopy category of arbitrary (truncated) simplicial sets
8181
(and specialized constructions for quasicategories and Kan complexes.). -/
82+
@[ext]
8283
structure CompStruct {x₀ x₁ x₂ : X _⦋0⦌₂}
8384
(e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) where
8485
/-- A `2`-simplex with prescribed `1`-dimensional faces -/
@@ -117,7 +118,7 @@ def idComp {x y : X _⦋0⦌₂} (e : Edge x y) :
117118
rw [← FunctorToTypes.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_zero]
118119
simp
119120

120-
/-- `e : Edge x y` is a composition of `Edge.id y` with `e`. -/
121+
/-- `e : Edge x y` is a composition of `e` with `Edge.id y`. -/
121122
def compId {x y : X _⦋0⦌₂} (e : Edge x y) :
122123
CompStruct e (.id y) e where
123124
simplex := X.map (σ₂ 1).op e.edge

0 commit comments

Comments
 (0)