CartanMultiplication.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Multiplication of overlapping Cartan factors

Compatible conjugation gives the actual multiplication homomorphism from the semidirect product. Its kernel records the overlap. Local surjectivity makes it globally surjective in a connected ambient group, and an open product map then has compact lifts of compact sets. No complementary subgroup is assumed.

theorem OAI.PolycyclicRecognition.isOpenMap_factorProduct_of_map_nhds_one line 31
Source documentation
For a product of two homomorphisms, openness at the identity propagates to every point by independent left and right translations.
```
theorem isOpenMap_factorProduct_of_map_nhds_one
    (ι : N →* G) (κ : D →* G)
    (hlocal : Filter.map (fun p : N × D => ι p.1 * κ p.2) (𝓝 1) = 𝓝 1) :
    IsOpenMap (fun p : N × D => ι p.1 * κ p.2) := by
…
```
def OAI.PolycyclicRecognition.cartanMultiplication line 61
Source documentation
Actual factor multiplication as a group homomorphism.
```
def cartanMultiplication : N ⋊[φ] D →* G :=
…
```
theorem OAI.PolycyclicRecognition.cartanMultiplication_apply line 66
theorem OAI.PolycyclicRecognition.mem_cartanMultiplication_ker line 70
Source documentation
This kernel equation retains the entire overlap of the factors.
```
theorem mem_cartanMultiplication_ker (z : N ⋊[φ] D) :
    z ∈ (cartanMultiplication ι κ φ hconj).ker ↔ ι z.left = (κ z.right)⁻¹ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanMultiplication
theorem OAI.PolycyclicRecognition.range_cartanMultiplication line 76
Source documentation
The range agrees with the ordinary product parameterization, even when its fibers are nontrivial.
```
theorem range_cartanMultiplication :
    Set.range (cartanMultiplication ι κ φ hconj) =
      Set.range (fun p : N × D => ι p.1 * κ p.2) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanMultiplication
theorem OAI.PolycyclicRecognition.cartan_kernel_projection_injective line 88
Source documentation
Projection of the kernel to the ambient group is injective when each factor inclusion is injective. Thus no further kernel is silently discarded.
```
theorem cartan_kernel_projection_injective
    (hι : Function.Injective ι) (hκ : Function.Injective κ) :
    Function.Injective (fun z : (cartanMultiplication ι κ φ hconj).ker => κ z.val.right) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanMultiplication
theorem OAI.PolycyclicRecognition.cartan_kernel_projection_range line 102
Source documentation
The image of that kernel projection is precisely the factor intersection.
```
theorem cartan_kernel_projection_range :
    Set.range (fun z : (cartanMultiplication ι κ φ hconj).ker => κ z.val.right) =
      (ι.range : Set G) ∩ (κ.range : Set G) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanMultiplication
theorem OAI.PolycyclicRecognition.cartanMultiplication_surjective_of_range_mem_nhds line 123
Source documentation
A local product neighborhood is enough for global factorization in the connected ambient group.
```
theorem cartanMultiplication_surjective_of_range_mem_nhds
    (hlocal : Set.range (fun p : N × D => ι p.1 * κ p.2) ∈ 𝓝 (1 : G)) :
    Function.Surjective (cartanMultiplication ι κ φ hconj) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanMultiplication

theorem OAI.PolycyclicRecognition.exists_compact_cartan_factor_lifts line 142

Source documentation

Once the local product map is open, every compact set admits compact factor lifts. The kernel can be arbitrary.

theorem exists_compact_cartan_factor_lifts
    (hlocal : Set.range (fun p : N × D => ι p.1 * κ p.2) ∈ 𝓝 (1 : G))
    (hopen : IsOpenMap (fun p : N × D => ι p.1 * κ p.2))
    {K : Set G} (hK : IsCompact K) :
    ∃ C : Set (N × D), IsCompact C ∧ K ⊆ (fun p : N × D => ι p.1 * κ p.2) '' C := by
…