OAI/AlgebraicGeometry/AbhyankarSathaye/FiberFormulas.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Explicit coordinates on the zero fiber

The inverse isomorphism sends X, Y, and T to x + s³, y - s², and α * u + β * (v + u * w). The forward isomorphism is given by the polynomials freeH, freeU, freeV, and freeW, with variables ordered X, Y, T.

  1. def OAI.AbhyankarSathaye.fiberParameter line 17
  2. theorem OAI.AbhyankarSathaye.fiberEquiv_symm_X0 line 19
  3. theorem OAI.AbhyankarSathaye.fiberEquiv_symm_X1 line 29
  4. theorem OAI.AbhyankarSathaye.fiberEquiv_symm_X2 line 39
  5. def OAI.AbhyankarSathaye.freeS line 48
  6. def OAI.AbhyankarSathaye.freeX line 49
  7. def OAI.AbhyankarSathaye.freeY line 50
  8. def OAI.AbhyankarSathaye.freeH line 51
  9. def OAI.AbhyankarSathaye.freeAlpha line 52
  10. def OAI.AbhyankarSathaye.freeBeta line 53
  11. def OAI.AbhyankarSathaye.freeU line 54
  12. def OAI.AbhyankarSathaye.freeG line 55
  13. def OAI.AbhyankarSathaye.freeW line 56
  14. def OAI.AbhyankarSathaye.freeV line 57
  15. theorem OAI.AbhyankarSathaye.symm_freeS line 59
  16. theorem OAI.AbhyankarSathaye.symm_freeX line 64
  17. theorem OAI.AbhyankarSathaye.symm_freeY line 67
  18. theorem OAI.AbhyankarSathaye.symm_freeH line 70
  19. theorem OAI.AbhyankarSathaye.symm_freeAlpha line 78
  20. theorem OAI.AbhyankarSathaye.symm_freeBeta line 80
  21. theorem OAI.AbhyankarSathaye.inverse_formulas_in_quotient line 83
  22. theorem OAI.AbhyankarSathaye.explicit_inverse_formulas line 98