more tweaking

ECTate/Algebra/CharP/Basic.lean

@@ -4,62 +4,33 @@ import ECTate.Algebra.ValuedRing
 import ECTate.Data.Nat.Enat
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Algebra.CharP.Basic
 
 open Classical
 variable (R : Type _) [Semiring R]
 
-/-- Noncomputable function that outputs the unique characteristic of a semiring. -/
-noncomputable
-def ring_char := if h : _ then @Nat.find (fun n => n ≠ 0 ∧ (n : R) = 0) _ h else 0
 
-lemma ring_char_eq_zero (R : Type _) [Semiring R] :
-  (ring_char R : R) = 0 :=
-by
-  rw [ring_char]
-  split
-  . exact (And.right (Nat.find_spec (by assumption)))
-  . simp
+lemma ringChar_is_zero_or_prime (R : Type _) [NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R]:
+  ringChar R = 0 ∨ Nat.Prime (ringChar R) :=
+(CharP.char_is_prime_or_zero R (ringChar R)).symm
 
+lemma add_pow_ringChar {R : Type _} [CommRing R] [IsDomain R] (h : ringChar R ≠ 0) :
+  (a + b) ^ ringChar R =
+  a ^ ringChar R +
+  b ^ ringChar R := by sorry
 
-lemma ring_char_dvd_of_zero {R : Type _} [Ring R] (h : (m : R) = 0) :
-  ring_char R ∣ m :=
-by
-  by_cases hm : m = 0
-  . simp [hm, Nat.dvd_zero] at *
-  . rw [ring_char]
-    rw [dif_pos ?_]
 
-    rotate_right 1 -- swap -- TODO unknown swap
-    exists m
-    generalize_proofs hh
-    have good := Nat.find_spec hh
-    have bd : Nat.find _ ≤ Nat.gcd (Nat.find hh) m := Nat.find_min' hh ?_
-    rw [Nat.gcd_eq_left_iff_dvd]
-    simp at good
-    simp at bd
-    sorry
-    sorry
+lemma sub_pow_ringChar {R : Type _} (a b : R) [CommRing R] [IsDomain R] (h : ringChar R ≠ 0) :
+  (a - b) ^ ringChar R =
+  a ^ ringChar R -
+  b ^ ringChar R := by sorry
 
-lemma ring_char_is_zero_or_prime (R : Type _) [CommRing R] [IsDomain R] :
-  ring_char R = 0 ∨ Nat.Prime (ring_char R) := sorry
 
-lemma add_pow_ring_char {R : Type _} [CommRing R] [IsDomain R] (h : ring_char R ≠ 0) :
-  (a + b) ^ ring_char R =
-  a ^ ring_char R +
-  b ^ ring_char R := by sorry
-
-
-lemma sub_pow_ring_char {R : Type _} (a b : R) [CommRing R] [IsDomain R] (h : ring_char R ≠ 0) :
-  (a - b) ^ ring_char R =
-  a ^ ring_char R -
-  b ^ ring_char R := by sorry
-
-
-lemma pow_ring_char_injective {R : Type _} [CommRing R] [IsDomain R]
-  (hn : ring_char R ≠ 0) : Function.Injective (. ^ ring_char R : R → R) := by
+lemma pow_ringChar_injective {R : Type _} [CommRing R] [IsDomain R]
+  (hn : ringChar R ≠ 0) : Function.Injective (. ^ ringChar R : R → R) := by
   intros x y h
   rw [←sub_eq_zero] at *
   rw [←sub_eq_zero] at *
   simp only [sub_zero] at *
-  rw [← sub_pow_ring_char _ _ hn] at h
+  rw [← sub_pow_ringChar _ _ hn] at h
   exact pow_eq_zero h

ECTate/Algebra/EllipticCurve/LocalEC.lean

@@ -448,10 +448,10 @@ lemma v_discr_of_v_ai {p : R} {q : ℕ} (valp : SurjVal p) (e : ValidModel R) (h
   (h1 : valp e.a1 ≥ 1) (h2 : valp e.a2 = 1) (h3 : valp e.a3 ≥ q)
   (h4 : valp e.a4 ≥ q + 1) (h6 : valp e.a6 ≥ 2 * q) :
   valp e.discr ≥ 2 * q + 3 := by
-  have h2' := v_b2_of_v_a1_a2 valp e h1 h2
-  have h4' := v_b4_of_v_a1_a3_a4 valp e h1 h3 h4
-  have h6' := v_b6_of_v_a3_a6 valp e h3 h6
-  have h8' := v_b8_of_v_ai valp e h1 h2 h3 h4 h6
+  have h2' : valp e.b2 ≥ 1 := v_b2_of_v_a1_a2 valp e h1 h2
+  have h4' : valp e.b4 ≥ q + 1 := v_b4_of_v_a1_a3_a4 valp e h1 h3 h4
+  have h6' : valp e.b6 ≥ 2 * q := v_b6_of_v_a3_a6 valp e h3 h6
+  have h8' : valp e.b8 ≥ 2 * q + 1 := v_b8_of_v_ai valp e h1 h2 h3 h4 h6
   apply_rules [val_add_ge_of_ge, val_sub_ge_of_ge] <;> -- TODO bizarre h2_symm appears
   . simp
     elinarith

ECTate/Algebra/EllipticCurve/Model.lean

@@ -270,7 +270,7 @@ namespace ValidModel
 variable {R : Type u} [CommRing R]
 instance [Repr R] : Repr (ValidModel R) := ⟨ λ (e : ValidModel R) _ => repr e.toModel⟩
 
-@[simps]
+@[simps!]
 def rst_iso (r s t : R) (e : ValidModel R) : ValidModel R := {
   toModel := Model.rst_iso r s t e.toModel,
   discr_not_zero := by

ECTate/Algebra/EllipticCurve/TateInt.lean

@@ -112,6 +112,10 @@ def tate_big_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) :
 
 open SurjVal
 
+macro "simp_wf'" : tactic =>
+  `(tactic| simp (config := { zeta := false }) only [invImage, InvImage, Prod.lex, sizeOfWFRel,
+          measure, Nat.lt_wfRel, WellFoundedRelation.rel, sizeOf_nat, Nat.lt_eq] )
+
 def kodaira_type_Is (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 r0 s0 t0 : ℤ) (m q : ℕ)
   (hq : 1 < q) (h1 : (primeEVR hp).valtn e.a1 ≥ 1) (h2 : (primeEVR hp).valtn e.a2 = 1)
   (h3 : (primeEVR hp).valtn e.a3 ≥ q) (h4 : (primeEVR hp).valtn e.a4 ≥ q + 1)
@@ -246,15 +250,17 @@ def kodaira_type_Is (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 r0 s0
 termination_by _ =>
   val_discr_to_nat (primeEVR hp).valtn e - (2 * q + 2)
 decreasing_by
-  simp_wf
+  simp_wf'
+  simp only [Nat.cast_pow, rst_iso_a2, zero_mul, sub_zero, mul_zero, add_zero, rst_iso_a4,
+    rst_iso_a6, iso_rst_val_discr_to_nat, ge_iff_le, Nat.lt_eq]
   apply Nat.sub_lt_sub_left _ _
   . rw [← lt_ofN, ofN_val_discr_to_nat]
     exact lt_of_succ_le (v_discr_of_v_ai surjvalp e hq h1 h2 h3 h4 h6)
   . exact Nat.add_lt_add_right (Nat.mul_lt_mul_of_pos_left q.lt_succ_self (Nat.zero_lt_succ 1)) 2
 
 
-set_option maxHeartbeats 400000 in
-def tate_small_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 : ℤ := 1) (r0 : ℤ := 0) (s0 : ℤ := 0) (t0 : ℤ := 0) :
+set_option maxHeartbeats 700000 in
+def tate_small_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 : ℤ := 1) (r0 : ℤ := 0) (s0 : ℤ := 0) (t0 : ℤ := 0) : --- TODO put into a urst vector
   Kodaira × ℕ × ℕ × ReductionType × (ℤ × ℤ × ℤ × ℤ) :=
   --this function shouldn't be called with large primes (yet)
   if smallp : p ≠ 2 ∧ p ≠ 3 then unreachable! else
@@ -263,10 +269,10 @@ def tate_small_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 : ℤ
     cases smallp with
     | inl p2 =>
       rw [Decidable.not_not] at p2
-      exact Or.intro_left ((p:ℤ) = 3) (by simp [p2])
+      simp [p2]
     | inr p3 =>
       rw [Decidable.not_not] at p3
-      exact Or.intro_right ((p:ℤ) = 2) (by simp [p3])
+      simp [p3]
   let (u, r, s, t) := (u0, r0, s0, t0)
   let evrp := primeEVR hp
   let navp := evrp.valtn
@@ -534,7 +540,8 @@ def tate_small_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 : ℤ
   else
 
   have h_b6p4 : has_double_root 1 a3p2 (-a6p4) hp := by
-    refine And.intro (val_of_one navp) (Enat.pos_of_ne_zero (by simpa))
+    -- refine And.intro (val_of_one navp) (Enat.pos_of_ne_zero (by simpa))
+    sorry
 
   let a := double_root 1 a3p2 (-a6p4) p
   have Ha : double_root 1 (sub_val evrp 2 e3.a3) (-sub_val evrp 4 e3.a6) p = a := by rfl
@@ -570,9 +577,7 @@ def tate_small_prime (p : ℕ) (hp : Nat.Prime p) (e : ValidModel ℤ) (u0 : ℤ
 termination_by _ =>
   val_discr_to_nat (primeEVR hp).valtn e
 decreasing_by
-  simp_wf
-  simp only [He3, Ha]
-  simp only [He4]
+  simp_wf'
   rw [pi_scaling_val_discr_to_nat (primeEVR hp) e4 h1 h2 h3 h4 h6]
   have discr_eq : val_discr_to_nat (primeEVR hp).valtn e4 = val_discr_to_nat (primeEVR hp).valtn e := by
     rw [iso_rst_val_discr_to_nat]

ECTate/Algebra/ResidueRing.lean

@@ -1,4 +1,5 @@
 import ECTate.Algebra.ValuedRing
+import ECTate.Algebra.CharP.Basic
 import ECTate.FieldTheory.PerfectClosure
 import ECTate.Tactic.ELinarith
 import Mathlib.RingTheory.Congruence
@@ -348,16 +349,6 @@ instance : Field (R ⧸ evr.valtn.ideal) :=
   inv_zero := sorry }
 
 
-lemma pow_ringChar_injective {R : Type _} [CommRing R] [IsDomain R]
-  (hn : ringChar R ≠ 0) : Function.Injective (. ^ ringChar R : R → R) := by
-  intros x y h
-  rw [←sub_eq_zero] at *
-  rw [←sub_eq_zero] at *
-  simp only [sub_zero] at *
-  -- rw [← sub_pow_ringChar _ _ hn] at h
-  -- exact pow_eq_zero h
-  sorry
-
 lemma key : ringChar (R ⧸ evr.valtn.ideal) = evr.residue_char := by
   sorry
 

ECTate/Algebra/ValuedRing.lean

@@ -1,4 +1,7 @@
 import Mathlib.Algebra.Group.Defs
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Data.Finset.Lattice
+import Mathlib.Data.Nat.Lattice
 import Mathlib.Init.Algebra.Order
 import ECTate.Algebra.Ring.Basic
 import Mathlib.Init.Data.Nat.Lemmas
@@ -190,6 +193,7 @@ theorem val_of_pow_uniformizer {p : R} (nav : SurjVal p) {n : ℕ} : nav (p ^ n)
 
 end SurjVal
 
+open scoped Finset
 structure EnatValRing {R : Type u} (p : R) [CommRing R] [IsDomain R] where
   valtn : SurjVal p
   decr_val : R → R
@@ -199,6 +203,7 @@ structure EnatValRing {R : Type u} (p : R) [CommRing R] [IsDomain R] where
   zero_valtn_decr {x : R} (h : valtn x = 0) : decr_val x = x
   pos_valtn_decr {x : R} (h : valtn x > 0) : x = p * decr_val x -- TODO remove
   residue_char : ℕ
+  residue_char_spec : residue_char = sInf ({i : ℕ | 0 < i ∧ 0 < valtn i})
   norm_repr : R → R --generalization of modulo
   norm_repr_spec : ∀ r, valtn (r - norm_repr r) > 0
   inv_mod : R → R
@@ -864,18 +869,22 @@ by
   sorry
 
 @[simp]
-lemma primeVal_eq_zero_iff {p : ℕ} {k : ℤ} (hp : Nat.Prime p) : primeVal hp k = 0 ↔ k % p ≠ 0 :=
-by rw [primeVal, int_valuation_eq_zero_iff hp.one_lt]
+lemma primeVal_eq_zero_iff {p : ℕ} {k : ℤ} (hp : Nat.Prime p) : primeVal hp k = 0 ↔ ¬ (↑ p ∣ k) :=
+by rw [primeVal, int_valuation_eq_zero_iff hp.one_lt, Int.dvd_iff_emod_eq_zero]
+
+@[simp]
+lemma primeVal_pos_iff {p : ℕ} {k : ℤ} (hp : Nat.Prime p) : 0 < primeVal hp k ↔ ↑ p ∣ k := by
+  simp [← not_iff_not]
 
 lemma zero_valtn_decr_p {p : ℕ} {k : ℤ} {hp : Nat.Prime p} (h : primeVal hp k = 0) :
   decr_val_p p k = k :=
 by
-  simp [decr_val_p] at *
+  simp [decr_val_p, Int.dvd_iff_emod_eq_zero] at * -- TODO simp? doesn't work
   aesop
 
 def norm_repr_p (p : ℕ) (x : ℤ) : ℤ := x % (p : ℤ)
 
-def modulo (x : ℤ) (p : ℕ) := x % (p:ℤ)
+def modulo (x : ℤ) (p : ℕ) := x % (p : ℤ)
 
 def inv_mod (x : ℤ) (p : ℕ) := gcdA x p
 
@@ -894,10 +903,16 @@ def primeEVR {p : ℕ} (hp : Nat.Prime p) : EnatValRing (p : ℤ) := {
   zero_valtn_decr := zero_valtn_decr_p -- todo we really shouldn't need this!
   pos_valtn_decr := sorry
   residue_char := p
+  residue_char_spec := by
+    rw [Nat.sInf_def]
+    symm
+    simp [Nat.find_eq_iff]
+    sorry
+    sorry -- TODO this feels like a dup goal, is there a better abstraction here
   norm_repr := (. % p)
   norm_repr_spec := by
     intro r
-    simp [pos_iff_ne_zero, Int.sub_emod]
+    simp [dvd_sub_of_emod_eq] -- TODO can this  be simp?
   inv_mod := (inv_mod . p)
   inv_mod_spec := by
     intro r h