Theorems · Definition · algebraic topology

SSet.prodStdSimplex.objEquiv

{p q n : ℕ} →
  (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }) ≃
    (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))

n-simplices in Δ[p] ⊗ Δ[q] identify to order preserving maps Fin (n + 1) →o Fin (p + 1) × Fin (q + 1).

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Cited by

21 results in Mathlib

Foundations

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