OAI/RingTheory/Multiplicity/HomogeneousRegradeIdentity.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.HomogeneousRegrade.identity line 25
  2. def OAI.Lech.HomogeneousRegrade.map line 28
  3. lemma OAI.Lech.HomogeneousRegrade.map_val line 30
  4. def OAI.Lech.HomogeneousRegrade.equiv line 35
  5. lemma OAI.Lech.HomogeneousRegrade.equiv_val line 46
  6. abbrev OAI.Lech.ExceptionalCoefficientChart.Coefficient line 55
  7. abbrev OAI.Lech.ExceptionalCoefficientChart.Projective line 56
  8. abbrev OAI.Lech.ExceptionalCoefficientChart.Source line 57
  9. def OAI.Lech.ExceptionalCoefficientChart.regrade line 62
  10. lemma OAI.Lech.ExceptionalCoefficientChart.regrade_val line 65
  11. def OAI.Lech.ExceptionalCoefficientChart.regradeAlg line 67
  12. def OAI.Lech.ExceptionalCoefficientChart.sourceEquiv line 79
  13. def OAI.Lech.ExceptionalCoefficientChart.map line 85
  14. lemma OAI.Lech.ExceptionalCoefficientChart.map_surjective line 88
  15. def OAI.Lech.ExceptionalCoefficientChart.kernelEquiv line 95
  16. theorem OAI.Lech.ExceptionalCoefficientChart.map_kernel_zero line 109
  17. lemma OAI.Lech.AllModuleLength.tensor_map_kernel_zero line 133
  18. def OAI.Lech.ExceptionalCoefficientChart.gradedHom line 159
  19. abbrev OAI.Lech.ExceptionalCoefficientChart.Target line 161
  20. def OAI.Lech.ExceptionalCoefficientChart.homogeneousMap line 168
  21. def OAI.Lech.ExceptionalCoefficientChart.coefficientToSource line 174
  22. def OAI.Lech.ExceptionalCoefficientChart.ringMap line 175
  23. lemma OAI.Lech.ExceptionalCoefficientChart.ringMap_apply line 177
  24. def OAI.Lech.ExceptionalCoefficientChart.algebraHom line 178
  25. instance OAI.Lech.ExceptionalCoefficientChart.targetAlgebra line 186
  26. instance OAI.Lech.ExceptionalCoefficientChart.targetTower line 190
  27. def OAI.Lech.ExceptionalCoefficientChart.algebraLinear line 195
  28. lemma OAI.Lech.ExceptionalCoefficientChart.algebraLinear_apply line 197
  29. lemma OAI.Lech.ExceptionalCoefficientChart.algebraLinear_surjective line 199
  30. def OAI.Lech.ExceptionalCoefficientChart.linearKernelEquiv line 201
  31. lemma OAI.Lech.ExceptionalCoefficientChart.algebraLinear_kernel_zero line 214
  32. theorem OAI.Lech.ExceptionalCoefficientChart.tensor_kernel_zero line 223
  33. theorem OAI.Lech.ExceptionalCoefficientChart.tensor_surjective line 229
  34. lemma OAI.Lech.AllModuleLength.tensor_right_map_kernel_zero line 247
  35. theorem OAI.Lech.ProductSourceCover.sectionModule_baseChange_properties line 271
  36. abbrev OAI.Lech.ExceptionalCoefficientChart.Root line 295
  37. abbrev OAI.Lech.ExceptionalCoefficientChart.ExceptionalRoot line 305
  38. def OAI.Lech.ExceptionalCoefficientChart.rootComparison line 307
  39. lemma OAI.Lech.ExceptionalCoefficientChart.rootComparison_apply line 310
  40. lemma OAI.Lech.ExceptionalCoefficientChart.rootComparison_surjective line 313
  41. theorem OAI.Lech.ExceptionalCoefficientChart.exceptionalRoot_properties line 318
  42. def OAI.Lech.ExceptionalCoefficientChart.rootKernelEquiv line 329
  43. theorem OAI.Lech.ExceptionalCoefficientChart.rootComparison_kernel_zero line 346
  44. lemma OAI.Lech.ExceptionalCoefficientChart.sourceEquiv_evaluate line 367
  45. lemma OAI.Lech.ExceptionalCoefficientChart.ringMap_evaluate line 377
  46. abbrev OAI.Lech.ExceptionalCoefficientChart.ActualOverlap line 388
  47. def OAI.Lech.ExceptionalCoefficientChart.actualOverlapMap line 390
  48. def OAI.Lech.ExceptionalCoefficientChart.actualOverlapAlgebra line 393
  49. lemma OAI.Lech.ExceptionalCoefficientChart.actualOverlap_isLocalization line 398