constantCoeff_wittStructureInt
theorem constantCoeff_wittStructureInt :
∀ (p : ℕ) {idx : Type u_2} [hp : Fact p.Prime] (Φ : MvPolynomial idx ℤ),
MvPolynomial.constantCoeff Φ = 0 → ∀ (n : ℕ), MvPolynomial.constantCoeff (wittStructureInt p Φ n) = 0
The `constantCoeff_wittStructureInt` theorem states that for any prime number `p` and any multivariate polynomial `Φ` with integer coefficients indexed by `idx`, if the constant coefficient of `Φ` is zero, then the constant coefficient of the `n`-th Witt structure of `Φ` is also zero, for all natural numbers `n`. Here, the Witt structure is a transformation that modifies the polynomial in a way depending upon the prime `p`.
More concisely: For any prime number p and multivariate polynomial Φ with integer coefficients, if the constant coefficient of Φ is zero then the constant coefficient of its n-th Witt structure modulo p is also zero for all natural numbers n.
|
map_wittStructureInt
theorem map_wittStructureInt :
∀ (p : ℕ) {idx : Type u_2} [hp : Fact p.Prime] (Φ : MvPolynomial idx ℤ) (n : ℕ),
(MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) =
wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n
The theorem `map_wittStructureInt` states that for any natural number `p`, which is a prime number, any multivariate polynomial `Φ` with coefficients in integers, and any natural number `n`, the multivariate polynomial obtained by mapping the Witt structure of `Φ` over integers to rational numbers (`ℚ`) using the ring homomorphism function (`Int.castRingHom ℚ`), is equal to the Witt structure of the multivariate polynomial obtained by mapping `Φ` itself to rational numbers. This theorem provides a link between the Witt structure of a polynomial over integers and its counterpart over rational numbers using a ring homomorphism.
More concisely: For any prime number p and multivariate polynomial Φ with integer coefficients, the Witt structure of Φ mapped to rational numbers via Int.castRingHom equals the Witt structure of Φ mapped to rational numbers directly.
|
wittStructureInt_vars
theorem wittStructureInt_vars :
∀ (p : ℕ) {idx : Type u_2} [hp : Fact p.Prime] [inst : Fintype idx] (Φ : MvPolynomial idx ℤ) (n : ℕ),
(wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
The theorem `wittStructureInt_vars` states that for any natural number `p`, any type `idx`, any multivariate polynomial `Φ` with coefficients in the set of integers, and any natural number `n`, if `p` is prime and `idx` is a finite type, then the set of variables appearing in the Witt structure of the polynomial `Φ` at the `n`th stage is a subset of the Cartesian product of the universal finite set and the set of natural numbers less than `n + 1`.
More concisely: For any prime number p, finite type idx, multivariate polynomial Φ with integer coefficients, and natural number n, the variables in the Witt structure of Φ at stage n are contained in the product of the universal finite set and the set {0, ..., n}.
|
wittStructureRat_rec
theorem wittStructureRat_rec :
∀ (p : ℕ) {idx : Type u_2} [hp : Fact p.Prime] (Φ : MvPolynomial idx ℚ) (n : ℕ),
wittStructureRat p Φ n =
MvPolynomial.C (1 / ↑p ^ n) *
((MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (wittPolynomial p ℚ n)) Φ -
(Finset.range n).sum fun i => MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
The theorem `wittStructureRat_rec` provides a recursive definition for the function `wittStructureRat`. For a given prime number `p`, and a multivariate polynomial `Φ` with rational coefficients indexed by `idx`, the theorem states that the `n`-th Witt Structure of `Φ` with respect to `p`, denoted `wittStructureRat p Φ n`, can be expressed in terms of previous Witt Structures (i.e., `wittStructureRat p Φ i` for `i` less than `n`).
Specifically, `wittStructureRat p Φ n` is equal to the constant polynomial `MvPolynomial.C (1 / ↑p ^ n)` times the difference between two terms: the first term being `Φ` after renaming and binding its variables according to the `n`-th Witt polynomial `wittPolynomial p ℚ n`, and the second term being the sum of `MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)` over all `i` in the range from `0` to `n-1`. Here, `MvPolynomial.C` creates a constant polynomial, `MvPolynomial.rename` renames all variables in a polynomial, and `MvPolynomial.bind₁` applies a function to all variables in a polynomial.
More concisely: The `n`-th Witt Structure of a multivariate polynomial `Φ` with rational coefficients with respect to a prime number `p` is given recursively as the constant `(1 / p^n)` times the difference between `Φ` with renamed and bound variables according to the `n`-th Witt polynomial and the sum of `p` raised to the `i`-th power times the `i`-th Witt Structure of `Φ` for `i` from `0` to `n-1`.
|