OAI/GroupTheory/PolycyclicRecognition/Geometry/InducingFromHeightKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.inducing_of_height_kernel line 20

   Source documentation

   Near the identity, a continuous quotient coordinate and an inducing representation on its kernel determine the topology on the whole group.

   theorem inducing_of_height_kernel
       (ρ : G →* A) (hρ : Continuous ρ) (π : G →* Q) (hπ : Continuous π)
       (s : C(Q, G)) (hs : ∀ q, π (s q) = q) (hsone : s 1 = 1)
       (hk : Topology.IsInducing (fun k : π.ker => ρ k))
       (f : A → Q) (hf : ContinuousAt f 1) (hf1 : f 1 = 1)
       (hfactor : ∀ g, f (ρ g) = π g) : Topology.IsInducing ρ := by
   …