OAI/RingTheory/Multiplicity/ActualCechTranspose.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.ActualCech.transpose line 21
  2. lemma OAI.Lech.ActualCech.transpose_apply line 30
  3. lemma OAI.Lech.ActualCech.transpose_symm_apply line 34
  4. def OAI.Lech.ActualCech.allowedSet line 40
  5. def OAI.Lech.ActualCech.supportedTranspose line 44
  6. def OAI.Lech.ActualCech.intersection line 66
  7. lemma OAI.Lech.ActualCech.mem_intersection line 68
  8. lemma OAI.Lech.ActualCech.mem_exponents_intersection line 71
  9. def OAI.Lech.ActualCech.exponentEquiv line 83
  10. abbrev OAI.Lech.ActualCech.laurentCochains line 92
  11. def OAI.Lech.ActualCech.laurentEquiv line 96
  12. lemma OAI.Lech.ActualCech.homogeneousEquiv_apply line 103
  13. lemma OAI.Lech.ActualCech.laurentEquiv_homogeneousEquiv line 108
  14. lemma OAI.Lech.ActualCech.laurentEquiv_coeff line 124
  15. lemma OAI.Lech.ActualCech.intersection_delete line 134
  16. def OAI.Lech.ActualCech.laurentD line 142
  17. lemma OAI.Lech.ActualCech.restrict_coeff_image line 156
  18. lemma OAI.Lech.ActualCech.restrict_coeff_zero line 166
  19. lemma OAI.Lech.ActualCech.laurentEquiv_restrict_coeff line 175
  20. def OAI.Lech.ActualCech.homogeneousD line 194
  21. lemma OAI.Lech.ActualCech.laurentD_equiv line 201
  22. theorem OAI.Lech.ActualCech.laurent_exact_nonnegative line 219
  23. lemma OAI.Lech.ActualCech.homogeneousD_square line 239
  24. lemma OAI.Lech.ActualCech.laurentD_square line 246
  25. def OAI.Lech.ActualCech.augmentedComplex line 252
  26. lemma OAI.Lech.ActualCech.augmentedComplex_exactAt line 260
  27. theorem OAI.Lech.ActualCech.augmentedComplex_homology_zero line 279
  28. lemma OAI.Lech.quasiIso_middle line 296
  29. lemma OAI.Lech.quasiIsoAt_localization_iff line 329
  30. lemma OAI.Lech.homology_middle_isoModSerre line 360
  31. lemma OAI.Lech.homology_isoModSerre_of_termwise line 397