CartanTrace.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Unimodularity on the Cartan ideal

The quotient of the ambient algebra by its nonzero-root ideal is generated by the nilpotent Cartan subalgebra. Its induced adjoint operators are nilpotent. Consequently restriction to the ideal preserves the trace.

theorem OAI.PolycyclicRecognition.cartan_quotient_ad_nilpotent line 25
theorem OAI.PolycyclicRecognition.trace_cartanRootIdeal_eq_zero line 59
Source documentation
The trace-zero action required by the support data follows from ambient unimodularity, even when the Cartan subgroup overlaps the root ideal.
```
theorem trace_cartanRootIdeal_eq_zero
    (hunimod : ∀ x : L, LinearMap.trace ℝ L (ad ℝ L x) = 0) (h : H) :
    LinearMap.trace ℝ (cartanRootIdeal H) (toEnd ℝ H (cartanRootIdeal H) h) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal