OAI/AlgebraicGeometry/AbhyankarSathaye/Presentation.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Elimination of auxiliary variables

Explicit mutually inverse complex algebra maps identify the lifting presentation with the quotient of the original polynomial ring by (F).

  1. abbrev OAI.AbhyankarSathaye.Presentation.B line 18
  2. abbrev OAI.AbhyankarSathaye.Presentation.hB line 19
  3. abbrev OAI.AbhyankarSathaye.Presentation.xB line 20
  4. abbrev OAI.AbhyankarSathaye.Presentation.yB line 21
  5. abbrev OAI.AbhyankarSathaye.Presentation.sB line 22
  6. abbrev OAI.AbhyankarSathaye.Presentation.L line 23
  7. abbrev OAI.AbhyankarSathaye.Presentation.D line 24
  8. def OAI.AbhyankarSathaye.Presentation.dmap line 26
  9. def OAI.AbhyankarSathaye.Presentation.lcoef line 27
  10. def OAI.AbhyankarSathaye.Presentation.lvar line 28
  11. theorem OAI.AbhyankarSathaye.Presentation.dmap_F line 30
  12. def OAI.AbhyankarSathaye.Presentation.auxValues line 33
  13. def OAI.AbhyankarSathaye.Presentation.auxEval line 34
  14. theorem OAI.AbhyankarSathaye.Presentation.auxEval_h line 36
  15. theorem OAI.AbhyankarSathaye.Presentation.auxEval_cusp line 42
  16. def OAI.AbhyankarSathaye.Presentation.auxToD line 47
  17. theorem OAI.AbhyankarSathaye.Presentation.auxToD_qvar line 50
  18. def OAI.AbhyankarSathaye.Presentation.liftValues line 54
  19. def OAI.AbhyankarSathaye.Presentation.liftEval line 55
  20. theorem OAI.AbhyankarSathaye.Presentation.liftEval_x line 57
  21. theorem OAI.AbhyankarSathaye.Presentation.liftEval_y line 60
  22. theorem OAI.AbhyankarSathaye.Presentation.liftEval_s line 63
  23. def OAI.AbhyankarSathaye.Presentation.toOriginal line 66
  24. theorem OAI.AbhyankarSathaye.Presentation.toOriginal_lvar line 70
  25. theorem OAI.AbhyankarSathaye.Presentation.toOriginal_lcoef line 74
  26. def OAI.AbhyankarSathaye.Presentation.originalValues line 78
  27. def OAI.AbhyankarSathaye.Presentation.originalEval line 79
  28. theorem OAI.AbhyankarSathaye.Presentation.originalEval_h line 81
  29. theorem OAI.AbhyankarSathaye.Presentation.originalEval_u line 83
  30. theorem OAI.AbhyankarSathaye.Presentation.originalEval_v line 85
  31. theorem OAI.AbhyankarSathaye.Presentation.originalEval_w line 87
  32. theorem OAI.AbhyankarSathaye.Presentation.originalEval_x line 90
  33. theorem OAI.AbhyankarSathaye.Presentation.originalEval_y line 92
  34. theorem OAI.AbhyankarSathaye.Presentation.originalEval_s line 94
  35. theorem OAI.AbhyankarSathaye.Presentation.originalEval_F line 97
  36. def OAI.AbhyankarSathaye.Presentation.fromOriginal line 102
  37. theorem OAI.AbhyankarSathaye.Presentation.fromOriginal_dmap line 111
  38. theorem OAI.AbhyankarSathaye.Presentation.to_from line 113
  39. theorem OAI.AbhyankarSathaye.Presentation.from_auxToD line 121
  40. theorem OAI.AbhyankarSathaye.Presentation.from_to line 129
  41. def OAI.AbhyankarSathaye.Presentation.eliminationEquiv line 142