OAI/NumberTheory/DukePrimeDegree/Geometry/RationalFixedVectors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Rational fixed vectors of matrix families

The common fixed-vector space of rational matrices is spanned by rational fixed vectors. This follows from rationality of matrix centralizers by adding one trivial coordinate.

  1. def OAI.DukePrimeDegree.rationalVectorCast line 20
  2. lemma OAI.DukePrimeDegree.rationalVectorCast_apply line 23
  3. lemma OAI.DukePrimeDegree.rationalVectorCast_vecMul line 26
  4. def OAI.DukePrimeDegree.trivialCoordinateExtension line 32
  5. def OAI.DukePrimeDegree.fixedRowMatrix line 36
  6. lemma OAI.DukePrimeDegree.fixedRowMatrix_commute line 40
  7. lemma OAI.DukePrimeDegree.fixedRow_of_commute line 52
  8. lemma OAI.DukePrimeDegree.rationalMatrixCast_trivialCoordinateExtension line 62
  9. theorem OAI.DukePrimeDegree.fixedVector_mem_span_rational line 72

    Source documentation

    A common real fixed vector is a real linear combination of common rational fixed vectors of the same actual matrix family.

    theorem fixedVector_mem_span_rational {n : ℕ} {κ : Type*}
    (B : κ → Matrix (Fin n) (Fin n) ℚ) (v : Fin n → ℝ)
    (hv : ∀ k, v ᵥ* rationalMatrixCast (B k) = v) :
    v ∈ Submodule.span ℝ
      (rationalVectorCast '' {q : Fin n → ℚ | ∀ k, q ᵥ* B k = q}) := by
…

    Mentions: OAI.DukePrimeDegree.rationalMatrixCast, OAI.DukePrimeDegree.rationalVectorCast

  10. theorem OAI.DukePrimeDegree.exists_nonzero_rational_fixedVector line 105