Projective affine charts commute with extension of coefficients. In particular the standard chart of a geometrically integral projective variety is geometrically integral.
theorem
CCDN.polynomialCoefficientLinear_affineChart
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{n : ℕ}
(φ : L →ₗ[K] K)
(f : MvPolynomial (Fin (n + 1)) L)
:
(polynomialCoefficientLinear φ) ((affineChart n) f) = (affineChart n) ((polynomialCoefficientLinear φ) f)
Applying a K-linear map φ : L → K to the coefficients commutes with the affine chart
affineChart n (setting the first variable to 1).
theorem
CCDN.projectiveChartIdeal_mem_iff_scaledHomogenize
{K : Type u_1}
[Field K]
{n D : ℕ}
(I : Ideal (MvPolynomial (Fin (n + 1)) K))
[I.IsPrime]
(hX : MvPolynomial.X 0 ∉ I)
(f : MvPolynomial (Fin n) K)
(hf : f.totalDegree ≤ D)
:
For a prime ideal I not containing X 0, a polynomial f of total degree at most D
lies in the chart ideal projectiveChartIdeal I if and only if its homogenization
scaledHomogenize D 1 f in degree D lies in I.
theorem
CCDN.projectiveChartIdeal_geometrically_prime
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{n : ℕ}
(I : Ideal (MvPolynomial (Fin (n + 1)) K))
[I.IsPrime]
[(Ideal.map (MvPolynomial.map (algebraMap K L)) I).IsPrime]
(hX : MvPolynomial.X 0 ∉ I)
:
(Ideal.map (MvPolynomial.map (algebraMap K L)) (projectiveChartIdeal I)).IsPrime
If a prime ideal I not containing X 0 stays prime after extending scalars from K to
L, then so does its affine chart ideal projectiveChartIdeal I.