OAI/RingTheory/Multiplicity/LechPiIso.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.pi_isoModSerre line 23
  2. lemma OAI.Lech.cech_homology_isoModSerre line 49
  3. lemma OAI.Lech.piLinear_factorization line 67
  4. lemma OAI.Lech.piLinear_isoModSerre line 81
  5. lemma OAI.Lech.isoModSerre_of_surjective_kernel line 89
  6. lemma OAI.Lech.homology_zeroClass_of_termwise_exactAt line 103
  7. def OAI.Lech.TwistedLocalization.fraction line 129
  8. def OAI.Lech.TwistedLocalization.piece line 137
  9. lemma OAI.Lech.TwistedLocalization.fraction_mem line 141
  10. lemma OAI.Lech.TwistedLocalization.raise_fraction line 147
  11. lemma OAI.Lech.TwistedLocalization.range_mono line 161
  12. lemma OAI.Lech.TwistedLocalization.exists_fraction line 169
  13. def OAI.Lech.TwistedLocalization.algHom line 181
  14. def OAI.Lech.TwistedLocalization.gradedMap line 190
  15. lemma OAI.Lech.TwistedLocalization.gradedMap_surjective line 195
  16. def OAI.Lech.TwistedLocalization.ambientMap line 205
  17. lemma OAI.Lech.TwistedLocalization.ambientMap_fraction line 211
  18. lemma OAI.Lech.TwistedLocalization.ambientMap_mem line 222
  19. def OAI.Lech.TwistedLocalization.pieceMap line 228
  20. def OAI.Lech.TwistedLocalization.pieceFraction line 233
  21. lemma OAI.Lech.TwistedLocalization.pieceMap_fraction line 237
  22. lemma OAI.Lech.TwistedLocalization.pieceMap_surjective line 243
  23. lemma OAI.Lech.TwistedLocalization.kernel_fraction line 255
  24. lemma OAI.Lech.TwistedLocalization.kernel_fraction_eq line 286
  25. def OAI.Lech.TwistedLocalization.kernelFraction line 294
  26. lemma OAI.Lech.TwistedLocalization.iSup_range_kernelFraction line 306
  27. theorem OAI.Lech.TwistedLocalization.kernel_property line 324
  28. def OAI.Lech.TwistedLocalization.ambientRestriction line 352
  29. lemma OAI.Lech.TwistedLocalization.ambientRestriction_algebraMap line 356
  30. lemma OAI.Lech.TwistedLocalization.ambientRestriction_mk line 363
  31. lemma OAI.Lech.TwistedLocalization.restriction_fraction line 379
  32. lemma OAI.Lech.TwistedLocalization.ambientRestriction_mem line 390
  33. def OAI.Lech.TwistedLocalization.pieceRestriction line 399
  34. lemma OAI.Lech.TwistedLocalization.pieceRestriction_val line 405
  35. def OAI.Lech.TwistedLocalization.ambientTo line 418
  36. lemma OAI.Lech.TwistedLocalization.ambientTo_algebraMap line 422
  37. lemma OAI.Lech.TwistedLocalization.ambientTo_comp line 427
  38. lemma OAI.Lech.TwistedLocalization.ambientTo_self line 435
  39. lemma OAI.Lech.TwistedLocalization.ambientTo_mk line 441
  40. lemma OAI.Lech.TwistedLocalization.ambientTo_mem line 453
  41. def OAI.Lech.TwistedLocalization.pieceTo line 460
  42. lemma OAI.Lech.TwistedLocalization.pieceTo_val line 466
  43. lemma OAI.Lech.TwistedLocalization.ambientMap_algebraMap line 474
  44. lemma OAI.Lech.TwistedLocalization.ambientMap_naturality line 481