From 409509d190aa8e6ef952d71b2983ce6069f375a6 Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Tue, 12 Nov 2024 21:33:19 +0000
Subject: [PATCH] fill in `valuation_comap` (#194)

* stash

* stash

* done?

* clean up
---
 .../FiniteAdeleRing/BaseChange.lean           | 78 ++++++++++++++++++-
 1 file changed, 74 insertions(+), 4 deletions(-)

diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 3097a39c..36710391 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -61,12 +61,82 @@ def comap (w : HeightOneSpectrum B) : HeightOneSpectrum A where
 
 open scoped algebraMap
 
+lemma mk_count_factors_map
+    (hAB : Function.Injective (algebraMap A B))
+    (w : HeightOneSpectrum B) (I : Ideal A) [DecidableEq (Associates (Ideal A))]
+  [DecidableEq (Associates (Ideal B))] [∀ p : Associates (Ideal A), Decidable (Irreducible p)]
+  [∀ p : Associates (Ideal B), Decidable (Irreducible p)] :
+    (Associates.mk w.asIdeal).count (Associates.mk (Ideal.map (algebraMap A B) I)).factors =
+    Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal *
+      (Associates.mk (comap A w).asIdeal).count (Associates.mk I).factors := by
+  classical
+  induction I using UniqueFactorizationMonoid.induction_on_prime with
+  | h₁ =>
+    rw [Associates.mk_zero, Ideal.zero_eq_bot, Ideal.map_bot, ← Ideal.zero_eq_bot,
+      Associates.mk_zero]
+    simp [Associates.count, Associates.factors_zero, w.associates_irreducible,
+      associates_irreducible (comap A w), Associates.bcount]
+  | h₂ I hI =>
+    obtain rfl : I = ⊤ := by simpa using hI
+    simp only [Submodule.zero_eq_bot, ne_eq, top_ne_bot, not_false_eq_true, Ideal.map_top]
+    simp only [← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one]
+    rw [Associates.count_zero (associates_irreducible _),
+      Associates.count_zero (associates_irreducible _), mul_zero]
+  | h₃ I p hI hp IH =>
+    simp only [Ideal.map_mul, ← Associates.mk_mul_mk]
+    have hp_bot : p ≠ ⊥ := hp.ne_zero
+    have hp_bot' := (Ideal.map_eq_bot_iff_of_injective hAB).not.mpr hp_bot
+    have hI_bot := (Ideal.map_eq_bot_iff_of_injective hAB).not.mpr hI
+    rw [Associates.count_mul (Associates.mk_ne_zero.mpr hp_bot) (Associates.mk_ne_zero.mpr hI)
+      (associates_irreducible _), Associates.count_mul (Associates.mk_ne_zero.mpr hp_bot')
+      (Associates.mk_ne_zero.mpr hI_bot) (associates_irreducible _)]
+    simp only [IH, mul_add]
+    congr 1
+    by_cases hw : (w.comap A).asIdeal = p
+    · have : Irreducible (Associates.mk p) := Associates.irreducible_mk.mpr hp.irreducible
+      rw [hw, Associates.factors_self this, Associates.count_some this]
+      simp only [UniqueFactorizationMonoid.factors_eq_normalizedFactors, Multiset.nodup_singleton,
+        Multiset.mem_singleton, Multiset.count_eq_one_of_mem, mul_one]
+      rw [count_associates_factors_eq hp_bot' w.2 w.3,
+        Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp_bot' w.2 w.3]
+    · have : (Associates.mk (comap A w).asIdeal).count (Associates.mk p).factors = 0 :=
+        Associates.count_eq_zero_of_ne (associates_irreducible _)
+          (Associates.irreducible_mk.mpr hp.irreducible)
+          (by rwa [ne_eq, Associates.mk_eq_mk_iff_associated, associated_iff_eq])
+      rw [this, mul_zero, eq_comm]
+      by_contra H
+      rw [eq_comm, ← ne_eq, Associates.count_ne_zero_iff_dvd hp_bot' (irreducible w),
+        Ideal.dvd_iff_le, Ideal.map_le_iff_le_comap] at H
+      apply hw (((Ideal.isPrime_of_prime hp).isMaximal hp_bot).eq_of_le (comap A w).2.ne_top H).symm
+
+lemma intValuation_comap (hAB : Function.Injective (algebraMap A B))
+    (w : HeightOneSpectrum B) (x : A) :
+    (comap A w).intValuation x ^
+    (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) =
+    w.intValuation (algebraMap A B x) := by
+  classical
+  have h_ne_zero : Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal ≠ 0 :=
+    Ideal.IsDedekindDomain.ramificationIdx_ne_zero
+      ((Ideal.map_eq_bot_iff_of_injective hAB).not.mpr (comap A w).3) w.2 Ideal.map_comap_le
+  by_cases hx : x = 0
+  · simpa [hx]
+  simp only [intValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
+  show (ite _ _ _) ^ _ = ite _ _ _
+  by_cases hx : x = 0
+  · subst hx; simp [h_ne_zero]
+  rw [map_eq_zero_iff _ hAB, if_neg hx, if_neg hx, ← Set.image_singleton, ← Ideal.map_span,
+    mk_count_factors_map _ _ hAB, mul_comm]
+  simp
+
 -- Need to know how the valuation `w` and its pullback are related on elements of `K`.
+omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] in
 lemma 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
-  sorry
+    (comap A w).valuation x ^
+    (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) =
+    w.valuation (algebraMap K L x) := by
+  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) x
+  simp [valuation, ← IsScalarTower.algebraMap_apply A K L, IsScalarTower.algebraMap_apply A B L,
+    ← intValuation_comap A B (algebraMap_injective_of_field_isFractionRing A B K L), div_pow]
 
 -- 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.