ScalarOrbitCommutant.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar real commutants of prime-degree finite root-pair orbits

Rationality of the actual lattice stabilizer's commutant turns the preceding rational scalar theorem into a real scalar theorem. In particular, no nontrivial real projection can commute with the orbit group. No orbit existence is assumed beyond the finite invariant orbit explicitly supplied.

def OAI.DukePrimeDegree.scalarMatrixSpace line 21
lemma OAI.DukePrimeDegree.mem_scalarMatrixSpace_iff line 24

theorem OAI.DukePrimeDegree.realStabilizer_scalar_of_finite_opposite_root_orbit line 35

Source documentation

The full real commutant in integral lattice coordinates is scalar.

theorem realStabilizer_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)
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : M ∈ (commutatorFamily
      (fun γ => rationalMatrixCast (latticeStabilizerMatrix g L γ))).ker) :
…

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

theorem OAI.DukePrimeDegree.pointStabilizer_scalar_of_finite_opposite_root_orbit line 61

Source documentation

The scalar conclusion in the actual orbit's real coordinates.

theorem pointStabilizer_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)
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ s : pointOrbitStabilizer g L, Commute M s.val.val) :
    ∃ c : ℝ, M = c • (1 : Matrix (Fin n) (Fin n) ℝ) := by
…

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