Smash products of pointed types

Content created by Fredrik Bakke, Egbert Rijke and maybemabeline.

Created on 2023-05-03.
Last modified on 2024-03-02.

module synthetic-homotopy-theory.smash-products-of-pointed-types where
Imports
open import foundation.action-on-higher-identifications-functions
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import structured-types.pointed-cartesian-product-types
open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.pointed-unit-type

open import synthetic-homotopy-theory.cocones-under-spans-of-pointed-types
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.pushouts-of-pointed-types
open import synthetic-homotopy-theory.wedges-of-pointed-types

Idea

Given two pointed types a : A and b : B we may form their smash product as the following pushout

 A ∨∗ B ----> A ×∗ B
    |           |
    |           |
    v        ⌜  v
  unit -----> A ∧∗ B

where the map A ∨∗ B → A ×∗ B is the canonical inclusion map-wedge-product-Pointed-Type from the wedge into the pointed cartesian product.

Definition

smash-product-Pointed-Type :
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) 
  Pointed-Type (l1  l2)
smash-product-Pointed-Type A B =
  pushout-Pointed-Type
    ( pointed-map-product-wedge-Pointed-Type A B)
    ( terminal-pointed-map (A ∨∗ B))

infixr 15 _∧∗_
_∧∗_ = smash-product-Pointed-Type

Note: The symbols used for the smash product _∧∗_ are the logical and (agda-input: \wedge \and), and the asterisk operator (agda-input: \ast), not the asterisk *.

cogap-smash-product-Pointed-Type :
  {l1 l2 l3 : Level}
  {A : Pointed-Type l1} {B : Pointed-Type l2} {X : Pointed-Type l3} 
  type-cocone-Pointed-Type
    ( pointed-map-product-wedge-Pointed-Type A B)
    ( terminal-pointed-map (A ∨∗ B)) X 
  (A ∧∗ B) →∗ X
cogap-smash-product-Pointed-Type {A = A} {B} =
  cogap-Pointed-Type
    ( pointed-map-product-wedge-Pointed-Type A B)
    ( terminal-pointed-map (A ∨∗ B))

map-cogap-smash-product-Pointed-Type :
  {l1 l2 l3 : Level}
  {A : Pointed-Type l1} {B : Pointed-Type l2} {X : Pointed-Type l3} 
  type-cocone-Pointed-Type
    ( pointed-map-product-wedge-Pointed-Type A B)
    ( terminal-pointed-map (A ∨∗ B))
    ( X) 
  type-Pointed-Type (A ∧∗ B)  type-Pointed-Type X
map-cogap-smash-product-Pointed-Type c =
  pr1 (cogap-smash-product-Pointed-Type c)

Properties

The canonical pointed map from the cartesian product to the smash product

module _
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
  where

  pointed-map-smash-product-product-Pointed-Type : (A ×∗ B) →∗ (A ∧∗ B)
  pointed-map-smash-product-product-Pointed-Type =
    inl-pushout-Pointed-Type
      ( pointed-map-product-wedge-Pointed-Type A B)
      ( terminal-pointed-map (A ∨∗ B))

  map-smash-product-product-Pointed-Type :
    type-Pointed-Type (A ×∗ B)  type-Pointed-Type (A ∧∗ B)
  map-smash-product-product-Pointed-Type =
    map-pointed-map pointed-map-smash-product-product-Pointed-Type

Pointed maps into pointed types A and B induce a pointed map into A ∧∗ B

module _
  {l1 l2 l3 : Level}
  {A : Pointed-Type l1} {B : Pointed-Type l2} {S : Pointed-Type l3}
  where

  gap-smash-product-Pointed-Type :
    (f : S →∗ A) (g : S →∗ B)  S →∗ (A ∧∗ B)
  gap-smash-product-Pointed-Type f g =
    pointed-map-smash-product-product-Pointed-Type A B ∘∗
    gap-product-Pointed-Type f g

  map-gap-smash-product-Pointed-Type :
    (f : S →∗ A) (g : S →∗ B)  type-Pointed-Type S  type-Pointed-Type (A ∧∗ B)
  map-gap-smash-product-Pointed-Type f g =
    pr1 (gap-smash-product-Pointed-Type f g)

The canonical map from the wedge sum to the smash product identifies all points

module _
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
  where

  pointed-map-smash-product-wedge-Pointed-Type : (A ∨∗ B) →∗ (A ∧∗ B)
  pointed-map-smash-product-wedge-Pointed-Type =
    pointed-map-smash-product-product-Pointed-Type A B ∘∗
    pointed-map-product-wedge-Pointed-Type A B

  map-smash-product-wedge-Pointed-Type :
    type-Pointed-Type (A ∨∗ B)  type-Pointed-Type (A ∧∗ B)
  map-smash-product-wedge-Pointed-Type =
    map-pointed-map pointed-map-smash-product-wedge-Pointed-Type

  contraction-map-smash-product-wedge-Pointed-Type :
    ( x : type-Pointed-Type (A ∨∗ B)) 
    map-smash-product-wedge-Pointed-Type x 
    point-Pointed-Type (A ∧∗ B)
  contraction-map-smash-product-wedge-Pointed-Type x =
    ( glue-pushout
      ( map-product-wedge-Pointed-Type A B)
      ( map-pointed-map {A = A ∨∗ B} {B = unit-Pointed-Type}
        ( terminal-pointed-map (A ∨∗ B)))
      ( x)) 
    ( right-whisker-comp
      ( htpy-pointed-htpy
        ( inr-pushout-Pointed-Type
          ( pointed-map-product-wedge-Pointed-Type A B)
          ( terminal-pointed-map (A ∨∗ B)))
        ( inclusion-point-Pointed-Type (A ∧∗ B))
        ( is-initial-unit-Pointed-Type
          ( A ∧∗ B)
          ( inr-pushout-Pointed-Type
            ( pointed-map-product-wedge-Pointed-Type A B)
            ( terminal-pointed-map (A ∨∗ B)))))
      ( map-terminal-pointed-map (A ∨∗ B))
      ( x)) 
    ( preserves-point-pointed-map
      ( inclusion-point-Pointed-Type (A ∧∗ B)))

  coh-contraction-map-smash-product-wedge-Pointed-Type :
    ( ap
      ( map-smash-product-wedge-Pointed-Type)
      ( glue-wedge-Pointed-Type A B)) 
    ( contraction-map-smash-product-wedge-Pointed-Type
        ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))) 
    ( contraction-map-smash-product-wedge-Pointed-Type
      ( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
  coh-contraction-map-smash-product-wedge-Pointed-Type =
    ( map-inv-compute-dependent-identification-eq-value-function
      ( map-smash-product-wedge-Pointed-Type)
      ( map-pointed-map
        ( constant-pointed-map (A ∨∗ B) (A ∧∗ B)))
      ( glue-wedge-Pointed-Type A B)
      ( contraction-map-smash-product-wedge-Pointed-Type
        ( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
      ( contraction-map-smash-product-wedge-Pointed-Type
        ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B)))
      ( apd
        ( contraction-map-smash-product-wedge-Pointed-Type)
        ( glue-wedge-Pointed-Type A B))) 
    ( left-whisker-concat
      ( contraction-map-smash-product-wedge-Pointed-Type
        ( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
      ( ap-const
        ( point-Pointed-Type (A ∧∗ B))
        ( glue-wedge-Pointed-Type A B))) 
    ( right-unit)

The map from the pointed product to the smash product identifies elements

of the form (x, b) and (a, y), where b and a are the base points of B and A respectively.

module _
  {l1 l2 : Level}
  (A : Pointed-Type l1) (B : Pointed-Type l2)
  where

  inl-glue-smash-product-Pointed-Type :
    ( x : type-Pointed-Type A) 
    map-smash-product-product-Pointed-Type A B
      ( x , point-Pointed-Type B) 
    map-smash-product-product-Pointed-Type A B
      ( point-Pointed-Type A , point-Pointed-Type B)
  inl-glue-smash-product-Pointed-Type x =
    ( ap
      ( map-smash-product-product-Pointed-Type A B)
      ( inv (compute-inl-product-wedge-Pointed-Type A B x))) 
    ( contraction-map-smash-product-wedge-Pointed-Type A B
      ( map-inl-wedge-Pointed-Type A B x))

  inr-glue-smash-product-Pointed-Type :
    ( y : type-Pointed-Type B) 
    map-smash-product-product-Pointed-Type A B
      ( point-Pointed-Type A , y) 
    map-smash-product-product-Pointed-Type A B
      ( point-Pointed-Type A , point-Pointed-Type B)
  inr-glue-smash-product-Pointed-Type y =
    ( ap
      ( map-smash-product-product-Pointed-Type A B)
      ( inv (compute-inr-product-wedge-Pointed-Type A B y))) 
    ( contraction-map-smash-product-wedge-Pointed-Type A B
      ( map-inr-wedge-Pointed-Type A B y))

  coh-glue-smash-product-Pointed-Type :
    inl-glue-smash-product-Pointed-Type (point-Pointed-Type A) 
    inr-glue-smash-product-Pointed-Type (point-Pointed-Type B)
  coh-glue-smash-product-Pointed-Type =
    ( left-whisker-concat
      ( ap
        ( map-smash-product-product-Pointed-Type A B)
        ( inv
          ( compute-inl-product-wedge-Pointed-Type A B (point-Pointed-Type A))))
      ( inv (coh-contraction-map-smash-product-wedge-Pointed-Type A B))) 
    ( inv
      ( assoc
        ( ap (map-smash-product-product-Pointed-Type A B)
          ( inv
            ( compute-inl-product-wedge-Pointed-Type A B
              ( point-Pointed-Type A))))
        ( ap (map-smash-product-wedge-Pointed-Type A B)
          ( glue-wedge-Pointed-Type A B))
        ( contraction-map-smash-product-wedge-Pointed-Type A B
          ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))) 
    ( right-whisker-concat
      ( ( left-whisker-concat
          ( ap (map-smash-product-product-Pointed-Type A B)
            ( inv
              ( compute-inl-product-wedge-Pointed-Type A B
                ( point-Pointed-Type A))))
          ( ap-comp
            ( map-smash-product-product-Pointed-Type A B)
            ( map-product-wedge-Pointed-Type A B)
            ( glue-wedge-Pointed-Type A B))) 
        ( inv
          ( ap-concat
            ( map-smash-product-product-Pointed-Type A B)
            ( inv
              ( compute-inl-product-wedge-Pointed-Type A B
                ( point-Pointed-Type A)))
            ( ap
              ( map-product-wedge-Pointed-Type A B)
              ( glue-wedge-Pointed-Type A B)))) 
        ( ap²
          ( map-smash-product-product-Pointed-Type A B)
          ( inv
            ( left-transpose-eq-concat
              ( compute-inl-product-wedge-Pointed-Type A B
                ( point-Pointed-Type A))
              ( inv
                ( compute-inr-product-wedge-Pointed-Type A B
                  ( point-Pointed-Type B)))
              ( ap
                ( map-product-wedge-Pointed-Type A B)
                ( glue-wedge-Pointed-Type A B))
              ( inv
                ( right-transpose-eq-concat
                  ( ap
                    ( map-product-wedge-Pointed-Type A B)
                    ( glue-wedge-Pointed-Type A B))
                  ( compute-inr-product-wedge-Pointed-Type A B
                    ( point-Pointed-Type B))
                  ( compute-inl-product-wedge-Pointed-Type A B
                    ( point-Pointed-Type A))
                  ( ( compute-glue-cogap
                      ( map-pointed-map
                        ( inclusion-point-Pointed-Type A))
                      ( map-pointed-map
                        ( inclusion-point-Pointed-Type B))
                      ( cocone-type-cocone-Pointed-Type
                        ( inclusion-point-Pointed-Type A)
                        ( inclusion-point-Pointed-Type B)
                        ( cocone-product-wedge-Pointed-Type A B))
                      ( point-Pointed-Type unit-Pointed-Type)) 
                    ( right-unit))))))))
      ( contraction-map-smash-product-wedge-Pointed-Type A B
        ( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))

The universal property of the smash product

Fixing a pointed type B, the universal property of the smash product states that the functor - ∧∗ B forms the left-adjoint to the functor B →∗ - of pointed maps with source B. In the language of type theory, this means that we have a pointed equivalence:

  ((A ∧∗ B) →∗ C) ≃∗ (A →∗ B →∗ C).

Note: The categorical product in the category of pointed types is the pointed cartesian product.

map-universal-property-smash-product-Pointed-Type :
  {l1 l2 l3 : Level}
  (A : Pointed-Type l1) (B : Pointed-Type l2) (C : Pointed-Type l3) 
  ((A ∧∗ B) →∗ C)  (type-Pointed-Type A)  (B →∗ C)
pr1 (map-universal-property-smash-product-Pointed-Type A B C f x) y =
  map-pointed-map f (map-smash-product-product-Pointed-Type A B (x , y))
pr2 (map-universal-property-smash-product-Pointed-Type A B C f x) =
  ( ap
    ( map-pointed-map f)
    ( inl-glue-smash-product-Pointed-Type A B x)) 
  ( preserves-point-pointed-map f)

universal-property-smash-product-Pointed-Type :
  {l1 l2 l3 : Level}
  (A : Pointed-Type l1) (B : Pointed-Type l2) (C : Pointed-Type l3) 
  ((A ∧∗ B) →∗ C)  (A →∗ (pointed-map-Pointed-Type B C))
pr1 (universal-property-smash-product-Pointed-Type A B C f) =
  map-universal-property-smash-product-Pointed-Type A B C f
pr2 (universal-property-smash-product-Pointed-Type A B C f) =
  eq-htpy-pointed-Π
    ( map-universal-property-smash-product-Pointed-Type A B C
      ( f)
      ( point-Pointed-Type A))
    ( constant-pointed-map B C)
    ( ( λ y 
        ( ap
          ( map-pointed-map f)
          ( inr-glue-smash-product-Pointed-Type A B y) 
        ( preserves-point-pointed-map f))) ,
      ( ( right-whisker-concat
          ( ap²
            ( map-pointed-map f)
            ( inv (coh-glue-smash-product-Pointed-Type A B)))
          ( preserves-point-pointed-map f)) 
        ( inv right-unit)))

See also

Recent changes