PairedRootCentralizer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The scalar commutant forced by an opposite root pair

The paired-coordinate algebra applies to the rational matrices conjugated by a lattice representative. The rational structure is transported through the matrix identity, rather than postulated. A finite invariant orbit and one opposite root pair then force its rational stabilizer commutant to consist of scalars.

lemma OAI.DukePrimeDegree.transpose_conjugate_rational_preserves_rowSpace line 23
lemma OAI.DukePrimeDegree.transpose_mulVec_coordinate_of_column line 41
lemma OAI.DukePrimeDegree.equal_diagonal_of_commute_root line 53
lemma OAI.DukePrimeDegree.slMatrixConjugation_smul_one line 61

theorem OAI.DukePrimeDegree.rationalMatrix_scalar_of_opposite_roots line 68

Source documentation

A conjugated rational matrix whose two indicated columns have a common scalar eigenvalue must itself be a rational scalar matrix.

theorem rationalMatrix_scalar_of_opposite_roots {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ k, v k ≠ 0)
    (B : Matrix (Fin n) (Fin n) ℚ) (i j : Fin n) (hij : i ≠ j)
    (hijB : Commute (slMatrixConjugation g (rationalMatrixCast B))
      (Matrix.transvection i j (1 : ℝ)))
    (hjiB : Commute (slMatrixConjugation g (rationalMatrixCast B))
      (Matrix.transvection j i (1 : ℝ))) :
    ∃ q : ℚ, B = q • (1 : Matrix (Fin n) (Fin n) ℚ) := by
…

Mentions: OAI.DukePrimeDegree.slMatrixConjugation, OAI.DukePrimeDegree.rationalMatrixCast

theorem OAI.DukePrimeDegree.rationalStabilizer_scalar_of_finite_opposite_root_orbit line 115

Source documentation

Actual finite-orbit specialization: both opposite roots are members of the orbit group; polynomial recurrence supplies commutation with each.

theorem rationalStabilizer_scalar_of_finite_opposite_root_orbit {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ k, v k ≠ 0)
    (L : Subgroup (G n))
    (μ : Measure (LatticeOrbitQuotient g L)) [IsFiniteMeasure μ] (hμ : μ ≠ 0)
    (hinv : ∀ h : L, μ.map (fun x => latticeOrbitRightAction g L x h) = μ)
    (i j : Fin n) (hij : i ≠ j)
    (hroot_ij : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (hroot_ji : Matrix.SpecialLinearGroup.transvection hij.symm (1 : ℝ) ∈ L)
    (B : Matrix (Fin n) (Fin n) ℚ)
    (hB : B ∈ (commutatorFamily (latticeStabilizerMatrix g L)).ker) :
    ∃ q : ℚ, B = q • (1 : Matrix (Fin n) (Fin n) ℚ) := by
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.commutatorFamily, OAI.DukePrimeDegree.latticeStabilizerMatrix