OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorExtensionMap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Maps between groups with the same quotient factor system

  1. def OAI.PolycyclicRecognition.FactorExtension.map line 16

    Source documentation

    Extend a kernel homomorphism compatible with both action and cocycle.

    def map : FactorExtension S →* FactorExtension T where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension

  2. theorem OAI.PolycyclicRecognition.FactorExtension.map_injective line 26
  3. def OAI.PolycyclicRecognition.FactorExtension.groupExtension line 35

    Source documentation

    The defining group extension of a factor system.

    def groupExtension : GroupExtension N (FactorExtension S) Q where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension