OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationalTwistLift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Subgroups whose multiplication is preserved by a rotational twist

  1. def OAI.PolycyclicRecognition.rotationalTwistLift line 17

    Source documentation

    The inverse-character graph is multiplicative on this subgroup.

    def rotationalTwistLift : A →* rotationalTwist α τ hinv where
…

    Mentions: OAI.PolycyclicRecognition.rotationalTwist

  2. theorem OAI.PolycyclicRecognition.rotationalTwistLift_left line 31
  3. theorem OAI.PolycyclicRecognition.continuous_rotationalTwistLift line 38

    Source documentation

    The lift retains exactly the original topology on its image.

    theorem continuous_rotationalTwistLift (hτ : Continuous τ) (hf : Continuous f) :
    Continuous (rotationalTwistLift α τ hinv f hfix) := by
…

    Mentions: OAI.PolycyclicRecognition.rotationalTwistLift