OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorExtensionConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugation on the completed kernel in factor coordinates

  1. theorem OAI.PolycyclicRecognition.FactorExtension.conjugation_inl line 10
  2. theorem OAI.PolycyclicRecognition.FactorExtension.conjugation_eq line 23
  3. theorem OAI.PolycyclicRecognition.FactorExtension.conjugation_section line 29

    Source documentation

    The coordinate section has exactly the prescribed kernel action.

    theorem conjugation_section (q : Q) :
    (groupExtension S).conjAct (⟨1, q⟩ : FactorExtension S) = S.action q := by
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension.groupExtension, OAI.PolycyclicRecognition.FactorExtension