Mathlib.RingTheory.WittVector.IsPoly._auxLemma.9
theorem Mathlib.RingTheory.WittVector.IsPoly._auxLemma.9 : ∀ {α : Sort u_1}, (α → True) = True
This theorem, named `Mathlib.RingTheory.WittVector.IsPoly._auxLemma.9`, states that for any type `α` (which can be any sort or kind), the statement "every element of type `α` satisfies the `True` proposition" is itself always `True`. It means the proposition that "for all elements of a certain type, a tautological statement holds" is always true regardless of the type.
More concisely: The theorem asserts that the proposition `(∀ x : α) (true : bool)` is always true for any type `α`.
|
WittVector.IsPoly₂.compLeft
theorem WittVector.IsPoly₂.compLeft :
∀ {p : ℕ} {g : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R}
{f : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [inst : WittVector.IsPoly₂ p g]
[inst : WittVector.IsPoly p f], WittVector.IsPoly₂ p fun _R _Rcr x y => g (f x) y
The theorem `WittVector.IsPoly₂.compLeft` states that for any natural number `p`, and any two polynomial functions `g` and `f`, where `g` is a binary polynomial function and `f` is a unary polynomial function, if `g` is a polynomial in two variables and `f` is a polynomial in one variable (within the context of a commutative ring `R`), then the composition of `g` with `f` in the first argument is also a polynomial in two variables. This new composed function takes two Witt vectors `x` and `y` as inputs, applies `f` to `x`, then feeds the result and `y` into `g`. This theorem is articulated within the space of the mathematical construct known as the Witt vector, denoted as `WittVector p R`.
More concisely: For any commutative ring R and binary polynomial g and unary polynomial f, the composition of g with f in the first argument is a polynomial in two variables within the Witt vector space WittVector p R.
|
WittVector.IsPoly.ext
theorem WittVector.IsPoly.ext :
∀ {p : ℕ} [inst : Fact p.Prime] {f g : ⦃R : Type u⦄ → [inst : CommRing R] → WittVector p R → WittVector p R},
WittVector.IsPoly p f →
WittVector.IsPoly p g →
(∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R) (n : ℕ),
(WittVector.ghostComponent n) (f x) = (WittVector.ghostComponent n) (g x)) →
∀ (R : Type u) [_Rcr : CommRing R] (x : WittVector p R), f x = g x
This theorem is stating that for any prime number `p` and any two functions `f` and `g` that take a `WittVector` with coefficients in a `CommRing R` and return a `WittVector` of the same kind, if both `f` and `g` are polynomials (this is what `WittVector.IsPoly p f` and `WittVector.IsPoly p g` represent), and for every commutative ring `R`, `WittVector` `x` and natural number `n`, the `n`th ghost component of `f(x)` is equal to the `n`th ghost component of `g(x)`, then `f(x)` is equal to `g(x)` for every `WittVector` `x` in the commutative ring `R`. In other words, if two polynomial functions acting on `WittVector`s give the same output when evaluated by the ghost component function for every `WittVector` and every natural number, then the two functions are the same.
More concisely: If `p` is a prime number, `f` and `g` are polynomial functions taking `WittVector` arguments with coefficients in a commutative ring `R`, and for all `WittVector x` and natural number `n`, the `n`th ghost component of `f(x)` equals the `n`th ghost component of `g(x)`, then `f(x) = g(x)` for all `WittVector x` in `R`.
|
WittVector.IsPoly₂.compRight
theorem WittVector.IsPoly₂.compRight :
∀ {p : ℕ} {g : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R → WittVector p R}
{f : ⦃R : Type u_3⦄ → [inst : CommRing R] → WittVector p R → WittVector p R} [inst : WittVector.IsPoly₂ p g]
[inst : WittVector.IsPoly p f], WittVector.IsPoly₂ p fun _R _Rcr x y => g x (f y)
The theorem `WittVector.IsPoly₂.compRight` asserts that, for any natural number `p`, a binary polynomial function `g` and a unary polynomial function `f` defined over any commutative ring `R`, the composition of `g` with `f` in the second argument is also a polynomial function. In mathematical terms, if `g` is a polynomial in two variables and `f` is a polynomial in one variable, then the function `g(x, f(y))` is a polynomial in two variables.
More concisely: For any commutative ring R, given a binary polynomial function g(x, y) and a unary polynomial function f(y) over R, the composition g(x, f(y)) is a polynomial function in two variables.
|