The smash product of pointed types

The smash product X ∧ Y of pointed types is the quotient of X × Y collapsing the wedge X × {y₀} ∪ {x₀} × Y to the basepoint. Pointed maps out of it are exactly functions of two variables sending the wedge to the basepoint. With unit S⁰ = PUnit₊ (Option PUnit pointed at none), the smash product makes Pointed a symmetric monoidal category, whose braiding swaps the two factors.

This is the levelwise input for the smash product of pointed simplicial sets, viewed as simplicial objects in Pointed.

Main definitions

• Pointed.smash X Y: the smash product, pointed at the collapsed wedge.
• Pointed.smash.mk x y: the class of a pair.
• Pointed.smash.lift: the pointed map induced by a function of two variables sending the wedge to the basepoint; Pointed.smash.hom_ext gives uniqueness.
• Pointed.smash.map: the smash product of two pointed maps.
• The instances MonoidalCategory Pointed and SymmetricCategory Pointed.

References

• A. Hatcher, Algebraic Topology, Chapter 0 (the smash product of pointed spaces).

def Pointed.smash (X Y : Pointed) : Pointed

The smash product X ∧ Y of pointed types: the quotient of X × Y collapsing the wedge X × {y₀} ∪ {x₀} × Y to a single point, which is the basepoint.

def Pointed.smash.mk {X Y : Pointed} (x : X.X) (y : Y.X) : (X.smash Y).X

The class of the pair (x, y) in the smash product.

theorem Pointed.smash.mk_surjective {X Y : Pointed} : Function.Surjective fun (p : X.X × Y.X) => mk p.1 p.2

theorem Pointed.smash.ind {X Y : Pointed} {motive : (X.smash Y).X → Prop} (h : ∀ (x : X.X) (y : Y.X), motive (mk x y)) (a : (X.smash Y).X) : motive a

Induction on the smash product: it suffices to treat the classes of pairs.

theorem Pointed.smash.point_def {X Y : Pointed} : (X.smash Y).point = mk X.point Y.point

theorem Pointed.smash.mk_eq_mk_iff {X Y : Pointed} {x x' : X.X} {y y' : Y.X} : mk x y = mk x' y' ↔ x = x' ∧ y = y' ∨ (x = X.point ∨ y = Y.point) ∧ (x' = X.point ∨ y' = Y.point)

Two pairs have the same class exactly when they are equal or both lie in the wedge.

@[simp]

theorem Pointed.smash.mk_eq_point_iff {X Y : Pointed} {x : X.X} {y : Y.X} : mk x y = (X.smash Y).point ↔ x = X.point ∨ y = Y.point

A pair represents the basepoint exactly when it lies in the wedge.

@[simp]

theorem Pointed.smash.mk_point_left {X Y : Pointed} (y : Y.X) : mk X.point y = (X.smash Y).point

@[simp]

theorem Pointed.smash.mk_point_right {X Y : Pointed} (x : X.X) : mk x Y.point = (X.smash Y).point

def Pointed.smash.lift {X Y Z : Pointed} (f : X.X → Y.X → Z.X) (hl : ∀ (y : Y.X), f X.point y = Z.point) (hr : ∀ (x : X.X), f x Y.point = Z.point) : X.smash Y ⟶ Z

The pointed map out of the smash product induced by a function of two variables sending the wedge to the basepoint.

@[simp]

theorem Pointed.smash.lift_mk {X Y Z : Pointed} (f : X.X → Y.X → Z.X) (hl : ∀ (y : Y.X), f X.point y = Z.point) (hr : ∀ (x : X.X), f x Y.point = Z.point) (x : X.X) (y : Y.X) : (lift f hl hr).toFun (mk x y) = f x y

theorem Pointed.smash.hom_ext {X Y Z : Pointed} {f g : X.smash Y ⟶ Z} (h : ∀ (x : X.X) (y : Y.X), f.toFun (mk x y) = g.toFun (mk x y)) : f = g

Pointed maps out of the smash product are determined by their values on pairs.

theorem Pointed.smash.hom_ext_iff {X Y Z : Pointed} {f g : X.smash Y ⟶ Z} : f = g ↔ ∀ (x : X.X) (y : Y.X), f.toFun (mk x y) = g.toFun (mk x y)

def Pointed.smash.map {X Y X' Y' : Pointed} (f : X ⟶ X') (g : Y ⟶ Y') : X.smash Y ⟶ X'.smash Y'

The smash product of two pointed maps.

@[simp]

theorem Pointed.smash.map_mk {X Y X' Y' : Pointed} (f : X ⟶ X') (g : Y ⟶ Y') (x : X.X) (y : Y.X) : (map f g).toFun (mk x y) = mk (f.toFun x) (g.toFun y)

def Pointed.smash.associator (X Y Z : Pointed) : (X.smash Y).smash Z ≅ X.smash (Y.smash Z)

The associativity isomorphism (X ∧ Y) ∧ Z ≅ X ∧ (Y ∧ Z).

def Pointed.smash.leftUnitor (X : Pointed) : (of none).smash X ≅ X

The left unit isomorphism S⁰ ∧ X ≅ X, where S⁰ = PUnit₊.

def Pointed.smash.rightUnitor (X : Pointed) : X.smash (of none) ≅ X

The right unit isomorphism X ∧ S⁰ ≅ X, where S⁰ = PUnit₊.

def Pointed.smash.braiding (X Y : Pointed) : X.smash Y ≅ Y.smash X

The isomorphism X ∧ Y ≅ Y ∧ X swapping the two factors.

@[instance_reducible]

instance Pointed.monoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct Pointed

The smash product, with unit the free pointed type S⁰ = PUnit₊ on one point.

theorem Pointed.tensorObj_def (X Y : Pointed) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = X.smash Y

theorem Pointed.tensorUnit_def : CategoryTheory.MonoidalCategoryStruct.tensorUnit Pointed = of none

@[simp]

theorem Pointed.tensorObj_point (X Y : Pointed) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).point = (X.smash Y).point

theorem Pointed.tensor_ext {X Y Z : Pointed} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z} (h : ∀ (x : X.X) (y : Y.X), f.toFun (smash.mk x y) = g.toFun (smash.mk x y)) : f = g

Pointed maps out of a tensor product are determined by their values on pairs.

theorem Pointed.tensor_ext_iff {X Y Z : Pointed} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z} : f = g ↔ ∀ (x : X.X) (y : Y.X), f.toFun (smash.mk x y) = g.toFun (smash.mk x y)

theorem Pointed.tensor_ext₃' {X Y Z W : Pointed} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ⟶ W} (h : ∀ (x : X.X) (y : Y.X) (z : Z.X), f.toFun (smash.mk (smash.mk x y) z) = g.toFun (smash.mk (smash.mk x y) z)) : f = g

Pointed maps out of (X ⊗ Y) ⊗ Z are determined by their values on triples.

theorem Pointed.tensor_ext₃ {X Y Z W : Pointed} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ W} (h : ∀ (x : X.X) (y : Y.X) (z : Z.X), f.toFun (smash.mk x (smash.mk y z)) = g.toFun (smash.mk x (smash.mk y z))) : f = g

Pointed maps out of X ⊗ (Y ⊗ Z) are determined by their values on triples.

@[simp]

theorem Pointed.tensorHom_mk {X Y X' Y' : Pointed} (f : X ⟶ X') (g : Y ⟶ Y') (x : X.X) (y : Y.X) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).toFun (smash.mk x y) = smash.mk (f.toFun x) (g.toFun y)

@[simp]

theorem Pointed.whiskerLeft_mk {X Y Y' : Pointed} (g : Y ⟶ Y') (x : X.X) (y : Y.X) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g).toFun (smash.mk x y) = smash.mk x (g.toFun y)

@[simp]

theorem Pointed.whiskerRight_mk {X Y X' : Pointed} (f : X ⟶ X') (x : X.X) (y : Y.X) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).toFun (smash.mk x y) = smash.mk (f.toFun x) y

@[simp]

theorem Pointed.associator_hom_mk {X Y Z : Pointed} (x : X.X) (y : Y.X) (z : Z.X) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.toFun (smash.mk (smash.mk x y) z) = smash.mk x (smash.mk y z)

@[simp]

theorem Pointed.associator_inv_mk {X Y Z : Pointed} (x : X.X) (y : Y.X) (z : Z.X) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.toFun (smash.mk x (smash.mk y z)) = smash.mk (smash.mk x y) z

@[simp]

theorem Pointed.leftUnitor_hom_mk {X : Pointed} (o : Option PUnit.{u + 1}) (x : X.X) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.toFun (smash.mk o x) = o.elim X.point fun (x_1 : PUnit.{u + 1}) => x

@[simp]

theorem Pointed.leftUnitor_inv_apply {X : Pointed} (x : X.X) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.toFun x = smash.mk (some PUnit.unit) x

@[simp]

theorem Pointed.rightUnitor_hom_mk {X : Pointed} (x : X.X) (o : Option PUnit.{u + 1}) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.toFun (smash.mk x o) = o.elim X.point fun (x_1 : PUnit.{u + 1}) => x

@[simp]

theorem Pointed.rightUnitor_inv_apply {X : Pointed} (x : X.X) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.toFun x = smash.mk x (some PUnit.unit)

@[instance_reducible]

instance Pointed.monoidalCategory : CategoryTheory.MonoidalCategory Pointed

The smash product makes Pointed a monoidal category.

@[instance_reducible]

instance Pointed.symmetricCategory : CategoryTheory.SymmetricCategory Pointed

The swap of factors makes the smash product symmetric monoidal.

@[simp]

theorem Pointed.braiding_hom_mk {X Y : Pointed} (x : X.X) (y : Y.X) : (β_ X Y).hom.toFun (smash.mk x y) = smash.mk y x

@[simp]

theorem Pointed.braiding_inv_mk {X Y : Pointed} (x : X.X) (y : Y.X) : (β_ X Y).inv.toFun (smash.mk y x) = smash.mk x y