OAI/GroupTheory/PolycyclicRecognition/Algebra/OpenProductRepresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_continuous_representation_of_open_factor_maps line 18

   Source documentation

   An open surjective factor product is a quotient map, so algebraic representation descent preserves continuity.

   theorem exists_continuous_representation_of_open_factor_maps
       (φ : D →* MulAut N) (iN : N →* G) (iD : D →* G)
       (hiN : Continuous iN) (hiD : Continuous iD)
       (hbase : ∀ d, iN.comp (φ d).toMonoidHom =
         (MulAut.conj (iD d)).toMonoidHom.comp iN)
       (hs : Function.Surjective (fun p : N × D => iN p.1 * iD p.2))
       (ho : IsOpenMap (fun p : N × D => iN p.1 * iD p.2))
       (fN : N →* A) (fD : D →* A) (hfN : Continuous fN) (hfD : Continuous fD)
       (hconj : ∀ d n, fN (φ d n) = fD d * fN n * (fD d)⁻¹)
       (hagree : ∀ n d, iN n = iD d → fN n = fD d) :
       ∃ f : G →* A, Continuous f ∧ ∀ n d, f (iN n * iD d) = fN n * fD d := by
   …