OAI/RingTheory/Multiplicity/ProductSourceCoverCechNat.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.ProductSourceCover.cechNatCohomologyComparison line 25
  2. theorem OAI.Lech.ProductSourceCover.targetEndpoint_isZero line 32
  3. def OAI.Lech.ProductSourceCover.targetHighTwistH0 line 37
  4. lemma OAI.Lech.ProductSourceCover.targetHighTwistHigher line 40
  5. def OAI.Lech.ProductSourceCover.targetHighTwistBasis line 43
  6. lemma OAI.Lech.ProductSourceCover.targetHighTwist_finrank line 46
  7. theorem OAI.Lech.ProductSourceCover.rootTarget_atRoot line 51
  8. lemma OAI.Lech.ProductSourceCover.rootTarget_above_finrank line 56
  9. lemma OAI.Lech.ProductSourceCover.negativeCount_root line 67
  10. lemma OAI.Lech.ProductSourceCover.signedRank_root line 71
  11. lemma OAI.Lech.pureCohomology_of_iso line 88
  12. def OAI.Lech.finiteCechEuler line 103
  13. lemma OAI.Lech.pureCohomology_finrank line 105
  14. lemma OAI.Lech.pureCohomology_finrank_eq_zero line 109
  15. lemma OAI.Lech.pureCohomology_finiteEuler line 114
  16. theorem OAI.Lech.ProductSourceCover.sourceSigned_pure line 139
  17. theorem OAI.Lech.ProductSourceCover.targetSigned_pure line 145
  18. theorem OAI.Lech.ProductSourceCover.rootTarget_pure line 151
  19. theorem OAI.Lech.ProductSourceCover.targetSigned_euler line 158
  20. theorem OAI.Lech.ProductSourceCover.rootTarget_euler line 163
  21. theorem OAI.Lech.ProductSourceCover.targetSigned_above line 171
  22. def OAI.Lech.ProductSourceCover.RootPositions line 182
  23. def OAI.Lech.ProductSourceCover.rootDegree line 184
  24. lemma OAI.Lech.ProductSourceCover.rootDegree_nonnegative_layer line 187
  25. lemma OAI.Lech.ProductSourceCover.rootDegree_negative_layer line 201
  26. theorem OAI.Lech.ProductSourceCover.rootLayer_nonnegative_isZero line 217
  27. theorem OAI.Lech.ProductSourceCover.rootLayer_negative_isZero line 227
  28. def OAI.Lech.ProductSourceCover.rootTwistRow line 244
  29. def OAI.Lech.ProductSourceCover.rootTwistRowHomologyIso line 246
  30. lemma OAI.Lech.ProductSourceCover.rootTwistRow_isZero line 252
  31. def OAI.Lech.ComplexPi.copies line 281
  32. def OAI.Lech.ComplexPi.matrixMap line 292
  33. lemma OAI.Lech.ComplexPi.matrixMap_f line 306
  34. lemma OAI.Lech.ComplexPi.matrixMap_zero line 309
  35. lemma OAI.Lech.ComplexPi.matrixMap_add line 314
  36. lemma OAI.Lech.ComplexPi.sum_f_apply line 321
  37. lemma OAI.Lech.ComplexPi.matrixMap_comp line 329
  38. def OAI.Lech.ComplexPi.map line 339
  39. lemma OAI.Lech.ComplexPi.map_f line 346
  40. lemma OAI.Lech.ComplexPi.map_id line 349
  41. lemma OAI.Lech.ComplexPi.map_comp line 350
  42. lemma OAI.Lech.ComplexPi.matrixMap_map line 352
  43. lemma OAI.Lech.ComplexPi.map_matrixMap line 356
  44. instance OAI.Lech.ComplexPi.map_mono line 361
  45. lemma OAI.Lech.ComplexPi.isZero_copies line 369
  46. lemma OAI.Lech.ComplexPi.copies_exactAt line 382
  47. lemma OAI.Lech.ComplexPi.copies_homology_isZero line 395
  48. def OAI.Lech.ProductSourceCover.rootLayerTerm line 408
  49. def OAI.Lech.ProductSourceCover.rootLayerDouble line 419
  50. lemma OAI.Lech.ProductSourceCover.rootLayerDouble_bounded line 422
  51. theorem OAI.Lech.ProductSourceCover.rootLayerTotal_nonnegative line 429
  52. theorem OAI.Lech.ProductSourceCover.rootLayerTotal_negative line 451