OAI/AlgebraicGeometry/AbhyankarSathaye/Plane.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

A polynomial presentation of the affine plane

The relations h = 1 + P x y s and x² + y³ = h * s give a polynomial algebra with coordinates x + s³ and y - s². The auxiliary variables are ordered as h, x, y, s.

  1. def OAI.AbhyankarSathaye.Plane.relH line 21
  2. def OAI.AbhyankarSathaye.Plane.relCusp line 22
  3. def OAI.AbhyankarSathaye.Plane.ideal line 23
  4. abbrev OAI.AbhyankarSathaye.Plane.Q line 24
  5. def OAI.AbhyankarSathaye.Plane.qmap line 25
  6. def OAI.AbhyankarSathaye.Plane.qvar line 26
  7. theorem OAI.AbhyankarSathaye.Plane.relation_h line 28
  8. theorem OAI.AbhyankarSathaye.Plane.relation_cusp line 37
  9. theorem OAI.AbhyankarSathaye.Plane.shift_s line 43
  10. theorem OAI.AbhyankarSathaye.Plane.bezout line 47
  11. def OAI.AbhyankarSathaye.Plane.planeS line 57
  12. def OAI.AbhyankarSathaye.Plane.planeX line 58
  13. def OAI.AbhyankarSathaye.Plane.planeY line 59
  14. def OAI.AbhyankarSathaye.Plane.planeH line 60
  15. def OAI.AbhyankarSathaye.Plane.values line 61
  16. theorem OAI.AbhyankarSathaye.Plane.plane_cusp line 64
  17. def OAI.AbhyankarSathaye.Plane.forward line 75
  18. theorem OAI.AbhyankarSathaye.Plane.forward_qvar line 80
  19. def OAI.AbhyankarSathaye.Plane.backward line 84
  20. theorem OAI.AbhyankarSathaye.Plane.backward_planeS line 87
  21. theorem OAI.AbhyankarSathaye.Plane.backward_planeX line 90
  22. theorem OAI.AbhyankarSathaye.Plane.backward_planeY line 94
  23. theorem OAI.AbhyankarSathaye.Plane.backward_planeH line 98
  24. theorem OAI.AbhyankarSathaye.Plane.forward_backward line 101
  25. theorem OAI.AbhyankarSathaye.Plane.backward_forward line 106
  26. def OAI.AbhyankarSathaye.Plane.equivalence line 114