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.

@[reducible, inline]

abbrev SSet.PtSimplex (X : SSet) (n : ℕ) (x : X.obj (Opposite.op { len := 0 })) : Type u

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, ⋯⟩)

theorem SSet.PtSimplex.comp_map_eq_const {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet} (φ : Y ⟶ stdSimplex.obj { len := n }) [Y.HasDimensionLT n] : CategoryTheory.CategoryStruct.comp φ s.map = const x

theorem SSet.PtSimplex.comp_map_eq_const_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (s : X.PtSimplex n x) {Y : SSet} (φ : Y ⟶ stdSimplex.obj { len := n }) [Y.HasDimensionLT n] {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp s.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.δ_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex (n + 1) x) (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i) f.map = const x

@[simp]

theorem SSet.PtSimplex.δ_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex (n + 1) x) (i : Fin (n + 2)) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i) (CategoryTheory.CategoryStruct.comp f.map h) = CategoryTheory.CategoryStruct.comp (const x) h

def SSet.PtSimplex.opEquiv {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} : X.op.PtSimplex n (opObjEquiv.symm x) ≃ X.PtSimplex n x

The bijection between n-simplices of X.op and of X that are constant on the boundary.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.opEquiv_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.op.PtSimplex n (opObjEquiv.symm x)) : (opEquiv f).map = yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map))

@[simp]

theorem SSet.PtSimplex.opEquiv_symm_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (g : X.PtSimplex n x) : (opEquiv.symm g).map = yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map))

@[reducible, inline]

abbrev SSet.PtSimplex.op {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) : X.op.PtSimplex n (opObjEquiv.symm x)

Given a n-simplex of X that is constant on the boundary, this is the corresponding n-simplex of X.op.

Equations

• f.op = SSet.PtSimplex.opEquiv.symm f

@[reducible, inline]

abbrev SSet.PtSimplex.unop {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.op.PtSimplex n (opObjEquiv.symm x)) : X.PtSimplex n x

Given a n-simplex of X.op that is constant on the boundary, this is the corresponding n-simplex of X.

Equations

• f.unop = SSet.PtSimplex.opEquiv f

structure SSet.PtSimplex.RelStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f g : X.PtSimplex n x) (i : Fin (n + 1)) : Type u

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.

• map : stdSimplex.obj { len := n + 1 } ⟶ X

  A n + 1-simplex

• δ_castSucc_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc) self.map = f.map
• δ_succ_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ) self.map = g.map
• δ_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

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_map_of_gt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) (j : Fin (n + 2)) (hj : i.succ < j) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_map_of_lt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) (j : Fin (n + 2)) (hj : j < i.castSucc) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_succ_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp g.map h

@[simp]

theorem SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (self : f.RelStruct g i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp f.map h

def SSet.PtSimplex.RelStruct.refl {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin (n + 1)) : f.RelStruct f i

RelStruct is reflexive.

Equations

• SSet.PtSimplex.RelStruct.refl f i = { map := CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i) f.map, δ_castSucc_map := ⋯, δ_succ_map := ⋯, δ_map_of_lt := ⋯, δ_map_of_gt := ⋯ }

@[simp]

theorem SSet.PtSimplex.RelStruct.refl_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin (n + 1)) : (refl f i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i) f.map

def SSet.PtSimplex.RelStruct.copy {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (r : f.RelStruct g i) {f' g' : X.PtSimplex n x} (hf : f = f') (hg : g = g') : f'.RelStruct g' i

The RelStruct f' g' i deduced from r : RelStruct f g i when f = f' and g = g'.

Equations

• r.copy hf hg = { map := r.map, δ_castSucc_map := ⋯, δ_succ_map := ⋯, δ_map_of_lt := ⋯, δ_map_of_gt := ⋯ }

@[simp]

theorem SSet.PtSimplex.RelStruct.copy_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)} (r : f.RelStruct g i) {f' g' : X.PtSimplex n x} (hf : f = f') (hg : g = g') : (r.copy hf hg).map = r.map

def SSet.PtSimplex.RelStruct.ofEq {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} (h : f = g) (i : Fin (n + 1)) : f.RelStruct g i

The RelStruct f g i deduced from an equality f = g.

Equations

• SSet.PtSimplex.RelStruct.ofEq h i = (SSet.PtSimplex.RelStruct.refl f i).copy ⋯ h

@[simp]

theorem SSet.PtSimplex.RelStruct.ofEq_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} (h : f = g) (i : Fin (n + 1)) : (ofEq h i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i) f.map

structure SSet.PtSimplex.MulStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f g fg : X.PtSimplex n x) (i : Fin n) : Type u

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.)

• map : stdSimplex.obj { len := n + 1 } ⟶ X

  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
• δ_succ_succ_map : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ.succ) self.map = f.map
• δ_map_of_lt (j : Fin (n + 2)) (hj : j < i.castSucc.castSucc) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x
• δ_map_of_gt (j : Fin (n + 2)) (hj : i.succ.succ < j) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) self.map = const x

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.castSucc) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp g.map h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_map_of_lt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) (j : Fin (n + 2)) (hj : j < i.castSucc.castSucc) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_map_of_gt_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) (j : Fin (n + 2)) (hj : i.succ.succ < j) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp (const x) h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.succ.succ) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp f.map h

@[simp]

theorem SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.δ i.castSucc.succ) (CategoryTheory.CategoryStruct.comp self.map h) = CategoryTheory.CategoryStruct.comp fg.map h

def SSet.PtSimplex.MulStruct.op {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : f.MulStruct g fg i) {j : Fin n} (hij : i.rev = j := by grind) : g.op.MulStruct f.op fg.op j

The MulStruct for X.op that is deduced from a MulStruct for the simplicial set X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.MulStruct.op_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : f.MulStruct g fg i) {j : Fin n} (hij : i.rev = j := by grind) : (h.op hij).map = yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map))

def SSet.PtSimplex.MulStruct.unop {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : g.op.MulStruct f.op fg.op i) {j : Fin n} (hij : i.rev = j := by grind) : f.MulStruct g fg j

The Mulstruct for a simplicial set X that is deduced from a Mulstruct for X.op.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.MulStruct.unop_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n} (h : g.op.MulStruct f.op fg.op i) {j : Fin n} (hij : i.rev = j := by grind) : (h.unop hij).map = yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map))

def SSet.PtSimplex.relStructCastSuccEquivMulStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} : f.RelStruct g i.castSucc ≃ MulStruct RelativeMorphism.const f g i

If f and g are in X.PtSimplex n x, then RelStruct f g i.castSucc identifies to MulStruct .const f g i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.relStructCastSuccEquivMulStruct_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : f.RelStruct g i.castSucc) : (relStructCastSuccEquivMulStruct h).map = h.map

@[simp]

theorem SSet.PtSimplex.relStructCastSuccEquivMulStruct_symm_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : MulStruct RelativeMorphism.const f g i) : (relStructCastSuccEquivMulStruct.symm h).map = h.map

def SSet.PtSimplex.relStructSuccEquivMulStruct {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} : f.RelStruct g i.succ ≃ g.MulStruct RelativeMorphism.const f i

If f and g are in X.PtSimplex n x, then RelStruct f g i.succ identifies to MulStruct g .const f i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SSet.PtSimplex.relStructSuccEquivMulStruct_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : f.RelStruct g i.succ) : (relStructSuccEquivMulStruct h).map = h.map

@[simp]

theorem SSet.PtSimplex.relStructSuccEquivMulStruct_symm_apply_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n} (h : g.MulStruct RelativeMorphism.const f i) : (relStructSuccEquivMulStruct.symm h).map = h.map

def SSet.PtSimplex.MulStruct.oneMul {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : MulStruct RelativeMorphism.const f f i

Given f : X.PtSimplex n x and i : Fin n (note that this implies n ≠ 0), this is the term in MulStruct .const f f i corresponding to stdSimplex.σ i.castSucc ≫ f.map.

Equations

• SSet.PtSimplex.MulStruct.oneMul f i = SSet.PtSimplex.relStructCastSuccEquivMulStruct (SSet.PtSimplex.RelStruct.refl f i.castSucc)

@[simp]

theorem SSet.PtSimplex.MulStruct.oneMul_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : (oneMul f i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i.castSucc) f.map

def SSet.PtSimplex.MulStruct.mulOne {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : f.MulStruct RelativeMorphism.const f i

Given f : X.PtSimplex n x and i : Fin n (note that this implies n ≠ 0), this is the term in MulStruct f .const f i corresponding to stdSimplex.σ i.succ ≫ f.map.

Equations

• SSet.PtSimplex.MulStruct.mulOne f i = SSet.PtSimplex.relStructSuccEquivMulStruct (SSet.PtSimplex.RelStruct.refl f i.succ)

@[simp]

theorem SSet.PtSimplex.MulStruct.mulOne_map {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} (f : X.PtSimplex n x) (i : Fin n) : (mulOne f i).map = CategoryTheory.CategoryStruct.comp (stdSimplex.σ i.succ) f.map