Documentation

GQ2.Roe.ChiR

The canonical orientation χ_R of D_R and its image (Roe note §3.3, ⟦prop:orientation⟧) #

Assembles the canonical Demushkin orientation χ_R : D_R → ℤ₂ˣ of the Roe pro-2 group (GQ2/Roe/DRPresentation.lean) out of the two halves that were kept parallel:

The note's display eq. (orientationvalues) reads

Y = -X²,      X³ + 2X² + 1 = 0,      S = -X³ / (X² + X + 1),
X ≡ 5 (mod 16),      S ≡ 13 (mod 16),      im χ_R = {±1} × (1 + 4ℤ₂).

Main definitions #

Main results #

The surjectivity proof #

Rather than build the 2-adic logarithm 1+4ℤ₂ ≅ 4ℤ₂ from the note, we run the pro-2 Burnside / Frattini criterion (surjective_of_forall_not_le_index_p, GQ2/FrattiniCriterion.lean): a continuous hom into a pro-2 group is surjective once its range escapes every index-2 open normal subgroup M. Such an M contains all squares (its quotient has order 2); the image contains χ_R(x) = X ≡ 5 and χ_R(y·x⁻²) = -1 ≡ 7, and by the mod-8 square decomposition mod8_sq (every unit is s·w² with s ∈ {1,-1,±(-3)}, and -3 ≡ 5 ≡ X (mod 8)) the classes {X, -1} with the squares generate ℤ₂ˣ, so M = ⊤ — impossible at index 2.

Cross-checked against ⟦prop:orientation⟧'s last display and the R2 spike (docs/orchestration/roe-r2-spike.md). All std-3.

Unit packaging of the orientation values #

R10's rootX, Sval, Yval are ℤ₂ elements; the character universal property and Labute datum both need them as ℤ₂ˣ units. (Sval_isUnit/Yval_isUnit are the "R10-side nice-to-haves" flagged in the R7 design memo §R10.)

source
theorem GQ2.Roe.Yval_isUnit :
IsUnit Yval

Y = -X² is a unit (a negated power of the unit X).

source
theorem GQ2.Roe.Sval_isUnit :
IsUnit Sval

S = -X³/(X²+X+1) is a unit: S·(X²+X+1) = -X³ is a unit and X²+X+1 is a unit (denom_isUnit), so S is.

source
noncomputable def GQ2.Roe.rootXUnit :
ℤ_[2]ˣ

X = χ_R(x) as a 2-adic unit.

Equations
Instances For
    source
    noncomputable def GQ2.Roe.SvalUnit :
    ℤ_[2]ˣ

    S = χ_R(s) as a 2-adic unit.

    Equations
    Instances For
      source
      noncomputable def GQ2.Roe.YvalUnit :
      ℤ_[2]ˣ

      Y = χ_R(y) as a 2-adic unit.

      Equations
      Instances For
        source
        @[simp]
        theorem GQ2.Roe.val_rootXUnit :
        ↑rootXUnit = rootX
        source
        @[simp]
        theorem GQ2.Roe.val_SvalUnit :
        ↑SvalUnit = Sval
        source
        @[simp]
        theorem GQ2.Roe.val_YvalUnit :
        ↑YvalUnit = Yval
        source
        theorem GQ2.Roe.YvalUnit_sq_eq :
        YvalUnit ^ 2 = rootXUnit ^ 4

        The character relation ⟦eq:charrelation⟧ in unit form: Y² = X⁴ (from Y = -X²).

        source
        theorem GQ2.Roe.YvalUnit_eq_neg_sq :
        YvalUnit = -rootXUnit ^ 2

        Y = -X² in unit form (the shape χ_R(t) = YX⁻² consumes).

        The orientation character χ_R #

        source
        noncomputable def GQ2.Roe.chiR :
        ↑DR.toProfinite.toTop →ₜ* ℤ_[2]ˣ

        The canonical orientation χ_R : D_R → ℤ₂ˣ ⟦prop:orientation⟧, built by the universal property of D_R (drLiftHom) at the triple (S, X, Y) = (SvalUnit, rootXUnit, YvalUnit). The relator r₂ dies because ℤ₂ˣ is abelian: drWord collapses to (X⁴)⁻¹Y² (drWord_comm) and Y² = X⁴ (YvalUnit_sq_eq).

        Equations
        Instances For
          source
          @[simp]
          theorem GQ2.Roe.chiR_drS :
          chiR drS = SvalUnit
          source
          @[simp]
          theorem GQ2.Roe.chiR_drX :
          chiR drX = rootXUnit
          source
          @[simp]
          theorem GQ2.Roe.chiR_drY :
          chiR drY = YvalUnit

          χ_R is the Labute orientation #

          source
          theorem GQ2.Roe.isLabuteOrientation_chiR :
          IsLabuteOrientation chiR.toMonoidHom

          χ_R is Labute's canonical orientation ⟦prop:orientation⟧: its generator values (S, X, Y) form a Labute orientation datum. Discharged from isLabuteOrientationDatum_of_root with R10's cubic root facts.

          source
          theorem GQ2.Roe.chiR_torsion :
          chiR drY * (chiR drX)⁻¹ ^ 2 = -1

          The torsion value ⟦eq:tR⟧: χ_R(y)·χ_R(x)⁻² = -1. Since Y = -X², this is (-X²)·X⁻² = -1. Phrased on the generators y, x (not on the abelianized t̄), so it is available before ticket R8's abelianization; ticket R15 transports it to t̄.

          Surjectivity: im χ_R = ℤ₂ˣ #

          source
          theorem GQ2.Roe.chiR_surjective :
          Function.Surjective ⇑chiR

          Surjectivity of χ_R ⟦prop:orientation⟧, the image statement im χ_R = ℤ₂ˣ. Because every 2-adic unit is ≡ ±1 (mod 4), the note's {±1}×(1+4ℤ₂) is all of ℤ₂ˣ, so this is the same encoding as B3c's surjective_chiTwo.

          Proof by the pro-2 Burnside/Frattini criterion (surjective_of_forall_not_le_index_p): fix an index-2 open normal M ≤ ℤ₂ˣ. Its quotient has order 2, so M contains every square. The range of χ_R contains χ_R(x) = X and χ_R(y·x⁻²) = -1; if M also contained the range then, by mod8_sq (every unit is s·w² with s ∈ {1,-1,±(-3)} and -3 ≡ 5 ≡ X (mod 8) is X times a square), M would be all of ℤ₂ˣ, contradicting index 2.

          Stress tests #

          source
          theorem GQ2.Roe.chiR_drX_toZModPow_four :
          (PadicInt.toZModPow 4) ↑(chiR drX) = 5

          Stress test (mod-16 value of χ_R(x)): χ_R(x) ≡ 5 (mod 16) (eq. orientationvalues). Catches a sign/branch slip in the value assignment.

          source
          theorem GQ2.Roe.chiR_drS_toZModPow_four :
          (PadicInt.toZModPow 4) ↑(chiR drS) = 13

          Stress test (mod-16 value of χ_R(s)): χ_R(s) ≡ 13 (mod 16).

          source
          theorem GQ2.Roe.chiR_drWord :
          chiR (drWord drS drX drY) = 1

          Stress test (the relator dies): χ_R(r₂) = 1. It holds already as χ_R(1) since r₂ = 1 in D_R (dr_relation); this checks the value assignment is consistent with the presentation.

          Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained) #