PrimeBlockRationality.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Rational diagonal stabilizers of actual lattices

The rational coordinate space below is constructed from an actual lattice matrix. Its diagonal stabilizer is a concrete subalgebra of real coordinate functions, not a separately assumed field action. The absence of lattice vectors on coordinate hyperplanes makes this algebra a field of degree dividing the ambient dimension.

def OAI.DukePrimeDegree.rationalRowMap line 26
Source documentation
Rational linear combinations of the rows of a real lattice matrix.
```
def rationalRowMap {n : ℕ} (g : Matrix (Fin n) (Fin n) ℝ) :
    (Fin n → ℚ) →ₗ[ℚ] (Fin n → ℝ) where
…
```
lemma OAI.DukePrimeDegree.rationalRowMap_apply line 33
lemma OAI.DukePrimeDegree.rationalRowMap_injective line 38
def OAI.DukePrimeDegree.rationalRowSpace line 46
instance OAI.DukePrimeDegree.(instance at line 49) line 49
lemma OAI.DukePrimeDegree.finrank_rationalRowSpace line 52
lemma OAI.DukePrimeDegree.row_mem_rationalRowSpace line 58
theorem OAI.DukePrimeDegree.real_span_rationalRowSpace line 67
Source documentation
The rational row space is small over ℚ, but spans the whole real coordinate space. This retains the actual invertible lattice matrix.
```
theorem real_span_rationalRowSpace {n : ℕ} (g : G n) :
    Submodule.span ℝ (rationalRowSpace g : Set (Fin n → ℝ)) = ⊤ := by
…
```
Mentions: OAI.DukePrimeDegree.rationalRowSpace
theorem OAI.DukePrimeDegree.rationalRowSpace_no_coordinate_zero line 81
Source documentation
The generic-lattice condition also excludes coordinate zeroes in the rational span; localization introduces no new linear relations.
```
theorem rationalRowSpace_no_coordinate_zero {n : ℕ} (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0) :
    ∀ v ∈ rationalRowSpace g, ∀ j, v j = 0 → v = 0 := by
…
```
Mentions: OAI.DukePrimeDegree.rationalRowSpace
def OAI.DukePrimeDegree.rationalDiagonalStabilizer line 105
Source documentation
Real diagonal coordinate functions preserving the rational space.
```
def rationalDiagonalStabilizer {n : ℕ} (W : Submodule ℚ (Fin n → ℝ)) :
    Subalgebra ℚ (Fin n → ℝ) where
…
```
lemma OAI.DukePrimeDegree.mem_rationalDiagonalStabilizer line 120
theorem OAI.DukePrimeDegree.mem_rationalDiagonalStabilizer_iff_rational_matrix line 127
Source documentation
The diagonal stabilizer is exactly the set of diagonals conjugate to rational matrices by the actual lattice matrix. In particular, this algebra is intrinsically attached to the rational lattice structure.
```
theorem mem_rationalDiagonalStabilizer_iff_rational_matrix {n : ℕ}
    (g : G n) (a : Fin n → ℝ) :
    a ∈ rationalDiagonalStabilizer (rationalRowSpace g) ↔
      ∃ B : Matrix (Fin n) (Fin n) ℚ,
        B.map (algebraMap ℚ ℝ) * g.val = g.val * Matrix.diagonal a := by
…
```
Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer, OAI.DukePrimeDegree.rationalRowSpace

theorem OAI.DukePrimeDegree.rationalDiagonalMatrix_unique line 159

Source documentation

The rational matrix representing a stabilizing diagonal is unique.

theorem rationalDiagonalMatrix_unique {n : ℕ} (g : G n) (a : Fin n → ℝ)
    {B C : Matrix (Fin n) (Fin n) ℚ}
    (hB : B.map (algebraMap ℚ ℝ) * g.val = g.val * Matrix.diagonal a)
    (hC : C.map (algebraMap ℚ ℝ) * g.val = g.val * Matrix.diagonal a) : B = C := by
…

instance OAI.DukePrimeDegree.rationalDiagonalStabilizerModule line 168
Source documentation
The stabilizer acts on its defining rational coordinate space.
```
instance rationalDiagonalStabilizerModule {n : ℕ} (W : Submodule ℚ (Fin n → ℝ)) :
    Module (rationalDiagonalStabilizer W) W where
…
```
Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer
lemma OAI.DukePrimeDegree.rationalDiagonalStabilizer_smul_val line 178
instance OAI.DukePrimeDegree.rationalDiagonalStabilizerTower line 182
def OAI.DukePrimeDegree.rationalDiagonalActionAt line 192
Source documentation
Evaluation of the action at a fixed vector is rational linear.
```
def rationalDiagonalActionAt {n : ℕ} (W : Submodule ℚ (Fin n → ℝ)) (w : W) :
    rationalDiagonalStabilizer W →ₗ[ℚ] W where
…
```
Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer
lemma OAI.DukePrimeDegree.rationalDiagonalActionAt_injective line 198
def OAI.DukePrimeDegree.rationalDiagonalEval line 213
Source documentation
Evaluation in any coordinate is faithful on the actual stabilizer.
```
def rationalDiagonalEval {n : ℕ} (W : Submodule ℚ (Fin n → ℝ)) (j : Fin n) :
    rationalDiagonalStabilizer W →ₐ[ℚ] ℝ where
…
```
Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer
lemma OAI.DukePrimeDegree.rationalDiagonalEval_injective line 222
theorem OAI.DukePrimeDegree.rationalDiagonalStabilizer_degree_dvd line 241
Source documentation
The field degree is forced by the concrete action on the rational coordinate space. The field structure itself is derived from faithful evaluation, rather than supplied as an input.
```
theorem rationalDiagonalStabilizer_degree_dvd {n : ℕ} (hn : 0 < n)
    (W : Submodule ℚ (Fin n → ℝ)) [FiniteDimensional ℚ W] [Nontrivial W]
    (hzero : ∀ v ∈ W, ∀ j, v j = 0 → v = 0) :
    Module.finrank ℚ (rationalDiagonalStabilizer W) ∣ Module.finrank ℚ W := by
…
```
Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer

theorem OAI.DukePrimeDegree.rationalDiagonalStabilizer_prime_dichotomy line 258

Source documentation

In prime dimension the rational diagonal stabilizer has degree one or full degree. This is applied to the actual row space of a lattice.

theorem rationalDiagonalStabilizer_prime_dichotomy {n : ℕ} (hn : n.Prime)
    (W : Submodule ℚ (Fin n → ℝ)) [FiniteDimensional ℚ W]
    (hdim : Module.finrank ℚ W = n)
    (hzero : ∀ v ∈ W, ∀ j, v j = 0 → v = 0) :
    Module.finrank ℚ (rationalDiagonalStabilizer W) = 1 ∨
      Module.finrank ℚ (rationalDiagonalStabilizer W) = n := by
…

Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer

theorem OAI.DukePrimeDegree.rationalRowSpace_prime_dichotomy line 269

Source documentation

Specialization to the rational span of the given lattice matrix.

theorem rationalRowSpace_prime_dichotomy {n : ℕ} (hn : n.Prime) (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0) :
    Module.finrank ℚ (rationalDiagonalStabilizer (rationalRowSpace g)) = 1 ∨
      Module.finrank ℚ (rationalDiagonalStabilizer (rationalRowSpace g)) = n :=
…

Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer, OAI.DukePrimeDegree.rationalRowSpace

theorem OAI.DukePrimeDegree.rationalDiagonalStabilizer_separates line 279

Source documentation

If the stabilizer has full degree, its coordinate embeddings are pairwise distinct. The real spanning condition rules out proportional coordinate functionals on the rational space.

theorem rationalDiagonalStabilizer_separates {n : ℕ}
    (W : Submodule ℚ (Fin n → ℝ)) [FiniteDimensional ℚ W] [Nontrivial W]
    (hzero : ∀ v ∈ W, ∀ j, v j = 0 → v = 0)
    (hspan : Submodule.span ℝ (W : Set (Fin n → ℝ)) = ⊤)
    (hdim : Module.finrank ℚ (rationalDiagonalStabilizer W) = Module.finrank ℚ W)
    {i j : Fin n} (hij : i ≠ j) :
    ∃ a : rationalDiagonalStabilizer W, a.val i ≠ a.val j := by
…

Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer

theorem OAI.DukePrimeDegree.rationalRowSpace_stabilizer_eq_bot_of_repeated_coordinate line 316

Source documentation

In prime dimension, a repeated coordinate embedding leaves only the rational scalars in the actual diagonal stabilizer.

theorem rationalRowSpace_stabilizer_eq_bot_of_repeated_coordinate {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    {i j : Fin n} (hij : i ≠ j)
    (heq : ∀ a : rationalDiagonalStabilizer (rationalRowSpace g), a.val i = a.val j) :
    rationalDiagonalStabilizer (rationalRowSpace g) = ⊥ := by
…

Mentions: OAI.DukePrimeDegree.rationalDiagonalStabilizer, OAI.DukePrimeDegree.rationalRowSpace

def OAI.DukePrimeDegree.blockCoordinateAlgebra line 341
Source documentation
Coordinate functions constant on each root block, viewed over ℚ.
```
def blockCoordinateAlgebra {n : ℕ} (r : Setoid (Fin n)) :
    Subalgebra ℚ (Fin n → ℝ) where
…
```
def OAI.DukePrimeDegree.rationalBlockStabilizer line 358
Source documentation
The actual rational lattice stabilizer intersected with the block centralizer. Both conditions refer to the given lattice and partition.
```
def rationalBlockStabilizer {n : ℕ} (g : G n) (r : Setoid (Fin n)) :
    Subalgebra ℚ (Fin n → ℝ) :=
…
```
theorem OAI.DukePrimeDegree.rationalBlockStabilizer_eq_bot line 365
Source documentation
In prime dimension, a nontrivial root block leaves only rational scalars in the rational block centralizer. No rationality of the real block algebra is assumed or asserted here.
```
theorem rationalBlockStabilizer_eq_bot {n : ℕ} (hn : n.Prime) (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ j, v j ≠ 0)
    (r : Setoid (Fin n)) (hblock : ∃ i j, i ≠ j ∧ r i j) :
    rationalBlockStabilizer g r = ⊥ := by
…
```
Mentions: OAI.DukePrimeDegree.rationalBlockStabilizer