Hopf problem: foundations · core 3

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

def Mathoverflow1973.standardLattice : Submodule ℤ RealPlane₄

The standard integral lattice spanned by the coordinate basis of RealPlane₄.

Equations

• Mathoverflow1973.standardLattice = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ (Fin 4)))

@[reducible, inline]

abbrev Mathoverflow1973.RealTorus₄ : Type

The four-dimensional real torus obtained from the standard lattice quotient.

Equations

• Mathoverflow1973.RealTorus₄ = (Mathoverflow1973.RealPlane₄ ⧸ Mathoverflow1973.standardLattice)