Hopf problem: uniformization · special periods 2

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

def Mathoverflow1973.SpecialPeriods.cyclicPowerHom {G : Type u_1} [Group G] (n : ℕ) (a : G) (ha : a ^ n = 1) : Multiplicative (ZMod n) →* G

The homomorphism from a finite cyclic group generated by an element of bounded order.

Equations

• Mathoverflow1973.SpecialPeriods.cyclicPowerHom n a ha = AddMonoidHom.toMultiplicativeLeft ((ZMod.lift n) ⟨(zmultiplesHom (Additive G)) (Additive.ofMul a), ⋯⟩)

@[reducible, inline]

abbrev Mathoverflow1973.SpecialPeriods.TriangleGroup : Type

The free product of cyclic groups of orders three and four.

Equations

• Mathoverflow1973.SpecialPeriods.TriangleGroup = Monoid.Coprod (Multiplicative (ZMod 3)) (Multiplicative (ZMod 4))

def Mathoverflow1973.SpecialPeriods.triangleLift {G : Type u_1} [Group G] (a b : G) (ha : a ^ 3 = 1) (hb : b ^ 4 = 1) : TriangleGroup →* G

The triangle-group homomorphism determined by elements of orders three and four.

Equations

• Mathoverflow1973.SpecialPeriods.triangleLift a b ha hb = Monoid.Coprod.lift (Mathoverflow1973.SpecialPeriods.cyclicPowerHom 3 a ha) (Mathoverflow1973.SpecialPeriods.cyclicPowerHom 4 b hb)

def Mathoverflow1973.SpecialPeriods.triangleLatticeT₁ : Matrix.SpecialLinearGroup (Fin 4) ℤ

The first special-linear lattice generator, of order three.

Equations

• Mathoverflow1973.SpecialPeriods.triangleLatticeT₁ = ⟨Mathoverflow1973.T₁✝, Mathoverflow1973.det_T₁✝⟩

def Mathoverflow1973.SpecialPeriods.triangleLatticeT₂ : Matrix.SpecialLinearGroup (Fin 4) ℤ

The second special-linear lattice generator, of order four.

Equations

• Mathoverflow1973.SpecialPeriods.triangleLatticeT₂ = ⟨Mathoverflow1973.T₂✝, Mathoverflow1973.det_T₂✝⟩

theorem Mathoverflow1973.SpecialPeriods.triangleLatticeT₁_cube : triangleLatticeT₁ ^ 3 = 1

theorem Mathoverflow1973.SpecialPeriods.triangleLatticeT₂_fourth : triangleLatticeT₂ ^ 4 = 1

def Mathoverflow1973.SpecialPeriods.triangleLatticeRepresentation : TriangleGroup →* Matrix.SpecialLinearGroup (Fin 4) ℤ

The special-linear representation of the triangle group on the lattice.

Equations

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

def Mathoverflow1973.SpecialPeriods.latticeContragredient : Matrix.SpecialLinearGroup (Fin 4) ℤ →* Matrix.SpecialLinearGroup (Fin 4) ℤ

The contragredient automorphism of the special linear lattice group.

Equations

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

def Mathoverflow1973.SpecialPeriods.triangleDualRepresentation : TriangleGroup →* Matrix.SpecialLinearGroup (Fin 4) ℤ

The contragredient triangle-group representation on the lattice.

Equations

• Mathoverflow1973.SpecialPeriods.triangleDualRepresentation = Mathoverflow1973.SpecialPeriods.latticeContragredient.comp Mathoverflow1973.SpecialPeriods.triangleLatticeRepresentation