Hopf problem: threefold · special periods 1

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

structure Mathoverflow1973.SpecialPeriods.CuspFamily.Data : Type

Analytic correction data defining a cusp family on a punctured disc.

• μ : ℂ → ℂ

  The diagonal holomorphic correction coefficient.

• b : ℂ → ℂ

  The lower-left holomorphic correction coefficient.

• h : ℂ → ℂ

  The off-diagonal holomorphic correction coefficient.

• radius : ℝ

  The radius on which the cusp-family estimates hold.

• radius_pos : 0 < self.radius
• radius_lt_one : self.radius < 1
• holomorphic (i j : Fin 2) : ContDiffOn ℂ ⊤ (fun (t : ℂ) => cuspCorrection self.μ self.b self.h t i j) (Metric.ball 0 self.radius)
• smallDrift : ToricSpace.SmallDrift (cuspCorrection self.μ self.b self.h) self.radius

@[reducible, inline]

abbrev Mathoverflow1973.SpecialPeriods.CuspFamily.Data.correction (D : Data) : ℂ → Matrix (Fin 2) (Fin 2) ℂ

The correction matrix associated to cusp-family data.

Equations

• D.correction = Mathoverflow1973.SpecialPeriods.cuspCorrection D.μ D.b D.h

def Mathoverflow1973.SpecialPeriods.CuspFamily.cuspTorusLinearEquiv (k : ℤ) : RealTorus₄ ≃ₗ[ℤ] RealTorus₄

The lattice-linear automorphism of the cusp torus with exponent k.

Equations

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

def Mathoverflow1973.SpecialPeriods.CuspFamily.cuspTorusHomeomorph (k : ℤ) : RealTorus₄ ≃ₜ RealTorus₄

The torus homeomorphism induced by the cusp lattice automorphism.

Equations

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

def Mathoverflow1973.SpecialPeriods.CuspFamily.Data.Space (D : Data) : Type

The quotient total space of a cusp family.

Equations

• D.Space = MulAction.orbitRel.Quotient (Multiplicative ℤ) (Mathoverflow1973.SpecialPeriods.CuspFamily.Data.TotalSpace✝ D)

noncomputable def Mathoverflow1973.SpecialPeriods.CuspFamily.Data.iteratedCover (D : Data) : ↥(CuspUniformization.LogCover D.radius) → D.Space

The covering map from the logarithmic cover to the cusp-family space.

Equations

• D.iteratedCover = Mathoverflow1973.SpecialPeriods.CuspFamily.Data.quotient✝ D ∘ Mathoverflow1973.SpecialPeriods.CuspFamily.Data.familyCover✝ D