CartanGenerators.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The subalgebra generated by nonzero roots

The subalgebra generated by the nonzero root spaces is already an ideal. Thus taking the ideal generated by them in the Cartan construction does not enlarge the subgroup that must later be integrated.

def OAI.PolycyclicRecognition.cartanRootSubalgebra line 21
theorem OAI.PolycyclicRecognition.cartanRootSubalgebra_stable line 25
def OAI.PolycyclicRecognition.cartanRootSubmodule line 46
Source documentation
Regard the generated subalgebra as a module for the Cartan subalgebra.
```
def cartanRootSubmodule : LieSubmodule ℝ H L where
…
```
theorem OAI.PolycyclicRecognition.cartanRootSubalgebra_sup_cartan line 50
theorem OAI.PolycyclicRecognition.cartanRootSubalgebra_ideal line 69
theorem OAI.PolycyclicRecognition.cartanRootSubalgebra_eq_ideal line 82
Source documentation
The actual generated subalgebra equals the ideal used in the model.
```
theorem cartanRootSubalgebra_eq_ideal [FiniteDimensional ℝ L]
    {n : ℕ} (T : TriangularAdjoint L n) :
    (cartanRootSubalgebra H).toSubmodule = (cartanRootIdeal H).toSubmodule := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootSubalgebra, OAI.PolycyclicRecognition.cartanRootIdeal