GenericRootCommutant.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A generic finite root orbit has a commutative stabilizer centralizer

One invariant root forces one column of every centralizing matrix to be scalar. In the rational centralizer, evaluation in that column is faithful by genericity of the actual lattice. Rational centralizing matrices therefore commute, and scalar extension gives the same result for the real centralizer. This removes any need to exclude singleton blocks before treating the larger homogeneous orbit group.

lemma OAI.DukePrimeDegree.offColumn_zero_of_commute_root line 23
theorem OAI.DukePrimeDegree.rationalMatrix_eq_zero_of_conjugate_column_zero line 34
Source documentation
Genericity makes any column of the lattice matrix faithful for rational matrices; the matrix here is not assumed diagonal.
```
theorem rationalMatrix_eq_zero_of_conjugate_column_zero {n : ℕ}
    (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (B : Matrix (Fin n) (Fin n) ℚ) (i : Fin n)
    (hB : ∀ a, slMatrixConjugation g (rationalMatrixCast B) a i = 0) : B = 0 := by
…
```
Mentions: OAI.DukePrimeDegree.slMatrixConjugation, OAI.DukePrimeDegree.rationalMatrixCast
lemma OAI.DukePrimeDegree.commute_root_of_finite_root_orbit line 59
lemma OAI.DukePrimeDegree.conjugate_offColumn_zero_of_finite_root_orbit line 90
lemma OAI.DukePrimeDegree.commutator_column_zero line 102

theorem OAI.DukePrimeDegree.rationalStabilizer_commutative_of_finite_root_orbit line 126

Source documentation

A single invariant root makes the rational stabilizer centralizer commutative at a generic lattice point.

theorem rationalStabilizer_commutative_of_finite_root_orbit {n : ℕ}
    (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 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 : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (B C : Matrix (Fin n) (Fin n) ℚ)
    (hB : B ∈ (commutatorFamily (latticeStabilizerMatrix g L)).ker)
    (hC : C ∈ (commutatorFamily (latticeStabilizerMatrix g L)).ker) : Commute B C := by
…

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

lemma OAI.DukePrimeDegree.commute_of_mem_span_pairwise line 163

theorem OAI.DukePrimeDegree.realStabilizer_commutative_of_finite_root_orbit line 188

Source documentation

Scalar extension transports the preceding commutativity to the full real centralizer of the actual integral stabilizer.

theorem realStabilizer_commutative_of_finite_root_orbit {n : ℕ}
    (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 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 : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (B C : Matrix (Fin n) (Fin n) ℝ)
    (hB : B ∈ (commutatorFamily
      (fun γ => rationalMatrixCast (latticeStabilizerMatrix g L γ))).ker)
    (hC : C ∈ (commutatorFamily
…

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

lemma OAI.DukePrimeDegree.inverseConjugate_mem_realStabilizer line 209
Source documentation
Transport a centralizer element to the original integral coordinates.
```
lemma inverseConjugate_mem_realStabilizer {n : ℕ} (g : G n) (L : Subgroup (G n))
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g L, Commute M s.val.val) :
    slMatrixConjugation g⁻¹ M ∈ (commutatorFamily
      (fun γ => rationalMatrixCast (latticeStabilizerMatrix g L γ))).ker := by
…
```
Mentions: OAI.DukePrimeDegree.pointOrbitStabilizer, OAI.DukePrimeDegree.slMatrixConjugation, OAI.DukePrimeDegree.commutatorFamily, OAI.DukePrimeDegree.rationalMatrixCast, OAI.DukePrimeDegree.latticeStabilizerMatrix

theorem OAI.DukePrimeDegree.pointStabilizer_commutative_of_finite_root_orbit line 236

Source documentation

Commutativity in the actual orbit coordinates, with no diagonal-flow or singleton-block hypothesis.

theorem pointStabilizer_commutative_of_finite_root_orbit {n : ℕ}
    (g : G n)
    (hgeneric : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 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 : Matrix.SpecialLinearGroup.transvection hij (1 : ℝ) ∈ L)
    (M N : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g L, Commute M s.val.val)
    (hN : ∀ s : pointOrbitStabilizer g L, Commute N s.val.val) : Commute M N := by
…

Mentions: OAI.DukePrimeDegree.LatticeOrbitQuotient, OAI.DukePrimeDegree.latticeOrbitRightAction, OAI.DukePrimeDegree.pointOrbitStabilizer