Point separation for polynomial sections

Powers of any nonzero element vanishing at the selected points give independent classes.

theorem CCDN.section_powers_independent {K : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [Field K] [CommRing A] [IsDomain A] [Algebra K A] [CommRing B] [Algebra K B] [Finite ι] (φ : A →ₐ[K] B) (h : ι → A) (hlin : LinearIndependent K fun (i : ι) => φ (h i)) (l : A) (hl : l ≠ 0) (hzero : φ l = 0) (N : ℕ) : LinearIndependent K fun (t : ι × Fin N) => h t.1 * l ^ ↑t.2

Powers of a nonzero element killed by an algebra homomorphism, times elements with independent images, form an independent family. The target algebra may be trivial.

theorem CCDN.separator_images_independent {K : Type u_1} {A : Type u_2} {ι : Type u_3} [Field K] [CommRing A] [Algebra K A] [Finite ι] [DecidableEq ι] (φ : ι → A →ₐ[K] K) (h : ι → A) (hsep : ∀ (i j : ι), (φ i) (h j) = if i = j then 1 else 0) : LinearIndependent K fun (j : ι) => (AlgHom.pi φ) (h j)

Elements separated by algebra homomorphisms have independent simultaneous images.

theorem CCDN.separator_powers_independent {K : Type u_1} {A : Type u_2} {ι : Type u_3} [Field K] [CommRing A] [IsDomain A] [Algebra K A] [Finite ι] [DecidableEq ι] (φ : ι → A →ₐ[K] K) (h : ι → A) (l : A) (hl : l ≠ 0) (hzero : ∀ (i : ι), (φ i) l = 0) (hsep : ∀ (i j : ι), (φ i) (h j) = if i = j then 1 else 0) (N : ℕ) : LinearIndependent K fun (t : ι × Fin N) => h t.1 * l ^ ↑t.2

Powers of a nonzero element times point separators are jointly independent when that element vanishes under all point evaluations.

theorem CCDN.exists_point_separators {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [Field K] [Finite ι] [DecidableEq ι] (z : ι → σ → K) (hz : Function.Injective z) : ∃ (h : ι → MvPolynomial σ K), ∀ (i j : ι), (MvPolynomial.eval (z i)) (h j) = if i = j then 1 else 0

Explicit polynomial interpolation at a finite family of distinct affine points.