Evaluating symmetric polynomials

Main declarations

• pow_smul_sum_map_aroots_aeval_mem_range_algebraMap: Given k a multiple of p.leadingCoeff and e ≥ q.natDegree, k ^ e • ∑ i ∈ p.aroots A, q.aeval i lies in the base ring.
• MvPolynomial.symmetricSubalgebra.aevalMultiset evaluates a symmetric polynomial at the elements of a multiset.
• MvPolynomial.symmetricSubalgebra.sumPolynomial maps X to ∑ i, X i.

These are used in the proof of Lindemann-Weierstrass.

noncomputable def MvPolynomial.symmetricSubalgebra.aevalMultiset (σ : Type u_1) (R : Type u_3) {S : Type u_4} [Fintype σ] [CommRing R] [CommSemiring S] [Algebra R S] (m : Multiset S) : ↥(symmetricSubalgebra σ R) →ₐ[R] S

aevalMultiset evaluates a symmetric polynomial at the elements of s.

Equations

• MvPolynomial.symmetricSubalgebra.aevalMultiset σ R m = (MvPolynomial.aeval fun (i : Fin (Fintype.card σ)) => m.esymm (↑i + 1)).comp ↑(MvPolynomial.esymmAlgEquiv σ R ⋯).symm

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_apply {σ : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype σ] [CommRing R] [CommSemiring S] [Algebra R S] (m : Multiset S) (p : ↥(symmetricSubalgebra σ R)) : (aevalMultiset σ R m) p = (aeval fun (i : Fin (Fintype.card σ)) => m.esymm (↑i + 1)) ((esymmAlgEquiv σ R ⋯).symm p)

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_esymm {σ : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype σ] [CommRing R] [CommSemiring S] [Algebra R S] (m : Multiset S) (i : Fin (Fintype.card σ)) : (aevalMultiset σ R m) ⟨esymm σ R (↑i + 1), ⋯⟩ = m.esymm (↑i + 1)

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype σ] [CommRing R] [CommSemiring S] [Algebra R S] (f : σ → S) (p : ↥(symmetricSubalgebra σ R)) : (aevalMultiset σ R (Multiset.map f Finset.univ.val)) p = (aeval f) ↑p

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_map_of_card_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype σ] [Fintype τ] [CommRing R] [CommSemiring S] [Algebra R S] (f : τ → S) (p : ↥(symmetricSubalgebra σ R)) (h : Fintype.card σ = Fintype.card τ) : (aevalMultiset σ R (Multiset.map f Finset.univ.val)) p = (aeval (f ∘ ⇑(Fintype.equivOfCardEq h))) ↑p

noncomputable def MvPolynomial.symmetricSubalgebra.sumPolynomial (σ : Type u_1) {R : Type u_3} [Fintype σ] [CommRing R] (p : Polynomial R) : ↥(symmetricSubalgebra σ R)

sumPolynomial σ p is the map sending X to ∑ i, X i.

Equations

• MvPolynomial.symmetricSubalgebra.sumPolynomial σ p = ⟨∑ i : σ, (Polynomial.aeval (MvPolynomial.X i)) p, ⋯⟩

theorem MvPolynomial.symmetricSubalgebra.coe_sumPolynomial {σ : Type u_1} {R : Type u_3} [Fintype σ] [CommRing R] (p : Polynomial R) : ↑(sumPolynomial σ p) = ∑ i : σ, (Polynomial.aeval (X i)) p

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_sumPolynomial {σ : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype σ] [CommRing R] [CommSemiring S] [Algebra R S] {m : Multiset S} {p : Polynomial R} (hm : m.card = Fintype.card σ) : (aevalMultiset σ R m) (sumPolynomial σ p) = (Multiset.map (fun (x : S) => (Polynomial.aeval x) p) m).sum

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_mem {σ : Type u_1} {R : Type u_3} {S : Type u_4} [Fintype σ] [CommRing R] [CommSemiring S] [Algebra R S] (B : Subalgebra R S) {m : Multiset S} {p : ↥(symmetricSubalgebra σ R)} (h : ∀ i < Fintype.card σ, m.esymm (i + 1) ∈ B) : (aevalMultiset σ R m) p ∈ B

theorem MvPolynomial.symmetricSubalgebra.esymm_map_smul_aroots_mem_range_algebraMap {S : Type u_4} {A : Type u_5} [CommRing S] [CommRing A] [Algebra S A] [IsDomain A] {q : Polynomial S} {r : ℕ} (hsplit : (Polynomial.map (algebraMap S A) q).Splits) : (Multiset.map (fun (x : A) => q.leadingCoeff • x) (q.aroots A)).esymm r ∈ Set.range ⇑(algebraMap S A)

theorem MvPolynomial.symmetricSubalgebra.aevalMultiset_map_aroots_mem_range_algebraMap {σ : Type u_1} {R : Type u_3} {S : Type u_4} {A : Type u_5} [Fintype σ] [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [IsDomain A] {q : Polynomial S} {p : ↥(symmetricSubalgebra σ R)} (hsplit : (Polynomial.map (algebraMap S A) q).Splits) : (aevalMultiset σ R (Multiset.map (fun (x : A) => q.leadingCoeff • x) (q.aroots A))) p ∈ Set.range ⇑(algebraMap S A)

theorem Polynomial.leadingCoeff_pow_natDegree_smul_sum_map_aroots_aeval_mem_range_algebraMap {R : Type u_6} {A : Type u_7} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] (p q : Polynomial R) (hsplit : (map (algebraMap R A) p).Splits) : p.leadingCoeff ^ q.natDegree • (Multiset.map (fun (x : A) => (aeval x) q) (p.aroots A)).sum ∈ Set.range ⇑(algebraMap R A)

p.leadingCoeff ^ q.natDegree • ∑ i ∈ p.aroots A, q.aeval i lies in the base ring.

theorem Polynomial.pow_smul_sum_map_aroots_aeval_mem_range_algebraMap {R : Type u_6} {A : Type u_7} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] (p q : Polynomial R) (k : R) (e : ℕ) (hk : p.leadingCoeff ∣ k) (he : q.natDegree ≤ e) (hsplit : (map (algebraMap R A) p).Splits) : k ^ e • (Multiset.map (fun (x : A) => (aeval x) q) (p.aroots A)).sum ∈ Set.range ⇑(algebraMap R A)

Given k a multiple of p.leadingCoeff and e ≥ q.natDegree, k ^ e • ∑ i ∈ p.aroots A, q.aeval i lies in the base ring.