SimultaneousAdjointBasis.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The simultaneous-basis form of Lie's theorem

Mathlib's Lie theorem supplies a common eigenvector for a solvable split action. We iterate it on invariant quotients and lift each quotient basis, obtaining the single upper triangular basis required by TriangularAdjoint.

theorem OAI.PolycyclicRecognition.exists_upperTriangular_lieModule_basis line 25

Source documentation

A finite-dimensional split action of a solvable split Lie algebra has a simultaneous upper triangular basis.

theorem exists_upperTriangular_lieModule_basis {𝕜 : Type*} [Field 𝕜] [CharZero 𝕜]
    (L V : Type*)
    [LieRing L] [LieAlgebra 𝕜 L] [LieAlgebra.IsSolvable L]
    [AddCommGroup V] [Module 𝕜 V] [LieRingModule L V] [LieModule 𝕜 L V]
    [FiniteDimensional 𝕜 V] [LieModule.IsTriangularizable 𝕜 L V] :
    ∃ (n : ℕ) (b : Basis (Fin n) 𝕜 V),
      ∀ x : L, (LinearMap.toMatrix b b (LieModule.toEnd 𝕜 L V x)).IsUpperTriangular := by
…

theorem OAI.PolycyclicRecognition.nonempty_triangularAdjoint_of_split line 112
Source documentation
Applying the proved simultaneous-basis theorem to the adjoint module produces exactly the basis structure used by the height construction.
```
theorem nonempty_triangularAdjoint_of_split (L : Type*)
    [LieRing L] [LieAlgebra ℝ L] [LieAlgebra.IsSolvable L]
    [FiniteDimensional ℝ L] [LieModule.IsTriangularizable ℝ L L] :
    ∃ n : ℕ, Nonempty (TriangularAdjoint L n) := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint