LatticeCentralizer.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Centralizers of actual lattice stabilizers

The matrix centralizer of an arbitrary family of rational matrices is spanned over ℝ by its rational matrices. Finite dimensionality reduces the family to a basis of its rational span. This applies, in particular, to the integral stabilizer of a homogeneous orbit in the lattice space. The identification of that centralizer with the real block algebra is kept separate from this rational linear algebra statement.

lemma OAI.DukePrimeDegree.commute_cast_of_mem_span line 25
lemma OAI.DukePrimeDegree.commute_rationalMatrixCast_iff line 44
theorem OAI.DukePrimeDegree.real_commutant_eq_span_rational_family line 52
Source documentation
No finiteness assumption on the matrix family is needed: only its linear span matters, and that span has finite dimension.
```
theorem real_commutant_eq_span_rational_family (B : κ → Matrix ι ι ℚ) :
    (commutatorFamily (fun k => rationalMatrixCast (B k))).ker =
      Submodule.span ℝ
        (rationalMatrixCast '' ((commutatorFamily B).ker : Set (Matrix ι ι ℚ))) := by
…
```
Mentions: OAI.DukePrimeDegree.commutatorFamily, OAI.DukePrimeDegree.rationalMatrixCast
def OAI.DukePrimeDegree.latticeOrbitStabilizer line 84
Source documentation
Integral elements whose conjugates lie in the given actual orbit group. These are precisely its lattice stabilizer in matrix coordinates.
```
def latticeOrbitStabilizer {n : ℕ} (g : G n) (H : Subgroup (G n)) :
    Subgroup (Matrix.SpecialLinearGroup (Fin n) ℤ) :=
…
```

theorem OAI.DukePrimeDegree.latticeOrbitStabilizer_fixes line 90

Source documentation

These conjugated integral elements fix the actual lattice point.

theorem latticeOrbitStabilizer_fixes {n : ℕ} (g : G n) (H : Subgroup (G n))
    (γ : latticeOrbitStabilizer g H) :
    rightAction (Quotient.mk _ g)
      ((MulAut.conj g⁻¹) (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) γ.val)) =
        (Quotient.mk _ g : X n) := by
…

Mentions: OAI.DukePrimeDegree.latticeOrbitStabilizer

theorem OAI.DukePrimeDegree.exists_latticeOrbitStabilizer_of_fixed line 106

Source documentation

Conversely, every element of the orbit group fixing this lattice point comes from its integral stabilizer.

theorem exists_latticeOrbitStabilizer_of_fixed {n : ℕ}
    (g : G n) (H : Subgroup (G n)) (h : G n) (hh : h ∈ H)
    (hfix : rightAction (Quotient.mk _ g) h = (Quotient.mk _ g : X n)) :
    ∃ γ : latticeOrbitStabilizer g H,
      (MulAut.conj g⁻¹) (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) γ.val) = h := by
…

Mentions: OAI.DukePrimeDegree.latticeOrbitStabilizer

def OAI.DukePrimeDegree.latticeStabilizerMatrix line 126
Source documentation
The rational matrices of the actual integral orbit stabilizer.
```
def latticeStabilizerMatrix {n : ℕ} (g : G n) (H : Subgroup (G n))
    (γ : latticeOrbitStabilizer g H) : Matrix (Fin n) (Fin n) ℚ :=
…
```
Mentions: OAI.DukePrimeDegree.latticeOrbitStabilizer
theorem OAI.DukePrimeDegree.latticeStabilizer_commutant_rational line 133
Source documentation
The centralizer of an actual homogeneous-orbit stabilizer is rational. The orbit group is arbitrary; no density or homogeneity classification is built into this statement.
```
theorem latticeStabilizer_commutant_rational {n : ℕ} (g : G n) (H : Subgroup (G n)) :
    (commutatorFamily (fun γ => rationalMatrixCast (latticeStabilizerMatrix g H γ))).ker =
      Submodule.span ℝ (rationalMatrixCast ''
        ((commutatorFamily (latticeStabilizerMatrix g H)).ker :
          Set (Matrix (Fin n) (Fin n) ℚ))) :=
…
```
Mentions: OAI.DukePrimeDegree.commutatorFamily, OAI.DukePrimeDegree.rationalMatrixCast, OAI.DukePrimeDegree.latticeStabilizerMatrix