OAI/GroupTheory/PolycyclicRecognition/Algebra/InductionAmbientQuotient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A common ambient representation for subgroup induction

All the induced restrictions of a fixed coefficient are quotients of the same module. The relations increase with the subgroup. The commuting right action on the group-ring factor gives the actual ambient group action.

  1. def OAI.PolycyclicRecognition.inductionAmbientAction line 20
  2. abbrev OAI.PolycyclicRecognition.inductionAmbient line 25
  3. abbrev OAI.PolycyclicRecognition.inductionDiagonalAction line 27
  4. theorem OAI.PolycyclicRecognition.inductionAmbient_diagonal_commute line 30
  5. theorem OAI.PolycyclicRecognition.inductionRelations_invariant line 36
  6. def OAI.PolycyclicRecognition.inductionAmbientQuotientIso line 63

    Source documentation

    The quotient action is the induction action, including its inverse convention.

    def inductionAmbientQuotientIso (H : Subgroup G) :
    Rep.quotient (inductionAmbient A)
      (subgroupCoinvariantRelations (inductionDiagonalAction A) H)
      (inductionRelations_invariant A H) ≅ Rep.ind H.subtype (Rep.res H.subtype A) where
…

    Mentions: OAI.PolycyclicRecognition.inductionAmbient, OAI.PolycyclicRecognition.subgroupCoinvariantRelations, OAI.PolycyclicRecognition.inductionDiagonalAction, OAI.PolycyclicRecognition.inductionRelations_invariant