OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorSystemTwist.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing a commuting quotient action from a factor system

The original cocycle is retained. Fixedness of its values is exactly the condition needed to remove the commuting semisimple quotient action.

  1. theorem OAI.PolycyclicRecognition.twist_inverse_fixed line 21
  2. theorem OAI.PolycyclicRecognition.twist_inverse_product line 27
  3. theorem OAI.PolycyclicRecognition.twist_inverse_commute line 34
  4. def OAI.PolycyclicRecognition.NonabelianFactorSystem.twist line 40

    Source documentation

    Remove the actual quotient homomorphism from every section action.

    def NonabelianFactorSystem.twist : NonabelianFactorSystem N Q where
…

    Mentions: OAI.PolycyclicRecognition.NonabelianFactorSystem

  5. theorem OAI.PolycyclicRecognition.factorSystem_twist_recompose line 60