CartanLocalProduct.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local multiplication of the actual Cartan factors

Surjectivity of the differential follows from spanning by the two Lie algebras. The factors may overlap. The resulting local open mapping property propagates to every point by left and right translations.

theorem OAI.PolycyclicRecognition.mfderiv_factorProduct_one line 36

Source documentation

The derivative of multiplication of homomorphisms at the identity is the sum of their derivatives.

theorem mfderiv_factorProduct_one
    (hι : ContMDiff (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ∞ ι)
    (hκ : ContMDiff (𝓘(ℝ, ED)) (𝓘(ℝ, EG)) ∞ κ)
    (v : TangentSpace ((𝓘(ℝ, EN)).prod (𝓘(ℝ, ED))) (1 : N × D)) :
    (tangentSpaceCast (𝓘(ℝ, EG)) (ι 1 * κ 1) 1)
      (mfderiv ((𝓘(ℝ, EN)).prod (𝓘(ℝ, ED))) (𝓘(ℝ, EG))
        (fun p : N × D => ι p.1 * κ p.2) 1 v) =
      (tangentSpaceCast (𝓘(ℝ, EG)) (ι 1) 1) (mfderiv (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ι 1 v.1) +
      (tangentSpaceCast (𝓘(ℝ, EG)) (κ 1) 1) (mfderiv (𝓘(ℝ, ED)) (𝓘(ℝ, EG)) κ 1 v.2) := by
…

theorem OAI.PolycyclicRecognition.factorProduct_map_nhds_one line 59

Source documentation

Spanning tangent images give the exact local open mapping property.

theorem factorProduct_map_nhds_one
    (hι : ContMDiff (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ∞ ι)
    (hκ : ContMDiff (𝓘(ℝ, ED)) (𝓘(ℝ, EG)) ∞ κ)
    (hspan : ∀ z : GroupLieAlgebra (𝓘(ℝ, EG)) G,
      ∃ u v, (tangentSpaceCast (𝓘(ℝ, EG)) (ι 1) 1) (mfderiv (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ι 1 u) +
        (tangentSpaceCast (𝓘(ℝ, EG)) (κ 1) 1) (mfderiv (𝓘(ℝ, ED)) (𝓘(ℝ, EG)) κ 1 v) = z) :
    map (fun p : N × D => ι p.1 * κ p.2) (𝓝 (1 : N × D)) = 𝓝 (1 : G) := by
…

theorem OAI.PolycyclicRecognition.cartanFactorProduct_map_nhds_one line 82

Source documentation

The previously proved Cartan spanning theorem supplies the differential surjectivity, including when the two subalgebras intersect.

theorem cartanFactorProduct_map_nhds_one
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, EG)) G) a)
    (H : LieSubalgebra ℝ (GroupLieAlgebra (𝓘(ℝ, EG)) G)) [H.IsCartanSubalgebra]
    (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
    (eD : H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, ED)) D)
    (hι : ContMDiff (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ∞ ι)
    (hκ : ContMDiff (𝓘(ℝ, ED)) (𝓘(ℝ, EG)) ∞ κ)
    (dι : ∀ x : cartanRootIdeal H,
      (tangentSpaceCast (𝓘(ℝ, EG)) (ι 1) 1)
        (mfderiv (𝓘(ℝ, EN)) (𝓘(ℝ, EG)) ι 1 (eN x)) = x)
    (dκ : ∀ x : H,
      (tangentSpaceCast (𝓘(ℝ, EG)) (κ 1) 1)
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.factorProduct_surjective_and_compact_lifts line 108

Source documentation

A local factor product gives both global factorization and compact lifts in a connected Lie group. No complement or global section is needed.

theorem factorProduct_surjective_and_compact_lifts
    [PreconnectedSpace G] [IsTopologicalGroup N] [IsTopologicalGroup D]
    [IsTopologicalGroup G] [LocallyCompactSpace N] [LocallyCompactSpace D]
    (φ : D →* MulAut N)
    (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (hlocal : map (fun p : N × D => ι p.1 * κ p.2) (𝓝 (1 : N × D)) = 𝓝 (1 : G)) :
    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 := by
…