ConeQuotientHaarAction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Identifying the descended group action with its Haar multiplier

theorem OAI.PolycyclicRecognition.CartanWordModel.descended_cone_adjoint_eq_exponentialConjugate line 28

Source documentation

The quotient action obtained by descending the actual source-group automorphism is exactly the exponential of the induced Lie automorphism. Thus the computed Haar multiplier applies to the descended group action.

theorem descended_cone_adjoint_eq_exponentialConjugate
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
    (ExpQ : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
    (hQbij : Function.Bijective ExpQ)
    (π : N →* Q.carrier) (s : Q.carrier → N) (hs : Function.RightInverse s π)
    (hπ : ∀ x : cartanRootIdeal H,
      π (ExpN (eN x)) = ExpQ (Q.equiv (M.coneProjection C x)))
    (hker : (π.ker : Set N) = ExpN '' (eN '' (M.coneWordIdeal C : Set (cartanRootIdeal H))))
    (h : H) :
    descendQuotientAutomorphism π s hs
      (M.adjointGroupAutomorphism T eN ExpN hExpN hNbij dynkin h)
…

Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.descendQuotientAutomorphism