Theorems · Definition · algebraic topology

SSet.StrictSegalCore.concat

{X : SSet} →
  {n : ℕ} →
    X.StrictSegalCore n →
      (x : X.obj (Opposite.op { len := 1 })) →
        (s : X.obj (Opposite.op { len := n })) →
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
              (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s →
            X.obj (Opposite.op { len := n + 1 })

Map which produces an n + 1-simplex from a 1-simplex and an n-simplex when the target vertex of the 1-simplex equals the zeroth simplex of the n-simplex.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Cited by

4 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound