Documentation

LeanPool.MarkoffModP.BGS.Markoff.MiddleGame.RightSubgroups

Concrete right subgroups for the middle game #

All split and nonsplit semisimple eigenvalues are placed in the common quadratic extension. For a candidate order d, the right subgroup is the subgroup of d-th roots of unity in that extension. Candidate divisibility by p - 1 or p + 1 implies that this subgroup has exactly d elements.

Parabolic traces are deliberately excluded from the representation theorem: their rotation orders are p or 2 * p, not semisimple torus orders dividing p - 1 or p + 1.

source
noncomputable def BGS.Markoff.middleGameRightSubgroup (p d : ℕ) [Fact (Nat.Prime p)] :
Subgroup (quadraticFiniteField p)ˣ

The canonical right subgroup of order d inside the common quadratic extension.

Equations
Instances For
    source
    theorem BGS.Markoff.mem_middleGameRightSubgroup_iff_pow_eq_one (p d : ℕ) [Fact (Nat.Prime p)] (u : (quadraticFiniteField p)ˣ) :
    u ∈ middleGameRightSubgroup p d ↔ u ^ d = 1
    source
    theorem BGS.Markoff.mem_middleGameRightSubgroup_of_orderOf_eq (p d : ℕ) [Fact (Nat.Prime p)] (u : (quadraticFiniteField p)ˣ) (hu : orderOf u = d) :
    u ∈ middleGameRightSubgroup p d

    Every element whose multiplicative order is d belongs to the canonical right subgroup.

    source
    theorem BGS.Markoff.middleGameCandidateOrder_dvd_quadraticUnitsCard (p currentOrder d : ℕ) [Fact (Nat.Prime p)] (hd : d ∈ middleGameCandidateOrders p currentOrder) :
    d ∣ Nat.card (quadraticFiniteField p)ˣ

    Candidate divisibility by p - 1 or p + 1 implies divisibility by the order of the multiplicative group of the quadratic extension.

    source
    theorem BGS.Markoff.middleGameRightSubgroup_natCard (p currentOrder d : ℕ) [Fact (Nat.Prime p)] (hd : d ∈ middleGameCandidateOrders p currentOrder) :
    Nat.card ↥(middleGameRightSubgroup p d) = d

    The canonical right subgroup indexed by a candidate order has exactly that cardinality.

    source
    theorem BGS.Markoff.exists_middleGameRightSubgroup_trace_of_split (p d : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (w : (ZMod p)ˣ) (htrace : splitTorusTrace w = t) (hw : ↑w ^ 2 ≠ 1) (hrotation : rotationOrder t = d) :
    ∃ (h₂ : ↥(middleGameRightSubgroup p d)), (algebraMap (ZMod p) (quadraticFiniteField p)) t = splitTorusTrace ↑h₂

    A split eigenvalue of rotation order d, embedded in the quadratic extension, lies in the canonical right subgroup and has the required reciprocal trace.

    source
    theorem BGS.Markoff.exists_middleGameRightSubgroup_trace_of_nonsplit (p d : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (hrotation : rotationOrder t = d) :
    ∃ (h₂ : ↥(middleGameRightSubgroup p d)), (algebraMap (ZMod p) (quadraticFiniteField p)) t = splitTorusTrace ↑h₂

    A nonsplit norm-one eigenvalue of rotation order d lies in the same canonical quadratic right subgroup and represents the scalar-extended base-field trace.

    source
    theorem BGS.Markoff.exists_middleGameRightSubgroup_trace_of_nonparabolic_rotationOrder (p d : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (hnonparabolic : t ^ 2 ≠ 4) (hrotation : rotationOrder t = d) :
    ∃ (h₂ : ↥(middleGameRightSubgroup p d)), (algebraMap (ZMod p) (quadraticFiniteField p)) t = splitTorusTrace ↑h₂

    Every nonparabolic normalized trace of rotation order d is represented in the canonical right subgroup. The hypothesis t^2 != 4 is the explicit boundary separating this theorem from the parabolic orders p and 2 * p.

    source
    theorem BGS.Markoff.normalizedTrace_sq_eq_four_iff_parabolic (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) :
    t ^ 2 = 4 ↔ t = 2 ∨ t = -2

    Over a prime field, the equation t^2 = 4 is exactly the explicit parabolic alternative t = 2 or t = -2.

    source
    theorem BGS.Markoff.middleGameRightSubgroup_exactCard_and_traceClassification (p currentOrder d : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hd : d ∈ middleGameCandidateOrders p currentOrder) (t : ZMod p) (hrotation : rotationOrder t = d) :
    Nat.card ↥(middleGameRightSubgroup p d) = d ∧ (t = 2 ∨ t = -2 ∨ ∃ (h₂ : ↥(middleGameRightSubgroup p d)), (algebraMap (ZMod p) (quadraticFiniteField p)) t = splitTorusTrace ↑h₂)

    Complete candidate-order classification. The canonical right subgroup always has exact cardinality d; a trace of rotation order d is either one of the two parabolic parameters or is represented by a reciprocal trace in that subgroup.