CartanSubgroupRealization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Closed Cartan factors in the actual ambient Lie group

Lie integration supplies the homomorphisms. The existing Dixmier and nilpotent exponential inputs then prove closedness and identify their exact ranges. Neither closedness nor the description of the overlap is assumed. The simply connected nilpotent Lie models themselves remain explicit here.

theorem OAI.PolycyclicRecognition.exists_closed_cartanRootIdeal_inclusion line 41

Source documentation

The actual nonzero-root ideal integrates injectively with closed image, which is exactly its ambient exponential image.

theorem exists_closed_cartanRootIdeal_inclusion
    (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N) :
    ∃ ι : N →* G, Topology.IsClosedEmbedding ι ∧
      ContMDiff (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ∞ ι ∧
      (∀ x : cartanRootIdeal H, mfderiv (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ι 1 (eN x) = (x : GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∧
      (∀ x : cartanRootIdeal H, ι (ExpN (eN x)) = ExpG x) ∧
      Set.range ι = ExpG '' (cartanRootIdeal H : Set (GroupLieAlgebra (𝓘(ℝ, EG)) G)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.exists_closed_normal_cartanRootIdeal_inclusion line 83
Source documentation
The integrated root ideal is normal by the published ideal criterion, applied to the exact differential of the constructed inclusion.
```
theorem exists_closed_normal_cartanRootIdeal_inclusion
    (normality : NilpotentIdealNormalityInput (EN := EN) (N := N) (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentIdealNormalityInput

theorem OAI.PolycyclicRecognition.exists_closed_cartan_inclusion line 120

Source documentation

The nilpotent Cartan algebra integrates to a closed subgroup with exactly its ambient exponential image; no complementary-subgroup claim is made.

theorem exists_closed_cartan_inclusion
    (eD : H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N) :
    ∃ ι : N →* G, Topology.IsClosedEmbedding ι ∧
      ContMDiff (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ∞ ι ∧
      (∀ x : H, mfderiv (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ι 1 (eD x) = (x : GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∧
      (∀ x : H, ι (ExpN (eD x)) = ExpG x) ∧
      Set.range ι = ExpG '' (H : Set (GroupLieAlgebra (𝓘(ℝ, EG)) G)) := by
…

theorem OAI.PolycyclicRecognition.exponential_factor_intersection line 162

Source documentation

Injectivity of the ambient exponential retains precisely the Cartan intersection, even when it is nontrivial.

theorem exponential_factor_intersection
    {V A B : Type*} (Exp : V → G) (hExp : Function.Injective Exp)
    (iA : A → G) (iB : B → G) (SA SB : Set V)
    (hA : Set.range iA = Exp '' SA) (hB : Set.range iB = Exp '' SB) :
    Set.range iA ∩ Set.range iB = Exp '' (SA ∩ SB) := by
…