Hopf problem: uniformization · cusp uniformization 2

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

def Mathoverflow1973.CuspUniformization.totalPeriodRelation (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (ε : ℝ) : Setoid ↥(LogCover ε)

The setoid of total-period equivalence on the logarithmic cover.

Equations

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

@[reducible, inline]

abbrev Mathoverflow1973.CuspUniformization.TotalPeriodQuotient (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (ε : ℝ) : Type

The quotient of the logarithmic cover by total-period equivalence.

Equations

• Mathoverflow1973.CuspUniformization.TotalPeriodQuotient C ε = Quotient (Mathoverflow1973.CuspUniformization.totalPeriodRelation C ε)

def Mathoverflow1973.CuspUniformization.totalPeriodQuotientMap (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (ε : ℝ) : ↥(LogCover ε) → TotalPeriodQuotient C ε

The canonical map to the total-period quotient.

Equations

• Mathoverflow1973.CuspUniformization.totalPeriodQuotientMap C ε = Quotient.mk (Mathoverflow1973.CuspUniformization.totalPeriodRelation C ε)

@[simp]

theorem Mathoverflow1973.CuspUniformization.totalPeriodQuotientMap_eq_iff (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (ε : ℝ) (p q : ↥(LogCover ε)) : totalPeriodQuotientMap C ε p = totalPeriodQuotientMap C ε q ↔ TotalPeriodRelated C ↑p ↑q