CartanConeAmbientAction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The ambient action on the actual cone quotient

The algebraic ideal and its integrated kernel determine the action and its stabilizer. No injective product decomposition of the ambient group is used.

theorem OAI.PolycyclicRecognition.exists_cartan_cone_ambient_action line 31

Source documentation

The constructed nilpotent quotient carries the ambient action in the cone-quotient lemma, with exact equivariance and stabilizer.

theorem exists_cartan_cone_ambient_action
    (j : GroupLieAlgebra (𝓘(ℝ, EG)) G →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ)
    (hρ : Function.Injective ρ)
    (hN : ∀ x : cartanRootIdeal H,
      ρ (F.inclusionN (F.ExpN (F.N.equiv x))) = algebraExpUnit (j x))
    (hD : ∀ h : H, ρ (F.inclusionD (F.ExpD (F.D.equiv h))) = algebraExpUnit (j h))
    (hNbij : Function.Bijective F.ExpN) (hDsurj : Function.Surjective F.ExpD)
    (dynkin : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (hzero : (0 : H →ₗ[ℝ] ℝ) ∉ C)
    (π : F.N.carrier →* Q) (s : Q → F.N.carrier) (hs : Function.RightInverse s π)
    (hker : (π.ker : Set F.N.carrier) =
…

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