BlockNormalizer.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The connected normalizer of the block algebra

Conjugation permutes the primitive block projections. In a connected family starting at the identity these projections cannot move, since their diagonal coordinates remain idempotents. Consequently the identity component of the block-algebra normalizer preserves every block.

def OAI.DukePrimeDegree.blockProjection line 23
lemma OAI.DukePrimeDegree.blockProjection_mem line 27
lemma OAI.DukePrimeDegree.blockProjection_mul_self line 30
lemma OAI.DukePrimeDegree.continuous_idempotent_constant line 39
def OAI.DukePrimeDegree.blockScalarNormalizer line 53
Source documentation
The concrete normalizer of the real block-scalar matrix algebra.
```
def blockScalarNormalizer {n : ℕ} (r : Setoid (Fin n)) : Subgroup (G n) where
…
```

theorem OAI.DukePrimeDegree.connected_normalizer_fixes_blockProjection line 68

Source documentation

A connected family of normalizer matrices through the identity fixes each block projection individually.

theorem connected_normalizer_fixes_blockProjection {n : ℕ}
    (r : Setoid (Fin n)) {T : Type*} [TopologicalSpace T] [PreconnectedSpace T]
    (f : T → G n) (hf : Continuous f) (t₀ : T) (h₀ : f t₀ = 1)
    (hnorm : ∀ t, f t ∈ blockScalarNormalizer r) (t : T) (k : Fin n) :
    slMatrixConjugation (f t) (blockProjection r k) = blockProjection r k := by
…

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

lemma OAI.DukePrimeDegree.slMatrixConjugation_eq_self_iff line 99

theorem OAI.DukePrimeDegree.connected_normalizer_mem_blockMatrixGroup line 114

Source documentation

Every matrix in such a connected family preserves each coordinate block. This is the connected part of the normalizer calculation.

theorem connected_normalizer_mem_blockMatrixGroup {n : ℕ}
    (r : Setoid (Fin n)) {T : Type*} [TopologicalSpace T] [PreconnectedSpace T]
    (f : T → G n) (hf : Continuous f) (t₀ : T) (h₀ : f t₀ = 1)
    (hnorm : ∀ t, f t ∈ blockScalarNormalizer r) (t : T) :
    f t ∈ blockMatrixGroup r := by
…

Mentions: OAI.DukePrimeDegree.blockScalarNormalizer, OAI.DukePrimeDegree.blockMatrixGroup

theorem OAI.DukePrimeDegree.blockScalarNormalizer_identityComponent_le line 139
Source documentation
The identity component of the block-algebra normalizer is contained in the actual block-diagonal matrix subgroup.
```
theorem blockScalarNormalizer_identityComponent_le {n : ℕ}
    (r : Setoid (Fin n))
    (g : Subgroup.connectedComponentOfOne (blockScalarNormalizer r)) :
    g.val.val ∈ blockMatrixGroup r := by
…
```
Mentions: OAI.DukePrimeDegree.blockScalarNormalizer, OAI.DukePrimeDegree.blockMatrixGroup