OAI/AlgebraicGeometry/AbhyankarSathaye/Fiber.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The polynomial algebra structure of the zero fiber

Composing elimination, lifting, the plane parametrization, and a permutation of variables gives the complex algebra isomorphism with ℂ[X,Y,T].

  1. def OAI.AbhyankarSathaye.variableOrder line 17
  2. def OAI.AbhyankarSathaye.flattenPlane line 23
  3. theorem OAI.AbhyankarSathaye.flattenPlane_symm_X0 line 26
  4. theorem OAI.AbhyankarSathaye.flattenPlane_symm_X1 line 31
  5. theorem OAI.AbhyankarSathaye.flattenPlane_symm_X2 line 36
  6. theorem OAI.AbhyankarSathaye.flattenPlane_C_X0 line 41
  7. theorem OAI.AbhyankarSathaye.flattenPlane_C_X1 line 44
  8. theorem OAI.AbhyankarSathaye.flattenPlane_X line 47
  9. def OAI.AbhyankarSathaye.liftedEquiv line 51
  10. def OAI.AbhyankarSathaye.planeExtensionEquiv line 55
  11. def OAI.AbhyankarSathaye.fiberEquiv line 58