feat(ring_theory/witt_vector): classify 1d isocrystals (#12041)

To show an application of semilinear maps that are not linear or conjugate-linear, we formalized the one-dimensional version of a theorem by Dieudonné and Manin classifying the isocrystals over an algebraically closed field with positive characteristic. This work is described in a recent draft from @dupuisf , @hrmacbeth , and myself: https://arxiv.org/abs/2202.05360

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

docs/references.bib

@@ -405,6 +405,16 @@ @InProceedings{   deligne_formulaire
   mrreviewer    = {Jacques Velu}
 }
 
+@Misc{            dupuis-lewis-macbeth2022,
+  title         = {Formalized functional analysis with semilinear maps},
+  author        = {Frédéric Dupuis and Robert Y. Lewis and Heather
+                  Macbeth},
+  year          = {2022},
+  eprint        = {2202.05360},
+  archiveprefix = {arXiv},
+  primaryclass  = {cs.LO}
+}
+
 @Article{         dyckhoff_1992,
   author        = {Dyckhoff, Roy},
   title         = {Contraction-free sequent calculi for intuitionistic
@@ -915,6 +925,23 @@ @Book{            LurieSAG
   year          = {last updated 2018}
 }
 
+@Article{         manin1963,
+  author        = {Manin, Ju. I.},
+  title         = {Theory of commutative formal groups over fields of finite
+                  characteristic},
+  journal       = {Uspehi Mat. Nauk},
+  fjournal      = {Akademiya Nauk SSSR i Moskovskoe Matematicheskoe
+                  Obshchestvo. Uspekhi Matematicheskikh Nauk},
+  volume        = {18},
+  year          = {1963},
+  number        = {6 (114)},
+  pages         = {3--90},
+  issn          = {0042-1316},
+  mrclass       = {14.50 (14.49)},
+  mrnumber      = {0157972},
+  mrreviewer    = {E. C. Dade}
+}
+
 @Book{            marcus1977number,
   title         = {Number fields},
   author        = {Marcus, Daniel A and Sacco, Emanuele},
@@ -1426,22 +1453,6 @@ @TechReport{      zaanen1966
   number        = {EUR 3140.e}
 }
 
-@Article{         zorn1937,
-  author        = {Zorn, Max},
-  title         = {On a theorem of {E}ngel},
-  journal       = {Bull. Amer. Math. Soc.},
-  fjournal      = {Bulletin of the American Mathematical Society},
-  volume        = {43},
-  year          = {1937},
-  number        = {6},
-  pages         = {401--404},
-  issn          = {0002-9904},
-  mrclass       = {DML},
-  mrnumber      = {1563550},
-  doi           = {10.1090/S0002-9904-1937-06565-7},
-  url           = {https://doi.org/10.1090/S0002-9904-1937-06565-7},
-}
-
 @Article{         zbMATH06785026,
   author        = {John F. {Clauser} and Michael A. {Horne} and Abner
                   {Shimony} and Richard A. {Holt}},
@@ -1460,3 +1471,19 @@ @Article{         zbMATH06785026
   doi           = {10.1103/PhysRevLett.23.880},
   url           = {https://doi.org/10.1103/PhysRevLett.23.880}
 }
+
+@Article{         zorn1937,
+  author        = {Zorn, Max},
+  title         = {On a theorem of {E}ngel},
+  journal       = {Bull. Amer. Math. Soc.},
+  fjournal      = {Bulletin of the American Mathematical Society},
+  volume        = {43},
+  year          = {1937},
+  number        = {6},
+  pages         = {401--404},
+  issn          = {0002-9904},
+  mrclass       = {DML},
+  mrnumber      = {1563550},
+  doi           = {10.1090/S0002-9904-1937-06565-7},
+  url           = {https://doi.org/10.1090/S0002-9904-1937-06565-7}
+}

src/linear_algebra/basic.lean

@@ -2459,7 +2459,7 @@ variables (K) (M)
 open _root_.linear_map
 
 /-- Multiplying by a nonzero element `a` of the field `K` is a linear equivalence. -/
-def smul_of_ne_zero (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M :=
+@[simps] def smul_of_ne_zero (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M :=
 smul_of_unit $ units.mk0 a ha
 
 section

src/ring_theory/witt_vector/frobenius_fraction_field.lean

@@ -0,0 +1,262 @@
+/-
+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, Heather Macbeth
+-/
+
+import field_theory.is_alg_closed.basic
+import ring_theory.witt_vector.discrete_valuation_ring
+
+/-!
+# Solving equations about the Frobenius map on the field of fractions of `𝕎 k`
+
+The goal of this file is to prove `witt_vector.exists_frobenius_solution_fraction_ring`,
+which says that for an algebraically closed field `k` of characteristic `p` and `a, b` in the
+field of fractions of Witt vectors over `k`,
+there is a solution `b` to the equation `φ b * a = p ^ m * b`, where `φ` is the Frobenius map.
+
+Most of this file builds up the equivalent theorem over `𝕎 k` directly,
+moving to the field of fractions at the end.
+See `witt_vector.frobenius_rotation` and its specification.
+
+The construction proceeds by recursively defining a sequence of coefficients as solutions to a
+polynomial equation in `k`. We must define these as generic polynomials using Witt vector API
+(`witt_vector.witt_mul`, `witt_polynomial`) to show that they satisfy the desired equation.
+
+Preliminary work is done in the dependency `ring_theory.witt_vector.mul_coeff`
+to isolate the `n+1`st coefficients of `x` and `y` in the `n+1`st coefficient of `x*y`.
+
+This construction is described in Dupuis, Lewis, and Macbeth,
+[Formalized functional analysis via semilinear maps][dupuis-lewis-macbeth2022].
+We approximately follow an approach sketched on MathOverflow:
+<https://mathoverflow.net/questions/62468/about-frobenius-of-witt-vectors>
+
+The result is a dependency for the proof of `witt_vector.isocrystal_classification`,
+the classification of one-dimensional isocrystals over an algebraically closed field.
+-/
+
+noncomputable theory
+
+namespace witt_vector
+
+variables (p : ℕ) [hp : fact p.prime]
+local notation `𝕎` := witt_vector p
+
+namespace recursion_main
+
+/-!
+
+## The recursive case of the vector coefficients
+
+The first coefficient of our solution vector is easy to define below.
+In this section we focus on the recursive case.
+The goal is to turn `witt_poly_prod n` into a univariate polynomial
+whose variable represents the `n`th coefficient of `x` in `x * a`.
+
+-/
+
+section comm_ring
+include hp
+variables {k : Type*} [comm_ring k] [char_p k p]
+open polynomial
+
+/-- The root of this polynomial determines the `n+1`st coefficient of our solution. -/
+def succ_nth_defining_poly (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : fin (n+1) → k) : polynomial k :=
+X^p * C (a₁.coeff 0 ^ (p^(n+1))) - X * C (a₂.coeff 0 ^ (p^(n+1)))
+  + C (a₁.coeff (n+1) * ((bs 0)^p)^(p^(n+1)) +
+      nth_remainder p n (λ v, (bs v)^p) (truncate_fun (n+1) a₁) -
+      a₂.coeff (n+1) * (bs 0)^p^(n+1) - nth_remainder p n bs (truncate_fun (n+1) a₂))
+
+lemma succ_nth_defining_poly_degree [is_domain k] (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : fin (n+1) → k)
+  (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  (succ_nth_defining_poly p n a₁ a₂ bs).degree = p :=
+begin
+  have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n+1))).degree = p,
+  { rw [degree_mul, degree_C],
+    { simp only [nat.cast_with_bot, add_zero, degree_X, degree_pow, nat.smul_one_eq_coe] },
+    { exact pow_ne_zero _ ha₁ } },
+  have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n+1)) - X * C (a₂.coeff 0 ^ p ^ (n+1))).degree = p,
+  { rw [degree_sub_eq_left_of_degree_lt, this],
+    rw [this, degree_mul, degree_C, degree_X, add_zero],
+    { exact_mod_cast hp.out.one_lt },
+    { exact pow_ne_zero _ ha₂ } },
+  rw [succ_nth_defining_poly, degree_add_eq_left_of_degree_lt, this],
+  apply lt_of_le_of_lt (degree_C_le),
+  rw [this],
+  exact_mod_cast hp.out.pos
+end
+
+end comm_ring
+
+section is_alg_closed
+include hp
+variables {k : Type*} [field k] [char_p k p] [is_alg_closed k]
+
+lemma root_exists (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : fin (n+1) → k)
+  (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  ∃ b : k, (succ_nth_defining_poly p n a₁ a₂ bs).is_root b :=
+is_alg_closed.exists_root _ $
+  by simp [(succ_nth_defining_poly_degree p n a₁ a₂ bs ha₁ ha₂), hp.out.ne_zero]
+
+/-- This is the `n+1`st coefficient of our solution, projected from `root_exists`. -/
+def succ_nth_val (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : fin (n+1) → k)
+  (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : k :=
+classical.some (root_exists p n a₁ a₂ bs ha₁ ha₂)
+
+lemma succ_nth_val_spec (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : fin (n+1) → k)
+  (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  (succ_nth_defining_poly p n a₁ a₂ bs).is_root (succ_nth_val p n a₁ a₂ bs ha₁ ha₂) :=
+classical.some_spec (root_exists p n a₁ a₂ bs ha₁ ha₂)
+
+lemma succ_nth_val_spec' (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : fin (n+1) → k)
+  (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  (succ_nth_val p n a₁ a₂ bs ha₁ ha₂)^p * a₁.coeff 0 ^ (p^(n+1)) +
+    a₁.coeff (n+1) * ((bs 0)^p)^(p^(n+1)) +
+    nth_remainder p n (λ v, (bs v)^p) (truncate_fun (n+1) a₁)
+   = (succ_nth_val p n a₁ a₂ bs ha₁ ha₂) * a₂.coeff 0 ^ (p^(n+1)) +
+     a₂.coeff (n+1) * (bs 0)^(p^(n+1)) + nth_remainder p n bs (truncate_fun (n+1) a₂) :=
+begin
+  rw ← sub_eq_zero,
+  have := succ_nth_val_spec p n a₁ a₂ bs ha₁ ha₂,
+  simp only [polynomial.map_add, polynomial.eval_X, polynomial.map_pow, polynomial.eval_C,
+    polynomial.eval_pow, succ_nth_defining_poly, polynomial.eval_mul, polynomial.eval_add,
+    polynomial.eval_sub, polynomial.map_mul, polynomial.map_sub, polynomial.is_root.def] at this,
+  convert this using 1,
+  ring
+end
+
+end is_alg_closed
+end recursion_main
+
+namespace recursion_base
+include hp
+variables {k : Type*} [field k] [is_alg_closed k]
+
+lemma solution_pow (a₁ a₂ : 𝕎 k) :
+  ∃ x : k, x^(p-1) = a₂.coeff 0 / a₁.coeff 0 :=
+is_alg_closed.exists_pow_nat_eq _ $ by linarith [hp.out.one_lt, le_of_lt hp.out.one_lt]
+
+/-- The base case (0th coefficient) of our solution vector. -/
+def solution (a₁ a₂ : 𝕎 k) : k :=
+classical.some $ solution_pow p a₁ a₂
+
+lemma solution_spec (a₁ a₂ : 𝕎 k) :
+  (solution p a₁ a₂)^(p-1) = a₂.coeff 0 / a₁.coeff 0 :=
+classical.some_spec $ solution_pow p a₁ a₂
+
+lemma solution_nonzero {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  solution p a₁ a₂ ≠ 0 :=
+begin
+  intro h,
+  have := solution_spec p a₁ a₂,
+  rw [h, zero_pow] at this,
+  { simpa [ha₁, ha₂] using _root_.div_eq_zero_iff.mp this.symm },
+  { linarith [hp.out.one_lt, le_of_lt hp.out.one_lt] }
+end
+
+lemma solution_spec' {a₁ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (a₂ : 𝕎 k) :
+  (solution p a₁ a₂)^p * a₁.coeff 0 = (solution p a₁ a₂) * a₂.coeff 0 :=
+begin
+  have := solution_spec p a₁ a₂,
+  cases nat.exists_eq_succ_of_ne_zero hp.out.ne_zero with q hq,
+  have hq' : q = p - 1 := by simp only [hq, tsub_zero, nat.succ_sub_succ_eq_sub],
+  conv_lhs {congr, congr, skip, rw hq},
+  rw [pow_succ', hq', this],
+  field_simp [ha₁, mul_comm],
+end
+
+end recursion_base
+
+open recursion_main recursion_base
+
+section frobenius_rotation
+
+section is_alg_closed
+include hp
+variables {k : Type*} [field k] [char_p k p] [is_alg_closed k]
+
+/--
+Recursively defines the sequence of coefficients for `witt_vector.frobenius_rotation`.
+-/
+noncomputable def frobenius_rotation_coeff {a₁ a₂ : 𝕎 k}
+  (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : ℕ → k
+| 0       := solution p a₁ a₂
+| (n + 1) := succ_nth_val p n a₁ a₂ (λ i, frobenius_rotation_coeff i.val) ha₁ ha₂
+using_well_founded { dec_tac := `[apply fin.is_lt] }
+
+/--
+For nonzero `a₁` and `a₂`, `frobenius_rotation a₁ a₂` is a Witt vector that satisfies the
+equation `frobenius (frobenius_rotation a₁ a₂) * a₁ = (frobenius_rotation a₁ a₂) * a₂`.
+-/
+def frobenius_rotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : 𝕎 k :=
+witt_vector.mk p (frobenius_rotation_coeff p ha₁ ha₂)
+
+lemma frobenius_rotation_nonzero {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  frobenius_rotation p ha₁ ha₂ ≠ 0 :=
+begin
+  intro h,
+  apply solution_nonzero p ha₁ ha₂,
+  simpa [← h, frobenius_rotation, frobenius_rotation_coeff] using witt_vector.zero_coeff p k 0
+end
+
+lemma frobenius_frobenius_rotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
+  frobenius (frobenius_rotation p ha₁ ha₂) * a₁ = (frobenius_rotation p ha₁ ha₂) * a₂ :=
+begin
+  ext n,
+  induction n with n ih,
+  { simp only [witt_vector.mul_coeff_zero, witt_vector.coeff_frobenius_char_p,
+      frobenius_rotation, frobenius_rotation_coeff],
+    apply solution_spec' _ ha₁ },
+  { simp only [nth_remainder_spec, witt_vector.coeff_frobenius_char_p, frobenius_rotation_coeff,
+      frobenius_rotation, fin.val_eq_coe],
+    have := succ_nth_val_spec' p n a₁ a₂
+      (λ (i : fin (n + 1)), frobenius_rotation_coeff p ha₁ ha₂ i.val) ha₁ ha₂,
+    simp only [frobenius_rotation_coeff, fin.val_eq_coe, fin.val_zero] at this,
+    convert this using 4,
+    apply truncated_witt_vector.ext,
+    intro i,
+    simp only [fin.val_eq_coe, witt_vector.coeff_truncate_fun, witt_vector.coeff_frobenius_char_p],
+    refl }
+end
+
+local notation `φ` := is_fraction_ring.field_equiv_of_ring_equiv
+  (ring_equiv.of_bijective _ (frobenius_bijective p k))
+
+lemma exists_frobenius_solution_fraction_ring {a : fraction_ring (𝕎 k)} (ha : a ≠ 0) :
+  ∃ (b : fraction_ring (𝕎 k)) (hb : b ≠ 0) (m : ℤ), φ b * a = p ^ m * b :=
+begin
+  revert ha,
+  refine localization.induction_on a _,
+  rintros ⟨r, q, hq⟩ hrq,
+  rw mem_non_zero_divisors_iff_ne_zero at hq,
+  have : r ≠ 0 := λ h, hrq (by simp [h]),
+  obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r this,
+  obtain ⟨n, q', hq', rfl⟩ := exists_eq_pow_p_mul q hq,
+  let b := frobenius_rotation p hr' hq',
+  refine ⟨algebra_map (𝕎 k) _ b, _, m - n, _⟩,
+  { simpa only [map_zero] using
+      (is_fraction_ring.injective (witt_vector p k) (fraction_ring (witt_vector p k))).ne
+        (frobenius_rotation_nonzero p hr' hq')},
+  have key : witt_vector.frobenius b * p ^ m * r' * p ^ n = p ^ m * b * (p ^ n * q'),
+  { have H := congr_arg (λ x : 𝕎 k, x * p ^ m * p ^ n) (frobenius_frobenius_rotation p hr' hq'),
+    dsimp at H,
+    refine (eq.trans _ H).trans _; ring },
+  have hq'' : algebra_map (𝕎 k) (fraction_ring (𝕎 k)) q' ≠ 0,
+  { have hq''' : q' ≠ 0 := λ h, hq' (by simp [h]),
+    simpa only [ne.def, map_zero] using
+      (is_fraction_ring.injective (𝕎 k) (fraction_ring (𝕎 k))).ne hq''' },
+  rw zpow_sub₀ (fraction_ring.p_nonzero p k),
+  field_simp [fraction_ring.p_nonzero p k],
+  simp only [is_fraction_ring.field_equiv_of_ring_equiv,
+    is_localization.ring_equiv_of_ring_equiv_eq, ring_equiv.coe_of_bijective],
+  convert congr_arg (λ x, algebra_map (𝕎 k) (fraction_ring (𝕎 k)) x) key using 1,
+  { simp only [ring_hom.map_mul, ring_hom.map_pow, map_nat_cast],
+    ring },
+  { simp only [ring_hom.map_mul, ring_hom.map_pow, map_nat_cast] }
+end
+
+end is_alg_closed
+
+end frobenius_rotation
+
+end witt_vector