Documentation

DerivedAlgGeo.Algebra.Finsupp.LaurentExponent

Laurent exponents of finitely supported natural vectors #

This file embeds finitely supported natural exponent vectors into integer exponent vectors and records the subtraction and degree identities used by Laurent monomials. It depends only on Finsupp; multivariate polynomials and graded localizations consume this API from their own algebraic layers.

source
noncomputable def Finsupp.natToIntExponent {ι : Type u} :
(ι →₀ ℕ) →+ ι →₀ ℤ

An exponent vector read in ℤ, so that an inverted variable can carry a negative exponent.

Equations
Instances For
    source
    theorem Finsupp.natToIntExponent_injective {ι : Type u} :
    Function.Injective ⇑natToIntExponent
    source
    theorem Finsupp.degree_natToIntExponent {ι : Type u} (β : ι →₀ ℕ) :
    degree (natToIntExponent β) = ↑(degree β)

    Reading an exponent vector in ℤ does not change its total degree.

    source
    noncomputable def Finsupp.laurentExponent {ι : Type u} (γ : ι →₀ ℕ) (m : ℕ) (β : ι →₀ ℕ) :
    ι →₀ ℤ

    The Laurent exponent of the formal fraction Xᵝ / (Xᵞ)ᵐ.

    Equations
    Instances For
      source
      @[simp]
      theorem Finsupp.laurentExponent_apply {ι : Type u} (γ : ι →₀ ℕ) (m : ℕ) (β : ι →₀ ℕ) (j : ι) :
      (γ.laurentExponent m β) j = ↑(β j) - ↑m * ↑(γ j)
      source
      theorem Finsupp.laurentExponent_eq_iff {ι : Type u} (γ : ι →₀ ℕ) (m m' : ℕ) (β β' : ι →₀ ℕ) :
      γ.laurentExponent m β = γ.laurentExponent m' β' ↔ m' • γ + β = m • γ + β'

      Laurent exponents agree exactly when the natural exponent vectors agree after clearing the formal denominators.

      source
      theorem Finsupp.degree_laurentExponent {ι : Type u} (γ β : ι →₀ ℕ) (m d : ℕ) (hβ : degree β = m • degree γ + d) :
      degree (γ.laurentExponent m β) = ↑d

      The total degree of a Laurent exponent after subtracting a natural denominator degree.

      source
      theorem Finsupp.laurentExponent_nonneg_of_apply_eq_zero {ι : Type u} (γ : ι →₀ ℕ) (m : ℕ) (β : ι →₀ ℕ) {j : ι} (hj : γ j = 0) :
      0 ≤ (γ.laurentExponent m β) j

      Off the support of γ, its Laurent exponent contribution is nonnegative.

      source
      theorem Finsupp.degree_laurentExponent_int {ι : Type u} (γ β : ι →₀ ℕ) (m : ℕ) (d : ℤ) (hβ : ↑(degree β) = m • ↑(degree γ) + d) :
      degree (γ.laurentExponent m β) = d

      The total-degree identity for an integer-valued twist.