OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorSystemGauge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Changing quotient lifts by an explicit kernel element

This permits inner corrections in the completed kernel without changing the extension. The correction need not belong to the original lattice.

  1. def OAI.PolycyclicRecognition.NonabelianFactorSystem.gauge line 15
  2. def OAI.PolycyclicRecognition.NonabelianFactorSystem.gaugeEquiv line 46

    Source documentation

    Right multiplication by the lift correction is an exact group isomorphism.

    def gaugeEquiv : FactorExtension (S.gauge b hb) ≃* FactorExtension S where
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension