Birational projection coordinates admit a rational inverse in the original
coordinate ring. Its denominator cuts out all possible noninjective fibers.
This module gives no bound on the degree of that denominator;
ExceptionalCount converts a denominator of degree D into at most d * D
exceptional points.
theorem
CCDN.exists_curve_reconstruction_identities
{K : Type u_1}
{F : Type u_2}
{σ : Type u_3}
{τ : Type u_4}
[Field K]
[Field F]
[Algebra K F]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
(φ : MvPolynomial τ K ⧸ I →ₐ[K] F)
(hφ : Function.Injective ⇑φ)
(a : σ → MvPolynomial τ K)
(hgen : IntermediateField.adjoin K (Set.range fun (j : σ) => φ ((Ideal.Quotient.mk I) (a j))) = ⊤)
:
∃ (Q : MvPolynomial σ K) (P : τ → MvPolynomial σ K),
(MvPolynomial.aeval a) Q ∉ I ∧ ∀ (i : τ), (MvPolynomial.aeval a) Q * MvPolynomial.X i - (MvPolynomial.aeval a) (P i) ∈ I
Generation of the field gives reconstruction identities modulo the original ideal, with a denominator that does not vanish identically.
theorem
CCDN.projection_injective_off_reconstruction
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
(Q : MvPolynomial σ K)
(P : τ → MvPolynomial σ K)
(hP : ∀ (i : τ), (MvPolynomial.aeval a) Q * MvPolynomial.X i - (MvPolynomial.aeval a) (P i) ∈ I)
(z w : τ → K)
(hz : z ∈ idealZeroLocus I)
(hw : w ∈ idealZeroLocus I)
(hQ : (MvPolynomial.eval z) ((MvPolynomial.aeval a) Q) ≠ 0)
(he : (fun (j : σ) => (MvPolynomial.eval z) (a j)) = fun (j : σ) => (MvPolynomial.eval w) (a j))
:
Polynomial reconstruction gives injectivity at every source point where the denominator is nonzero.