ZeroLocusInterface.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Complex zero loci and ideal transport

This module supplies the geometric interface needed when an ambient polynomial isomorphism is described on complex points. Polynomial substitutions induce mutually inverse polynomial maps, not arbitrary set-theoretic bijections. Hilbert's Nullstellensatz then recovers radical defining ideals from their complex zero loci. No conclusion about the manuscript's polynomial is assumed.

def OAI.StableCoordinate.ZeroLocusInterface.pointMap line 25
Source documentation
The map on affine points contravariantly induced by a polynomial substitution.
```
def pointMap (φ : MvPolynomial σ k →ₐ[k] MvPolynomial σ k)
    (x : σ → k) : σ → k :=
…
```
theorem OAI.StableCoordinate.ZeroLocusInterface.aeval_pointMap line 30
Source documentation
Substitution and evaluation commute, for every polynomial.
```
theorem aeval_pointMap (φ : MvPolynomial σ k →ₐ[k] MvPolynomial σ k)
    (x : σ → k) (p : MvPolynomial σ k) :
    aeval (pointMap φ x) p = aeval x (φ p) := by
…
```
Mentions: OAI.StableCoordinate.ZeroLocusInterface.pointMap
theorem OAI.StableCoordinate.ZeroLocusInterface.pointMap_id line 39
theorem OAI.StableCoordinate.ZeroLocusInterface.pointMap_comp line 45
Source documentation
Composition reverses because coordinate-ring homomorphisms are pullbacks.
```
theorem pointMap_comp (φ ψ : MvPolynomial σ k →ₐ[k] MvPolynomial σ k)
    (x : σ → k) :
    pointMap (φ.comp ψ) x = pointMap ψ (pointMap φ x) := by
…
```
Mentions: OAI.StableCoordinate.ZeroLocusInterface.pointMap
def OAI.StableCoordinate.ZeroLocusInterface.pointEquiv line 53
Source documentation
A polynomial algebra automorphism induces an affine-space automorphism on points; both directions are explicitly given by polynomial evaluation.
```
def pointEquiv (e : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k) :
    (σ → k) ≃ (σ → k) where
…
```
theorem OAI.StableCoordinate.ZeroLocusInterface.pointEquiv_apply line 69
theorem OAI.StableCoordinate.ZeroLocusInterface.preimage_zeroLocus line 73
Source documentation
Pullback of a zero locus agrees with extension of its defining ideal.
```
theorem preimage_zeroLocus (e : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k)
    (I : Ideal (MvPolynomial σ k)) :
    (pointEquiv e) ⁻¹' zeroLocus k I = zeroLocus k (I.map e.toRingHom) := by
…
```
Mentions: OAI.StableCoordinate.ZeroLocusInterface.pointEquiv
theorem OAI.StableCoordinate.ZeroLocusInterface.image_zeroLocus line 91
Source documentation
The inverse point map carries a closed algebraic set to the zero locus of its transported ideal. This fixes the usual contravariance convention.
```
theorem image_zeroLocus (e : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k)
    (I : Ideal (MvPolynomial σ k)) :
    (pointEquiv e).symm '' zeroLocus k I = zeroLocus k (I.map e.toRingHom) := by
…
```
Mentions: OAI.StableCoordinate.ZeroLocusInterface.pointEquiv
theorem OAI.StableCoordinate.ZeroLocusInterface.radical_ideal_eq_of_zeroLocus_eq line 101
Source documentation
Over an algebraically closed field, radical ideals are determined by their sets of rational points. The finite-variable hypothesis is essential.
```
theorem radical_ideal_eq_of_zeroLocus_eq
    {I J : Ideal (MvPolynomial σ k)} (hI : I.IsRadical) (hJ : J.IsRadical)
    (h : zeroLocus k I = zeroLocus k J) : I = J := by
…
```
theorem OAI.StableCoordinate.ZeroLocusInterface.map_ideal_eq_of_image_zeroLocus_eq line 112
Source documentation
Equality of geometric images under a polynomial ambient automorphism recovers equality of the transported radical defining ideals.
```
theorem map_ideal_eq_of_image_zeroLocus_eq
    (e : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k)
    {I J : Ideal (MvPolynomial σ k)} (hI : I.IsRadical) (hJ : J.IsRadical)
    (h : (pointEquiv e).symm '' zeroLocus k I = zeroLocus k J) :
    I.map e.toRingHom = J := by
…
```
Mentions: OAI.StableCoordinate.ZeroLocusInterface.pointEquiv
theorem OAI.StableCoordinate.ZeroLocusInterface.image_zeroLocus_eq_iff_map_eq line 133
Source documentation
For prime defining ideals, image equality and ideal transport are exactly equivalent; no extra geometric assumption is introduced.
```
theorem image_zeroLocus_eq_iff_map_eq
    (e : MvPolynomial σ k ≃ₐ[k] MvPolynomial σ k)
    (I J : Ideal (MvPolynomial σ k)) [I.IsPrime] [J.IsPrime] :
    (pointEquiv e).symm '' zeroLocus k I = zeroLocus k J ↔
      I.map e.toRingHom = J := by
…
```
Mentions: OAI.StableCoordinate.ZeroLocusInterface.pointEquiv
theorem OAI.StableCoordinate.ZeroLocusInterface.zeroLocus_fiber_ideal line 147
Source documentation
The zero locus of the principal fiber ideal is exactly the named fiber, including the parameter value zero.
```
theorem zeroLocus_fiber_ideal (p : MvPolynomial σ k) (t : k) :
    zeroLocus k (Ideal.span ({p - C t} : Set (MvPolynomial σ k))) =
      {x : σ → k | aeval x p = t} := by
…
```