OAI/Algebra/FiniteTensor/TensorKernels.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Tensor representatives, kernel support and projected operator reduction.

  1. abbrev OAI.PD4Tensor.SuperReduction.Representatives line 19
  2. def OAI.PD4Tensor.SuperReduction.repProject line 21
  3. def OAI.PD4Tensor.SuperReduction.repInclude line 23
  4. theorem OAI.PD4Tensor.SuperReduction.repProject_apply line 25
  5. theorem OAI.PD4Tensor.SuperReduction.repInclude_apply line 26
  6. theorem OAI.PD4Tensor.SuperReduction.project_include line 28
  7. theorem OAI.PD4Tensor.SuperReduction.d_include line 34
  8. theorem OAI.PD4Tensor.SuperReduction.project_d line 39
  9. theorem OAI.PD4Tensor.SuperReduction.project_map_project line 44
  10. def OAI.PD4Tensor.SuperReduction.repMap line 55
  11. theorem OAI.PD4Tensor.SuperReduction.repMap_apply line 58
  12. theorem OAI.PD4Tensor.SuperReduction.repMap_zero line 61
  13. theorem OAI.PD4Tensor.SuperReduction.repMap_id line 64
  14. theorem OAI.PD4Tensor.SuperReduction.repMap_add line 68
  15. theorem OAI.PD4Tensor.SuperReduction.repMap_neg line 71
  16. theorem OAI.PD4Tensor.SuperReduction.repMap_comp line 75
  17. theorem OAI.PD4Tensor.SuperReduction.exists_induced_reduction line 85
  18. theorem OAI.PD4Tensor.factor_of_ker_le line 162
  19. def OAI.PD4Tensor.partialTensor line 177
  20. def OAI.PD4Tensor.kernelSupport line 182
  21. theorem OAI.PD4Tensor.triple_kernel_support line 188
  22. theorem OAI.PD4Tensor.SuperReduction.cycle_of_project_zero line 262
  23. abbrev OAI.PD4Tensor.CohomologyTensor.Factors line 277
  24. def OAI.PD4Tensor.CohomologyTensor.project line 279
  25. def OAI.PD4Tensor.CohomologyTensor.embed line 282
  26. theorem OAI.PD4Tensor.CohomologyTensor.project_include line 286
  27. theorem OAI.PD4Tensor.CohomologyTensor.include_project line 298
  28. theorem OAI.PD4Tensor.CohomologyTensor.finiteD_eq line 304
  29. theorem OAI.PD4Tensor.CohomologyTensor.project_d line 306
  30. theorem OAI.PD4Tensor.CohomologyTensor.d_include line 310
  31. theorem OAI.PD4Tensor.CohomologyTensor.odd_sandwich line 315
  32. theorem OAI.PD4Tensor.CohomologyTensor.partial_sandwich line 324
  33. theorem OAI.PD4Tensor.CohomologyTensor.partial_commute line 343
  34. theorem OAI.PD4Tensor.CohomologyTensor.pairing_projection line 355
  35. theorem OAI.PD4Tensor.CohomologyTensor.operator_projection line 366