From 0c8d1e14afe2dbef8315dd0fdb9a45a088240336 Mon Sep 17 00:00:00 2001
From: javierlcontreras <“jlopezcontreras10@gmail.com”>
Date: Mon, 11 Nov 2024 15:19:22 +0000
Subject: [PATCH] Proves continuity of map K_v -> L_w modulo some lemmas that
 need to be refactored in Mathlib

---
 .../FiniteAdeleRing/BaseChange.lean           | 46 ++++++++++++++-----
 .../Order/GroupWithZero/Unbundled.lean        | 16 +++++++
 .../Order/Monoid/Unbundled/TypeTags.lean      |  4 ++
 3 files changed, 55 insertions(+), 11 deletions(-)
 create mode 100644 FLT/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
 create mode 100644 FLT/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean

diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 7d65fbd2..246db965 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -1,4 +1,6 @@
 import Mathlib -- **TODO** fix when finished or if `exact?` is too slow
+import FLT.Mathlib.Algebra.Order.GroupWithZero.Unbundled
+import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
 /-!
 
 # Base change of adele rings.
@@ -60,7 +62,7 @@ def comap (w : HeightOneSpectrum B) : HeightOneSpectrum A where
 lemma map_comap (w : HeightOneSpectrum B) :
     (w.comap A).asIdeal.map (algebraMap A B) =
     w.asIdeal ^ ((Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal)) := by
-  -- This must be standard? Maybe a hole in the library for Dedekind domains
+  -- This mus t be standard? Maybe a hole in the library for Dedekind domains
   -- or maybe I just missed it?
   sorry
 
@@ -69,18 +71,23 @@ open scoped algebraMap
 
 
 -- Need to know how the valuation `w` and its pullback are related on elements of `K`.
-def valuation_comap (w : HeightOneSpectrum B) (x : K) :
-    (comap A w).valuation x =
-    w.valuation (algebraMap K L x) ^
-    (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) := by
+lemma valuation_comap (w : HeightOneSpectrum B) (x : K) :
+    w.valuation (algebraMap K L x) = (comap A w).valuation x ^
+    (comap A w).asIdeal.ramificationIdx (algebraMap A B) w.asIdeal := by
   -- This should follow from map_comap?
   sorry
 
+instance :  MulLeftStrictMono (WithZero (Multiplicative ℤ)) := sorry
+
+@[simp]
+lemma symm_monotone {a b : Multiplicative ℤ} : WithZero.unitsWithZeroEquiv.symm a ≤ WithZero.unitsWithZeroEquiv.symm b ↔ (a ≤ b)  := by
+  sorry
+
 -- Say w is a finite place of L lying above v a finite places
 -- of K. Then there's a ring hom K_v -> L_w.
 variable {B L} in
 noncomputable def adicCompletion_comap (w : HeightOneSpectrum B) :
-    (adicCompletion K (comap A w)) →+* (adicCompletion L w) :=
+    adicCompletion K (comap A w) →+* adicCompletion L w :=
   letI : UniformSpace K := (comap A w).adicValued.toUniformSpace;
   letI : UniformSpace L := w.adicValued.toUniformSpace;
   UniformSpace.Completion.mapRingHom (algebraMap K L) <| by
@@ -95,11 +102,28 @@ noncomputable def adicCompletion_comap (w : HeightOneSpectrum B) :
   rw [(@Valued.hasBasis_nhds_zero K _ _ _ (comap A w).adicValued).tendsto_iff
     (@Valued.hasBasis_nhds_zero L _ _ _ w.adicValued)]
   simp only [HeightOneSpectrum.adicValued_apply, Set.mem_setOf_eq, true_and, true_implies]
-  -- Modulo the fact that the division doesn't make sense, the next line is
-  -- "refine fun i ↦ ⟨i ^ (1 / Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal), fun _ h ↦ ?_⟩"
-  -- now use `valuation_comap` to finish
-  sorry
-
+  rw [WithZero.unitsWithZeroEquiv.forall_congr_left, Multiplicative.forall]
+  intro a
+  rw [WithZero.unitsWithZeroEquiv.exists_congr_left, Multiplicative.exists]
+  let m := Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal
+  have hm : m ≠ 0 := by
+    refine Ideal.IsDedekindDomain.ramificationIdx_ne_zero ?_ w.2 (Ideal.map_comap_le)
+    exact (Ideal.map_eq_bot_iff_of_injective (algebraMap_injective_of_field_isFractionRing A B K L)).not.mpr (comap A w).3
+  refine ⟨a / m, ?_⟩
+  simp_rw [valuation_comap A]
+  rintro x hx
+  refine (pow_lt_pow_left' hm hx).trans_le ?_
+  change _^m ≤ _
+  norm_cast
+  calc WithZero.unitsWithZeroEquiv.symm (Multiplicative.ofAdd (a / ↑m)) ^ m
+  _ = WithZero.unitsWithZeroEquiv.symm (Multiplicative.ofAdd (m • (a / ↑m))) := by
+    rw [ofAdd_nsmul]
+    symm
+    exact map_pow _ _ _
+  _ ≤ WithZero.unitsWithZeroEquiv.symm (Multiplicative.ofAdd a) := by
+    simp [-Int.ofAdd_mul, -map_zpow]
+    rw [mul_comm]
+    refine Int.mul_le_of_le_ediv (by positivity) le_rfl
 
 noncomputable local instance (w : HeightOneSpectrum B) :
     Algebra K (adicCompletion L w) := RingHom.toAlgebra <|
diff --git a/FLT/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/FLT/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
new file mode 100644
index 00000000..b66f4d6c
--- /dev/null
+++ b/FLT/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@@ -0,0 +1,16 @@
+import Mathlib.Algebra.Order.Ring.Basic
+
+variable {G₀ : Type*} [GroupWithZero G₀] [LinearOrder G₀]
+variable {a b : G₀}
+
+@[mono, gcongr, bound]
+theorem zpow_le_zpow_left (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n : ℤ, a ^ n ≤ b ^ n :=
+  by sorry
+
+@[mono, gcongr, bound]
+theorem zpow_lt_zpow_left (ha : 0 ≤ a) (hab : a < b) : ∀ {n : ℤ}, a ^ n < b ^ n :=
+  by sorry
+
+
+theorem lt_of_zpow_lt_zpow_left (n : ℤ) (hb : 0 ≤ b) (h : a^n < b^n) : a < b :=
+  lt_of_not_ge fun hn => not_lt_of_ge (zpow_le_zpow_left hb hn _) h
diff --git a/FLT/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean b/FLT/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
new file mode 100644
index 00000000..6abec17b
--- /dev/null
+++ b/FLT/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
@@ -0,0 +1,4 @@
+import Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+
+@[gcongr]
+alias ⟨_, ofAdd_mono⟩ := Multiplicative.ofAdd_le