OAI/NumberTheory/PiExponent/Cohomology/GradedCech.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.GradedCech.divisor_isUnit line 13
  2. theorem OAI.PiExponent.GradedCech.divisor_powers_isUnit line 22
  3. def OAI.PiExponent.GradedCech.restriction line 28
  4. theorem OAI.PiExponent.GradedCech.restriction_mk_one line 35
  5. theorem OAI.PiExponent.GradedCech.restriction_fraction_zero line 39
  6. theorem OAI.PiExponent.GradedCech.power_smul_fraction line 43
  7. theorem OAI.PiExponent.GradedCech.restriction_fraction line 48
  8. theorem OAI.PiExponent.GradedCech.restriction_refl line 63
  9. theorem OAI.PiExponent.GradedCech.restriction_comp line 71
  10. theorem OAI.PiExponent.GradedCech.restriction_localizedMap line 81
  11. def OAI.PiExponent.GradedCech.degreeRestriction line 101
  12. theorem OAI.PiExponent.GradedCech.degreeRestriction_coe line 117
  13. def OAI.PiExponent.GradedCech.coverProduct line 127
  14. theorem OAI.PiExponent.GradedCech.coverProduct_mem line 130
  15. theorem OAI.PiExponent.GradedCech.coverProduct_factor line 140
  16. theorem OAI.PiExponent.GradedCech.coverProduct_dvd line 149
  17. abbrev OAI.PiExponent.GradedCech.IntersectionPiece line 154
  18. def OAI.PiExponent.GradedCech.setRestriction line 157
  19. theorem OAI.PiExponent.GradedCech.setRestriction_coe line 162
  20. theorem OAI.PiExponent.GradedCech.setRestriction_refl line 167
  21. theorem OAI.PiExponent.GradedCech.setRestriction_comp line 173
  22. def OAI.PiExponent.GradedCech.tupleSet line 182
  23. theorem OAI.PiExponent.GradedCech.tupleSet_comp_subset line 184
  24. abbrev OAI.PiExponent.GradedCech.Cochain line 190
  25. def OAI.PiExponent.GradedCech.differential line 193
  26. theorem OAI.PiExponent.GradedCech.differential_zero line 198
  27. theorem OAI.PiExponent.GradedCech.differential_sub line 203
  28. theorem OAI.PiExponent.GradedCech.tupleSet_subset line 208
  29. def OAI.PiExponent.GradedCech.evaluate line 214
  30. theorem OAI.PiExponent.GradedCech.evaluate_differential line 219
  31. theorem OAI.PiExponent.GradedCech.differential_squared line 228
  32. def OAI.PiExponent.GradedCech.differentialHom line 240
  33. def OAI.PiExponent.GradedCech.augmentation line 248
  34. theorem OAI.PiExponent.GradedCech.augmentation_coe line 262
  35. theorem OAI.PiExponent.GradedCech.differential_augmentation line 265
  36. theorem OAI.PiExponent.GradedCech.pieceMap_setRestriction line 280
  37. def OAI.PiExponent.GradedCech.cochainMap line 291
  38. theorem OAI.PiExponent.GradedCech.cochainMap_differential line 297
  39. theorem OAI.PiExponent.GradedCech.cochainMap_injective line 304
  40. def OAI.PiExponent.GradedCech.globalPieceMap line 313
  41. theorem OAI.PiExponent.GradedCech.augmentation_natural line 318
  42. theorem OAI.PiExponent.GradedCech.cochainMap_surjective line 339
  43. theorem OAI.PiExponent.GradedCech.cochainMap_exact line 351