The homotopy category functor is monoidal

Given 2-truncated simplicial sets X and Y, we introduce ad operation Truncated.Edge.tensor : Edge x x' → Edge y y' → Edge (x, y) (x', y'). We shall use this in order to construct an equivalence of categories (X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory (TODO @joelriou).

def SSet.Truncated.Edge.tensor {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : Edge (x, y) (x', y')

The external product of edges of 2-truncated simplicial sets.

Equations

• e₁.tensor e₂ = { edge := (e₁.edge, e₂.edge), src_eq := ⋯, tgt_eq := ⋯ }

@[simp]

theorem SSet.Truncated.Edge.tensor_edge {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : (e₁.tensor e₂).edge = (e₁.edge, e₂.edge)

theorem SSet.Truncated.Edge.tensor_surjective {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e : Edge (x, y) (x', y')) : ∃ (e₁ : Edge x x') (e₂ : Edge y y'), e₁.tensor e₂ = e

@[simp]

theorem SSet.Truncated.Edge.id_tensor_id {X Y : Truncated 2} (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })) (y : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })) : (id x).tensor (id y) = id (x, y)

@[simp]

theorem SSet.Truncated.Edge.map_tensorHom {X Y X' Y' : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') (f : X ⟶ X') (g : Y ⟶ Y') : (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = (e₁.map f).tensor (e₂.map g)

@[simp]

theorem SSet.Truncated.Edge.map_whiskerRight {X Y X' : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') (f : X ⟶ X') : (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) = (e₁.map f).tensor e₂

@[simp]

theorem SSet.Truncated.Edge.map_whiskerLeft {X Y Y' : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') (g : Y ⟶ Y') : (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) = e₁.tensor (e₂.map g)

@[simp]

theorem SSet.Truncated.Edge.map_associator_hom {X Y Z : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') {z z' : Z.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₃ : Edge z z') : ((e₁.tensor e₂).tensor e₃).map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = e₁.tensor (e₂.tensor e₃)

@[simp]

theorem SSet.Truncated.Edge.map_fst {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : (e₁.tensor e₂).map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) = e₁

@[simp]

theorem SSet.Truncated.Edge.map_snd {X Y : Truncated 2} {x x' : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₁ : Edge x x') {y y' : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := tensor._proof_1 })} (e₂ : Edge y y') : (e₁.tensor e₂).map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) = e₂

def SSet.Truncated.Edge.CompStruct.tensor {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (hx : e₀₁.CompStruct e₁₂ e₀₂) {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e'₀₁ : Edge y₀ y₁} {e'₁₂ : Edge y₁ y₂} {e'₀₂ : Edge y₀ y₂} (hy : e'₀₁.CompStruct e'₁₂ e'₀₂) : (e₀₁.tensor e'₀₁).CompStruct (e₁₂.tensor e'₁₂) (e₀₂.tensor e'₀₂)

The external product of CompStruct between edges of 2-truncated simplicial sets.

Equations

• hx.tensor hy = { simplex := (hx.simplex, hy.simplex), d₂ := ⋯, d₀ := ⋯, d₁ := ⋯ }

@[simp]

theorem SSet.Truncated.Edge.CompStruct.tensor_simplex_fst {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (hx : e₀₁.CompStruct e₁₂ e₀₂) {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e'₀₁ : Edge y₀ y₁} {e'₁₂ : Edge y₁ y₂} {e'₀₂ : Edge y₀ y₂} (hy : e'₀₁.CompStruct e'₁₂ e'₀₂) : (hx.tensor hy).simplex.1 = hx.simplex

@[simp]

theorem SSet.Truncated.Edge.CompStruct.tensor_simplex_snd {X Y : Truncated 2} {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₀₂ : Edge x₀ x₂} (hx : e₀₁.CompStruct e₁₂ e₀₂) {y₀ y₁ y₂ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} {e'₀₁ : Edge y₀ y₁} {e'₁₂ : Edge y₁ y₂} {e'₀₂ : Edge y₀ y₂} (hy : e'₀₁.CompStruct e'₁₂ e'₀₂) : (hx.tensor hy).simplex.2 = hy.simplex

instance SSet.Truncated.HomotopyCategory.instUniqueObjOppositeTruncatedTensorUnit {n : ℕ} (d : (SimplexCategory.Truncated n)ᵒᵖ) : Unique ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (Truncated n)).obj d)

Equations

• SSet.Truncated.HomotopyCategory.instUniqueObjOppositeTruncatedTensorUnit d = inferInstanceAs (Unique PUnit.{?u.13 + 1})

def SSet.Truncated.HomotopyCategory.isoTerminal (X : Truncated 2) [Unique (X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := isoTerminal._proof_1 }))] : CategoryTheory.Cat.of X.HomotopyCategory ≅ CategoryTheory.Cat.chosenTerminal

If X : Truncated 2 has a unique 0-simplex and (at most) one 1-simplex, this is the isomorphism Cat.of X.HomotopyCategory ≅ Cat.chosenTerminal in Cat.

Equations

• SSet.Truncated.HomotopyCategory.isoTerminal X = (SSet.Truncated.HomotopyCategory.isTerminal X).uniqueUpToIso CategoryTheory.Cat.chosenTerminalIsTerminal

theorem SSet.Truncated.HomotopyCategory.square {X Y : Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (ex : Edge x₀ x₁) {y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := Edge.tensor._proof_1 })} (ey : Edge y₀ y₁) : CategoryTheory.CategoryStruct.comp (homMk (ex.tensor (Edge.id y₀))) (homMk ((Edge.id x₁).tensor ey)) = CategoryTheory.CategoryStruct.comp (homMk ((Edge.id x₀).tensor ey)) (homMk (ex.tensor (Edge.id y₁)))