TruncatedWittVector.commutes
theorem TruncatedWittVector.commutes :
∀ (p : ℕ) [hp : Fact p.Prime] (n : ℕ) {m : ℕ} (hm : n ≤ m),
(TruncatedWittVector.truncate hm).comp (TruncatedWittVector.zmodEquivTrunc p m).toRingHom =
(TruncatedWittVector.zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))
This theorem states that for any prime number `p` and natural numbers `n` and `m` such that `n` is less than or equal to `m`, there is a commutative diagram involving the integers modulo `p^n` and `p^m`, and the truncated Witt vectors of lengths `n` and `m` over the integers modulo `p`. This diagram involves the isomorphisms `TruncatedWittVector.zmodEquivTrunc` mapping from integers modulo a power of a prime to the corresponding truncated Witt vectors, the ring homomorphism `ZMod.castHom` mapping from integers modulo `p^n` to integers modulo `p^m`, and the truncation operation `TruncatedWittVector.truncate` mapping from truncated Witt vectors of length `m` to truncated Witt vectors of length `n`. Specifically, the diagram states that going from the integers modulo `p^n` to the truncated Witt vectors of length `n` and then to `m` is the same as going from the integers modulo `p^n` to the integers modulo `p^m` and then to the truncated Witt vectors of length `m`.
More concisely: For any prime number p and natural numbers n ≤ m, the diagram commutes between the integer modules p^n, the truncated Witt vectors of lengths n and m over the integers modulo p, and the ring homomorphism and truncation operations, i.e., TruncatedWittVector.truncate (ZMod.castHom (X : ZMod p^n) : TruncatedWittVector p X n) = TruncatedWittVector.truncate (X : ZMod p^m) : TruncatedWittVector p X m.
|
TruncatedWittVector.commutes_symm
theorem TruncatedWittVector.commutes_symm :
∀ (p : ℕ) [hp : Fact p.Prime] (n : ℕ) {m : ℕ} (hm : n ≤ m),
(TruncatedWittVector.zmodEquivTrunc p n).symm.toRingHom.comp (TruncatedWittVector.truncate hm) =
(ZMod.castHom ⋯ (ZMod (p ^ n))).comp (TruncatedWittVector.zmodEquivTrunc p m).symm.toRingHom
This theorem states that for a prime number `p` and natural numbers `n` and `m` with `n ≤ m`, there exists a commutative diagram with four mathematical objects and four morphisms between them. The objects are the `TruncatedWittVector` of `p` and `n` over the integers modulo `p`, the `TruncatedWittVector` of `p` and `m` over the integers modulo `p`, the integers modulo `p^n`, and the integers modulo `p^m`. The morphisms are the inverse of the unique isomorphism `TruncatedWittVector.zmodEquivTrunc` from integers modulo `p^n` to `TruncatedWittVector` of `p` and `n` over the integers modulo `p`, the ring homomorphism `TruncatedWittVector.truncate` that truncates a `TruncatedWittVector` of length `m` to a `TruncatedWittVector` of length `n`, the ring homomorphism `ZMod.castHom` from integers modulo `p^n` to a ring of characteristic dividing `p^n`, and the inverse of the unique isomorphism `TruncatedWittVector.zmodEquivTrunc` from integers modulo `p^m` to `TruncatedWittVector` of `p` and `m` over the integers modulo `p`. The theorem asserts that the composition of the morphisms along both paths in the diagram is the same.
More concisely: For a prime number p and natural numbers n ≤ m, the commutative diagram has four objects (TruncatedWittVector of p and n, TruncatedWittVector of p and m over integers modulo p, integers modulo p^n, and integers modulo p^m) and four morphisms (inverse of TruncatedWittVector.zmodEquivTrunc, TruncatedWittVector.truncate, ZMod.castHom, and inverse of TruncatedWittVector.zmodEquivTrunc), and their composition along both paths is equal.
|