Hopf problem: period family · period domain

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

@[reducible, inline]

abbrev Mathoverflow1973.FullPeriodMatrix.IntegerPeriods : Type

The type of four integral period vectors.

Equations

• Mathoverflow1973.FullPeriodMatrix.IntegerPeriods = ((Fin 2 → ℤ) × (Fin 2 → ℤ))

def Mathoverflow1973.FullPeriodMatrix.periodVector (p : FullPeriodMatrix) : IntegerPeriods →+ ComplexPlane₂

The integral period vector selected by an index.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathoverflow1973.FullPeriodMatrix.periodVector_injective (p : FullPeriodMatrix) : Function.Injective ⇑p.periodVector