ExponentialEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Closed embeddings from compatible global exponential charts

An injective map of finite-dimensional real Lie algebras is closed in linear coordinates. Compatible global exponential charts transfer that property to the integrated subgroup map. This supplies the properness required for fixed-slice packing, without adding a closed-subgroup hypothesis.

theorem OAI.PolycyclicRecognition.isClosedEmbedding_of_compatible_charts line 27
Source documentation
Global exponential charts turn an injective linear inclusion into a closed topological embedding. No group-theoretic splitting is required.
```
theorem isClosedEmbedding_of_compatible_charts
    (cN : V ≃ₜ N) (cG : U ≃ₜ G) (j : V →ₗ[ℝ] U)
    (hj : Function.Injective j) (f : N → G)
    (hf : ∀ x, f (cN x) = cG (j x)) : Topology.IsClosedEmbedding f := by
…
```

theorem OAI.PolycyclicRecognition.isClosedEmbedding_of_exponential_compatibility line 40

Source documentation

The same conclusion with separately named intrinsic exponentials.

theorem isClosedEmbedding_of_exponential_compatibility
    (cN : V ≃ₜ N) (cG : U ≃ₜ G) (ExpN : V → N) (ExpG : U → G)
    (hN : ∀ x, cN x = ExpN x) (hG : ∀ x, cG x = ExpG x)
    (j : V →ₗ[ℝ] U) (hj : Function.Injective j) (f : N → G)
    (hf : ∀ x, f (ExpN x) = ExpG (j x)) : Topology.IsClosedEmbedding f := by
…

theorem OAI.PolycyclicRecognition.isCompact_preimage_of_exponential_compatibility line 52

Source documentation

In particular compact ambient regions have compact sets of subgroup parameters. This will bound fixed-radius ball multiplicities.

theorem isCompact_preimage_of_exponential_compatibility
    (cN : V ≃ₜ N) (cG : U ≃ₜ G) (ExpN : V → N) (ExpG : U → G)
    (hN : ∀ x, cN x = ExpN x) (hG : ∀ x, cG x = ExpG x)
    (j : V →ₗ[ℝ] U) (hj : Function.Injective j) (f : N → G)
    (hf : ∀ x, f (ExpN x) = ExpG (j x))
    {K : Set G} (hK : IsCompact K) : IsCompact (f ⁻¹' K) :=
…