Theorems · Theorem · algebraic topology

SSet.Subcomplex.ofSimplexProd_eq_range

∀ {X₁ X₂ : SSet} {p q : ℕ} (x₁ : X₁.obj (Opposite.op { len := p })) (x₂ : X₂.obj (Opposite.op { len := q })),
  (SSet.Subcomplex.ofSimplex x₁).prod (SSet.Subcomplex.ofSimplex x₂) =
    SSet.Subcomplex.range
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.yonedaEquiv.symm x₁) (SSet.yonedaEquiv.symm x₂))

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd

Cited by

1 results in Mathlib

Foundations

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