Pointed simplices #
Given a simplicial set X, n : ℕ and x : X _⦋0⦌, we introduce the
type X.PtSimplex n x of morphisms Δ[n] ⟶ X which send ∂Δ[n] to x.
We introduce structures PtSimplex.RelStruct and PtSimplex.MulStruct
which will be used in the definition of homotopy groups of Kan complexes.
Given a simplicial set X, n : ℕ and x : X _⦋0⦌, this is the type
of morphisms Δ[n] ⟶ X which are constant with value x on the boundary.
Equations
- X.PtSimplex n x = SSet.RelativeMorphism (SSet.boundary n) (SSet.Subcomplex.ofSimplex x) (SSet.const ⟨x, ⋯⟩)
Instances For
For each i : Fin (n + 1), this is a variant of the homotopy relation on
n-simplices that are constant on the boundary. Simplices f and g are related
if they appear respectively as the i.castSucc and i.succ faces of a
n + 1-simplex such that all the other faces are constant.
A
n + 1-simplex- δ_map_of_lt (j : Fin (n + 2)) (hj : j < i.castSucc) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x
- δ_map_of_gt (j : Fin (n + 2)) (hj : i.succ < j) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x
Instances For
For each i : Fin n, this structure is a candidate for the relation saying
that fg is the product of f and g in the homotopy group (of a Kan complex).
It is so if g, fg and f are respectively the i.castSucc.castSucc,
i.castSucc.succ and i.succ.succ faces of a n + 1-simplex such that
all the other faces are constant. (The multiplication on homotopy groups will be
defined using i := Fin.last _, but in general, this structure is useful in
order to obtain properties of RelStruct.)
A
n + 1-simplex- δ_castSucc_castSucc_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.castSucc) self.map = g.map
- δ_succ_castSucc_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.succ) self.map = fg.map