DiagonalCommutatorCurve.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Diagonal commutator curves and maximal root blocks

For a subgroup normalized by the split diagonal group, conjugating any member by a small diagonal and taking a commutator produces a curve in the subgroup. Its velocity has explicit entries. Root extraction then forces conjugated coordinate projections to preserve every maximal root block; connectedness gives global block preservation.

def OAI.DukePrimeDegree.diagonalCommutatorCurve line 22
lemma OAI.DukePrimeDegree.diagonalCommutatorCurve_zero line 26
lemma OAI.DukePrimeDegree.diagonalCommutatorCurve_entry line 31
def OAI.DukePrimeDegree.diagonalCommutatorVelocity line 41
Source documentation
The actual velocity of the diagonal commutator curve.
```
def diagonalCommutatorVelocity {n : ℕ} (ell : Fin n → ℝ) (g : G n) :
    Matrix (Fin n) (Fin n) ℝ :=
…
```
lemma OAI.DukePrimeDegree.hasDerivAt_diagonalCommutatorCurve line 45
lemma OAI.DukePrimeDegree.hasMatrixVelocity_diagonalCommutatorCurve line 61
def OAI.DukePrimeDegree.coordinateProjectionWeights line 68
Source documentation
Integral zero-sum weights detecting the k-th coordinate projection.
```
def coordinateProjectionWeights {n : ℕ} (k a : Fin n) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.coordinateProjectionWeights_sum line 71
lemma OAI.DukePrimeDegree.diagonalCommutatorVelocity_coordinate line 75

theorem OAI.DukePrimeDegree.projection_products_zero_of_maximal_roots line 100

Source documentation

If every nonzero root found in L belongs to r, conjugated coordinate projections have no entries between different r-blocks.

theorem projection_products_zero_of_maximal_roots {n : ℕ}
    (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n)))
    (hnormal : ∀ (ell : Fin n → ℝ) (hsum : ∑ a, ell a = 0) (t : ℝ),
      ∀ g ∈ L, diagonalOneParameter ell hsum t * g * diagonalOneParameter ell hsum (-t) ∈ L)
    (r : Setoid (Fin n))
    (hmax : ∀ (a b : Fin n) (hab : a ≠ b) (c : ℝ), c ≠ 0 →
      Matrix.SpecialLinearGroup.transvection hab c ∈ L → r a b)
    (g : L) (a b : Fin n) (hab : ¬ r a b) (k : Fin n) :
    g.val.val a k * g.val⁻¹.val k b = 0 := by
…

theorem OAI.DukePrimeDegree.blockIntersection_isOpen_of_maximal_roots line 131

Source documentation

Root maximality makes the block-preserving subgroup open in the actual homogeneous orbit group L, including when L is disconnected.

theorem blockIntersection_isOpen_of_maximal_roots {n : ℕ}
    (L : Subgroup (G n)) (hclosed : IsClosed (L : Set (G n)))
    (hnormal : ∀ (ell : Fin n → ℝ) (hsum : ∑ a, ell a = 0) (t : ℝ),
      ∀ g ∈ L, diagonalOneParameter ell hsum t * g * diagonalOneParameter ell hsum (-t) ∈ L)
    (r : Setoid (Fin n))
    (hmax : ∀ (a b : Fin n) (hab : a ≠ b) (c : ℝ), c ≠ 0 →
      Matrix.SpecialLinearGroup.transvection hab c ∈ L → r a b) :
    IsOpen (((blockMatrixGroup r).comap L.subtype : Subgroup L) : Set L) :=
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup

theorem OAI.DukePrimeDegree.connected_subgroup_le_blocks_of_maximal_roots line 145

Source documentation

A connected, closed subgroup normalized by the split diagonal group preserves the partition given by its maximal root subgroups. This uses only the explicit commutator curves and connectedness.

theorem connected_subgroup_le_blocks_of_maximal_roots {n : ℕ}
    (L : Subgroup (G n)) [PreconnectedSpace L]
    (hclosed : IsClosed (L : Set (G n)))
    (hnormal : ∀ (ell : Fin n → ℝ) (hsum : ∑ a, ell a = 0) (t : ℝ),
      ∀ g ∈ L, diagonalOneParameter ell hsum t * g * diagonalOneParameter ell hsum (-t) ∈ L)
    (r : Setoid (Fin n))
    (hmax : ∀ (a b : Fin n) (hab : a ≠ b) (c : ℝ), c ≠ 0 →
      Matrix.SpecialLinearGroup.transvection hab c ∈ L → r a b) :
    L ≤ blockMatrixGroup r :=
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup