OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteIndexTraceRetract.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Relative trace-one coefficients are retracts of induced restrictions

The averaging is over a finite coset space, so the subgroup itself may be infinite. The trace element is invariant under that subgroup.

  1. def OAI.PolycyclicRecognition.subgroupRightCosetMulEquiv line 20

    Source documentation

    Right multiplication is well-defined on right cosets without normality.

    def subgroupRightCosetMulEquiv (g : G) : subgroupRightCosets N ≃ subgroupRightCosets N where
…

    Mentions: OAI.PolycyclicRecognition.subgroupRightCosets

  2. theorem OAI.PolycyclicRecognition.subgroupRightCosetMulEquiv_mk line 33
  3. theorem OAI.PolycyclicRecognition.induced_mk_mul_left line 37
  4. abbrev OAI.PolycyclicRecognition.relativeTraceRepresentation line 47
  5. def OAI.PolycyclicRecognition.relativeTraceTerm line 49
  6. theorem OAI.PolycyclicRecognition.relativeTraceTerm_mul line 55
  7. def OAI.PolycyclicRecognition.relativeTraceCosetTerm line 66
  8. theorem OAI.PolycyclicRecognition.relativeTraceCosetTerm_mk line 76
  9. theorem OAI.PolycyclicRecognition.relativeTraceCosetTerm_action line 80
  10. def OAI.PolycyclicRecognition.relativeTraceSectionLinear line 92
  11. def OAI.PolycyclicRecognition.relativeTraceSection line 96
  12. def OAI.PolycyclicRecognition.relativeTraceCounit line 111
  13. theorem OAI.PolycyclicRecognition.relativeTraceCounit_mk line 118
  14. theorem OAI.PolycyclicRecognition.relativeTraceSection_counit line 123
  15. theorem OAI.PolycyclicRecognition.relativeTrace_dimension_le line 146