OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRayActionTopology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the actual ray quotient action

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_ray_factor_action line 41

    Source documentation

    Each actual Cartan factor acts continuously on the ray quotient. This follows from its previously identified exponential conjugation.

    theorem continuous_ray_factor_action (d : F.D.carrier) : Continuous (α d) := by
…
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_ambient_ray_action line 54

    Source documentation

    Every fixed ambient group element acts continuously; no continuity assumption on a chosen factorization is needed.

    theorem continuous_ambient_ray_action
    (act : G →* Equiv.Perm Q.carrier)
    (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = π u * α d q)
    (g : G) : Continuous (act g) := by
…