Lie algebra properties of generalised Whitehead products - Githubissues

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

459 stars 141 forks source link

Lie algebra properties of generalised Whitehead products #1170

Open aljungstrom opened 1 week ago

aljungstrom commented 1 week ago

This (draft) PR so far contains:

Main result: (appropriate versions of) bilinearity, 'graded' commutativity and the Jacobi identity for generalised Whitehead products. These are all found in Cubical.Homotopy.WhiteheadProducts.Generalised.Properties
Some refactoring: gave Whitehead products their own file under Cubical.Homotopy.
Co-H-Space structure on joins.

WIP:

Lift everything to WH products on homotopy groups -- all results are in the library, just a matter of combining them...
Cleaning (lol)