Binary product of standard simplices

In this file, we show that Δ[p] ⊗ Δ[q] identifies to the nerve of ULift (Fin (p + 1) × Fin (q + 1)). We relate the n-simplices of Δ[p] ⊗ Δ[q] to order preserving maps Fin (n + 1) →o Fin (p + 1) × Fin (q + 1), Via this bijection, a simplex in Δ[p] ⊗ Δ[q] is nondegenerate iff the corresponding monotone map Fin (n + 1) →o Fin (p + 1) × Fin (q + 1) is injective (or a strict mono).

We also show that the dimension of Δ[p] ⊗ Δ[q] is ≤ p + q.

def SSet.prodStdSimplex.objEquiv {p q n : ℕ} : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk 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).

@[simp]

theorem SSet.prodStdSimplex.objEquiv_apply_fst {p q n : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) (i : Fin (n + 1)) : ((objEquiv x) i).1 = x.1 i

@[simp]

theorem SSet.prodStdSimplex.objEquiv_apply_snd {p q n : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) (i : Fin (n + 1)) : ((objEquiv x) i).2 = x.2 i

theorem SSet.prodStdSimplex.objEquiv_naturality {p q m n : ℕ} (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) : (objEquiv z).comp (SimplexCategory.Hom.toOrderHom f) = objEquiv ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).map f.op z)

theorem SSet.prodStdSimplex.objEquiv_map_apply {p q n m : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) (f : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (i : Fin (m + 1)) : (objEquiv ((CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).map f.op x)) i = (objEquiv x) ((SimplexCategory.Hom.toOrderHom f) i)

theorem SSet.prodStdSimplex.objEquiv_δ_apply {p q n : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk (n + 1)))) (i : Fin (n + 2)) (j : Fin (n + 1)) : (objEquiv (CategoryTheory.SimplicialObject.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))) i x)) j = (objEquiv x) (i.succAbove j)

def SSet.prodStdSimplex.isoNerve (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q)) ≅ CategoryTheory.nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))

The binary product Δ[p] ⊗ Δ[q] identifies to the nerve of ULift (Fin (p + 1) × Fin (q + 1)).

theorem SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv {p q n : ℕ} (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) : z ∈ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).nonDegenerate n ↔ Function.Injective ⇑(objEquiv z)

theorem SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv {p q n : ℕ} (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) : z ∈ (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).nonDegenerate n ↔ StrictMono ⇑(objEquiv z)

def SSet.prodStdSimplex.orderHomOfSimplex {p q n : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) {m : ℕ} (hm : p + q = m) : Fin (n + 1) →o Fin (m + 1)

Given a n-simplex x in Δ[p] ⊗ Δ[q], this is the order preserving map Fin (n + 1) →o Fin (m + 1) (with p + q = m) which corresponds to the sum of the two components of objEquiv x : Fin (n + 1) →o Fin (p + 1) × Fin (q + 1).

@[simp]

theorem SSet.prodStdSimplex.orderHomOfSimplex_coe {p q n : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) {m : ℕ} (hm : p + q = m) (i : Fin (n + 1)) : (orderHomOfSimplex x hm) i = ⟨↑(x.1 i) + ↑(x.2 i), ⋯⟩

theorem SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff {p q n : ℕ} (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).obj (Opposite.op (SimplexCategory.mk n))) {m : ℕ} (hm : p + q = m) : StrictMono ⇑(orderHomOfSimplex x hm) ↔ StrictMono ⇑(objEquiv x)

instance SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat {p q : ℕ} : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).HasDimensionLE (p + q)

instance SSet.prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk {p q : ℕ} : (CategoryTheory.MonoidalCategoryStruct.tensorObj (stdSimplex.obj (SimplexCategory.mk p)) (stdSimplex.obj (SimplexCategory.mk q))).Finite