ActiveBlockProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Local fixation of a nontrivial block projection

The commutant of the root directions can have a large part on singleton coordinates. That part does not obstruct local fixation of a nontrivial block projection: after subtracting the original projection it is an idempotent tending to zero. A nonzero idempotent has norm at least one. Thus this local step needs no hypothesis excluding singleton blocks.

lemma OAI.DukePrimeDegree.matrix_idempotent_eq_zero_of_norm_lt_one line 22
lemma OAI.DukePrimeDegree.matrix_idempotent_eq_of_absorbs line 32
lemma OAI.DukePrimeDegree.commute_single_root_entries line 42
lemma OAI.DukePrimeDegree.blockProjection_eq_diagonal line 60

theorem OAI.DukePrimeDegree.commutant_mul_nontrivial_blockProjection line 66

Source documentation

Commutation with the within-block root directions makes the action on a nontrivial block scalar, even if singleton blocks are present.

theorem commutant_mul_nontrivial_blockProjection {n : ℕ}
    (r : Setoid (Fin n)) (k : Fin n) (hk : ∃ l, k ≠ l ∧ r k l)
    (M : Matrix (Fin n) (Fin n) ℝ)
    (hM : ∀ i j, i ≠ j → r i j → Commute M (Matrix.single i j (1 : ℝ))) :
    M * blockProjection r k = M k k • blockProjection r k ∧
      blockProjection r k * M = M k k • blockProjection r k := by
…

Mentions: OAI.DukePrimeDegree.blockProjection

theorem OAI.DukePrimeDegree.commutant_idempotent_eq_blockProjection line 112

theorem OAI.DukePrimeDegree.nontrivial_blockProjection_fixed_near_identity line 139

Source documentation

Every element sufficiently near the identity in the actual subgroup fixes each specified nontrivial block projection. Singleton blocks are allowed throughout this statement.

theorem nontrivial_blockProjection_fixed_near_identity {n : ℕ}
    (L : Subgroup (G n)) (r : Setoid (Fin n))
    (hroot : ∀ i j (hij : i ≠ j), r i j →
      ∀ t : ℝ, Matrix.SpecialLinearGroup.transvection hij t ∈ L)
    (hsupport : ∀ V ∈ matrixVelocitySpace L, ∀ i j, ¬r i j → V i j = 0)
    (k : Fin n) (hk : ∃ l, k ≠ l ∧ r k l) :
    {g : L | slMatrixConjugation g.val (blockProjection r k) = blockProjection r k} ∈
      𝓝 (1 : L) := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace, OAI.DukePrimeDegree.slMatrixConjugation, OAI.DukePrimeDegree.blockProjection