Smash powers of pointed types

The smash power X^∧ι of a pointed type X, indexed by a type ι, is the quotient of the product ι → X collapsing the fat wedge (the families with some coordinate at the basepoint) to the basepoint, with a basepoint adjoined disjointly when ι is empty. We use the model whose elements are the basepoint and the families avoiding the basepoint in every coordinate; the class of an arbitrary family is Pointed.smashPow.mk. In particular X^∧∅ = S⁰ has exactly two elements, while for nonempty ι every element is the class of a family.

The smash power is functorial in pointed maps of X, acts on bijections of the index type by reindexing coordinates, and concatenation of families sends X^∧ι and X^∧κ to X^∧(ι ⊕ κ). These are the levelwise inputs for the smash powers of pointed simplicial sets, which form the sphere sequence underlying symmetric spectra.

Main definitions

• Pointed.smashPow X ι: the smash power X^∧ι.
• Pointed.smashPow.mk f: the class of a family f : ι → X.
• Pointed.smashPow.lift: the pointed map induced by a function of families sending the fat wedge to the basepoint; Pointed.smashPow.hom_ext gives uniqueness.
• Pointed.smashPow.map: the smash power of a pointed map, and Pointed.smashPowFunctor ι, the smash power as an endofunctor of pointed types.
• Pointed.smashPow.reindex: the action of a bijection of index types.
• Pointed.smashPow.append: concatenation of classes of families.

References

• M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 1.

def Pointed.smashPow (X : Pointed) (ι : Type v) : Pointed

The smash power X^∧ι of a pointed type: the basepoint together with the families ι → X avoiding the basepoint in every coordinate.

noncomputable def Pointed.smashPow.mk {X : Pointed} {ι : Type v} (f : ι → X.X) : (X.smashPow ι).X

The class in the smash power X^∧ι of a family f : ι → X. It is the basepoint exactly when some coordinate of f is the basepoint.

@[simp]

theorem Pointed.smashPow.mk_eq_point_iff {X : Pointed} {ι : Type v} {f : ι → X.X} : mk f = (X.smashPow ι).point ↔ ∃ (i : ι), f i = X.point

A family represents the basepoint exactly when it lies in the fat wedge.

theorem Pointed.smashPow.mk_eq_point {X : Pointed} {ι : Type v} {f : ι → X.X} (i : ι) (hi : f i = X.point) : mk f = (X.smashPow ι).point

theorem Pointed.smashPow.mk_eq_mk_iff {X : Pointed} {ι : Type v} {f g : ι → X.X} : mk f = mk g ↔ f = g ∨ (∃ (i : ι), f i = X.point) ∧ ∃ (i : ι), g i = X.point

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

theorem Pointed.smashPow.ind {X : Pointed} {ι : Type v} {motive : (X.smashPow ι).X → Prop} (point : motive (X.smashPow ι).point) (mk : ∀ (f : ι → X.X), motive (mk f)) (a : (X.smashPow ι).X) : motive a

Induction on the smash power: it suffices to treat the basepoint and the classes of families.

noncomputable def Pointed.smashPow.lift {X : Pointed} {W : Pointed} {ι : Type v} (F : (ι → X.X) → W.X) (_hF : ∀ (f : ι → X.X) (i : ι), f i = X.point → F f = W.point) : X.smashPow ι ⟶ W

The pointed map out of the smash power induced by a function of families sending the fat wedge to the basepoint. The hypothesis is not needed to define the map in this model, only to compute it on every class (lift_mk).

@[simp]

theorem Pointed.smashPow.lift_mk {X : Pointed} {W : Pointed} {ι : Type v} (F : (ι → X.X) → W.X) (hF : ∀ (f : ι → X.X) (i : ι), f i = X.point → F f = W.point) (f : ι → X.X) : (lift F hF).toFun (mk f) = F f

theorem Pointed.smashPow.hom_ext {X : Pointed} {W : Pointed} {ι : Type v} {g h : X.smashPow ι ⟶ W} (H : ∀ (f : ι → X.X), g.toFun (mk f) = h.toFun (mk f)) : g = h

Pointed maps out of the smash power are determined by their values on classes of families.

theorem Pointed.smashPow.hom_ext_iff {X : Pointed} {W : Pointed} {ι : Type v} {g h : X.smashPow ι ⟶ W} : g = h ↔ ∀ (f : ι → X.X), g.toFun (mk f) = h.toFun (mk f)

noncomputable def Pointed.smashPow.map {X Y : Pointed} (ι : Type v) (g : X ⟶ Y) : X.smashPow ι ⟶ Y.smashPow ι

The smash power of a pointed map, applied in every coordinate.

@[simp]

theorem Pointed.smashPow.map_mk {X Y : Pointed} {ι : Type v} (g : X ⟶ Y) (f : ι → X.X) : (map ι g).toFun (mk f) = mk (g.toFun ∘ f)

@[simp]

theorem Pointed.smashPow.map_id {X : Pointed} {ι : Type v} : map ι (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (X.smashPow ι)

@[simp]

theorem Pointed.smashPow.map_comp {X Y Z : Pointed} {ι : Type v} (g : X ⟶ Y) (h : Y ⟶ Z) : map ι (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (map ι g) (map ι h)

noncomputable def Pointed.smashPowFunctor (ι : Type v) : CategoryTheory.Functor Pointed Pointed

The smash power X ↦ X^∧ι as a functor of pointed types.

@[simp]

theorem Pointed.smashPowFunctor_obj (ι : Type v) (X : Pointed) : (smashPowFunctor ι).obj X = X.smashPow ι

@[simp]

theorem Pointed.smashPowFunctor_map (ι : Type v) {X✝ Y✝ : Pointed} (g : X✝ ⟶ Y✝) : (smashPowFunctor ι).map g = smashPow.map ι g

noncomputable def Pointed.smashPow.reindex {ι κ : Type v} (X : Pointed) (e : ι ≃ κ) : X.smashPow ι ⟶ X.smashPow κ

The action of a bijection of index types on smash powers, reindexing the coordinates.

@[simp]

theorem Pointed.smashPow.reindex_mk {X : Pointed} {ι κ : Type v} (e : ι ≃ κ) (f : ι → X.X) : (reindex X e).toFun (mk f) = mk (f ∘ ⇑e.symm)

@[simp]

theorem Pointed.smashPow.reindex_refl {X : Pointed} {ι : Type v} : reindex X (Equiv.refl ι) = CategoryTheory.CategoryStruct.id (X.smashPow ι)

@[simp]

theorem Pointed.smashPow.reindex_trans {X : Pointed} {ι κ μ : Type v} (e : ι ≃ κ) (e' : κ ≃ μ) : reindex X (e.trans e') = CategoryTheory.CategoryStruct.comp (reindex X e) (reindex X e')

theorem Pointed.smashPow.map_reindex {X Y : Pointed} {ι κ : Type v} (g : X ⟶ Y) (e : ι ≃ κ) : CategoryTheory.CategoryStruct.comp (map ι g) (reindex Y e) = CategoryTheory.CategoryStruct.comp (reindex X e) (map κ g)

Reindexing commutes with the smash power of a pointed map.

theorem Pointed.smashPow.map_reindex_assoc {X Y : Pointed} {ι κ : Type v} (g : X ⟶ Y) (e : ι ≃ κ) {Z : Pointed} (h : Y.smashPow κ ⟶ Z) : CategoryTheory.CategoryStruct.comp (map ι g) (CategoryTheory.CategoryStruct.comp (reindex Y e) h) = CategoryTheory.CategoryStruct.comp (reindex X e) (CategoryTheory.CategoryStruct.comp (map κ g) h)

Reindexing commutes with the smash power of a pointed map.

noncomputable def Pointed.smashPow.append {X : Pointed} {ι κ : Type v} (a : (X.smashPow ι).X) (b : (X.smashPow κ).X) : (X.smashPow (ι ⊕ κ)).X

Concatenation of classes of families, from X^∧ι and X^∧κ to X^∧(ι ⊕ κ).

@[simp]

theorem Pointed.smashPow.append_mk_mk {X : Pointed} {ι κ : Type v} (f : ι → X.X) (g : κ → X.X) : append (mk f) (mk g) = mk (Sum.elim f g)

@[simp]

theorem Pointed.smashPow.append_point_left {X : Pointed} {ι κ : Type v} (b : (X.smashPow κ).X) : append (X.smashPow ι).point b = (X.smashPow (ι ⊕ κ)).point

@[simp]

theorem Pointed.smashPow.append_point_right {X : Pointed} {ι κ : Type v} (a : (X.smashPow ι).X) : append a (X.smashPow κ).point = (X.smashPow (ι ⊕ κ)).point

theorem Pointed.smashPow.map_append {X Y : Pointed} {ι κ : Type v} (g : X ⟶ Y) (a : (X.smashPow ι).X) (b : (X.smashPow κ).X) : (map (ι ⊕ κ) g).toFun (append a b) = append ((map ι g).toFun a) ((map κ g).toFun b)

Concatenation commutes with the smash power of a pointed map.