Lemma 12.7: nonresonant polynomials #
deformation-refinements.tex (lem:nonresonant-polynomials): grade k[t_1, …, t_s] by
deg t_i = χ_i in an abelian group L. If the χ_i are pairwise distinct and no χ_j is a
sum ∑ n_i χ_i with n_i ≥ 0 and ∑ n_i ≥ 2, then a homogeneous polynomial of weight χ_j
with zero constant term is a_j t_j.
The remark after the lemma ("characters forming part of an integer basis of a lattice satisfy
these hypotheses") is nonresonant_of_basis.
def
MultiplicativeBasisDeformations.Nonresonant
{L : Type u_2}
[AddCommGroup L]
{σ : Type u_3}
(χ : σ → L)
:
The nonresonance hypotheses of Lemma 12.7.
Instances For
theorem
MultiplicativeBasisDeformations.eq_C_mul_X_of_nonresonant
{k : Type u_1}
[CommRing k]
{L : Type u_2}
[AddCommGroup L]
{σ : Type u_3}
{χ : σ → L}
(hχ : Nonresonant χ)
(j : σ)
{F : MvPolynomial σ k}
(hF : MvPolynomial.IsWeightedHomogeneous χ F (χ j))
(h0 : MvPolynomial.constantCoeff F = 0)
:
∃ (a : k), F = MvPolynomial.C a * MvPolynomial.X j
Lemma 12.7.
theorem
MultiplicativeBasisDeformations.nonresonant_of_basis
{L : Type u_2}
[AddCommGroup L]
{σ : Type u_3}
{ι : Type u_4}
(B : Module.Basis ι ℤ L)
{e : σ → ι}
(he : Function.Injective e)
:
Nonresonant fun (i : σ) => B (e i)
Characters forming part of an integer basis are nonresonant.