CartanFactorization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Ambient Cartan factorization

The simply connected nilpotent factors have normal inclusions, a conjugation action, surjective multiplication, compact lifts and a precisely described overlap.

theorem OAI.PolycyclicRecognition.exists_ambient_cartan_factorization line 46

Source documentation

Cartan factors with their exact ambient maps and overlap. The local and global factorization conclusions are proved, not included in a Lie input.

theorem exists_ambient_cartan_factorization :
    ∃ (ι : N →* G) (κ : D →* G) (φ : D →* MulAut N),
      Topology.IsClosedEmbedding ι ∧ Topology.IsClosedEmbedding κ ∧
      (∀ x : cartanRootIdeal H, ι (ExpN (eN x)) = ExpG x) ∧
      (∀ x : H, κ (ExpD (eD x)) = ExpG x) ∧
      ι.range.Normal ∧
      (∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹) ∧
      Function.Surjective (fun p : N × D => ι p.1 * κ p.2) ∧
      (∀ K : Set G, IsCompact K → ∃ C : Set (N × D), IsCompact C ∧
        K ⊆ (fun p : N × D => ι p.1 * κ p.2) '' C) ∧
      Set.range ι ∩ Set.range κ = ExpG ''
        ((cartanRootIdeal H : Set (GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∩
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal