Coordinate permutations preserve projective heights, homogeneous Hilbert functions, and prime coordinate ideals.

noncomputable def CCDN.projectivePermutedIdeal {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : Equiv.Perm (Fin (n + 1))) : Ideal (MvPolynomial (Fin (n + 1)) K)

The ideal obtained from I by permuting the coordinates by e: the polynomials f with rename e f ∈ I.

Equations

• CCDN.projectivePermutedIdeal I e = RingHom.ker ((Ideal.Quotient.mkₐ K I).comp ↑(MvPolynomial.renameEquiv K e))

theorem CCDN.mem_projectivePermutedIdeal {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : Equiv.Perm (Fin (n + 1))) (f : MvPolynomial (Fin (n + 1)) K) : f ∈ projectivePermutedIdeal I e ↔ (MvPolynomial.rename ⇑e) f ∈ I

A polynomial f lies in the permuted ideal projectivePermutedIdeal I e if and only if rename e f lies in I.

instance CCDN.projectivePermutedIdeal_isPrime {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) [I.IsPrime] (e : Equiv.Perm (Fin (n + 1))) : (projectivePermutedIdeal I e).IsPrime

theorem CCDN.projectiveCurveDegree_permuted {K : Type u_1} [Field K] {n d : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : Equiv.Perm (Fin (n + 1))) (hdegree : HasProjectiveCurveDegree I d) : HasProjectiveCurveDegree (projectivePermutedIdeal I e) d

Permuting the coordinates preserves the degree of a projective curve.

theorem CCDN.projectiveCount_le_permuted {n : ℕ} (I : Ideal (CoordinatePolynomial (n + 1))) (e : Equiv.Perm (Fin (n + 1))) (B : ℝ) : projectiveCount (projectiveIdealZeroLocus I) B ≤ projectiveCount (projectiveIdealZeroLocus (projectivePermutedIdeal I e)) B

Permuting the coordinates does not decrease the number of rational projective points of height at most B on the zero locus of I.