|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Robert Y. Lewis. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Robert Y. Lewis, Heather Macbeth, Johan Commelin |
| 5 | +-/ |
| 6 | + |
| 7 | +import ring_theory.witt_vector.domain |
| 8 | +import ring_theory.witt_vector.mul_coeff |
| 9 | +import ring_theory.discrete_valuation_ring |
| 10 | +import tactic.linear_combination |
| 11 | + |
| 12 | +/-! |
| 13 | +
|
| 14 | +# Witt vectors over a perfect ring |
| 15 | +
|
| 16 | +This file establishes that Witt vectors over a perfect field are a discrete valuation ring. |
| 17 | +When `k` is a perfect ring, a nonzero `a : 𝕎 k` can be written as `p^m * b` for some `m : ℕ` and |
| 18 | +`b : 𝕎 k` with nonzero 0th coefficient. |
| 19 | +When `k` is also a field, this `b` can be chosen to be a unit of `𝕎 k`. |
| 20 | +
|
| 21 | +## Main declarations |
| 22 | +
|
| 23 | +* `witt_vector.exists_eq_pow_p_mul`: the existence of this element `b` over a perfect ring |
| 24 | +* `witt_vector.exists_eq_pow_p_mul'`: the existence of this unit `b` over a perfect field |
| 25 | +* `witt_vector.discrete_valuation_ring`: `𝕎 k` is a discrete valuation ring if `k` is a perfect |
| 26 | + field |
| 27 | +
|
| 28 | +-/ |
| 29 | + |
| 30 | +noncomputable theory |
| 31 | + |
| 32 | +namespace witt_vector |
| 33 | + |
| 34 | +variables {p : ℕ} [hp : fact p.prime] |
| 35 | +include hp |
| 36 | +local notation `𝕎` := witt_vector p |
| 37 | + |
| 38 | +section comm_ring |
| 39 | +variables {k : Type*} [comm_ring k] [char_p k p] |
| 40 | + |
| 41 | +/-- This is the `n+1`st coefficient of our inverse. -/ |
| 42 | +def succ_nth_val_units (n : ℕ) (a : units k) (A : 𝕎 k) (bs : fin (n+1) → k) : k := |
| 43 | +- ↑(a⁻¹ ^ (p^(n+1))) |
| 44 | +* (A.coeff (n + 1) * ↑(a⁻¹ ^ (p^(n+1))) + nth_remainder p n (truncate_fun (n+1) A) bs) |
| 45 | + |
| 46 | +/-- |
| 47 | +Recursively defines the sequence of coefficients for the inverse to a Witt vector whose first entry |
| 48 | +is a unit. |
| 49 | +-/ |
| 50 | +noncomputable def inverse_coeff (a : units k) (A : 𝕎 k) : ℕ → k |
| 51 | +| 0 := ↑a⁻¹ |
| 52 | +| (n + 1) := succ_nth_val_units n a A (λ i, inverse_coeff i.val) |
| 53 | + using_well_founded { dec_tac := `[apply fin.is_lt] } |
| 54 | + |
| 55 | +/-- |
| 56 | +Upgrade a Witt vector `A` whose first entry `A.coeff 0` is a unit to be, itself, a unit in `𝕎 k`. |
| 57 | +-/ |
| 58 | +def mk_unit {a : units k} {A : 𝕎 k} (hA : A.coeff 0 = a) : units (𝕎 k) := |
| 59 | +units.mk_of_mul_eq_one A (witt_vector.mk p (inverse_coeff a A)) |
| 60 | + begin |
| 61 | + ext n, |
| 62 | + induction n with n ih, |
| 63 | + { simp [witt_vector.mul_coeff_zero, inverse_coeff, hA] }, |
| 64 | + let H_coeff := A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) |
| 65 | + + nth_remainder p n (truncate_fun (n + 1) A) (λ (i : fin (n + 1)), inverse_coeff a A i), |
| 66 | + have H := units.mul_inv (a ^ p ^ (n + 1)), |
| 67 | + linear_combination (H, -H_coeff) { normalize := ff }, |
| 68 | + have ha : (a:k) ^ (p ^ (n + 1)) = ↑(a ^ (p ^ (n + 1))) := by norm_cast, |
| 69 | + have ha_inv : (↑(a⁻¹):k) ^ (p ^ (n + 1)) = ↑(a ^ (p ^ (n + 1)))⁻¹ := |
| 70 | + by exact_mod_cast inv_pow _ _, |
| 71 | + simp only [nth_remainder_spec, inverse_coeff, succ_nth_val_units, hA, fin.val_eq_coe, |
| 72 | + one_coeff_eq_of_pos, nat.succ_pos', H_coeff, ha_inv, ha, inv_pow], |
| 73 | + ring!, |
| 74 | + end |
| 75 | + |
| 76 | +@[simp] lemma coe_mk_unit {a : units k} {A : 𝕎 k} (hA : A.coeff 0 = a) : (mk_unit hA : 𝕎 k) = A := |
| 77 | +rfl |
| 78 | + |
| 79 | +end comm_ring |
| 80 | + |
| 81 | +section field |
| 82 | +variables {k : Type*} [field k] [char_p k p] |
| 83 | + |
| 84 | +lemma is_unit_of_coeff_zero_ne_zero (x : 𝕎 k) (hx : x.coeff 0 ≠ 0) : is_unit x := |
| 85 | +begin |
| 86 | + let y : kˣ := units.mk0 (x.coeff 0) hx, |
| 87 | + have hy : x.coeff 0 = y := rfl, |
| 88 | + exact (mk_unit hy).is_unit |
| 89 | +end |
| 90 | + |
| 91 | +variables (p) |
| 92 | +lemma irreducible : irreducible (p : 𝕎 k) := |
| 93 | +begin |
| 94 | + have hp : ¬ is_unit (p : 𝕎 k), |
| 95 | + { intro hp, |
| 96 | + simpa only [constant_coeff_apply, coeff_p_zero, not_is_unit_zero] |
| 97 | + using constant_coeff.is_unit_map hp, }, |
| 98 | + refine ⟨hp, λ a b hab, _⟩, |
| 99 | + obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0, |
| 100 | + { rw ← mul_ne_zero_iff, intro h, rw h at hab, exact p_nonzero p k hab }, |
| 101 | + obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0, |
| 102 | + obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0, |
| 103 | + cases m, { exact or.inl (is_unit_of_coeff_zero_ne_zero a ha) }, |
| 104 | + cases n, { exact or.inr (is_unit_of_coeff_zero_ne_zero b hb) }, |
| 105 | + rw iterate_verschiebung_mul at hab, |
| 106 | + apply_fun (λ x, coeff x 1) at hab, |
| 107 | + simp only [coeff_p_one, nat.add_succ, add_comm _ n, function.iterate_succ', function.comp_app, |
| 108 | + verschiebung_coeff_add_one, verschiebung_coeff_zero] at hab, |
| 109 | + exact (one_ne_zero hab).elim |
| 110 | +end |
| 111 | + |
| 112 | +end field |
| 113 | + |
| 114 | +section perfect_ring |
| 115 | +variables {k : Type*} [comm_ring k] [char_p k p] [perfect_ring k p] |
| 116 | + |
| 117 | +lemma exists_eq_pow_p_mul (a : 𝕎 k) (ha : a ≠ 0) : |
| 118 | + ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = p ^ m * b := |
| 119 | +begin |
| 120 | + obtain ⟨m, c, hc, hcm⟩ := witt_vector.verschiebung_nonzero ha, |
| 121 | + obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c, |
| 122 | + rw witt_vector.iterate_frobenius_coeff at hc, |
| 123 | + have := congr_fun (witt_vector.verschiebung_frobenius_comm.comp_iterate m) b, |
| 124 | + simp only [function.comp_app] at this, |
| 125 | + rw ← this at hcm, |
| 126 | + refine ⟨m, b, _, _⟩, |
| 127 | + { contrapose! hc, |
| 128 | + have : 0 < p ^ m := pow_pos (nat.prime.pos (fact.out _)) _, |
| 129 | + simp [hc, zero_pow this] }, |
| 130 | + { rw ← mul_left_iterate (p : 𝕎 k) m, |
| 131 | + convert hcm, |
| 132 | + ext1 x, |
| 133 | + rw [mul_comm, ← witt_vector.verschiebung_frobenius x] }, |
| 134 | +end |
| 135 | + |
| 136 | +end perfect_ring |
| 137 | + |
| 138 | +section perfect_field |
| 139 | +variables {k : Type*} [field k] [char_p k p] [perfect_ring k p] |
| 140 | + |
| 141 | +lemma exists_eq_pow_p_mul' (a : 𝕎 k) (ha : a ≠ 0) : |
| 142 | + ∃ (m : ℕ) (b : units (𝕎 k)), a = p ^ m * b := |
| 143 | +begin |
| 144 | + obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha, |
| 145 | + let b₀ := units.mk0 (b.coeff 0) h₁, |
| 146 | + have hb₀ : b.coeff 0 = b₀ := rfl, |
| 147 | + exact ⟨m, mk_unit hb₀, h₂⟩, |
| 148 | +end |
| 149 | + |
| 150 | +instance : discrete_valuation_ring (𝕎 k) := |
| 151 | +discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization |
| 152 | +begin |
| 153 | + refine ⟨p, irreducible p, λ x hx, _⟩, |
| 154 | + obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx, |
| 155 | + exact ⟨n, b, hb.symm⟩, |
| 156 | +end |
| 157 | + |
| 158 | +end perfect_field |
| 159 | +end witt_vector |
0 commit comments