Laurent exponents of monomial fractions

A degree-zero fraction away from a monomial Xᵞ has, by DegreeZeroLocalization.exists_awayMk, the normal form p / (Xᵞ)ᵐ. When the numerator is itself a monomial Xᵝ, the fraction is determined by a single Laurent exponent

laurentExponent γ m β = β - m • γ  :  ι →₀ ℤ

with negative entries allowed exactly on the variables Xᵞ inverts. This file constructs that exponent and proves the three facts that make it an index: it determines the fraction, its Finsupp.degree is the twist d, and it is nonnegative off the support of γ.

Main definitions

• natToIntExponent — an exponent vector read in ℤ;
• laurentExponent — the Laurent exponent β - m • γ of the fraction Xᵝ / (Xᵞ)ᵐ.

Main statements

• awayMk_monomial_eq_iff_laurentExponent — two monomial fractions over powers of Xᵞ are equal exactly when their Laurent exponents agree. This is what makes the exponent an index rather than a convenience.
• degree_laurentExponent — the exponent has total degree d, the twist, with no dependence on m. Raising the denominator moves β and m • γ together, so this is the invariant that survives.
• laurentExponent_nonneg_of_apply_eq_zero — off the support of γ the exponent is nonnegative. Together with the previous statement this is the index set {α | Finsupp.degree α = d ∧ ∀ j ∉ γ.support, 0 ≤ α j} that #491's basis is indexed by.
• exists_sum_awayMk_monomial — the monomial fractions span. Every degree-zero fraction away from Xᵞ is a finite sum of monomial fractions over one common denominator, and laurentExponent_mem_index says the exponents they contribute are exactly the admissible ones.

Implementation notes

The equality criterion descends from DegreeZeroLocalization.awayMk_eq_awayMk_iff, which is where the domain hypothesis is spent, to MvPolynomial.monomial_eq_monomial_iff. Only the IsDomain R instance is needed: Module.IsTorsionFree R R is already an instance, so the polynomial case supplies nothing by hand.

laurentExponent is stated with m and β separate rather than packaged, because the caller that matters — a Čech cochain — produces them separately from exists_awayMk and never has the pair in hand.

Tags

Laurent monomial, homogeneous localization, projective space

Monomials as homogeneous denominators and numerators

theorem MvPolynomial.monomial_one_mem_polynomialGrading {ι R : Type u} [CommRing R] (γ : ι →₀ ℕ) : (monomial γ) 1 ∈ polynomialGrading ι R (Finsupp.degree γ)

Xᵞ is homogeneous of degree γ.degree, which is the certificate awayMk consumes.

theorem MvPolynomial.monomial_one_pow {ι R : Type u} [CommRing R] (γ : ι →₀ ℕ) (m : ℕ) : (monomial γ) 1 ^ m = (monomial (m • γ)) 1

theorem MvPolynomial.monomial_one_ne_zero {ι R : Type u} [CommRing R] [Nontrivial R] (γ : ι →₀ ℕ) : (monomial γ) 1 ≠ 0

theorem MvPolynomial.monomial_mem_natShift {ι R : Type u} [CommRing R] (γ β : ι →₀ ℕ) (d m : ℕ) (hβ : Finsupp.degree β = m • Finsupp.degree γ + d) : (monomial β) 1 ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)

A monomial of the right total degree is a legitimate numerator over (Xᵞ)ᵐ for the twist d.

The equality criterion

theorem MvPolynomial.awayMk_monomial_eq_iff {ι R : Type u} [CommRing R] [IsDomain R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] [AddSubgroupClass σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι R) 𝓜] (γ : ι →₀ ℕ) {m m' : ℕ} {β β' : ι →₀ ℕ} (hβ : (monomial β) 1 ∈ 𝓜 (m • Finsupp.degree γ)) (hβ' : (monomial β') 1 ∈ 𝓜 (m' • Finsupp.degree γ)) : GradedModule.DegreeZeroLocalization.awayMk ⋯ m ((monomial β) 1) hβ = GradedModule.DegreeZeroLocalization.awayMk ⋯ m' ((monomial β') 1) hβ' ↔ m' • γ + β = m • γ + β'

Two monomial fractions over powers of Xᵞ are equal exactly when they cross-multiply to the same monomial. This is awayMk_eq_awayMk_iff followed by monomial_eq_monomial_iff; the coefficient side of the latter is discharged by 1 ≠ 0.

theorem MvPolynomial.awayMk_monomial_eq_iff_laurentExponent {ι R : Type u} [CommRing R] [IsDomain R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] [AddSubgroupClass σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι R) 𝓜] (γ : ι →₀ ℕ) {m m' : ℕ} {β β' : ι →₀ ℕ} (hβ : (monomial β) 1 ∈ 𝓜 (m • Finsupp.degree γ)) (hβ' : (monomial β') 1 ∈ 𝓜 (m' • Finsupp.degree γ)) : GradedModule.DegreeZeroLocalization.awayMk ⋯ m ((monomial β) 1) hβ = GradedModule.DegreeZeroLocalization.awayMk ⋯ m' ((monomial β') 1) hβ' ↔ γ.laurentExponent m β = γ.laurentExponent m' β'

The Laurent exponent is a complete invariant of a monomial fraction.

This is the statement #491's basis is built on: the assignment (m, β) ↦ β - m • γ separates distinct fractions and identifies the ones that only differ by a common denominator. Combined with degree_laurentExponent and laurentExponent_nonneg_of_apply_eq_zero, it says the monomial fractions of the twist d are indexed by {α : ι →₀ ℤ | α.degree = d ∧ ∀ j, γ j = 0 → 0 ≤ α j}.

Spanning

awayMk_monomial_eq_iff_laurentExponent says the monomial fractions are indexed by their Laurent exponents. This section says they exhaust the localization: every degree-zero fraction away from Xᵞ is a finite sum of monomial fractions over one common denominator.

The route is short because both halves are already available. exists_awayMk puts an arbitrary element in the form p / (Xᵞ)ᵐ, MvPolynomial.as_sum splits the numerator, and awayMk_sum distributes the fraction over that splitting. No denominators have to be aligned afterwards: splitting a numerator never touches m.

theorem MvPolynomial.monomial_one_pow_ne_zero {ι R : Type u} [CommRing R] [Nontrivial R] (γ : ι →₀ ℕ) (n : ℕ) : (monomial γ) 1 ^ n ≠ 0

(Xᵞ)ⁿ is never zero, which is the hypothesis exists_awayMk consumes.

Twists of either sign, abstractly

The Laurent argument reads a numerator in exactly one way: an element of 𝓜 n is a homogeneous polynomial whose degree exceeds n by the twist. IsPolynomialTwist isolates that reading, so that the whole stack above it can be stated once and instantiated at natShift for d : ℕ and at intShift for d : ℤ. Nothing else about the graded module is used, and in particular no step below needs the twist to be nonnegative.

The p = 0 disjunct is what makes intShift fit: it carries zero in every degree, including the degrees where n + d is negative and there is no graded piece to name. For natShift the disjunct is redundant — zero lies in every homogeneous piece anyway — so the two instances have the same content.

def MvPolynomial.IsPolynomialTwist {ι R : Type u} [CommRing R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] (𝓜 : ℕ → σM) (d : ℤ) : Prop

𝓜 presents the degree-d twist of the polynomial grading: membership in 𝓜 n is homogeneity in degree n + d, read in ℤ so that either sign of d is expressible.

Equations

• MvPolynomial.IsPolynomialTwist 𝓜 d = ∀ (n : ℕ) (p : MvPolynomial ι R), p ∈ 𝓜 n ↔ p = 0 ∨ ∃ (e : ℕ), ↑e = ↑n + d ∧ p ∈ MvPolynomial.polynomialGrading ι R e

theorem MvPolynomial.isPolynomialTwist_natShift {ι R : Type u} [CommRing R] (d : ℕ) : IsPolynomialTwist (GradedModule.natShift (polynomialGrading ι R) d) ↑d

A nonnegative twist is a twist: natShift 𝒜 d n is literally 𝒜 (n + d).

theorem MvPolynomial.isPolynomialTwist_intShift {ι R : Type u} [CommRing R] (d : ℤ) : IsPolynomialTwist (GradedModule.intShift (polynomialGrading ι R) d) d

An integer twist is a twist, by definition of intShiftPiece.

theorem MvPolynomial.IsPolynomialTwist.degree_eq_of_mem_support {ι R : Type u} [CommRing R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {p : MvPolynomial ι R} (hp : p ∈ 𝓜 n) {β : ι →₀ ℕ} (hβ : β ∈ p.support) : ↑(Finsupp.degree β) = ↑n + d

Every exponent occurring in a numerator over (Xᵞ)ᵐ has total degree m • γ.degree + d, read in ℤ. This is homogeneity on the support, for a twist of either sign.

theorem MvPolynomial.IsPolynomialTwist.monomial_coeff_mem {ι R : Type u} [CommRing R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} {p : MvPolynomial ι R} (hp : p ∈ 𝓜 n) (β : ι →₀ ℕ) : (monomial β) (coeff β p) ∈ 𝓜 n

Each monomial of a numerator is itself a numerator, for a twist of either sign.

The statement is for every β, not only those in the support, because the splitting lemmas take a total membership hypothesis. Off the support the monomial is zero, which the p = 0 disjunct covers.

theorem MvPolynomial.IsPolynomialTwist.smul_mem {ι R : Type u} [CommRing R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {n : ℕ} (c : R) {p : MvPolynomial ι R} (hp : p ∈ 𝓜 n) : c • p ∈ 𝓜 n

A twist family is closed under the base-ring action: the graded pieces it is built from are submodules, and the zero disjunct is closed under anything.

theorem MvPolynomial.IsPolynomialTwist.degree_laurentExponent_of_mem_support {ι R : Type u} [CommRing R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {γ : ι →₀ ℕ} {m : ℕ} {p : MvPolynomial ι R} (hp : p ∈ 𝓜 (m • Finsupp.degree γ)) {β : ι →₀ ℕ} (hβ : β ∈ p.support) : Finsupp.degree (γ.laurentExponent m β) = d

The Laurent exponent of a monomial of a numerator has total degree the twist.

theorem MvPolynomial.degree_eq_of_mem_support {ι R : Type u} [CommRing R] {d m : ℕ} {γ : ι →₀ ℕ} {p : MvPolynomial ι R} (hp : p ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)) {β : ι →₀ ℕ} (hβ : β ∈ p.support) : Finsupp.degree β = m • Finsupp.degree γ + d

Every exponent occurring in a numerator of the twist d over (Xᵞ)ᵐ has total degree m • γ.degree + d. This is homogeneity read on the support.

theorem MvPolynomial.monomial_coeff_mem_natShift {ι R : Type u} [CommRing R] {d m : ℕ} {γ : ι →₀ ℕ} {p : MvPolynomial ι R} (hp : p ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)) (β : ι →₀ ℕ) : (monomial β) (coeff β p) ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)

Each monomial of a legitimate numerator is itself a legitimate numerator.

The statement is for every β, not only those in the support, because awayMk_sum takes a total membership hypothesis. Off the support the monomial is zero, which lies in every graded piece, so nothing is lost.

theorem MvPolynomial.awayMk_eq_sum_monomial {ι R : Type u} [CommRing R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] [AddSubgroupClass σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι R) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) {m : ℕ} (γ : ι →₀ ℕ) (p : MvPolynomial ι R) (hp : p ∈ 𝓜 (m • Finsupp.degree γ)) : GradedModule.DegreeZeroLocalization.awayMk ⋯ m p hp = ∑ β ∈ p.support, GradedModule.DegreeZeroLocalization.awayMk ⋯ m ((monomial β) (coeff β p)) ⋯

A fraction splits over the monomials of its numerator, at a fixed denominator.

Stated for a twist of either sign: IsPolynomialTwist.monomial_coeff_mem supplies the numerator certificate for each monomial, and nothing else here mentions the grading.

The local hcongr step is not decoration. MvPolynomial.as_sum rewrites p, which appears in the type of awayMk's membership argument, so rewriting it in the goal fails on a non-type-correct motive. Substituting the equation and appealing to proof irrelevance sidesteps that; the same obstruction is why awayMk_sum itself descends into LocalizedModule.

theorem MvPolynomial.exists_sum_awayMk_monomial {ι R : Type u} [CommRing R] [Nontrivial R] {σM : Type u} [SetLike σM (MvPolynomial ι R)] [AddSubgroupClass σM (MvPolynomial ι R)] {𝓜 : ℕ → σM} [SetLike.GradedSMul (polynomialGrading ι R) 𝓜] {d : ℤ} (h𝓜 : IsPolynomialTwist 𝓜 d) (γ : ι →₀ ℕ) (z : ↥(GradedModule.DegreeZeroLocalization (polynomialGrading ι R) 𝓜 (Submonoid.powers ((monomial γ) 1)))) : ∃ (m : ℕ) (p : MvPolynomial ι R) (hp : p ∈ 𝓜 (m • Finsupp.degree γ)), z = ∑ β ∈ p.support, GradedModule.DegreeZeroLocalization.awayMk ⋯ m ((monomial β) (coeff β p)) ⋯

The monomial fractions span. Every degree-zero fraction away from Xᵞ is a finite sum of monomial fractions over a single common denominator (Xᵞ)ᵐ.

The denominator is shared across the whole sum, which is what makes this usable: a map defined by its effect on monomial fractions extends without any further alignment.

theorem MvPolynomial.laurentExponent_mem_index {ι R : Type u} [CommRing R] {d m : ℕ} {γ : ι →₀ ℕ} {p : MvPolynomial ι R} (hp : p ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)) {β : ι →₀ ℕ} (hβ : β ∈ p.support) : Finsupp.degree (γ.laurentExponent m β) = ↑d ∧ ∀ (j : ι), γ j = 0 → 0 ≤ (γ.laurentExponent m β) j

Every exponent occurring in a spanning decomposition lands in the index set: total degree the twist, and nonnegative off the support of γ.

Together with exists_sum_awayMk_monomial and awayMk_monomial_eq_iff_laurentExponent this is the spanning half of #491's basis — the monomial fractions exhaust the localization, and the exponents they contribute are exactly the admissible ones.

Independence

Spanning says the monomial fractions reach everything. This section says they do so in exactly one way at a fixed denominator: a vanishing combination has vanishing coefficients.

DegreeZeroLocalization.awayMk_eq_zero_iff does the work by moving the question off the localization entirely — a fraction is zero exactly when its numerator is — after which it is the ordinary statement that distinct monomials of MvPolynomial are independent. Nothing here needs the Laurent exponent; it enters only when denominators differ, and there awayMk_monomial_eq_iff_laurentExponent already decides equality.

theorem MvPolynomial.sum_monomial_eq_zero_iff {ι R : Type u} [CommRing R] (s : Finset (ι →₀ ℕ)) (c : (ι →₀ ℕ) → R) : ∑ β ∈ s, (monomial β) (c β) = 0 ↔ ∀ β ∈ s, c β = 0

Distinct monomials are independent: a vanishing sum over a Finset of exponents has every coefficient zero.

theorem MvPolynomial.sum_awayMk_monomial_eq_zero_iff {ι R : Type u} [CommRing R] [IsDomain R] {γ : ι →₀ ℕ} {d m : ℕ} (s : Finset (ι →₀ ℕ)) (c : (ι →₀ ℕ) → R) (hc : ∀ (β : ι →₀ ℕ), (monomial β) (c β) ∈ GradedModule.natShift (polynomialGrading ι R) d (m • Finsupp.degree γ)) : ∑ β ∈ s, GradedModule.DegreeZeroLocalization.awayMk ⋯ m ((monomial β) (c β)) ⋯ = 0 ↔ ∀ β ∈ s, c β = 0

The monomial fractions are independent at a fixed denominator.

Combined with exists_sum_awayMk_monomial this is the basis statement of #491 in usable form: every element is a monomial combination over a common denominator, and that combination is unique. A map may therefore be defined by its effect on the monomial fractions, which is what the sign projection of #340's contracting homotopy needs.