OAI/AlgebraicGeometry/AbhyankarSathaye/Stabilization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Adjoining unused variables

For every n ≥ 4, renaming F into the first four variables gives a quotient isomorphic to a polynomial algebra in n - 1 variables. The extended critical point still has value -1 and zero gradient, so the polynomial is not a coordinate.

  1. def OAI.AbhyankarSathaye.fourInclusion line 20

    Also declared: ComparatorChallenges/CommutingDerivations.lean:32 (same declaration text).

  2. def OAI.AbhyankarSathaye.extendedF line 23

    Also declared: ComparatorChallenges/CommutingDerivations.lean:35 (same declaration text).

  3. def OAI.AbhyankarSathaye.blocksToAmbient line 26

    Also declared: ComparatorChallenges/CommutingDerivations.lean:38 (same declaration text).

  4. theorem OAI.AbhyankarSathaye.blocksToAmbient_original line 29
  5. theorem OAI.AbhyankarSathaye.blocksToAmbient_symm_original line 34
  6. def OAI.AbhyankarSathaye.splitAmbient line 38
  7. theorem OAI.AbhyankarSathaye.splitAmbient_comp_original line 43
  8. theorem OAI.AbhyankarSathaye.splitAmbient_F line 53
  9. def OAI.AbhyankarSathaye.blocksToOutput line 56

    Also declared: ComparatorChallenges/CommutingDerivations.lean:41 (same declaration text).

  10. def OAI.AbhyankarSathaye.extendedFiberEquiv line 59
  11. def OAI.AbhyankarSathaye.extendedPoint line 72
  12. theorem OAI.AbhyankarSathaye.extendedPoint_original line 75
  13. theorem OAI.AbhyankarSathaye.extendedPoint_unused line 79
  14. theorem OAI.AbhyankarSathaye.extended_eval line 83
  15. theorem OAI.AbhyankarSathaye.extendedF_eval line 91
  16. theorem OAI.AbhyankarSathaye.extendedF_critical line 94
  17. theorem OAI.AbhyankarSathaye.extendedF_not_coordinate line 106