PairedCoordinateAlgebra.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Rational operators scalar on two coordinates

The algebra below consists of concrete real matrices preserving the rational row space and acting by a common scalar on two specified coordinate functionals. In prime dimension, the generic-lattice condition forces this algebra to contain only rational scalar matrices. No diagonal condition is imposed on the other coordinates. This is the arithmetic form needed when singleton root blocks are still present.

def OAI.DukePrimeDegree.pairedCoordinateAlgebra line 26
Source documentation
A concrete matrix algebra, with the common coordinate eigenvalue recorded as its first component.
```
def pairedCoordinateAlgebra {n : ℕ} (W : Submodule ℚ (Fin n → ℝ))
    (i j : Fin n) : Subalgebra ℚ (ℝ × Matrix (Fin n) (Fin n) ℝ) where
…
```
def OAI.DukePrimeDegree.pairedCoordinateEval line 78

theorem OAI.DukePrimeDegree.pairedCoordinateEval_injective line 89

Source documentation

The generic coordinate functional is faithful on the concrete matrix algebra: it detects an operator on the rational space, which spans over ℝ.

theorem pairedCoordinateEval_injective {n : ℕ}
    (W : Submodule ℚ (Fin n → ℝ)) (i j : Fin n)
    (hzero : ∀ w ∈ W, ∀ k, w k = 0 → w = 0)
    (hspan : Submodule.span ℝ (W : Set (Fin n → ℝ)) = ⊤) :
    Function.Injective (pairedCoordinateEval W i j) := by
…

Mentions: OAI.DukePrimeDegree.pairedCoordinateEval

instance OAI.DukePrimeDegree.pairedCoordinateModule line 118
instance OAI.DukePrimeDegree.pairedCoordinateTower line 145
def OAI.DukePrimeDegree.pairedCoordinateActionAt line 151
theorem OAI.DukePrimeDegree.pairedCoordinateActionAt_injective line 157

theorem OAI.DukePrimeDegree.pairedCoordinateAlgebra_eq_bot line 173

Source documentation

Prime dimension rules out non-scalar operators with two equal coordinate eigenvalues, even when their action on the remaining coordinates is arbitrary.

theorem pairedCoordinateAlgebra_eq_bot {n : ℕ} (hn : n.Prime)
    (W : Submodule ℚ (Fin n → ℝ)) [FiniteDimensional ℚ W]
    (hdim : Module.finrank ℚ W = n)
    (hzero : ∀ v ∈ W, ∀ k, v k = 0 → v = 0)
    (hspan : Submodule.span ℝ (W : Set (Fin n → ℝ)) = ⊤)
    (i j : Fin n) (hij : i ≠ j) : pairedCoordinateAlgebra W i j = ⊥ := by
…

Mentions: OAI.DukePrimeDegree.pairedCoordinateAlgebra

theorem OAI.DukePrimeDegree.rationalRowSpace_pairedCoordinateAlgebra_eq_bot line 217
Source documentation
Actual lattice specialization. The rational structure is the row space of the supplied matrix, not an independent field-action assumption.
```
theorem rationalRowSpace_pairedCoordinateAlgebra_eq_bot {n : ℕ}
    (hn : n.Prime) (g : G n)
    (hzero : ∀ v ∈ rowLattice g.val, v ≠ 0 → ∀ k, v k ≠ 0)
    (i j : Fin n) (hij : i ≠ j) :
    pairedCoordinateAlgebra (rationalRowSpace g) i j = ⊥ :=
…
```
Mentions: OAI.DukePrimeDegree.pairedCoordinateAlgebra, OAI.DukePrimeDegree.rationalRowSpace