CartanDecomposition.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cartan models for the real triangular adjoint action

The nilpotent ideal and Cartan subalgebra span the algebra, and the Cartan subalgebra maps onto the actual canonical height quotient.

theorem OAI.PolycyclicRecognition.triangular_cartan_spanning line 21
theorem OAI.PolycyclicRecognition.cartan_height_surjective line 28
Source documentation
Every height has a representative in the Cartan subalgebra.
```
theorem cartan_height_surjective (H : LieSubalgebra ℝ L) [H.IsCartanSubalgebra] :
    Function.Surjective ((heightProjection T.character).comp H.subtype) := by
…
```
Mentions: OAI.PolycyclicRecognition.heightProjection

theorem OAI.PolycyclicRecognition.exists_cartan_model line 44

Source documentation

Existence and the Lie-algebra assertions of the manuscript's Cartan model lemma. All terms are constructed from the actual adjoint basis.

theorem exists_cartan_model :
    ∃ H : LieSubalgebra ℝ L, ∃ _ : H.IsCartanSubalgebra,
      LieRing.IsNilpotent (cartanRootIdeal H) ∧
      cartanRootIdeal H ≤ derivedSeries ℝ L 1 ∧
      (cartanRootIdeal H).toSubmodule ⊔ H.toSubmodule = ⊤ ∧
      Function.Surjective ((heightProjection T.character).comp H.subtype) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.heightProjection

theorem OAI.PolycyclicRecognition.cartanRootIdeal_eq_bot_of_nilpotent line 58
Source documentation
A nilpotent ambient algebra has no nonzero Cartan roots.
```
theorem cartanRootIdeal_eq_bot_of_nilpotent
    (H : LieSubalgebra ℝ L) [H.IsCartanSubalgebra] [LieRing.IsNilpotent L] :
    cartanRootIdeal H = ⊥ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.cartanRootIdeal_eq_bot_iff line 71
Source documentation
The model's nilpotent root ideal vanishes exactly in the nilpotent case.
```
theorem cartanRootIdeal_eq_bot_iff (T : TriangularAdjoint L n)
    (H : LieSubalgebra ℝ L) [H.IsCartanSubalgebra] :
    cartanRootIdeal H = ⊥ ↔ LieRing.IsNilpotent L := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal