OAI/RingTheory/Multiplicity/ProductSourceCoverAllowedEmpty.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.ProductSourceCover.allowed_empty line 21
  2. abbrev OAI.Lech.ProductSourceCover.GlobalIndex line 25
  3. def OAI.Lech.ProductSourceCover.globalIndexEquiv line 26
  4. instance OAI.Lech.ProductSourceCover.globalIndexFintype line 32
  5. lemma OAI.Lech.ProductSourceCover.globalIndex_card line 34
  6. def OAI.Lech.ProductSourceCover.globalCoefficientEquiv line 42
  7. def OAI.Lech.ProductSourceCover.globalBasis line 46
  8. instance OAI.Lech.ProductSourceCover.globalSections_finite line 48
  9. instance OAI.Lech.ProductSourceCover.globalSections_free line 50
  10. lemma OAI.Lech.ProductSourceCover.globalSections_finrank line 52
  11. lemma OAI.Lech.ProductSourceCover.globalSections_isZero line 55
  12. abbrev OAI.Lech.ProductSourceCover.unaugmentedSource line 69
  13. def OAI.Lech.ProductSourceCover.highTwistH0 line 73
  14. lemma OAI.Lech.ProductSourceCover.highTwistHigher line 79
  15. lemma OAI.Lech.ProductSourceCover.highTwistH0_isZero line 85
  16. def OAI.Lech.ProductSourceCover.highTwistH0Basis line 88
  17. lemma OAI.Lech.ProductSourceCover.highTwistH0_finrank line 91
  18. def OAI.Lech.ProductSourceCover.ringEndpointProjector line 103
  19. lemma OAI.Lech.ProductSourceCover.ringEndpointProjector_coeff line 107
  20. lemma OAI.Lech.ProductSourceCover.ringEndpointProjector_sum line 112
  21. lemma OAI.Lech.ProductSourceCover.ringEndpointProjector_carrier line 117
  22. lemma OAI.Lech.ProductSourceCover.ringEndpointProjector_zero line 124
  23. theorem OAI.Lech.ProductSourceCover.ring_endpoint_acyclic line 132
  24. theorem OAI.Lech.ProductSourceCover.ring_endpoint_sorted_acyclic line 141
  25. theorem OAI.Lech.ProductSourceCover.endpointCohomology_isZero line 149
  26. def OAI.Lech.AlternatingCech.rawDelta line 170
  27. lemma OAI.Lech.AlternatingCech.rawDelta_sorted line 180
  28. lemma OAI.Lech.AlternatingCech.rawDelta_post line 186
  29. def OAI.Lech.AlternatingCech.familyMap line 205
  30. lemma OAI.Lech.AlternatingCech.familyMap_injective line 208
  31. lemma OAI.Lech.AlternatingCech.familyMap_surjective line 212
  32. def OAI.Lech.AlternatingCech.familyEquiv line 216
  33. def OAI.Lech.AlternatingCech.sortedFamilyEquiv line 220
  34. lemma OAI.Lech.AlternatingCech.sortedFamilyEquiv_apply line 223
  35. lemma OAI.Lech.AlternatingCech.sortedFamilyEquiv_delta line 227
  36. def OAI.Lech.AlternatingCech.sortedFamilyIso line 236
  37. def OAI.Lech.AlternatingCech.sortedUnaugmentedFamilyIso line 254
  38. lemma OAI.Lech.ProductSourceCover.ringSections_coeff_map line 274
  39. def OAI.Lech.ProductSourceCover.ordinaryRingIso line 279
  40. def OAI.Lech.ProductSourceCover.ordinaryCohomologyIso line 298
  41. lemma OAI.Lech.ProductSourceCover.ordinary_zero_isZero line 302
  42. lemma OAI.Lech.ProductSourceCover.ordinary_homology_zero line 307
  43. theorem OAI.Lech.ProductSourceCover.ordinary_endpoint_acyclic line 311
  44. def OAI.Lech.AlternatingCech.complexSequence line 337
  45. lemma OAI.Lech.AlternatingCech.complexSequence_shortExact line 344
  46. lemma OAI.Lech.AlternatingCech.complexSequence_shortExact_injective line 362
  47. lemma OAI.Lech.ProductSourceCover.ordinary_slice_zero line 378
  48. def OAI.Lech.ProductSourceCover.ordinaryDivisorSequence line 387
  49. theorem OAI.Lech.ProductSourceCover.ordinaryDivisorSequence_shortExact line 394
  50. lemma OAI.Lech.ProductSourceCover.ordinaryDivisorSequence_X1 line 420
  51. lemma OAI.Lech.ProductSourceCover.ordinaryDivisorSequence_X2 line 422
  52. lemma OAI.Lech.ProductSourceCover.ordinaryDivisorSequence_X3 line 424
  53. def OAI.Lech.PureCohomology line 435
  54. lemma OAI.Lech.pureCohomology_acyclic line 438
  55. def OAI.Lech.cohomologyShortComplex line 445
  56. lemma OAI.Lech.cohomologyShortComplex_shortExact line 449
  57. lemma OAI.Lech.pureCohomology_middle line 456
  58. def OAI.Lech.boundaryShortComplex line 465
  59. lemma OAI.Lech.boundaryShortComplex_shortExact line 467
  60. lemma OAI.Lech.pureCohomology_left line 473