OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactLiftQuotient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.isQuotientMap_of_compact_lifts line 16

   Source documentation

   A continuous surjection with compact lifts of compact sets is a quotient map into a Hausdorff compactly generated space.

   theorem isQuotientMap_of_compact_lifts
       {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
       [T2Space Y] [CompactlyGeneratedSpace Y]
       (f : X → Y) (hf : Continuous f) (hsurj : Function.Surjective f)
       (hlift : ∀ K : Set Y, IsCompact K → ∃ C : Set X, IsCompact C ∧ K ⊆ f '' C) :
       IsQuotientMap f := by
   …

2. theorem OAI.PolycyclicRecognition.CartanFactorModel.orbitMap_isQuotientMap line 51

   Source documentation

   The actual orbit map is a quotient map. Its topology follows from compact Cartan lifts and a continuous section of the nilpotent projection.

   theorem orbitMap_isQuotientMap
       (π : F.N.carrier →* Q) (hπ : Continuous π)
       (s : Q → F.N.carrier) (hs : Continuous s) (hsection : Function.RightInverse s π)
       (α : F.D.carrier →* MulAut Q) (act : G →* Equiv.Perm Q)
       (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = π u * α d q) :
       IsQuotientMap (fun g => act g 1) := by
   …