CartanIntegratedAction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Cartan action, assembled from actual conjugation

The action laws are derived from a faithful ambient inclusion. They are not assumed for the logarithmically parameterized adjoint automorphisms.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_integrated_cartan_action line 39

Source documentation

Pointwise adjoint automorphisms acquire the exact group action law because their images under the injective inclusion are conjugations.

theorem exists_integrated_cartan_action
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (ιN : N →* G) (hιN : Function.Injective ιN) (ιD : D →* G)
    (hN : ∀ x : cartanRootIdeal H, ρ (ιN (ExpN (eN x))) = algebraExpUnit (j x))
    (hD : ∀ h : H, ρ (ιD (ExpD (eD h))) = algebraExpUnit (j h)) :
    ∃ φ : D →* MulAut N,
      (∀ d, φ d = M.adjointGroupAutomorphism T eN ExpN hExpN hbijN dynkinN
        (cartanLog H eD ExpD hbijD d)) ∧
      ∀ d g, ιN (φ d g) = ιD d * ιN g * (ιD d)⁻¹ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.cartanLog