IntegratedCartanRotations.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Compact Cartan rotations on the original simply connected group

theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.cartan_conjugation_mem line 28
Source comment
The actual tangent conjugation preserves the nilpotent ideal.
```
theorem cartan_conjugation_mem (h : H) (x : T.kernelIdeal) :
    adjointLinearMap (E := E) (G := G) (Exp h) (x : GroupLieAlgebra (𝓘(ℝ,E)) G) ∈ T.kernelIdeal := by
…
```
Mentions: OAI.PolycyclicRecognition.adjointLinearMap
theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.action_cartan_exponential line 41
theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.expN_surjective line 50
theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.expD_surjective line 61
theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotation_commutes_action line 75

theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.rotation_fixes_overlap line 94

Source comment

The compact rotations fix the entire overlap of the two actual factors.

theorem rotation_fixes_overlap
    (α : realRotationTorus (GroupLieAlgebra (𝓘(ℝ, E)) G) H →* MulAut F.N.carrier)
    (hα : ∀ z x, α z (F.ExpN (F.N.equiv x)) =
      F.ExpN (F.N.equiv (T.nilradicalRotation H z x))) :
    ∀ z n d, F.inclusionN n = F.inclusionD d → α z n = n := by
…

Mentions: OAI.PolycyclicRecognition.realRotationTorus

theorem OAI.PolycyclicRecognition.ComplexWeightFactorModel.exists_compact_rotation_action line 115