OAI/RingTheory/Multiplicity/RestrictedPolynomialImageCechComparisonHomology.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.RestrictedPolynomialImageCech.comparison_homology line 30
  2. lemma OAI.Lech.RestrictedPolynomialImageCech.homology_mem line 36
  3. lemma OAI.Lech.TwistedLocalization.kernel_length_zero line 57
  4. def OAI.Lech.SourceGraded.twistMapR line 88
  5. lemma OAI.Lech.SourceGraded.twist_kernel_zero line 96
  6. lemma OAI.Lech.SourceGraded.twist_surjective line 108
  7. lemma OAI.Lech.AllModuleLength.mem_zeroClass line 118
  8. def OAI.Lech.SourceGraded.exceptionalCech line 133
  9. def OAI.Lech.SourceGraded.exceptionalComparison line 138
  10. lemma OAI.Lech.SourceGraded.exceptionalMapTerm_kernel_zero line 144
  11. theorem OAI.Lech.SourceGraded.exceptionalComparison_termwise line 157
  12. theorem OAI.Lech.SourceGraded.exceptionalComparison_homology line 174
  13. lemma OAI.Lech.SourceGraded.exceptionalCech_homology_zero line 192
  14. abbrev OAI.Lech.LocalizationCech.ambient line 217
  15. def OAI.Lech.LocalizationCech.restrict line 223
  16. lemma OAI.Lech.LocalizationCech.restrict_comp line 227
  17. abbrev OAI.Lech.LocalizationCech.cochains line 232
  18. def OAI.Lech.LocalizationCech.d line 235
  19. lemma OAI.Lech.LocalizationCech.intersection_comp_subset line 248
  20. def OAI.Lech.LocalizationCech.toFixed line 257
  21. lemma OAI.Lech.LocalizationCech.toFixed_self line 262
  22. lemma OAI.Lech.LocalizationCech.toFixed_d line 270
  23. lemma OAI.Lech.LocalizationCech.d_square line 297
  24. def OAI.Lech.LocalizationCech.complex line 308
  25. lemma OAI.Lech.IdealGraded.monomial_mul line 322
  26. instance OAI.Lech.IdealGraded.reesGradedAlgebra line 328
  27. def OAI.Lech.IdealGraded.evaluate line 342
  28. lemma OAI.Lech.IdealGraded.evaluate_monomial line 345
  29. lemma OAI.Lech.IdealGraded.evaluate_injective_on_grade line 350
  30. def OAI.Lech.FilteredFraction.fraction line 367
  31. def OAI.Lech.FilteredFraction.piece line 373
  32. lemma OAI.Lech.FilteredFraction.fraction_mem line 376
  33. lemma OAI.Lech.FilteredFraction.raise_fraction line 382
  34. lemma OAI.Lech.FilteredFraction.range_mono line 396
  35. lemma OAI.Lech.FilteredFraction.exists_fraction line 402
  36. lemma OAI.Lech.FilteredFraction.antitone line 410
  37. abbrev OAI.Lech.FilteredFraction.layer line 418
  38. abbrev OAI.Lech.FilteredFraction.thickening line 421
  39. lemma OAI.Lech.FilteredFraction.restriction_fraction line 432
  40. lemma OAI.Lech.FilteredFraction.restriction_mem line 445
  41. def OAI.Lech.FilteredFraction.restrict line 454
  42. lemma OAI.Lech.FilteredFraction.restrict_val line 458
  43. def OAI.Lech.FilteredFraction.inclusion line 463
  44. lemma OAI.Lech.FilteredFraction.restrict_inclusion line 466