Counterexample.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A polynomial hypersurface with a non-coordinate equation

The explicit polynomial F has zero fiber isomorphic to affine three-space, but has a critical point on the fiber of value -1, obstructing its being a polynomial coordinate. Both conclusions persist after adjoining any number of unused variables.

theorem OAI.AbhyankarSathaye.counterexample line 20

Source documentation

The explicit hypersurface has a polynomial coordinate ring but its defining polynomial is not a coordinate, in every ambient dimension at least four.

theorem counterexample :
    Nonempty ((R ⧸ Ideal.span {F}) ≃ₐ[ℂ] MvPolynomial (Fin 3) ℂ) ∧
    (∀ index : Fin 4, MvPolynomial.eval criticalPoint (MvPolynomial.pderiv index F) = 0) ∧
    MvPolynomial.eval criticalPoint F = -1 ∧
    (¬ ∃ (equiv : R ≃ₐ[ℂ] R) (index : Fin 4), equiv (MvPolynomial.X index) = F) ∧
    ∀ (dimension : ℕ) (bound : 4 ≤ dimension),
      Nonempty ((MvPolynomial (Fin dimension) ℂ ⧸ Ideal.span {extendedF bound}) ≃ₐ[ℂ]
        MvPolynomial (Fin (dimension - 1)) ℂ) ∧
      ¬ ∃ (equiv : MvPolynomial (Fin dimension) ℂ ≃ₐ[ℂ] MvPolynomial (Fin dimension) ℂ)
        (index : Fin dimension), equiv (MvPolynomial.X index) = extendedF bound :=
…

Mentions: OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.F, OAI.AbhyankarSathaye.criticalPoint, OAI.AbhyankarSathaye.extendedF

theorem OAI.AbhyankarSathaye.exists_noncoordinate_polynomial line 35
Source documentation
In every dimension at least four, a polynomial can define affine space without being a coordinate of the ambient polynomial ring.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, MvPolynomial, Fin, Complex, And, Nonempty, AlgEquiv, HasQuotient.Quotient, Ideal, Finsupp, Ideal.span, Singleton.singleton, Set, HSub.hSub, Not, Eq, MvPolynomial.X
Proof uses: Exists.intro, OAI.AbhyankarSathaye.extendedF, And.right, OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.F, RingHom, MvPolynomial.eval, OAI.AbhyankarSathaye.criticalPoint, Neg.neg, Derivation, MvPolynomial.pderiv, OAI.AbhyankarSathaye.counterexample
63 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/AbhyankarSathaye.lean:11 (same statement text; different proof or body). Qualify references as OAI.AbhyankarSathaye.exists_noncoordinate_polynomial@path.
```
theorem exists_noncoordinate_polynomial (n : ℕ) (hn : 4 ≤ n) :
    ∃ F : MvPolynomial (Fin n) ℂ,
      Nonempty ((MvPolynomial (Fin n) ℂ ⧸ Ideal.span {F}) ≃ₐ[ℂ]
        MvPolynomial (Fin (n - 1)) ℂ) ∧
      ¬ ∃ (equiv : MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ)
        (index : Fin n), equiv (MvPolynomial.X index) = F :=
…
```
Mentions: OAI.AbhyankarSathaye.F