OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactLifts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact lifts under an open quotient

A compact target set has lifts in one compact source set for an open surjection from a locally compact space. This is the precise bounded-step lifting consequence needed by the Cartan multiplication map.

  1. theorem OAI.PolycyclicRecognition.exists_compact_lifts_of_open_surjection line 21

    Source documentation

    Compact lifts need no global section, properness, or injectivity of the quotient map. Finite local compact neighborhoods suffice.

    theorem exists_compact_lifts_of_open_surjection
    {X Y : Type*} [TopologicalSpace X] [LocallyCompactSpace X] [TopologicalSpace Y]
    (f : X → Y) (hopen : IsOpenMap f) (hsurj : Function.Surjective f)
    {K : Set Y} (hK : IsCompact K) :
    ∃ C : Set X, IsCompact C ∧ K ⊆ f '' C := by
…