Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Steenrod squares via unordered joins

Axel Ljungström, David Wärn

TL;DR

This paper develops a synthetic framework in HoTT for Steenrod squares by reframing cohomology operations through unordered joins and the unordered cup product. It proves stability, Cartan's formula, and Adem relations for the $n$th Steenrod square $ extnormal{$ ext{Sq}^n$}$, using a polynomial representation of maps from $ extnormal{$ ext{RP}^ obreak ext{infty}$}$ and a crucial Fubini-type theorem for unordered joins. The approach is carried out within Cubical Agda, highlighting both the power and current limitations of HoTT for higher-coherence constructions and abelian cohomology operations. The paper also applies these results to compute a nontrivial $ obreak ext{pi}_4( ext{S}^3)$ and discusses future directions towards $E_ obreak ext{infty}$-monoids and extensions to odd primes.

Abstract

The Steenrod squares are cohomology operations with important applications in algebraic topology. While these operations are well-understood classically, little is known about them in the setting of homotopy type theory. Although a definition of the Steenrod squares was put forward by Brunerie (2017), proofs of their characterising properties have remained elusive. In this paper, we revisit Brunerie's definition and provide proofs of these properties, including stability, Cartan's formula and the Adem relations. This is done by studying a higher inductive type called the unordered join. This approach is inherently synthetic and, consequently, many of our proofs differ significantly from their classical counterparts. Along the way, we discuss upshots and limitations of homotopy type theory as a synthetic language for homotopy theory. The paper is accompanied by a computer formalisation in Cubical Agda.

The Steenrod squares via unordered joins

TL;DR

This paper develops a synthetic framework in HoTT for Steenrod squares by reframing cohomology operations through unordered joins and the unordered cup product. It proves stability, Cartan's formula, and Adem relations for the th Steenrod square ext{Sq}^n, using a polynomial representation of maps from ext{RP}^ obreak ext{infty} and a crucial Fubini-type theorem for unordered joins. The approach is carried out within Cubical Agda, highlighting both the power and current limitations of HoTT for higher-coherence constructions and abelian cohomology operations. The paper also applies these results to compute a nontrivial and discusses future directions towards -monoids and extensions to odd primes.

Abstract

The Steenrod squares are cohomology operations with important applications in algebraic topology. While these operations are well-understood classically, little is known about them in the setting of homotopy type theory. Although a definition of the Steenrod squares was put forward by Brunerie (2017), proofs of their characterising properties have remained elusive. In this paper, we revisit Brunerie's definition and provide proofs of these properties, including stability, Cartan's formula and the Adem relations. This is done by studying a higher inductive type called the unordered join. This approach is inherently synthetic and, consequently, many of our proofs differ significantly from their classical counterparts. Along the way, we discuss upshots and limitations of homotopy type theory as a synthetic language for homotopy theory. The paper is accompanied by a computer formalisation in Cubical Agda.

Paper Structure

This paper contains 23 sections, 27 theorems, 38 equations.

Table of Contents

  1. Introduction
  2. Contributions and outline
  3. Notation and basic definitions
  4. Pi- and sigma-types
  5. Equality
  6. Equivalences and univalence
  7. Pointed structures
  8. Loop spaces
  9. H-levels
  10. Truncations
  11. Connectedness
  12. Pushouts
  13. Eilenberg--MacLane spaces and cohomology
  14. Unordered pairs and commutativity structures
  15. Basic facts about $\textnormal{$\mathbb{R}P^\infty$}$
  16. ...and 8 more sections

Key Result

Theorem 1

There is a set of pointed maps $\textnormal{$\mathsf{Sq}_{m}^{n}$} : K_m \to_\textup{pt} K_{m+n}$ for $m,n \geq 0$, called the Steenrod squares, usually written $\textnormal{$\mathsf{Sq}^{n}$}$ leaving the $m$ implicit, which satisfy the following identities. In addition, the squares are stable and satisfy the Adem relations:

Theorems & Definitions (57)

  • Theorem 1: The Steenrod squares, axiomatically
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • proof : Proof/construction of \ref{['lem:PRinf-invol']}
  • Lemma 5
  • proof
  • Lemma 6
  • Lemma 7
  • Definition 8: Brunerie Brunerie17
  • ...and 47 more