Multivariate Polynomials
Results named in Tau Ceti's TauCeti.RingTheory.MvPolynomial modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremBuchberger's criterion#
A set G whose nonzero members have unit leading coefficients is a
Gröbner basis of I if and only if it generates I and the S-polynomial of any two members of G
has remainder 0 on division by G.
MonomialOrder.isGroebnerBasis_iff_span_eq_and_isRemainder_sPolynomial_zero.{u_1, u_2, u_3}
{σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)}
{I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) :
m.IsGroebnerBasis G I ↔
Ideal.span G = I ∧ ∀ g₁ ∈ G, ∀ g₂ ∈ G, m.IsRemainder (m.sPolynomial g₁ g₂) G 0
Lean
Formalized in Tau Ceti as MonomialOrder.isGroebnerBasis_iff_span_eq_and_isRemainder_sPolynomial_zero.
Other forms
Buchberger's criterion. Formalized in Tau Ceti as MonomialOrder.isGroebnerBasis_span_iff_isRemainder_sPolynomial_zero.
MonomialOrder.isGroebnerBasis_span_iff_isRemainder_sPolynomial_zero.{u_1, u_2, u_3} {σ : Type u_1}
{R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)}
(hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) :
m.IsGroebnerBasis G (Ideal.span G) ↔ ∀ g₁ ∈ G, ∀ g₂ ∈ G, m.IsRemainder (m.sPolynomial g₁ g₂) G 0
Buchberger's criterion. Formalized in Tau Ceti as MonomialOrder.isGroebnerBasis_span_of_isRemainder_sPolynomial_zero.
MonomialOrder.isGroebnerBasis_span_of_isRemainder_sPolynomial_zero.{u_1, u_2, u_3} {σ : Type u_1}
{R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)}
(hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g))
(hS : ∀ g₁ ∈ G, ∀ g₂ ∈ G, m.IsRemainder (m.sPolynomial g₁ g₂) G 0) :
m.IsGroebnerBasis G (Ideal.span G)
Sources
TheoremThe Cauchy identity#
for families f : σ → S and g : τ → S,
∑_λ s_λ(f) s_λ(g) t^{|λ|} = ∏_{i,j} (1 - fᵢ gⱼ t)⁻¹,
as power series over S, the coefficient of tⁿ on the left summing over the partitions λ of
n, and the factor (1 - fᵢ gⱼ t)⁻¹ on the right written as the geometric series
∑ₘ (fᵢ gⱼ)ᵐ tᵐ.
TauCeti.mk_sum_aeval_schurPoly_mul_aeval_schurPoly.{u_1, u_2, u_3, u_4} {σ : Type u_1}
{τ : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype σ] [Fintype τ] [CommSemiring R]
[CommSemiring S] [Algebra R S] (f : σ → S) (g : τ → S) :
(PowerSeries.mk fun n =>
∑ μ,
(MvPolynomial.aeval f) (TauCeti.schurPoly σ R μ) *
(MvPolynomial.aeval g) (TauCeti.schurPoly τ R μ)) =
∏ i, ∏ j, PowerSeries.mk fun m => (f i * g j) ^ m
Lean
Formalized in Tau Ceti as TauCeti.mk_sum_aeval_schurPoly_mul_aeval_schurPoly.
Other forms
The Cauchy identity in degree n. Formalized in Tau Ceti as TauCeti.sum_aeval_schurPoly_mul_aeval_schurPoly.
TauCeti.sum_aeval_schurPoly_mul_aeval_schurPoly.{u_1, u_2, u_3, u_4} {σ : Type u_1} {τ : Type u_2}
{R : Type u_3} {S : Type u_4} [Fintype σ] [DecidableEq σ] [Fintype τ] [DecidableEq τ]
[CommSemiring R] [CommSemiring S] [Algebra R S] (f : σ → S) (g : τ → S) (n : ℕ) :
∑ μ,
(MvPolynomial.aeval f) (TauCeti.schurPoly σ R μ) *
(MvPolynomial.aeval g) (TauCeti.schurPoly τ R μ) =
(MvPolynomial.aeval fun p => f p.1 * g p.2) (MvPolynomial.hsymm (σ × τ) R n)
Sources
Uses 1
TheoremThe dimension theorem at the origin#
let K be an algebraically closed extension of k.
Fewer than #σ polynomials in k[X_σ] vanishing at the origin have a common zero in K^σ other
than the origin.
MvPolynomial.exists_ne_zero_forall_aeval_eq_zero.{u_1, u_2, u_3} {k : Type u_1} {K : Type u_2}
{σ : Type u_3} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] [Finite σ]
{s : Finset (MvPolynomial σ k)} (hs : s.card < Nat.card σ)
(h0 : ∀ p ∈ s, MvPolynomial.constantCoeff p = 0) :
∃ x, x ≠ 0 ∧ ∀ p ∈ s, (MvPolynomial.aeval x) p = 0
Lean
Formalized in Tau Ceti as MvPolynomial.exists_ne_zero_forall_aeval_eq_zero.
Sources
TheoremThe dual Jacobi--Trudi identity#
The Schur polynomial of a Young diagram μ in the
alphabet Fin N is the determinant det (e_{μ'ᵢ - i + j})_{0 ≤ i, j < r} of elementary symmetric
polynomials, where μ'ᵢ is the length of the i-th column, for every r at least the number of
columns of μ. The index μ'ᵢ - i + j is an integer, and e_m = 0 for m < 0
(TauCeti.esymmInt).
TauCeti.diagramSchurPoly_eq_det_esymmInt.{u_1} {R : Type u_1} [CommRing R] (N : ℕ)
(μ : YoungDiagram) {r : ℕ} (hr : μ.rowLen 0 ≤ r) :
TauCeti.diagramSchurPoly N R μ =
(Matrix.of fun i j => TauCeti.esymmInt (Fin N) R (↑(μ.colLen ↑i) - ↑↑i + ↑↑j)).det
Lean
Formalized in Tau Ceti as TauCeti.diagramSchurPoly_eq_det_esymmInt.
Other forms
The dual Jacobi--Trudi identity for partitions. Formalized in Tau Ceti as Nat.Partition.schurPoly_eq_det_esymmInt.
Nat.Partition.schurPoly_eq_det_esymmInt.{u_1, u_2} {R : Type u_1} [CommRing R] {σ : Type u_2}
[Fintype σ] {n : ℕ} (μ : n.Partition) {r : ℕ} (hr : (YoungDiagram.ofPartition μ).rowLen 0 ≤ r) :
TauCeti.schurPoly σ R μ =
(Matrix.of fun i j =>
TauCeti.esymmInt σ R (↑((YoungDiagram.ofPartition μ).colLen ↑i) - ↑↑i + ↑↑j)).det
Sources
TheoremThe elimination theorem#
Let m be an elimination order for the variables e τ: every
monomial below a monomial in these variables is again a monomial in these variables. If G is a
Gröbner basis of I for m, then the members of G in the variables e τ form a Gröbner basis
of the elimination ideal I.comap (rename e) for every monomial order m' on τ which e
carries to m.
MonomialOrder.IsGroebnerBasis.comap_rename.{u_1, u_2, u_3, u_4, u_5} {σ : Type u_1} {τ : Type u_2}
{R : Type u_3} [CommSemiring R] {m : MonomialOrder σ} {m' : MonomialOrder τ} {e : τ → σ}
{G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I)
(hm :
∀ (a b : τ →₀ ℕ),
m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b))
(helim :
∀ (a b : σ →₀ ℕ), m.toSyn a ≤ m.toSyn b → ↑b.support ⊆ Set.range e → ↑a.support ⊆ Set.range e) :
m'.IsGroebnerBasis (⇑(MvPolynomial.rename e) ⁻¹' G) (Ideal.comap (MvPolynomial.rename e) I)
Used by 1
TheoremThe elimination theorem for the lexicographic order#
If e : τ → σ is strictly monotone
with image an upper set of variables, then the members of a lexicographic Gröbner basis of I in
the variables e τ form a lexicographic Gröbner basis of the elimination ideal.
MonomialOrder.IsGroebnerBasis.comap_rename_lex.{u_1, u_2, u_3} {σ : Type u_1} {τ : Type u_2}
{R : Type u_3} [CommSemiring R] {e : τ → σ} [LinearOrder σ] [WellFoundedGT σ] [LinearOrder τ]
[WellFoundedGT τ] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)}
(h : MonomialOrder.lex.IsGroebnerBasis G I) (he : StrictMono e) (hup : IsUpperSet (Set.range e)) :
MonomialOrder.lex.IsGroebnerBasis (⇑(MvPolynomial.rename e) ⁻¹' G)
(Ideal.comap (MvPolynomial.rename e) I)
Uses 1
TheoremEuler's identity (TauCeti.jacobiMatrixAt_mulVec_self)#
Euler's identity for the Jacobian matrix of a family of homogeneous polynomials: applied to the point itself, it returns each equation's value scaled by its degree.
TauCeti.jacobiMatrixAt_mulVec_self.{u_1, u_2, u_3} {R : Type u_1} {σ : Type u_2} {ι : Type u_3}
[CommSemiring R] [Fintype σ] {p : ι → MvPolynomial σ R} {d : ι → ℕ}
(hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) (v : σ → R) :
(TauCeti.jacobiMatrixAt p v).mulVec v = fun i => d i • (MvPolynomial.eval v) (p i)
TheoremThe Fischer decomposition#
every homogeneous polynomial of degree e + 2 is the sum of a
harmonic one and r² times a homogeneous polynomial of degree e. The sum is direct by
MvPolynomial.disjoint_ker_laplacian_map_mulLeft_normSq.
MvPolynomial.harmonicSubmodule_sup_map_mulLeft_normSq.{u_1, u_3} {σ : Type u_1} {K : Type u_3}
[Field K] [Fintype σ] [CharZero K] [Nonempty σ] (e : ℕ) :
MvPolynomial.harmonicSubmodule σ K (e + 2) ⊔
Submodule.map (LinearMap.mulLeft K (MvPolynomial.normSq σ K))
(MvPolynomial.homogeneousSubmodule σ K e) =
MvPolynomial.homogeneousSubmodule σ K (e + 2)
Lean
Formalized in Tau Ceti as MvPolynomial.harmonicSubmodule_sup_map_mulLeft_normSq.
Other forms
The Fischer decomposition, disjointness. Formalized in Tau Ceti as MvPolynomial.disjoint_ker_laplacian_map_mulLeft_normSq.
MvPolynomial.disjoint_ker_laplacian_map_mulLeft_normSq.{u_1, u_3} {σ : Type u_1} {K : Type u_3}
[Field K] [Fintype σ] [CharZero K] [Nonempty σ] (e : ℕ) :
Disjoint MvPolynomial.laplacian.ker
(Submodule.map (LinearMap.mulLeft K (MvPolynomial.normSq σ K))
(MvPolynomial.homogeneousSubmodule σ K e))
Sources
TheoremThe generalized Wronskian criterion#
Over a field of characteristic zero, a family of
multivariate polynomials is linearly independent if and only if some generalized Wronskian with
admissible rows |D k| ≤ k is nonzero.
MvPolynomial.linearIndependent_iff_exists_genWronskian_ne_zero.{u_3, u_4} {σ : Type u_3} {m : ℕ}
{K : Type u_4} [Field K] [CharZero K] {f : Fin m → MvPolynomial σ K} :
LinearIndependent K f ↔
∃ D, (∀ (k : Fin m), Finsupp.degree (D k) ≤ ↑k) ∧ MvPolynomial.genWronskian D f ≠ 0
Lean
Formalized in Tau Ceti as MvPolynomial.linearIndependent_iff_exists_genWronskian_ne_zero.
Sources
TheoremJacobi's bialternant formula#
For a Young diagram μ with at most N rows, the Schur
polynomial s_μ in the alphabet Fin N times the Vandermonde alternant a_δ, δ_j = N - 1 - j,
is the alternant a_{λ+δ} of the row lengths λ_j = μ.rowLen j shifted by the staircase:
s_μ · a_δ = a_{λ+δ}. This is the division-free form of s_μ = a_{λ+δ} / a_δ.
The row bound is necessary: for a taller shape s_μ vanishes, while the right-hand side, which
only sees the first N rows, need not.
TauCeti.diagramSchurPoly_mul_alternant.{u_1} {R : Type u_1} [CommRing R] (N : ℕ) (μ : YoungDiagram)
(hμ : μ.colLen 0 ≤ N) :
(TauCeti.diagramSchurPoly N R μ * TauCeti.alternant (Fin N) R fun j => N - 1 - ↑j) =
TauCeti.alternant (Fin N) R fun j => μ.betaNumber N ↑j
Lean
Formalized in Tau Ceti as TauCeti.diagramSchurPoly_mul_alternant.
Other forms
Jacobi's bialternant formula for partitions. Formalized in Tau Ceti as TauCeti.schurPoly_mul_alternant.
TauCeti.schurPoly_mul_alternant.{u_1, u_2} {R : Type u_1} [CommRing R] {σ : Type u_2} [Fintype σ]
{n : ℕ} (μ : n.Partition) (hμ : (YoungDiagram.ofPartition μ).colLen 0 ≤ Fintype.card σ) :
TauCeti.schurPoly σ R μ *
(MvPolynomial.rename ⇑(Fintype.equivFin σ).symm)
(TauCeti.alternant (Fin (Fintype.card σ)) R fun j => Fintype.card σ - 1 - ↑j) =
(MvPolynomial.rename ⇑(Fintype.equivFin σ).symm)
(TauCeti.alternant (Fin (Fintype.card σ)) R fun j =>
(YoungDiagram.ofPartition μ).betaNumber (Fintype.card σ) ↑j)
Sources
TheoremJacobi's complementary-minor identity for the two Toeplitz matrices of symmetric polynomials#
A minor of (h_{j - i}) on the rows ρ (p) and the columns π (p) is the
complementary minor of ((-1)^{j - i} e_{j - i}), on the rows π (m) and the columns ρ (m),
signed by π and ρ.
TauCeti.det_submatrix_hsymmToeplitz.{u_1, u_2, u_3, u_4} (σ : Type u_1) [Fintype σ] [DecidableEq σ]
(R : Type u_2) [CommRing R] {m : Type u_3} {p : Type u_4} [Fintype m] [Fintype p] [DecidableEq m]
[DecidableEq p] (N : ℕ) (e : m ⊕ p ≃ Fin N) (π ρ : Equiv.Perm (Fin N)) :
((TauCeti.hsymmToeplitz σ R N).submatrix (⇑ρ ∘ ⇑e ∘ Sum.inr) (⇑π ∘ ⇑e ∘ Sum.inr)).det =
↑↑(Equiv.Perm.sign π) * ↑↑(Equiv.Perm.sign ρ) *
((TauCeti.esymmToeplitz σ R N).submatrix (⇑π ∘ ⇑e ∘ Sum.inl) (⇑ρ ∘ ⇑e ∘ Sum.inl)).det
Uses 1 · Used by 1
TheoremThe Jacobi--Trudi identity#
The Schur polynomial of a Young diagram μ in the alphabet
Fin N is the determinant det (h_{μᵢ - i + j})_{0 ≤ i, j < r} of complete homogeneous symmetric
polynomials, for every r at least the number of rows of μ. The index μᵢ - i + j is an
integer, and h_m = 0 for m < 0 (TauCeti.hsymmInt).
There is no condition relating N to μ: when μ has more than N rows, both sides vanish.
TauCeti.diagramSchurPoly_eq_det_hsymmInt.{u_1} {R : Type u_1} [CommRing R] (N : ℕ)
(μ : YoungDiagram) {r : ℕ} (hr : μ.colLen 0 ≤ r) :
TauCeti.diagramSchurPoly N R μ =
(Matrix.of fun i j => TauCeti.hsymmInt (Fin N) R (↑(μ.rowLen ↑i) - ↑↑i + ↑↑j)).det
Lean
Formalized in Tau Ceti as TauCeti.diagramSchurPoly_eq_det_hsymmInt.
Other forms
The Jacobi--Trudi identity for partitions. Formalized in Tau Ceti as TauCeti.schurPoly_eq_det_hsymmInt.
TauCeti.schurPoly_eq_det_hsymmInt.{u_1, u_2} {R : Type u_1} [CommRing R] {σ : Type u_2} [Fintype σ]
[DecidableEq σ] {n : ℕ} (μ : n.Partition) {r : ℕ} (hr : μ.parts.card ≤ r) :
TauCeti.schurPoly σ R μ =
(Matrix.of fun i j =>
TauCeti.hsymmInt σ R (↑((YoungDiagram.ofPartition μ).rowLen ↑i) - ↑↑i + ↑↑j)).det
Sources
Uses 1 · Used by 1
TheoremThe Jacobian criterion in a ratio chart#
at a common zero b of a family of homogeneous
equations with b i ≠ 0, the Jacobian matrix of the dehomogenized equations at the coordinate
ratios b (i.succAbove j) / b i has the same rank as the Jacobian matrix of the homogeneous
equations at b.
TauCeti.rank_jacobiMatrixAt_dehomogenize_div.{u_3, u_4} {ι : Type u_3} {K : Type u_4} [Field K]
[Finite ι] {n : ℕ} (i : Fin (n + 1)) {p : ι → MvPolynomial (Fin (n + 1)) K} {d : ι → ℕ}
(hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) {b : Fin (n + 1) → K} (hi : b i ≠ 0)
(hb : ∀ (k : ι), (MvPolynomial.eval b) (p k) = 0) :
(TauCeti.jacobiMatrixAt (fun k => (TauCeti.dehomogenize i) (p k)) fun j =>
b (i.succAbove j) / b i).rank =
(TauCeti.jacobiMatrixAt p b).rank
Lean
Formalized in Tau Ceti as TauCeti.rank_jacobiMatrixAt_dehomogenize_div.
Other forms
The Jacobian criterion for a single equation. Formalized in Tau Ceti as TauCeti.mulVec_surjective_jacobiMatrixAt_iff_exists_eval_pderiv_ne_zero.
TauCeti.mulVec_surjective_jacobiMatrixAt_iff_exists_eval_pderiv_ne_zero.{u_2, u_3, u_4}
{σ : Type u_2} {ι : Type u_3} {K : Type u_4} [Field K] [Unique ι] [Fintype σ]
{p : ι → MvPolynomial σ K} {v : σ → K} :
Function.Surjective (TauCeti.jacobiMatrixAt p v).mulVec ↔
∃ j, (MvPolynomial.eval v) ((MvPolynomial.pderiv j) (p default)) ≠ 0
Sources
TheoremNewton's identities for a multiset#
k times the k-th elementary symmetric function of
the elements of s is an explicit combination of the lower elementary symmetric functions and
the power sums (s.map (· ^ j)).sum. This is MvPolynomial.mul_esymm_eq_sum evaluated at the
elements of s.
Multiset.mul_esymm_eq_sum.{u_1} {R : Type u_1} [CommRing R] (s : Multiset R) (k : ℕ) :
↑k * s.esymm k =
(-1) ^ (k + 1) *
∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 < k,
(-1) ^ a.1 * s.esymm a.1 * (Multiset.map (fun x => x ^ a.2) s).sum
Lean
Formalized in Tau Ceti as Multiset.mul_esymm_eq_sum.
Other forms
Newton's identities express eₖ through the power sums. Formalized in Tau Ceti as TauCeti.esymm_mem_adjoin_psum.
TauCeti.esymm_mem_adjoin_psum.{u_1, u_2} (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R]
[Algebra ℚ R] (k : ℕ) :
MvPolynomial.esymm σ R k ∈ Algebra.adjoin R (MvPolynomial.psum σ R '' Set.Icc 1 k)
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.