TriangularAdjointEmbedding.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

A triangular adjoint basis from a faithful triangular representation

Order matrix units by increasing row and decreasing column. Commuting with an upper triangular matrix then gives an upper triangular operator. Restricting this action to a faithfully embedded Lie algebra supplies its actual adjoint basis.

def OAI.PolycyclicRecognition.triangularMatrixOrder line 27
Source documentation
Rows increase and columns decrease in the ordering of matrix units.
```
def triangularMatrixOrder (n : ℕ) : Fin n × Fin n ≃ Fin (n * n) :=
…
```
theorem OAI.PolycyclicRecognition.triangularMatrixOrder_val line 30
def OAI.PolycyclicRecognition.triangularMatrixCoordinates line 34
Source documentation
Matrix coordinates with respect to this ordering.
```
def triangularMatrixCoordinates (n : ℕ) :
    Matrix (Fin n) (Fin n) ℝ ≃ₗ[ℝ] (Fin (n * n) → ℝ) where
…
```
theorem OAI.PolycyclicRecognition.triangularMatrixCoordinates_apply line 44
theorem OAI.PolycyclicRecognition.triangularMatrixCoordinates_symm_apply line 49
def OAI.PolycyclicRecognition.triangularMatrixBasis line 55
Source documentation
The ordered matrix units.
```
def triangularMatrixBasis (n : ℕ) :
    Basis (Fin (n * n)) ℝ (Matrix (Fin n) (Fin n) ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.triangularMatrixBasis_apply line 59
theorem OAI.PolycyclicRecognition.triangularMatrixBasis_repr_apply line 68
theorem OAI.PolycyclicRecognition.triangularMatrixBasis_repr line 74
theorem OAI.PolycyclicRecognition.matrix_commutator_single_zero line 80

theorem OAI.PolycyclicRecognition.upperTriangular_matrix_ad line 113

Source documentation

Commutation by an upper triangular matrix is upper triangular on the full matrix algebra in the ordered matrix-unit basis.

theorem upperTriangular_matrix_ad {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.IsUpperTriangular) :
    (LinearMap.toMatrix (triangularMatrixBasis n) (triangularMatrixBasis n)
      (LieAlgebra.ad ℝ (Matrix (Fin n) (Fin n) ℝ) A)).IsUpperTriangular := by
…

Mentions: OAI.PolycyclicRecognition.triangularMatrixBasis

theorem OAI.PolycyclicRecognition.nonempty_triangularAdjoint_of_triangular_representation line 127

Source documentation

A faithful triangular matrix representation produces the precise simultaneous adjoint basis used by the height development.

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

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint