BlockDiagonalAlgebra.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The algebra of scalars on root blocks

For a partition of the coordinate indices, the block-scalar algebra is the actual diagonal matrix algebra whose diagonal is constant on each block. Its dimension is the number of blocks. It is also the common centralizer of the full diagonal algebra and the elementary root matrices within the blocks. These are algebraic statements, without any homogeneous-measure classification assumption.

def OAI.DukePrimeDegree.blockScalarAlgHom line 29
Source documentation
The diagonal representation of functions on the coordinate blocks.
```
def blockScalarAlgHom (r : Setoid ι) :
    (Quotient r → ℝ) →ₐ[ℝ] Matrix ι ι ℝ where
…
```
lemma OAI.DukePrimeDegree.blockScalarAlgHom_apply line 41
lemma OAI.DukePrimeDegree.blockScalarAlgHom_injective line 44
def OAI.DukePrimeDegree.blockScalarAlgebra line 54
Source documentation
The real algebra of diagonal matrices constant on each root block.
```
def blockScalarAlgebra (r : Setoid ι) : Subalgebra ℝ (Matrix ι ι ℝ) :=
…
```
lemma OAI.DukePrimeDegree.mem_blockScalarAlgebra_iff line 57
theorem OAI.DukePrimeDegree.finrank_blockScalarAlgebra line 77
Source documentation
The dimension counts the actual coordinate blocks.
```
theorem finrank_blockScalarAlgebra (r : Setoid ι) :
    Module.finrank ℝ (blockScalarAlgebra r) = Nat.card (Quotient r) := by
…
```
Mentions: OAI.DukePrimeDegree.blockScalarAlgebra

theorem OAI.DukePrimeDegree.matrix_eq_diagonal_of_commute_diagonals line 86

Source documentation

Commutation with all diagonal matrices forces a matrix to be diagonal.

theorem matrix_eq_diagonal_of_commute_diagonals (M : Matrix ι ι ℝ)
    (hM : ∀ c : ι → ℝ, Commute M (Matrix.diagonal c)) :
    M = Matrix.diagonal (fun i => M i i) := by
…

theorem OAI.DukePrimeDegree.diagonal_commute_transvection_iff line 100
Source documentation
A diagonal matrix commutes with an elementary root exactly when its two corresponding diagonal entries coincide.
```
theorem diagonal_commute_transvection_iff (c : ι → ℝ) {i j : ι} (hij : i ≠ j) :
    Commute (Matrix.diagonal c) (Matrix.transvection i j 1) ↔ c i = c j := by
…
```

theorem OAI.DukePrimeDegree.mem_blockScalarAlgebra_iff_commutes line 125

Source documentation

The block-scalar algebra is the exact common matrix centralizer of diagonals and within-block root generators.

theorem mem_blockScalarAlgebra_iff_commutes (r : Setoid ι) (M : Matrix ι ι ℝ) :
    M ∈ blockScalarAlgebra r ↔
      (∀ c : ι → ℝ, Commute M (Matrix.diagonal c)) ∧
      ∀ i j, i ≠ j → r i j → Commute M (Matrix.transvection i j 1) := by
…

Mentions: OAI.DukePrimeDegree.blockScalarAlgebra

theorem OAI.DukePrimeDegree.commute_blockScalars_iff line 152
Source documentation
A matrix commuting with every block scalar has no entries between different coordinate blocks.
```
theorem commute_blockScalars_iff (r : Setoid ι) (M : Matrix ι ι ℝ) :
    (∀ A ∈ blockScalarAlgebra r, Commute M A) ↔
      ∀ i j, ¬ r i j → M i j = 0 := by
…
```
Mentions: OAI.DukePrimeDegree.blockScalarAlgebra
theorem OAI.DukePrimeDegree.blockScalarAlgebra_eq_bot_of_universal line 178
Source documentation
A single root block has only scalar matrices in its centralizer.
```
theorem blockScalarAlgebra_eq_bot_of_universal [Nonempty ι] (r : Setoid ι)
    (hr : ∀ i j, r i j) : blockScalarAlgebra r = ⊥ := by
…
```
Mentions: OAI.DukePrimeDegree.blockScalarAlgebra
theorem OAI.DukePrimeDegree.universal_of_blockScalarAlgebra_eq_bot line 197
Source documentation
Conversely, a proper partition always has a non-scalar block projection. This turns a scalar-centralizer conclusion into one block.
```
theorem universal_of_blockScalarAlgebra_eq_bot (r : Setoid ι)
    (hbot : blockScalarAlgebra r = ⊥) : ∀ i j, r i j := by
…
```
Mentions: OAI.DukePrimeDegree.blockScalarAlgebra