OAI/AlgebraicGeometry/AbhyankarSathaye/Quotient.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial maps and finitely presented quotients

Ring homomorphisms preserve the defining polynomial expressions. Algebra maps annihilating two or three relations descend to the corresponding quotient.

  1. theorem OAI.AbhyankarSathaye.map_S line 20
  2. theorem OAI.AbhyankarSathaye.map_P line 23
  3. theorem OAI.AbhyankarSathaye.map_Alpha line 26
  4. theorem OAI.AbhyankarSathaye.map_Beta line 29
  5. def OAI.AbhyankarSathaye.lift_pair line 38
  6. theorem OAI.AbhyankarSathaye.lift_pair_mk line 49
  7. def OAI.AbhyankarSathaye.lift_triple line 52
  8. theorem OAI.AbhyankarSathaye.lift_triple_mk line 65
  9. theorem OAI.AbhyankarSathaye.quotient_pair_left line 68
  10. theorem OAI.AbhyankarSathaye.quotient_pair_right line 71
  11. theorem OAI.AbhyankarSathaye.quotient_triple_first line 74
  12. theorem OAI.AbhyankarSathaye.quotient_triple_second line 78
  13. theorem OAI.AbhyankarSathaye.quotient_triple_third line 82