OAI/RingTheory/Multiplicity/GradedChartCochains.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.GradedChart.cochains line 23
  2. def OAI.Lech.GradedChart.d line 26
  3. abbrev OAI.Lech.PartialLaurent.polynomialCochains line 47
  4. def OAI.Lech.PartialLaurent.polynomialD line 51
  5. def OAI.Lech.PartialLaurent.polynomialCochainsEquiv line 54
  6. lemma OAI.Lech.PartialLaurent.polynomialCochainsEquiv_d line 58
  7. lemma OAI.Lech.PartialLaurent.polynomialD_square line 68
  8. def OAI.Lech.PartialLaurent.polynomialComplex line 74
  9. lemma OAI.Lech.PartialLaurent.polynomial_exact line 82
  10. lemma OAI.Lech.PartialLaurent.polynomialComplex_exactAt line 93
  11. abbrev OAI.Lech.RestrictedPolynomialCech.grade line 119
  12. def OAI.Lech.RestrictedPolynomialCech.termEquiv line 123
  13. lemma OAI.Lech.RestrictedPolynomialCech.termEquiv_naturality line 130
  14. abbrev OAI.Lech.RestrictedPolynomialCech.cochains line 139
  15. def OAI.Lech.RestrictedPolynomialCech.d line 141
  16. def OAI.Lech.RestrictedPolynomialCech.cochainsEquiv line 144
  17. lemma OAI.Lech.RestrictedPolynomialCech.cochainsEquiv_d line 148
  18. lemma OAI.Lech.RestrictedPolynomialCech.d_square line 162
  19. def OAI.Lech.RestrictedPolynomialCech.complex line 167
  20. lemma OAI.Lech.RestrictedPolynomialCech.exact line 175
  21. lemma OAI.Lech.RestrictedPolynomialCech.exactAt line 185
  22. abbrev OAI.Lech.ImageCech.term line 216
  23. lemma OAI.Lech.ImageCech.image_denominator line 220
  24. def OAI.Lech.ImageCech.restrict line 225
  25. def OAI.Lech.ImageCech.mapTerm line 232
  26. lemma OAI.Lech.ImageCech.mapTerm_naturality line 236
  27. abbrev OAI.Lech.ImageCech.cochains line 245
  28. def OAI.Lech.ImageCech.d line 248
  29. def OAI.Lech.ImageCech.mapCochains line 261
  30. lemma OAI.Lech.ImageCech.mapCochains_naturality line 265
  31. lemma OAI.Lech.ImageCech.mapTerm_surjective line 276
  32. lemma OAI.Lech.ImageCech.mapCochains_surjective line 281
  33. abbrev OAI.Lech.RestrictedPolynomialImageCech.cochains line 299
  34. def OAI.Lech.RestrictedPolynomialImageCech.d line 301
  35. def OAI.Lech.RestrictedPolynomialImageCech.mapCochains line 304
  36. lemma OAI.Lech.RestrictedPolynomialImageCech.mapCochains_naturality line 307
  37. lemma OAI.Lech.RestrictedPolynomialImageCech.mapCochains_surjective line 313
  38. lemma OAI.Lech.RestrictedPolynomialImageCech.d_square line 319
  39. def OAI.Lech.RestrictedPolynomialImageCech.complex line 326
  40. def OAI.Lech.RestrictedPolynomialImageCech.comparison line 335
  41. lemma OAI.Lech.ActualCech.laurentD_zero_injective line 357
  42. lemma OAI.Lech.PartialLaurent.polynomialD_zero_injective line 381
  43. lemma OAI.Lech.RestrictedPolynomialCech.d_zero_injective line 395
  44. lemma OAI.Lech.RestrictedPolynomialCech.exactAt_zero line 402
  45. lemma OAI.Lech.RestrictedPolynomialCech.exactAt_all line 416
  46. lemma OAI.Lech.RestrictedPolynomialImageCech.comparison_f line 433
  47. lemma OAI.Lech.RestrictedPolynomialImageCech.comparison_termwise line 436