Exact power-cover multiplicities in the endgame

The paper divides its trace-cover point count by the two power-map degrees. This module proves that step exactly for finite cyclic groups: a cover solution is a target trace solution together with one point in each power-map fiber, and every such fiber is equivalent to the corresponding kernel. No asymptotic or geometric estimate enters this multiplicity identity.

def BGS.Markoff.powerTraceCoverSolutions {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] (leftTrace : G → T) (rightTrace : H → T) (d e : ℕ) : Type (max 0 u_1 u_2)

Solutions of a trace equation after applying power maps to two finite groups.

Equations

• BGS.Markoff.powerTraceCoverSolutions leftTrace rightTrace d e = { z : G × H // leftTrace (z.1 ^ d) = rightTrace (z.2 ^ e) }

def BGS.Markoff.powerTraceRangeSolutions {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] (leftTrace : G → T) (rightTrace : H → T) (d e : ℕ) : Type (max 0 u_1 u_2)

The corresponding equation on the two power-map images.

Equations

• BGS.Markoff.powerTraceRangeSolutions leftTrace rightTrace d e = { z : ↥(powMonoidHom d).range × ↥(powMonoidHom e).range // leftTrace ↑z.1 = rightTrace ↑z.2 }

def BGS.Markoff.powerTraceCoverEquivSigmaFibers {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] (leftTrace : G → T) (rightTrace : H → T) (d e : ℕ) : powerTraceCoverSolutions leftTrace rightTrace d e ≃ (s : powerTraceRangeSolutions leftTrace rightTrace d e) × ↑(⇑(powMonoidHom d) ⁻¹' {↑(↑s).1}) × ↑(⇑(powMonoidHom e) ⁻¹' {↑(↑s).2})

A power-cover solution is a target solution together with one point in each power-map fiber.

Equations

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

theorem BGS.Markoff.natCard_powerMapFiber_eq_ker {G : Type u_1} [CommGroup G] (d : ℕ) (x : ↥(powMonoidHom d).range) : Nat.card ↑(⇑(powMonoidHom d) ⁻¹' {↑x}) = Nat.card ↥(powMonoidHom d).ker

theorem BGS.Markoff.natCard_powerTraceCoverSolutions {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (d e : ℕ) : Nat.card (powerTraceCoverSolutions leftTrace rightTrace d e) = Nat.card ↥(powMonoidHom d).ker * Nat.card ↥(powMonoidHom e).ker * Nat.card (powerTraceRangeSolutions leftTrace rightTrace d e)

theorem BGS.Markoff.natCard_powerTraceCoverSolutions_of_dvd {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] [IsCyclic G] [IsCyclic H] (leftTrace : G → T) (rightTrace : H → T) (d e : ℕ) (hd : d ∣ Nat.card G) (he : e ∣ Nat.card H) : Nat.card (powerTraceCoverSolutions leftTrace rightTrace d e) = d * e * Nat.card (powerTraceRangeSolutions leftTrace rightTrace d e)