# An effective proof of the Cartan formula: the even prime

## TL;DR

This paper provides a constructive proof of the Cartan formula at the cochain level over _2, applicable to general algebras over the Barratt-Eccles operad, including singular cochains of spaces.

## Contribution

It introduces an explicit, natural coboundary construction that verifies the Cartan formula at the cochain level for _2-cohomology.

## Key findings

- Constructs a natural coboundary for the Cartan formula at the cochain level.
- The proof applies to algebras over the Barratt-Eccles operad.
- Works for singular cochains of topological spaces.

## Abstract

The Cartan formula encodes the relationship between the cup product and the action of the Steenrod algebra in $\mathbb F_p$-cohomology. In this work, we present an effective proof of the Cartan formula at the cochain level when the field is $\mathbb F_2$. More explicitly, for an arbitrary pair of cocycles and any non-negative integer, we construct a natural coboundary that descends to the associated instance of the Cartan formula. Our construction works for general algebras over the Barratt-Eccles operad, in particular, for the singular cochains of spaces.