OAI/GroupTheory/PolycyclicRecognition/Analysis/IntegralKernelRepresentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The categorical kernel and its concrete group-ring module

  1. abbrev OAI.PolycyclicRecognition.integralKernelObject line 16
  2. def OAI.PolycyclicRecognition.integralKernelInclusion line 20
  3. theorem OAI.PolycyclicRecognition.integralKernelInclusion_apply line 23
  4. instance OAI.PolycyclicRecognition.integralKernelInclusion_mono line 26
  5. theorem OAI.PolycyclicRecognition.integralKernelInclusion_comp line 29
  6. def OAI.PolycyclicRecognition.integralKernelLift line 34
  7. theorem OAI.PolycyclicRecognition.integralKernelLift_comp line 41
  8. def OAI.PolycyclicRecognition.integralKernelIsLimit line 46
  9. def OAI.PolycyclicRecognition.integralKernelIso line 51
  10. def OAI.PolycyclicRecognition.integralKernelModuleEquiv line 54
  11. theorem OAI.PolycyclicRecognition.integralKernel_finite line 60