CartanModel.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent ideal in the Cartan model

Nonzero generalized root vectors lie in the derived algebra. Their generated ideal is nilpotent for an actual triangular adjoint representation, and its sum with the Cartan subalgebra is the full Lie algebra.

theorem OAI.PolycyclicRecognition.mem_submodule_of_generalized_eigenvector line 22

Source documentation

A generalized eigenvector for a nonzero eigenvalue lies in every submodule containing the image of the operator.

theorem mem_submodule_of_generalized_eigenvector
    {V : Type*} [AddCommGroup V] [Module ℝ V]
    (S : Submodule ℝ V) (f : Module.End ℝ V) (hf : ∀ v, f v ∈ S)
    {a : ℝ} (ha : a ≠ 0) (k : ℕ) (v : V)
    (hv : ((f - a • 1) ^ k) v = 0) : v ∈ S := by
…

theorem OAI.PolycyclicRecognition.nonzero_root_le_ideal line 46

Source documentation

Nonzero generalized roots lie in every ideal containing the brackets.

theorem nonzero_root_le_ideal (I : LieIdeal ℝ L)
    (hI : ∀ x y : L, ⁅x, y⁆ ∈ I)
    (χ : Weight ℝ H L) (hχ : χ.IsNonZero) : rootSpace H χ ≤ I.restr H := by
…

def OAI.PolycyclicRecognition.cartanRootIdeal line 61
Source documentation
The ideal generated by the nonzero generalized root spaces.
```
def cartanRootIdeal : LieIdeal ℝ L :=
…
```
theorem OAI.PolycyclicRecognition.cartanRootIdeal_le_derived line 64
theorem OAI.PolycyclicRecognition.cartanRootIdeal_le_kernel line 74
Source documentation
The real upper triangular adjoint representation makes the nonzero-root ideal a subideal of the canonical nilpotent kernel.
```
theorem cartanRootIdeal_le_kernel {n : ℕ} (T : TriangularAdjoint L n) :
    cartanRootIdeal H ≤ T.kernelIdeal := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.cartanRootIdeal_nilpotent line 83
Source documentation
The Cartan-model ideal is genuinely nilpotent, not assumed nilpotent.
```
theorem cartanRootIdeal_nilpotent [FiniteDimensional ℝ L]
    {n : ℕ} (T : TriangularAdjoint L n) : LieRing.IsNilpotent (cartanRootIdeal H) := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.cartanRootIdeal_sup_cartan line 90
Source documentation
The Cartan subalgebra and the nonzero-root ideal span the full algebra. Their overlap is retained; no complementary-subalgebra assertion is used.
```
theorem cartanRootIdeal_sup_cartan [FiniteDimensional ℝ L]
    [LieModule.IsTriangularizable ℝ H L] :
    (cartanRootIdeal H).toSubmodule ⊔ H.toSubmodule = ⊤ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal