OAI/Algebra/FiniteTensor/CohomologyReduction.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Cohomology projections, contractions and finite tensor-cycle reduction.

  1. theorem OAI.PD4Tensor.exists_retraction_preserving line 15
  2. theorem OAI.PD4Tensor.exists_cohomology_projection line 36
  3. theorem OAI.PD4Tensor.exists_even_cohomology_projection line 77
  4. theorem OAI.PD4Tensor.exists_contraction line 126
  5. theorem OAI.PD4Tensor.exists_odd_contraction line 171
  6. structure OAI.PD4Tensor.SuperReduction line 212
  7. theorem OAI.PD4Tensor.exists_superReduction line 229
  8. def OAI.PD4Tensor.SuperReduction.tensorD line 256
  9. def OAI.PD4Tensor.SuperReduction.tensorG line 260
  10. def OAI.PD4Tensor.SuperReduction.tensorP line 263
  11. def OAI.PD4Tensor.SuperReduction.tensorH line 266
  12. theorem OAI.PD4Tensor.SuperReduction.tensorD_tmul line 270
  13. theorem OAI.PD4Tensor.SuperReduction.tensorG_tmul line 273
  14. theorem OAI.PD4Tensor.SuperReduction.tensorP_tmul line 276
  15. theorem OAI.PD4Tensor.SuperReduction.tensorH_tmul line 279
  16. theorem OAI.PD4Tensor.SuperReduction.tensor_hom line 283
  17. def OAI.PD4Tensor.SuperReduction.tensor line 297
  18. theorem OAI.PD4Tensor.SuperReduction.tensor_cycle_mod_projection line 338
  19. def OAI.PD4Tensor.SuperReduction.dcoord line 357
  20. def OAI.PD4Tensor.SuperReduction.hcoord line 360
  21. def OAI.PD4Tensor.SuperReduction.finiteD line 363
  22. def OAI.PD4Tensor.SuperReduction.finiteH line 366
  23. def OAI.PD4Tensor.SuperReduction.finiteP line 369
  24. theorem OAI.PD4Tensor.SuperReduction.coord_dh_lt line 373
  25. theorem OAI.PD4Tensor.SuperReduction.pair_offdiagonal line 391
  26. theorem OAI.PD4Tensor.SuperReduction.pair_diagonal line 412
  27. theorem OAI.PD4Tensor.SuperReduction.finite_hom line 443
  28. theorem OAI.PD4Tensor.SuperReduction.finite_cycle_mod_projection line 483