Theorems · Inductive type · algebraic topology

SSet.PtSimplex.MulStruct

{X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} → X.PtSimplex n x → X.PtSimplex n x → X.PtSimplex n x → 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.)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Cited by

19 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound