WittVector.map_teichmuller
theorem WittVector.map_teichmuller :
∀ (p : ℕ) {R : Type u_1} {S : Type u_2} [hp : Fact p.Prime] [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S)
(r : R), (WittVector.map f) ((WittVector.teichmuller p) r) = (WittVector.teichmuller p) (f r)
The theorem `WittVector.map_teichmuller` states that for any prime `p`, and for any ring homomorphism `f` from `R` to `S` (where `R` and `S` are commutative rings), the "Teichmüller lift" operation and the "map" operation (which essentially applies `f` to each coefficient of a Witt vector) are commutative. In more specific terms, applying `f` to the result of the Teichmüller lift of an element `r` from `R` (i.e., `WittVector.map f (WittVector.teichmuller p r)`) yields the same result as first applying `f` to `r` and then performing the Teichmüller lift (i.e., `WittVector.teichmuller p (f r)`). This property is essentially saying that the Teichmüller lift is a "natural transformation" in the category-theoretic sense.
More concisely: For any prime `p` and ring homomorphism `f` from `R` to `S`, the Teichmüller lift `WittVector.teichmuller p` commutes with the `map` operation `WittVector.map f` on Witt vectors.
|
WittVector.ghostComponent_teichmuller
theorem WittVector.ghostComponent_teichmuller :
∀ (p : ℕ) {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] (r : R) (n : ℕ),
(WittVector.ghostComponent n) ((WittVector.teichmuller p) r) = r ^ p ^ n
This theorem states that the `n`-th ghost component of the Teichmüller lift of an element `r` from a commutative ring `R` to the ring of Witt vectors `𝕎 R`, under a prime number `p`, is equal to `r` raised to the power of `p` to the `n`-th power. In other words, it states that for any natural number `p` that is prime, any commutative ring `R`, any element `r` of `R`, and any natural number `n`, applying the `n`-th ghost component to the Teichmüller lift of `r` under `p`, gives the result as `r` raised to the power of `p` to the nth power.
More concisely: For any prime number p, commutative ring R, element r of R, and natural number n, the n-th ghost component of the Teichmüller lift of r under p equals r raised to the power of p to the n-th power.
|