Hopf problem: foundations · period torus type one one

Supporting definitions and proofs for this stage of the six-sphere construction.

def Mathoverflow1973.PeriodTorusTypeOneOne.coefficientPair : Fin 6 → Fin 4 × Fin 4

The ordered coordinate pair represented by each exterior-square basis index.

Equations

• Mathoverflow1973.PeriodTorusTypeOneOne.coefficientPair = ![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]

theorem Mathoverflow1973.PeriodTorusCohomologyCup.pairIndices_eq_coefficientPair (k : Fin 6) : LocalSystemMatrices.pairIndices k = ![(PeriodTorusTypeOneOne.coefficientPair k).1, (PeriodTorusTypeOneOne.coefficientPair k).2]