OAI/AlgebraicGeometry/AbhyankarSathaye/Lifting.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Lifting a cusp relation

If x² + y³ = h * s and α * h + β * y = 1, the quotient defined by U³ + h * V = x, -U² + h * W = y, and S h U V W = s is a polynomial algebra in one variable. This includes the zero ring and rings with zero divisors.

  1. def OAI.AbhyankarSathaye.Lifting.relX line 23
  2. def OAI.AbhyankarSathaye.Lifting.relY line 24
  3. def OAI.AbhyankarSathaye.Lifting.relS line 25
  4. def OAI.AbhyankarSathaye.Lifting.ideal line 26
  5. abbrev OAI.AbhyankarSathaye.Lifting.Q line 28
  6. def OAI.AbhyankarSathaye.Lifting.qmap line 29
  7. def OAI.AbhyankarSathaye.Lifting.qvar line 31
  8. theorem OAI.AbhyankarSathaye.Lifting.quotient_relations line 33
  9. def OAI.AbhyankarSathaye.Lifting.polyU line 54
  10. def OAI.AbhyankarSathaye.Lifting.polyG line 56
  11. def OAI.AbhyankarSathaye.Lifting.polyW line 58
  12. def OAI.AbhyankarSathaye.Lifting.polyV line 61
  13. def OAI.AbhyankarSathaye.Lifting.values line 63
  14. theorem OAI.AbhyankarSathaye.Lifting.values_relations line 66
  15. def OAI.AbhyankarSathaye.Lifting.forward line 86
  16. theorem OAI.AbhyankarSathaye.Lifting.forward_qvar line 93
  17. def OAI.AbhyankarSathaye.Lifting.backward line 98
  18. theorem OAI.AbhyankarSathaye.Lifting.forward_backward line 102
  19. theorem OAI.AbhyankarSathaye.Lifting.backward_forward line 111
  20. def OAI.AbhyankarSathaye.Lifting.equivalence line 133