OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorBridgeComposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.factorTranslate_assoc line 11
2. theorem OAI.PolycyclicRecognition.factor_bridge_projection line 19
3. theorem OAI.PolycyclicRecognition.factor_bridge_right_coordinate line 25
4. theorem OAI.PolycyclicRecognition.exists_thickened_factor_bridge line 32

   Source documentation

   Composition preserves a uniform right-cell restriction after the bridge's exponential error has been absorbed.

   theorem exists_thickened_factor_bridge {V I Q : Type*}
       (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
       (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (Exp : V → N) (ExpI : I → N) (qsec : Q → N)
       (small : V → Prop) (ideal : I → Prop) (DB DF : D → Prop)
       (cell : Set (N × D)) (u₂ : N) (d₂ : D) (g : G)
       (habsorb : ∀ v, small v → ∃ i q,
         u₂ * φ d₂ (Exp v) = ExpI i * qsec q ∧ ideal i)
       (hD : ∀ d, DB d → DF (d₂ * d))
       (hbridge : ∃ ub db, ι ub * κ db = g ∧ ∀ z ∈ cell,
         (∃ v, Exp v = ub * φ db z.1 ∧ small v) ∧ DB (db * z.2)) :
       ∃ u d, ι u * κ d = (ι u₂ * κ d₂) * g ∧ ∀ z ∈ cell,
   …