WittVector.map_frobeniusPoly.key₂
theorem WittVector.map_frobeniusPoly.key₂ :
∀ (p : ℕ) [hp : Fact p.Prime] {n i j : ℕ},
i ≤ n →
j < p ^ (n - i) →
j - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩ + n =
i + j + (n - i - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩)
This theorem, labeled `WittVector.map_frobeniusPoly.key₂`, is a key numerical identity required for the proof of `WittVector.map_frobeniusPoly`. It states that for a natural number `p` that is prime, and for given natural numbers `n`, `i`, and `j` such that `i` is less than or equal to `n` and `j` is less than `p` to the power of `(n - i)`, the equation `j - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩ + n` equals `i + j + (n - i - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩)`. The `WittVector.pnat_multiplicity` function here is presumably calculating the multiplicity of the prime `p` in the prime factorization of `j + 1`.
More concisely: For prime number p and natural numbers n, i, j with i <= n and j < p^(n-i), the equality i + j + (n-i - multiplicity of p in j+1) = j - multiplicity of p in the sequence (j+1, ...) holds.
|
WittVector.coeff_frobenius_charP
theorem WittVector.coeff_frobenius_charP :
∀ (p : ℕ) {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] [inst_1 : CharP R p] (x : WittVector p R) (n : ℕ),
(WittVector.frobenius x).coeff n = x.coeff n ^ p
This theorem, `WittVector.coeff_frobenius_charP`, states that, for any natural number `p`, any type `R` which is a commutative ring, and any Witt vector `x` in the ring `R`, if `R` has characteristic `p` and `p` is prime, then the `n`-th coefficient of the Frobenius endomorphism of `x` is equal to the `p`-th power of the `n`-th coefficient of `x`. In mathematical terms, if $\text{coeff}_{\text{frobenius}}(x,n) = \text{coeff}(x,n)^p$. This theorem is crucial in the field of number theory, particularly in the exploration of p-adic numbers and their applications.
More concisely: For any prime number p and Witt vector x in a commutative ring R of characteristic p, the n-th coefficient of the Frobenius endomorphism of x equals the p-th power of the n-th coefficient of x.
|
WittVector.ghostComponent_frobeniusFun
theorem WittVector.ghostComponent_frobeniusFun :
∀ {p : ℕ} {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] (n : ℕ) (x : WittVector p R),
(WittVector.ghostComponent n) x.frobeniusFun = (WittVector.ghostComponent (n + 1)) x
The theorem `WittVector.ghostComponent_frobeniusFun` states that for any prime number `p`, any commutative ring `R`, any natural number `n` and any Witt vector `x` in that ring, applying the `frobeniusFun` function to `x` and then evaluating the `n`th ghost component is equivalent to evaluating the `(n+1)`th ghost component of `x` directly. In other words, the action of the Frobenius function on a Witt vector effectively shifts the index of the ghost component by one.
More concisely: For any prime number p, commutative ring R, natural number n, and Witt vector x in R, the n-th ghost component of the FrobeniusFun(x) equals the (n+1)-th ghost component of x.
|
Mathlib.RingTheory.WittVector.Frobenius._auxLemma.5
theorem Mathlib.RingTheory.WittVector.Frobenius._auxLemma.5 :
∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], (α → b) = b
This theorem from the Mathlib's Ring Theory, specifically related to Witt Vectors and the Frobenius function, states that for any proposition `b` and any sort `α` (which is nonempty), the function type from `α` to `b` is equal to `b`. In other words, if there exists at least one element of type `α`, then a function that takes any `α` as input and returns a `b` is essentially equivalent to `b` itself.
More concisely: For any nonempty sort `α` and proposition `b`, the type of functions from `α` to `b` is equivalent to `b`.
|
WittVector.map_frobeniusPoly.key₁
theorem WittVector.map_frobeniusPoly.key₁ :
∀ (p : ℕ) [hp : Fact p.Prime] (n j : ℕ),
j < p ^ n → p ^ (n - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩) ∣ (p ^ n).choose (j + 1)
This theorem, `WittVector.map_frobeniusPoly.key₁`, states that for any prime number `p`, and any pair of natural numbers `n` and `j` such that `j` is less than `p` raised to the power of `n`, the prime power `p` raised to the power of (`n` minus the multiplicity of `p` in `j + 1`) divides the binomial coefficient of `p` raised to the power of `n` and `j + 1`. This is an important divisibility property used in the proof of `WittVector.map_frobeniusPoly`.
More concisely: For any prime number $p$ and natural numbers $n$ and $j$ with $j < p^n$, $p$ raises to the power of $n-v_p(j+1)$ divides the binomial coefficient $\binom{p^n}{j+1}$.
|