OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationalTwistCharacter.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Characters preserved by a rotational twist

  1. def OAI.PolycyclicRecognition.rotationalTwistCharacter line 15

    Source documentation

    An invariant character is still a homomorphism on the modified group.

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

    Mentions: OAI.PolycyclicRecognition.rotationalTwist

  2. theorem OAI.PolycyclicRecognition.rotationalTwistCharacter_apply line 22
  3. theorem OAI.PolycyclicRecognition.continuous_rotationalTwistCharacter line 29

    Source documentation

    Continuity is retained in the original topology.

    theorem continuous_rotationalTwistCharacter (h : Continuous π) :
    Continuous (rotationalTwistCharacter α τ hinv π hπ) :=
…

    Mentions: OAI.PolycyclicRecognition.rotationalTwistCharacter