CartanWeights.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cartan roots descend to and separate canonical height

The roots vanish on the canonical nilpotent kernel. Conversely, vanishing of all nonzero roots forces zero canonical height. Thus the weight coordinates used by the box estimates are coordinates on the actual canonical quotient.

theorem OAI.PolycyclicRecognition.cartan_weight_zero_of_height_zero line 27
theorem OAI.PolycyclicRecognition.cartan_ad_nilpotent_of_weights_zero line 33
def OAI.PolycyclicRecognition.cartanHeightSection line 50
Source documentation
Choose a linear Cartan representative of each height.
```
def cartanHeightSection : HeightSpace T.character →ₗ[ℝ] H :=
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.cartanHeightSection_height line 54
def OAI.PolycyclicRecognition.cartanHeightWeight line 61
Source documentation
A Cartan root as a linear form on the canonical height quotient.
```
def cartanHeightWeight (χ : Weight ℝ H L) : HeightSpace T.character →ₗ[ℝ] ℝ :=
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.cartanHeightWeight_projection line 64
theorem OAI.PolycyclicRecognition.cartanHeightWeights_separate line 77
Source documentation
The finite family of nonzero Cartan roots separates canonical height.
```
theorem cartanHeightWeights_separate (w : HeightSpace T.character)
    (hw : ∀ χ : Weight ℝ H L, χ.IsNonZero → cartanHeightWeight T H χ w = 0) : w = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.cartanHeightWeight
theorem OAI.PolycyclicRecognition.trace_ad_eq_sum_cartan_roots line 93
Source documentation
The trace of the adjoint action is the dimension-weighted sum of the actual Cartan roots, including their nonsemisimple parts.
```
theorem trace_ad_eq_sum_cartan_roots (T : TriangularAdjoint L n) (h : H) :
    LinearMap.trace ℝ L (LieAlgebra.ad ℝ L h) =
      ∑ χ : Weight ℝ H L, Module.finrank ℝ (rootSpace H χ) • χ h := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint

theorem OAI.PolycyclicRecognition.balanced_cartanHeightWeights line 109

Source documentation

Unimodularity supplies the balancing relation on the canonical quotient.

theorem balanced_cartanHeightWeights
    (hunimod : ∀ x : L, LinearMap.trace ℝ L (LieAlgebra.ad ℝ L x) = 0)
    (w : HeightSpace T.character) :
    ∑ χ : Weight ℝ H L,
      (Module.finrank ℝ (rootSpace H χ) : ℝ) * cartanHeightWeight T H χ w = 0 := by
…

Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.cartanHeightWeight