CartanHomKernel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Vanishing on the actual Cartan root factor

Logarithmic distortion kills each root generator under a linearly bounded continuous homomorphism. The proved generator schemes then kill the whole constructed nilpotent factor, including every point of its group model.

theorem OAI.PolycyclicRecognition.CartanWordModel.hom_eq_one_on_letter line 35
Source documentation
The actual homogeneous letters lie in the kernel.
```
theorem hom_eq_one_on_letter (i : Fin M.letterCount) (t : ℝ) :
    l (Exp (t • (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G))) = 1 :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.hom_eq_one_on_root_factor_exp line 41
Source documentation
Every exponential in the root ideal lies in the kernel.
```
theorem hom_eq_one_on_root_factor_exp
    (F : CartanFactorModel H Exp)
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (v : cartanRootIdeal H) : l (F.inclusionN (F.ExpN (F.N.equiv v))) = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanFactorModel, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.CartanWordModel.hom_eq_one_on_root_factor line 61
Source documentation
Surjectivity of the intrinsic nilpotent exponential gives vanishing on all points of the factor, not only its logarithmic coordinate model.
```
theorem hom_eq_one_on_root_factor
    (F : CartanFactorModel H Exp)
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (n : F.N.carrier) : l (F.inclusionN n) = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanFactorModel, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput