OAI/RingTheory/Multiplicity/AlternatingCechUnaugmentedComplex.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.AlternatingCech.unaugmentedComplex line 24
  2. def OAI.Lech.AlternatingCech.unaugmentedInclusion line 25
  3. lemma OAI.Lech.AlternatingCech.unaugmentedInclusion_injective line 35
  4. lemma OAI.Lech.AlternatingCech.unaugmentedInclusion_delta line 40
  5. lemma OAI.Lech.AlternatingCech.unaugmentedInclusion_surjective line 48
  6. def OAI.Lech.AlternatingCech.unaugmentedEquiv line 53
  7. lemma OAI.Lech.AlternatingCech.unaugmented_isZero_zero line 56
  8. lemma OAI.Lech.AlternatingCech.unaugmented_exactAt line 66
  9. def OAI.Lech.AlternatingCech.sortedZeroEquiv line 95
  10. lemma OAI.Lech.AlternatingCech.sorted_zero_injective line 104
  11. def OAI.Lech.AlternatingCech.unaugmentedAugmentation line 116
  12. lemma OAI.Lech.AlternatingCech.unaugmentedAugmentation_square line 119
  13. def OAI.Lech.AlternatingCech.augmentationShortComplex line 130
  14. lemma OAI.Lech.AlternatingCech.augmentationShortComplex_exact line 134
  15. instance OAI.Lech.AlternatingCech.augmentationShortComplex_mono line 156
  16. def OAI.Lech.AlternatingCech.unaugmented_homology_one line 161
  17. lemma OAI.Lech.AlternatingCech.zeroAug_cochains_le line 183
  18. lemma OAI.Lech.AlternatingCech.zeroAug_cochains_pos line 192
  19. lemma OAI.Lech.AlternatingCech.zeroAug_cochains_zero line 202
  20. def OAI.Lech.AlternatingCech.complexMap line 225
  21. lemma OAI.Lech.AlternatingCech.complexMap_apply line 230
  22. abbrev OAI.Lech.ProductSourceCover.ordinarySections line 240
  23. lemma OAI.Lech.ProductSourceCover.ordinarySections_mono line 241
  24. abbrev OAI.Lech.ProductSourceCover.ordinaryCochains line 243
  25. lemma OAI.Lech.ProductSourceCover.ordinaryCochains_pos line 245
  26. lemma OAI.Lech.ProductSourceCover.ordinaryCochains_zero line 248
  27. lemma OAI.Lech.ProductSourceCover.ordinary_slice_mem line 250
  28. lemma OAI.Lech.ProductSourceCover.ordinary_lift_mem line 263
  29. lemma OAI.Lech.ProductSourceCover.ordinary_neighbor_le line 275
  30. def OAI.Lech.ProductSourceCover.ordinaryInclusion line 284
  31. def OAI.Lech.ProductSourceCover.ordinaryRestriction line 287
  32. def OAI.Lech.ProductSourceCover.ordinarySection line 290
  33. def OAI.Lech.ProductSourceCover.ordinaryComplex line 293
  34. abbrev OAI.Lech.ProductSourceCover.Ambient line 303
  35. def OAI.Lech.ProductSourceCover.ringSections line 306
  36. lemma OAI.Lech.ProductSourceCover.ringSections_mem line 308
  37. lemma OAI.Lech.ProductSourceCover.single_mem line 311
  38. lemma OAI.Lech.ProductSourceCover.allowed_add line 317
  39. lemma OAI.Lech.ProductSourceCover.mul_mem line 321
  40. lemma OAI.Lech.ProductSourceCover.one_mem line 332
  41. lemma OAI.Lech.ProductSourceCover.pow_mem line 337
  42. lemma OAI.Lech.ProductSourceCover.ringSections_mono line 343
  43. lemma OAI.Lech.ProductSourceCover.twist_mono line 346
  44. def OAI.Lech.ProductSourceCover.twistExponent line 354
  45. lemma OAI.Lech.ProductSourceCover.twistExponent_apply line 356
  46. def OAI.Lech.ProductSourceCover.affineExponent line 358
  47. lemma OAI.Lech.ProductSourceCover.affineExponent_allowed line 360
  48. def OAI.Lech.ProductSourceCover.affineCoordinates line 365
  49. lemma OAI.Lech.ProductSourceCover.affineExponent_coordinates line 367
  50. def OAI.Lech.ProductSourceCover.chartLine line 380
  51. lemma OAI.Lech.ProductSourceCover.chartLine_monomial line 383
  52. lemma OAI.Lech.ProductSourceCover.chartLine_mem line 388
  53. theorem OAI.Lech.ProductSourceCover.chartLine_range line 397
  54. def OAI.Lech.ProductSourceCover.ringProjector line 418
  55. lemma OAI.Lech.ProductSourceCover.ringProjector_coeff line 421
  56. lemma OAI.Lech.ProductSourceCover.ringProjector_sum line 425
  57. lemma OAI.Lech.ProductSourceCover.ringProjector_mem line 430
  58. theorem OAI.Lech.ProductSourceCover.ring_augmented_acyclic line 438
  59. theorem OAI.Lech.ProductSourceCover.ring_sorted_acyclic line 443