feat(ring_theory/witt_vector): Witt vectors over a domain are a domain (

#11346)




Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/ring_theory/witt_vector/basic.lean

@@ -246,6 +246,8 @@ lemma ghost_component_apply (n : ℕ) (x : 𝕎 R) : ghost_component n x = aeval
 
 @[simp] lemma ghost_map_apply (x : 𝕎 R) (n : ℕ) : ghost_map x n = ghost_component n x := rfl
 
+section invertible
+
 variables (p R) [invertible (p : R)]
 
 /-- `witt_vector.ghost_map` is a ring isomorphism when `p` is invertible in `R`. -/
@@ -257,4 +259,19 @@ def ghost_equiv : 𝕎 R ≃+* (ℕ → R) :=
 lemma ghost_map.bijective_of_invertible : function.bijective (ghost_map : 𝕎 R → ℕ → R) :=
 (ghost_equiv p R).bijective
 
+end invertible
+
+/-- `witt_vector.coeff x 0` as a `ring_hom` -/
+@[simps]
+def constant_coeff : 𝕎 R →+* R :=
+{ to_fun := λ x, x.coeff 0,
+  map_zero' := by simp,
+  map_one' := by simp,
+  map_add' := add_coeff_zero,
+  map_mul' := mul_coeff_zero }
+
+instance [nontrivial R] : nontrivial (𝕎 R) :=
+constant_coeff.domain_nontrivial
+
+
 end witt_vector

src/ring_theory/witt_vector/defs.lean

@@ -311,6 +311,12 @@ lemma neg_coeff (x : 𝕎 R) (n : ℕ) :
   (-x).coeff n = peval (witt_neg p n) ![x.coeff] :=
 by simp [has_neg.neg, eval, matrix.cons_fin_one]
 
+lemma add_coeff_zero (x y : 𝕎 R) : (x + y).coeff 0 = x.coeff 0 + y.coeff 0 :=
+by simp [add_coeff, peval]
+
+lemma mul_coeff_zero (x y : 𝕎 R) : (x * y).coeff 0 = x.coeff 0 * y.coeff 0 :=
+by simp [mul_coeff, peval]
+
 end coeff
 
 lemma witt_add_vars (n : ℕ) :

src/ring_theory/witt_vector/domain.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2022 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Y. Lewis
+-/
+
+import ring_theory.witt_vector.identities
+
+/-!
+
+# Witt vectors over a domain
+
+This file builds to the proof `witt_vector.is_domain`,
+an instance that says if `R` is an integral domain, then so is `𝕎 R`.
+It depends on the API around iterated applications
+of `witt_vector.verschiebung` and `witt_vector.frobenius`
+found in `identities.lean`.
+
+The [proof sketch](https://math.stackexchange.com/questions/4117247/ring-of-witt-vectors-over-an-integral-domain/4118723#4118723)
+goes as follows:
+any nonzero $x$ is an iterated application of $V$
+to some vector $w_x$ whose 0th component is nonzero (`witt_vector.verschiebung_nonzero`).
+Known identities (`witt_vector.iterate_verschiebung_mul`) allow us to transform
+the product of two such $x$ and $y$
+to the form $V^{m+n}\left(F^n(w_x) \cdot F^m(w_y)\right)$,
+the 0th component of which must be nonzero.
+
+## Main declarations
+
+* `witt_vector.iterate_verschiebung_mul_coeff` : an identity from [Haze09]
+* `witt_vector.is_domain`
+
+-/
+
+noncomputable theory
+open_locale classical
+
+namespace witt_vector
+open function
+
+variables {p : ℕ} {R : Type*}
+
+local notation `𝕎` := witt_vector p -- type as `\bbW`
+
+/-!
+## The `shift` operator
+-/
+
+/--
+`witt_vector.verschiebung` translates the entries of a Witt vector upward, inserting 0s in the gaps.
+`witt_vector.shift` does the opposite, removing the first entries.
+This is mainly useful as an auxiliary construction for `witt_vector.verschiebung_nonzero`.
+-/
+def shift (x : 𝕎 R) (n : ℕ) : 𝕎 R := mk p (λ i, x.coeff (n + i))
+
+lemma shift_coeff (x : 𝕎 R) (n k : ℕ) : (x.shift n).coeff k = x.coeff (n + k) :=
+rfl
+
+variables [hp : fact p.prime] [comm_ring R]
+include hp
+
+lemma verschiebung_shift (x : 𝕎 R) (k : ℕ) (h : ∀ i < k+1, x.coeff i = 0) :
+  verschiebung (x.shift k.succ) = x.shift k :=
+begin
+  ext ⟨j⟩,
+  { rw [verschiebung_coeff_zero, shift_coeff, h],
+    apply nat.lt_succ_self },
+  { simp only [verschiebung_coeff_succ, shift],
+    congr' 1,
+    rw [nat.add_succ, add_comm, nat.add_succ, add_comm] }
+end
+
+lemma eq_iterate_verschiebung {x : 𝕎 R} {n : ℕ} (h : ∀ i < n, x.coeff i = 0) :
+  x = (verschiebung^[n] (x.shift n)) :=
+begin
+  induction n with k ih,
+  { cases x; simp [shift] },
+  { dsimp, rw verschiebung_shift,
+    { exact ih (λ i hi, h _ (hi.trans (nat.lt_succ_self _))), },
+    { exact h } }
+end
+
+lemma verschiebung_nonzero {x : 𝕎 R} (hx : x ≠ 0) :
+  ∃ n : ℕ, ∃ x' : 𝕎 R, x'.coeff 0 ≠ 0 ∧ x = (verschiebung^[n] x') :=
+begin
+  have hex : ∃ k : ℕ, x.coeff k ≠ 0,
+  { by_contradiction hall,
+    push_neg at hall,
+    apply hx,
+    ext i,
+    simp only [hall, zero_coeff] },
+  let n := nat.find hex,
+  use [n, x.shift n],
+  refine ⟨nat.find_spec hex, eq_iterate_verschiebung (λ i hi, not_not.mp _)⟩,
+  exact nat.find_min hex hi,
+end
+
+/-!
+## Witt vectors over a domain
+
+If `R` is an integral domain, then so is `𝕎 R`.
+This argument is adapted from
+<https://math.stackexchange.com/questions/4117247/ring-of-witt-vectors-over-an-integral-domain/4118723#4118723>.
+-/
+
+instance [char_p R p] [no_zero_divisors R] : no_zero_divisors (𝕎 R) :=
+⟨λ x y, begin
+  contrapose!,
+  rintros ⟨ha, hb⟩,
+  rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩,
+  rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩,
+  refine ne_of_apply_ne (λ x, x.coeff (na + nb)) _,
+  rw [iterate_verschiebung_mul_coeff, zero_coeff],
+  refine mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0),
+end⟩
+
+instance [char_p R p] [is_domain R] : is_domain (𝕎 R) :=
+{ ..witt_vector.no_zero_divisors,
+  ..witt_vector.nontrivial }
+
+end witt_vector

src/ring_theory/witt_vector/identities.lean

@@ -17,6 +17,7 @@ In this file we derive common identities between the Frobenius and Verschiebung
 
 * `frobenius_verschiebung`: the composition of Frobenius and Verschiebung is multiplication by `p`
 * `verschiebung_mul_frobenius`: the “projection formula”: `V(x * F y) = V x * y`
+* `iterate_verschiebung_mul_coeff`: an identity from [Haze09] 6.2
 
 ## References
 
@@ -27,9 +28,9 @@ In this file we derive common identities between the Frobenius and Verschiebung
 
 namespace witt_vector
 
-variables {p : ℕ} {R : Type*} [fact p.prime] [comm_ring R]
+variables {p : ℕ} {R : Type*} [hp : fact p.prime] [comm_ring R]
 local notation `𝕎` := witt_vector p -- type as `\bbW`
-
+include hp
 noncomputable theory
 
 /-- The composition of Frobenius and Verschiebung is multiplication by `p`. -/
@@ -50,9 +51,120 @@ begin
         verschiebung_coeff_succ, h, one_pow], }
 end
 
+lemma coeff_p_pow_eq_zero [char_p R p] {i j : ℕ} (hj : j ≠ i) : (p ^ i : 𝕎 R).coeff j = 0 :=
+begin
+  induction i with i hi generalizing j,
+  { rw [pow_zero, one_coeff_eq_of_pos],
+    exact nat.pos_of_ne_zero hj },
+  { rw [pow_succ', ← frobenius_verschiebung, coeff_frobenius_char_p],
+    cases j,
+    { rw [verschiebung_coeff_zero, zero_pow],
+      exact nat.prime.pos hp.out },
+    { rw [verschiebung_coeff_succ, hi, zero_pow],
+      { exact nat.prime.pos hp.out },
+      { exact ne_of_apply_ne (λ (j : ℕ), j.succ) hj } } }
+end
+
 /-- The “projection formula” for Frobenius and Verschiebung. -/
 lemma verschiebung_mul_frobenius (x y : 𝕎 R) :
   verschiebung (x * frobenius y) = verschiebung x * y :=
 by { ghost_calc x y, rintro ⟨⟩; ghost_simp [mul_assoc] }
 
+lemma mul_char_p_coeff_zero [char_p R p] (x : 𝕎 R) : (x * p).coeff 0 = 0 :=
+begin
+  rw [← frobenius_verschiebung, coeff_frobenius_char_p, verschiebung_coeff_zero, zero_pow],
+  exact nat.prime.pos hp.out
+end
+
+lemma mul_char_p_coeff_succ [char_p R p] (x : 𝕎 R) (i : ℕ) :
+  (x * p).coeff (i + 1) = (x.coeff i)^p :=
+by rw [← frobenius_verschiebung, coeff_frobenius_char_p, verschiebung_coeff_succ]
+
+lemma verschiebung_frobenius [char_p R p] (x : 𝕎 R) :
+  verschiebung (frobenius x) = x * p :=
+begin
+  ext ⟨i⟩,
+  { rw [mul_char_p_coeff_zero, verschiebung_coeff_zero], },
+  { rw [mul_char_p_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_char_p], }
+end
+
+lemma verschiebung_frobenius_comm [char_p R p] :
+  function.commute (verschiebung : 𝕎 R → 𝕎 R) frobenius :=
+λ x, by rw [verschiebung_frobenius, frobenius_verschiebung]
+
+
+/-!
+## Iteration lemmas
+-/
+
+open function
+
+lemma iterate_verschiebung_coeff (x : 𝕎 R) (n k : ℕ) :
+  (verschiebung^[n] x).coeff (k + n) = x.coeff k :=
+begin
+  induction n with k ih,
+  { simp },
+  { rw [iterate_succ_apply', nat.add_succ, verschiebung_coeff_succ],
+    exact ih }
+end
+
+lemma iterate_verschiebung_mul_left (x y : 𝕎 R) (i : ℕ) :
+  (verschiebung^[i] x) * y = (verschiebung^[i] (x * (frobenius^[i] y))) :=
+begin
+  induction i with i ih generalizing y,
+  { simp },
+  { rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply'], refl }
+end
+
+section char_p
+
+variable [char_p R p]
+
+lemma iterate_verschiebung_mul (x y : 𝕎 R) (i j : ℕ) :
+  (verschiebung^[i] x) * (verschiebung^[j] y) =
+    (verschiebung^[i + j] ((frobenius^[j] x) * (frobenius^[i] y))) :=
+begin
+  calc
+  _ = (verschiebung^[i] (x * (frobenius^[i] ((verschiebung^[j] y))))) : _
+... = (verschiebung^[i] (x * (verschiebung^[j] ((frobenius^[i] y))))) : _
+... = (verschiebung^[i] ((verschiebung^[j] ((frobenius^[i] y)) * x))) : _
+... = (verschiebung^[i] ((verschiebung^[j] ((frobenius^[i] y) * (frobenius^[j] x))))) : _
+... = (verschiebung^[i + j] ((frobenius^[i] y) * (frobenius^[j] x))) : _
+... = _ : _,
+  { apply iterate_verschiebung_mul_left },
+  { rw verschiebung_frobenius_comm.iterate_iterate; apply_instance },
+  { rw mul_comm },
+  { rw iterate_verschiebung_mul_left },
+  { rw iterate_add_apply },
+  { rw mul_comm }
+end
+
+lemma iterate_frobenius_coeff (x : 𝕎 R) (i k : ℕ) :
+  ((frobenius^[i] x)).coeff k = (x.coeff k)^(p^i) :=
+begin
+  induction i with i ih,
+  { simp },
+  { rw [iterate_succ_apply', coeff_frobenius_char_p, ih],
+    ring_exp }
+end
+
+/-- This is a slightly specialized form of [Hazewinkel, *Witt Vectors*][Haze09] 6.2 equation 5. -/
+lemma iterate_verschiebung_mul_coeff (x y : 𝕎 R) (i j : ℕ) :
+  ((verschiebung^[i] x) * (verschiebung^[j] y)).coeff (i + j) =
+    (x.coeff 0)^(p ^ j) * (y.coeff 0)^(p ^ i) :=
+begin
+  calc
+  _ = (verschiebung^[i + j] ((frobenius^[j] x) * (frobenius^[i] y))).coeff (i + j) : _
+... = ((frobenius^[j] x) * (frobenius^[i] y)).coeff 0 : _
+... = (frobenius^[j] x).coeff 0 * ((frobenius^[i] y)).coeff 0 : _
+... = _ : _,
+  { rw iterate_verschiebung_mul },
+  { convert iterate_verschiebung_coeff _ _ _ using 2,
+    rw zero_add },
+  { apply mul_coeff_zero },
+  { simp only [iterate_frobenius_coeff] }
+end
+
+end char_p
+
 end witt_vector