Smash products of pointed types

Content created by Fredrik Bakke, Egbert Rijke and maybemabeline.

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

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.constant-pointed-maps
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-pointed-span-diagrams
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} →
  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} →
  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
        ( 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-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-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.

module _
  {l1 l2 l3 : Level}
  (A : Pointed-Type l1) (B : Pointed-Type l2) (C : Pointed-Type l3)
  (f : (A ∧∗ B) →∗ C)
  where

  map-map-universal-property-smash-product-Pointed-Type :
    type-Pointed-Type A → type-Pointed-Type B → type-Pointed-Type C
  map-map-universal-property-smash-product-Pointed-Type x y =
    map-pointed-map f (map-smash-product-product-Pointed-Type A B (x , y))

  preserves-point-map-map-universal-property-smash-product-Pointed-Type :
    (x : type-Pointed-Type A) →
    map-map-universal-property-smash-product-Pointed-Type x
      ( point-Pointed-Type B) ＝
    point-Pointed-Type C
  preserves-point-map-map-universal-property-smash-product-Pointed-Type x =
    ( ap
      ( map-pointed-map f)
      ( inl-glue-smash-product-Pointed-Type A B x)) ∙
    ( preserves-point-pointed-map f)

  map-universal-property-smash-product-Pointed-Type :
    type-Pointed-Type A → (B →∗ C)
  pr1 (map-universal-property-smash-product-Pointed-Type x) =
    map-map-universal-property-smash-product-Pointed-Type x
  pr2 (map-universal-property-smash-product-Pointed-Type x) =
    preserves-point-map-map-universal-property-smash-product-Pointed-Type x

  htpy-preserves-point-map-universal-property-smash-product-Pointed-Type :
    map-map-universal-property-smash-product-Pointed-Type
      ( point-Pointed-Type A) ~
    map-constant-pointed-map B C
  htpy-preserves-point-map-universal-property-smash-product-Pointed-Type y =
    ( ap (map-pointed-map f) (inr-glue-smash-product-Pointed-Type A B y)) ∙
    ( preserves-point-pointed-map f)

  coherence-point-preserves-point-map-universal-property-smash-product-Pointed-Type :
    coherence-point-unpointed-htpy-pointed-Π
      ( map-universal-property-smash-product-Pointed-Type
        ( point-Pointed-Type A))
      ( constant-pointed-map B C)
      ( htpy-preserves-point-map-universal-property-smash-product-Pointed-Type)
  coherence-point-preserves-point-map-universal-property-smash-product-Pointed-Type =
    ( right-whisker-concat
      ( ap²
        ( map-pointed-map f)
        ( coh-glue-smash-product-Pointed-Type A B))
      ( preserves-point-pointed-map f)) ∙
    ( inv right-unit)

  pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type :
    map-universal-property-smash-product-Pointed-Type (point-Pointed-Type A) ~∗
    constant-pointed-map B C
  pr1
    pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type =
    htpy-preserves-point-map-universal-property-smash-product-Pointed-Type
  pr2
    pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type =
    coherence-point-preserves-point-map-universal-property-smash-product-Pointed-Type

  preserves-point-map-universal-property-smash-product-Pointed-Type :
    map-universal-property-smash-product-Pointed-Type (point-Pointed-Type A) ＝
    constant-pointed-map B C
  preserves-point-map-universal-property-smash-product-Pointed-Type =
    eq-pointed-htpy
      ( map-universal-property-smash-product-Pointed-Type
        ( point-Pointed-Type A))
      ( constant-pointed-map B C)
      ( pointed-htpy-preserves-point-map-universal-property-smash-product-Pointed-Type)

  pointed-map-universal-property-smash-product-Pointed-Type :
    A →∗ (pointed-map-Pointed-Type B C)
  pr1 pointed-map-universal-property-smash-product-Pointed-Type =
    map-universal-property-smash-product-Pointed-Type
  pr2 pointed-map-universal-property-smash-product-Pointed-Type =
    preserves-point-map-universal-property-smash-product-Pointed-Type

See also

Recent changes