OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorSystemTwistAction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The removed action and the original extension

The removed quotient action acts on the twisted extension. The original extension embeds into its semidirect product as the graph of the quotient.

  1. theorem OAI.PolycyclicRecognition.twist_action_commutes line 21
  2. def OAI.PolycyclicRecognition.factorTwistAction line 35
  3. def OAI.PolycyclicRecognition.factorTwistGraph line 72

    Source documentation

    The graph embedding retains both coordinates of the original group.

    def factorTwistGraph : FactorExtension R →*
    (FactorExtension (R.twist χ hcomm hfix) ⋊[factorTwistAction R χ hcomm hfix] Q) where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension, OAI.PolycyclicRecognition.factorTwistAction

  4. theorem OAI.PolycyclicRecognition.factorTwistGraph_injective line 86