OAI/GroupTheory/PolycyclicRecognition/Algebra/NonabelianFactorSystem.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Groups from a normalized nonabelian factor system

The multiplication retains the inner correction, so quotient lifts are not required to commute or to give a splitting.

  1. structure OAI.PolycyclicRecognition.NonabelianFactorSystem line 14
  2. theorem OAI.PolycyclicRecognition.NonabelianFactorSystem.action_mul_apply line 27
  3. structure OAI.PolycyclicRecognition.FactorExtension line 34
  4. instance OAI.PolycyclicRecognition.FactorExtension.(instance at line 42) line 42
  5. instance OAI.PolycyclicRecognition.FactorExtension.(instance at line 43) line 43
  6. instance OAI.PolycyclicRecognition.FactorExtension.(instance at line 46) line 46
  7. theorem OAI.PolycyclicRecognition.FactorExtension.one_left line 49
  8. theorem OAI.PolycyclicRecognition.FactorExtension.one_right line 50
  9. theorem OAI.PolycyclicRecognition.FactorExtension.mul_left line 51
  10. theorem OAI.PolycyclicRecognition.FactorExtension.mul_right line 53
  11. theorem OAI.PolycyclicRecognition.FactorExtension.inv_left line 54
  12. theorem OAI.PolycyclicRecognition.FactorExtension.inv_right line 56
  13. instance OAI.PolycyclicRecognition.FactorExtension.(instance at line 58) line 58
  14. def OAI.PolycyclicRecognition.FactorExtension.inl line 82

    Source documentation

    The kernel inclusion into the group with the given factor system.

    def inl : N →* FactorExtension S where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension

  15. def OAI.PolycyclicRecognition.FactorExtension.projection line 91

    Source documentation

    Projection to the original quotient.

    def projection : FactorExtension S →* Q where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension

  16. theorem OAI.PolycyclicRecognition.FactorExtension.inl_injective line 96
  17. theorem OAI.PolycyclicRecognition.FactorExtension.projection_surjective line 100
  18. def OAI.PolycyclicRecognition.FactorExtension.equivProd line 104

    Source documentation

    The product coordinates are an actual equivalence of sets.

    def equivProd : FactorExtension S ≃ N × Q where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension