TriangularMatrixLieAlgebra.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Solvability of a faithful triangular matrix representation

Successive derived algebras vanish on successively larger bands above the diagonal. This proves the solvability needed after differentiating a triangular Lie-group realization, without assuming that passage from the group to its Lie algebra.

def OAI.PolycyclicRecognition.matrixUpperGap line 26
Source documentation
Matrices whose entries vanish below the kth upper diagonal.
```
def matrixUpperGap (n k : ℕ) : Submodule ℝ (Matrix (Fin n) (Fin n) ℝ) where
…
```
theorem OAI.PolycyclicRecognition.matrixUpperGap_zero_iff line 36
theorem OAI.PolycyclicRecognition.matrixUpperGap_anti line 44
theorem OAI.PolycyclicRecognition.matrixUpperGap_mul line 49
theorem OAI.PolycyclicRecognition.upperTriangular_mul_diagonal line 60

theorem OAI.PolycyclicRecognition.matrixUpperGap_lie line 73

Source documentation

A commutator improves the vanishing band by at least one.

theorem matrixUpperGap_lie {n k : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ}
    (hA : A ∈ matrixUpperGap n k) (hB : B ∈ matrixUpperGap n k) :
    ⁅A, B⁆ ∈ matrixUpperGap n (k + 1) := by
…

Mentions: OAI.PolycyclicRecognition.matrixUpperGap

theorem OAI.PolycyclicRecognition.lieAlgebra_isSolvable_of_triangular_representation line 100

Source documentation

A faithful finite-dimensional triangular representation has a solvable Lie algebra. The proof uses actual matrix entries, not a solvability assumption about the source group.

theorem lieAlgebra_isSolvable_of_triangular_representation
    {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n : ℕ}
    (ρ : L →ₗ⁅ℝ⁆ Matrix (Fin n) (Fin n) ℝ)
    (hρ : Function.Injective ρ) (htri : ∀ x, (ρ x).IsUpperTriangular) :
    LieAlgebra.IsSolvable L := by
…