RationalCentralizer.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Rationality of matrix centralizers

The commutant of a finite collection of rational matrices is spanned over the reals by its rational matrices. This is the linear algebra part of the homogeneous-orbit rationality step: it uses exactness of scalar extension, and does not assert that a lattice stabilizer is dense in a block group.

theorem OAI.DukePrimeDegree.kernel_spanned_of_baseChange line 32

Source documentation

Exact scalar extension expresses every real kernel vector as a real linear combination of rational kernel vectors.

private theorem kernel_spanned_of_baseChange
    (f : V →ₗ[ℚ] U) (f' : V' →ₗ[ℝ] U')
    (cV : V →ₗ[ℚ] V') (cU : U →ₗ[ℚ] U')
    (hV : IsBaseChange ℝ cV) (hU : IsBaseChange ℝ cU)
    (hcomm : cU.comp f = (f'.restrictScalars ℚ).comp cV) :
    f'.ker = Submodule.span ℝ (cV '' (f.ker : Set V)) := by
…

def OAI.DukePrimeDegree.rationalMatrixCast line 73
Source documentation
Entrywise rational-to-real scalar extension for matrices.
```
def rationalMatrixCast : Matrix ι ι ℚ →ₗ[ℚ] Matrix ι ι ℝ :=
…
```
lemma OAI.DukePrimeDegree.rationalMatrixCast_apply line 76
lemma OAI.DukePrimeDegree.rationalMatrixCast_isBaseChange line 79

def OAI.DukePrimeDegree.commutatorFamily line 84

Source documentation

The equations for commuting with every member of a matrix family.

def commutatorFamily {K : Type*} [Field K] (B : κ → Matrix ι ι K) :
    Matrix ι ι K →ₗ[K] (κ → Matrix ι ι K) :=
…

lemma OAI.DukePrimeDegree.commutatorFamily_apply line 88
lemma OAI.DukePrimeDegree.mem_commutatorFamily_ker line 92

theorem OAI.DukePrimeDegree.real_commutant_eq_span_rational line 101

Source documentation

The exact rationality statement for a finite matrix centralizer.

theorem real_commutant_eq_span_rational (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

theorem OAI.DukePrimeDegree.mem_span_rational_commutant line 120
Source documentation
Every real matrix commuting with the given rational matrices is a real linear combination of rational matrices with the same property.
```
theorem mem_span_rational_commutant (B : κ → Matrix ι ι ℚ)
    (M : Matrix ι ι ℝ) (hM : ∀ k, Commute M (rationalMatrixCast (B k))) :
    M ∈ Submodule.span ℝ
      (rationalMatrixCast '' ((commutatorFamily B).ker : Set (Matrix ι ι ℚ))) := by
…
```
Mentions: OAI.DukePrimeDegree.rationalMatrixCast, OAI.DukePrimeDegree.commutatorFamily