CartanWeightDilation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Exact dilations of generalized Cartan weight spaces

Scalar multiplication by exp (χ h) on every generalized root space defines an actual Lie automorphism. The nilpotent parts of the Cartan action do not enter this construction. These are the exact weight dilations used in the box-translation argument.

def OAI.PolycyclicRecognition.cartanWeightDecomposition line 28
def OAI.PolycyclicRecognition.cartanWeightScale line 39
Source documentation
Scalar dilation on the actual generalized-root direct sum.
```
def cartanWeightScale (h : H) : L →ₗ[ℝ] L := by
…
```
theorem OAI.PolycyclicRecognition.cartanWeightScale_apply_root line 45
theorem OAI.PolycyclicRecognition.cartanWeightScale_apply_genWeight line 61
Source documentation
This also applies when the weight function is zero or its root space is zero; it does not require choosing a nonzero root vector.
```
theorem cartanWeightScale_apply_genWeight (h : H) (χ : H → ℝ) {x : L}
    (hx : x ∈ genWeightSpace L χ) :
    cartanWeightScale T H h x = Real.exp (χ h) • x := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanWeightScale
theorem OAI.PolycyclicRecognition.cartan_root_induction line 69
theorem OAI.PolycyclicRecognition.cartanWeightScale_map_lie line 81
Source documentation
Addition of generalized weights makes the scalar dilation respect Lie brackets, even when the Cartan representation is not semisimple.
```
theorem cartanWeightScale_map_lie (h : H) (x y : L) :
    cartanWeightScale T H h ⁅x, y⁆ =
      ⁅cartanWeightScale T H h x, cartanWeightScale T H h y⁆ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanWeightScale
theorem OAI.PolycyclicRecognition.cartanWeightScale_add_apply line 100
theorem OAI.PolycyclicRecognition.cartanWeightScale_zero_apply line 113
def OAI.PolycyclicRecognition.cartanWeightDilation line 123
Source documentation
Exact dilation as a Lie algebra automorphism, with inverse parameter -h.
```
def cartanWeightDilation (h : H) : L ≃ₗ⁅ℝ⁆ L where
…
```
theorem OAI.PolycyclicRecognition.cartanWeightDilation_apply line 134
theorem OAI.PolycyclicRecognition.cartanWeightDilation_mem_ideal line 138
Source documentation
Exact dilations preserve the nilpotent ideal generated by nonzero roots.
```
theorem cartanWeightDilation_mem_ideal (h : H) {x : L} (hx : x ∈ cartanRootIdeal H) :
    cartanWeightDilation T H h x ∈ cartanRootIdeal H := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanWeightDilation
def OAI.PolycyclicRecognition.cartanIdealWeightDilation line 168
Source documentation
Restriction to the actual nilpotent Cartan ideal.
```
def cartanIdealWeightDilation (h : H) : cartanRootIdeal H ≃ₗ⁅ℝ⁆ cartanRootIdeal H where
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal