Documentation

LeanPool.Stafford38.Proofs.WeylPurePower

Pure-power Weyl certificates #

This file formalizes the all-degree part of the one-variable Weyl--Bézout calculation. It works in an arbitrary ring containing a Weyl pair d * x - x * d = 1; the only coefficient input is the ordinary polynomial Bézout relation between the two disjoint Euler products.

The remaining universal monic problem is not hidden here: it is the passage from a pure power to a general monic polynomial.

source
def Stafford.eulerElement {A : Type u_1} [Ring A] (x d : A) :
A

The Euler element associated with the coordinate and momentum.

Equations
Instances For
    source
    def Stafford.fallingPolynomial :
    ℕ → Polynomial ℚ

    The monic polynomial with roots 0, ..., n - 1.

    Equations
    Instances For
      source
      def Stafford.risingPolynomial :
      ℕ → Polynomial ℚ

      The monic polynomial with roots -1, ..., -n.

      Equations
      Instances For
        source
        def Stafford.eulerPolynomialEval {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) :
        Polynomial ℚ →+* A

        Evaluation of a rational polynomial at the Euler element x*d.

        Equations
        Instances For
          source
          @[simp]
          theorem Stafford.eulerPolynomialEval_X {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) :
          (eulerPolynomialEval x d) Polynomial.X = x * d
          source
          @[simp]
          theorem Stafford.eulerPolynomialEval_C {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (q : ℚ) :
          (eulerPolynomialEval x d) (Polynomial.C q) = (algebraMap ℚ A) q
          source
          theorem Stafford.exists_eulerPolynomial_x_pow_mul_d_pow {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (h : d * x = x * d + 1) (n : ℕ) :
          ∃ (f : Polynomial ℚ), (eulerPolynomialEval x d) f = x ^ n * d ^ n

          Equal powers x^n*d^n are a rational polynomial in the Euler element.

          source
          theorem Stafford.exists_eulerPolynomial_d_pow_mul_x_pow {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (h : d * x = x * d + 1) (n : ℕ) :
          ∃ (f : Polynomial ℚ), (eulerPolynomialEval x d) f = d ^ n * x ^ n

          Equal powers d^n*x^n are also a rational polynomial in x*d.

          source
          theorem Stafford.pure_power_weyl_certificate {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (h : d * x = x * d + 1) (n : ℕ) (a b : Polynomial ℚ) (hab : a * fallingPolynomial n + b * risingPolynomial n = 1) :
          ∃ (p : A) (q : A), 1 = p * x ^ n + q * (x ^ n * d ^ n)

          The pure-power certificate, assuming the ordinary Euler products are coprime in the coefficient polynomial ring.

          source
          theorem Stafford.pure_power_weyl_certificate_exists {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (h : d * x = x * d + 1) (n : ℕ) :
          ∃ (p : A) (q : A), 1 = p * x ^ n + q * (x ^ n * d ^ n)
          source
          theorem Stafford.euler_products_right_bezout_exists {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (h : d * x = x * d + 1) (n : ℕ) :
          ∃ (u : A) (v : A), d ^ n * x ^ n * u + x ^ n * d ^ n * v = 1

          The two Euler products admit a Bezout identity with right cofactors. This is the orientation used by the canonical right quotient.

          source
          theorem Stafford.euler_products_polynomial_right_bezout_exists {A : Type u_1} [Ring A] [Algebra ℚ A] (x d : A) (h : d * x = x * d + 1) (n : ℕ) :
          ∃ (u : Polynomial ℚ) (v : Polynomial ℚ), d ^ n * x ^ n * (eulerPolynomialEval x d) u + x ^ n * d ^ n * (eulerPolynomialEval x d) v = 1

          The right Bezout cofactors may be retained as rational polynomials in the Euler element.

          source
          theorem Stafford.pure_power_translate_weyl_certificate_exists {A : Type u_1} [Ring A] [Algebra ℚ A] (x d c : A) (h : d * x = x * d + 1) (hcd : Commute c d) (n : ℕ) :
          ∃ (p : A) (q : A), 1 = p * (x - c) ^ n + q * ((x - c) ^ n * d ^ n)
          source
          theorem Stafford.nilpotent_constant_weyl_certificate_exists {A : Type u_1} [Ring A] [Algebra ℚ A] (x d e : A) (h : d * x = x * d + 1) (he : IsNilpotent e) (hcentral : ∀ (a : A), Commute e a) (n : ℕ) :
          ∃ (p : A) (q : A), 1 = p * (x ^ n - e) + q * ((x ^ n - e) * d ^ n)

          A nilpotent central constant can be added to a pure power without losing the Weyl--Bézout certificate. This is the formal constant-coefficient instance of the nilpotent thickening step; the general nilpotent coefficient ideal is deliberately not hidden in this statement.