Theorems · Definition · algebraic topology

SSet.prodStdSimplex.pairingCore.IsIndex

{m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) → {d : ℕ} → x.dim = d → Fin (d + 1) → Prop

Let x be a nondegenerate d-simplex of Δ[m + 1] ⊗ Δ[n] which does not belong to Λ[m + 1, k.castSucc].unionProd ∂Δ[n]. In particular, x induces a strictly monotone map from Fin (d + 1) to {0, ..., m + 1} × {0, ..., n}. We introduce a predicate on elements in Fin (d + 1) which shall be satisfied for l.succ (l : Fin d) if x l.castSucc = (k.castSucc, t) and x l.succ = (k.succ, t) for some t. The nondegenerate simplices x such that there exists such a l shall be the type (I) simplices of a pairing, and the corresponding type (II) simplex shall be obtained by deleting x l.castSucc.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Cited by

26 results in Mathlib

Foundations

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