OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalInductionTensor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Induced restriction as the quotient regular representation tensored with a coefficient

  1. abbrev OAI.PolycyclicRecognition.quotientRegularTensor line 15
  2. def OAI.PolycyclicRecognition.normalInductionTensorRaw line 18
  3. theorem OAI.PolycyclicRecognition.normalInductionTensorRaw_single line 25
  4. theorem OAI.PolycyclicRecognition.normalInductionTensorRaw_invariant line 30
  5. def OAI.PolycyclicRecognition.normalInductionTensorLinear line 46
  6. theorem OAI.PolycyclicRecognition.normalInductionTensorLinear_mk line 51
  7. def OAI.PolycyclicRecognition.normalInductionTensorHom line 56
  8. def OAI.PolycyclicRecognition.normalTensorTerm line 67
  9. theorem OAI.PolycyclicRecognition.normalTensorTerm_eq line 70
  10. def OAI.PolycyclicRecognition.normalTensorQuotientTerm line 83
  11. theorem OAI.PolycyclicRecognition.normalTensorQuotientTerm_mk line 88
  12. def OAI.PolycyclicRecognition.normalInductionTensorInvLinear line 92
  13. theorem OAI.PolycyclicRecognition.normalInductionTensorInvLinear_single line 99
  14. theorem OAI.PolycyclicRecognition.normalInductionTensor_left_inv line 110
  15. theorem OAI.PolycyclicRecognition.normalInductionTensor_right_inv line 121
  16. def OAI.PolycyclicRecognition.normalInductionTensorEquiv line 135
  17. def OAI.PolycyclicRecognition.normalInductionTensorIso line 141

    Source documentation

    This is an isomorphism of the actual ambient group representations.

    def normalInductionTensorIso :
    Rep.ind N.subtype (Rep.res N.subtype A) ≅ quotientRegularTensor N A :=
…

    Mentions: OAI.PolycyclicRecognition.quotientRegularTensor