Strict Segal simplicial sets #
A simplicial set X
satisfies the StrictSegal
condition if for all n
, the map
X.spine n : X _⦋n⦌ → X.Path n
is an equivalence, with equivalence inverse
spineToSimplex {n : ℕ} : Path X n → X _⦋n⦌
.
Examples of StrictSegal
simplicial sets are given by nerves of categories.
TODO: Show that these are the only examples: that a StrictSegal
simplicial set is isomorphic to
the nerve of its homotopy category.
StrictSegal
simplicial sets have an important property of being 2-coskeletal which is proven
in Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
.
An n + 1
-truncated simplicial set satisfies the strict Segal condition if
its m
-simplices are uniquely determined by their spine for all m ≤ n + 1
.
- spineToSimplex (m : ℕ) (h : m ≤ n + 1 := by omega) : X.Path m → X.obj (Opposite.op { obj := SimplexCategory.mk m, property := h })
The inverse to
spine X m
. spineToSimplex
is a right inverse tospine X m
.spineToSimplex
is a left inverse tospine X m
.
Instances For
For an n + 1
-truncated simplicial set X
, IsStrictSegal X
asserts the
mere existence of an inverse to spine X m
for all m ≤ n + 1
.
Instances
Given IsStrictSegal X
, a choice of inverse to spine X m
for all
m ≤ n + 1
determines an inhabitant of StrictSegal X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The fields of StrictSegal
define an equivalence between X _⦋m⦌ₙ₊₁
and Path X m
.
Equations
- sx.spineEquiv m h = { toFun := X.spine m h, invFun := sx.spineToSimplex m h, left_inv := ⋯, right_inv := ⋯ }
Instances For
In the presence of the strict Segal condition, a path of length m
can be
"composed" by taking the diagonal edge of the resulting m
-simplex.
Equations
- sx.spineToDiagonal m h = X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.diag m) ⋯ h).op ∘ sx.spineToSimplex m h
Instances For
The unique existence of an inverse to spine X m
for all m ≤ n + 1
implies the mere existence of such an inverse.
For any σ : X ⟶ Y
between n + 1
-truncated StrictSegal
simplicial sets,
spineToSimplex
commutes with Path.map
.
If we take the path along the spine of the j
th face of a spineToSimplex
,
the common vertices will agree with those of the original path f
. In particular,
a vertex i
with i < j
can be identified with the same vertex in f
.
If we take the path along the spine of the j
th face of a spineToSimplex
,
a vertex i
with j ≤ i
can be identified with vertex i + 1
in the original
path.
If we take the path along the spine of the j
th face of a spineToSimplex
,
the common arrows will agree with those of the original path f
. In particular,
an arrow i
with i + 1 < j
can be identified with the same arrow in f
.
If we take the path along the spine of the j
th face of a spineToSimplex
,
an arrow i
with i + 1 > j
can be identified with arrow i + 1
in the
original path.
A simplicial set X
satisfies the strict Segal condition if its simplices
are uniquely determined by their spine.
- spineToSimplex {n : ℕ} : X.Path n → X.obj (Opposite.op (SimplexCategory.mk n))
The inverse to
spine X n
. spineToSimplex
is a right inverse tospine X n
.spineToSimplex
is a left inverse tospine X n
.
Instances For
For X
a simplicial set, IsStrictSegal X
asserts the mere existence of
an inverse to spine X n
for all n : ℕ
.
- segal (n : ℕ) : Function.Bijective (X.spine n)
Instances
Given IsStrictSegal X
, a choice of inverse to spine X n
for all n : ℕ
determines an inhabitant of StrictSegal X
.
Equations
- SSet.StrictSegal.ofIsStrictSegal X = { spineToSimplex := fun {n : ℕ} => (Equiv.ofBijective (X.spine n) ⋯).invFun, spine_spineToSimplex := ⋯, spineToSimplex_spine := ⋯ }
Instances For
A StrictSegal
structure on a simplicial set X
restricts to a
Truncated.StrictSegal
structure on the n + 1
-truncation of X
.
Equations
- sx.truncation n = { spineToSimplex := fun (x : ℕ) (x_1 : autoParam (x ≤ n + 1) _auto✝) => sx.spineToSimplex, spine_spineToSimplex := ⋯, spineToSimplex_spine := ⋯ }
Instances For
The fields of StrictSegal
define an equivalence between X _⦋n⦌
and Path X n
.
Equations
- sx.spineEquiv n = { toFun := X.spine n, invFun := sx.spineToSimplex, left_inv := ⋯, right_inv := ⋯ }
Instances For
The unique existence of an inverse to spine X n
forall n : ℕ
implies
the mere existence of such an inverse.
In the presence of the strict Segal condition, a path of length n
can be
"composed" by taking the diagonal edge of the resulting n
-simplex.
Equations
Instances For
For any σ : X ⟶ Y
between StrictSegal
simplicial sets, spineToSimplex
commutes with Path.map
.
If we take the path along the spine of the j
th face of a spineToSimplex
,
the common vertices will agree with those of the original path f
. In particular,
a vertex i
with i < j
can be identified with the same vertex in f
.
If we take the path along the spine of the j
th face of a spineToSimplex
,
a vertex i
with i ≥ j
can be identified with vertex i + 1
in the original
path.
If we take the path along the spine of the j
th face of a spineToSimplex
,
the common arrows will agree with those of the original path f
. In particular,
an arrow i
with i + 1 < j
can be identified with the same arrow in f
.
If we take the path along the spine of the j
th face of a spineToSimplex
,
an arrow i
with i + 1 > j
can be identified with arrow i + 1
in the
original path.
If we take the path along the spine of a face of a spineToSimplex
, the
arrows not contained in the original path can be recovered as the diagonal edge
of the spineToSimplex
that "composes" arrows i
and i + 1
.
Simplices in the nerve of categories are uniquely determined by their spine. Indeed, this property describes the essential image of the nerve functor.
Equations
- One or more equations did not get rendered due to their size.