Merge branch 'main' of github.com:ImperialCollegeLondon/FLT into main

.github/workflows/create-release.yml

@@ -4,13 +4,14 @@ on:
   push:
     branches:
       - main
-    paths:
-      - 'lean-toolchain'
-
+
 jobs:
   create_release:
+    paths:
+      - 'lean-toolchain'
+
     runs-on: ubuntu-latest
-
+    
     steps:
       - name: Checkout code
         uses: actions/checkout@v4

FLT/AutomorphicRepresentation/Example.lean

@@ -96,8 +96,7 @@ lemma _root_.Nat.sum_factorial_lt_factorial_succ {j : ℕ} (hj : 1 < j) :
     ∑ i ∈ range (j + 1), i ! < ∑ _i ∈ range (j + 1), j ! := ?_
     _ = (j + 1) * (j !) := by rw [sum_const, card_range, smul_eq_mul]
     _ = (j + 1)! := Nat.factorial_succ _
-  apply sum_lt_sum
-  apply (fun i hi => factorial_le <| by simpa only [mem_range, lt_succ] using hi)
+  apply sum_lt_sum (fun i hi => factorial_le <| by simpa only [mem_range, lt_succ] using hi) ?_
   use 0
   rw [factorial_zero]
   simp [hj]

FLT/Basic/Reductions.lean

@@ -254,17 +254,10 @@ lemma FreyCurve.j (P : FreyPackage) :
   rw [mul_div_right_comm, EllipticCurve.j, FreyCurve.Δ'inv, FreyCurve.c₄']
 
 private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b := by
-  cases le_or_lt 0 (a * b) with
-  | inl h =>
-    calc
-      0 < a * a + a * b + b * b := ?_
-      _ = _ := by ring
-    apply add_pos_of_nonneg_of_pos
-    apply add_nonneg (mul_self_nonneg _) h
-    apply mul_self_pos.mpr hb
-  | inr h =>
-    rw [sub_pos]
-    exact h.trans_le (sq_nonneg _)
+  rify
+  calc
+    (0 : ℝ) < (a ^ 2 + (a + b) ^ 2 + b ^ 2) / 2 := by positivity
+    _ = (a + b) ^ 2 - a * b := by ring
 
 /-- The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is
 a prime of bad reduction. -/
@@ -344,13 +337,14 @@ It follows that there is no Frey package.
 work of Mazur and Wiles/Ribet to rule out all possibilities for the
 $p$-torsion in the corresponding Frey curve. -/
 theorem FreyPackage.false (P : FreyPackage) : False := by
+  -- by Wiles' result, the p-torsion is not irreducible
   apply Wiles_Frey P
+  -- but by Mazur's result, the p-torsion is irreducible!
   exact Mazur_Frey P
+  -- Contradiction!
 
 -- Fermat's Last Theorem is true
 theorem Wiles_Taylor_Wiles : FermatLastTheorem := by
-  apply of_p_ge_5
-  intro p hp5 pp a b c ha hb _ h
-  refine Nonempty.elim ?_ FreyPackage.false
+  refine of_p_ge_5 fun p hp5 pp a b c ha hb _ h ↦  Nonempty.elim ?_ FreyPackage.false
   apply FreyPackage.of_not_FermatLastTheorem_p_ge_5 (a := a) (b := b) (c := c)
     <;> assumption_mod_cast

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -36,9 +36,11 @@ variable [IsDomain B]
 -- example : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra A L
 variable [Algebra.IsIntegral A B]
 
--- I can't find in mathlib the assertion that B is a finite A-moduie.
--- It should follow from L/K finite.
-example : Module.Finite A B := by sorry -- I assume this is correct
+-- I can't find in mathlib the assertion that B is a finite A-module.
+-- But it is!
+example : Module.Finite A B := by
+  have := IsIntegralClosure.isNoetherian A K L B
+  exact Module.IsNoetherian.finite A B
 
 /-
 In this generality there's a natural isomorphism `L ⊗[K] 𝔸_K^∞ → 𝔸_L^∞` .
@@ -61,12 +63,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.

FLT/ForMathlib/MiscLemmas.lean

@@ -2,8 +2,6 @@ import Mathlib.Algebra.Module.Projective
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.RingTheory.OreLocalization.Ring
 import Mathlib
-
-
 section elsewhere
 
 variable {A : Type*} [AddCommGroup A]
@@ -54,9 +52,7 @@ theorem coinduced_prod_eq_prod_coinduced {X Y S T : Type*} [AddCommGroup X] [Add
   · intro h x y hxy
     rw [Set.mem_preimage, Prod.map_apply] at hxy
     obtain ⟨U1, U2, hU1, hU2, hx1, hy2, h12⟩ := h (f x) (g y) hxy
-    use f ⁻¹' U1, g ⁻¹' U2, hU1, hU2, hx1, hy2
-    intro ⟨x', y'⟩ ⟨hx', hy'⟩
-    exact h12 ⟨hx', hy'⟩
+    exact ⟨f ⁻¹' U1, g ⁻¹' U2, hU1, hU2, hx1, hy2, fun ⟨x', y'⟩ ⟨hx', hy'⟩ ↦ h12 ⟨hx', hy'⟩⟩
 
 end elsewhere
 
@@ -103,7 +99,7 @@ theorem finsum_option {ι : Type*} {B : Type*} [Finite ι]
   rw [← finsum_mem_univ]
   convert finsum_mem_insert φ (show none ∉ Set.range Option.some by aesop)
     (Set.finite_range some)
-  · aesop
+  · exact (Set.insert_none_range_some ι).symm
   · rw [finsum_mem_range]
     exact Option.some_injective ι
 
@@ -126,8 +122,8 @@ def LinearEquiv.sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
     [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)] :
     (∀ (st : S ⊕ T), A st) ≃ₗ[R] (∀ (s : S), A (.inl s)) × (∀ (t : T), A (.inr t)) where
       toFun f := (fun s ↦ f (.inl s), fun t ↦ f (.inr t))
-      map_add' f g := by aesop
-      map_smul' := by aesop
+      map_add' f g := rfl
+      map_smul' _ _ := rfl
       invFun fg st := Sum.rec (fun s => fg.1 s) (fun t => fg.2 t) st
       left_inv := by intro x; aesop
       right_inv := by intro x; aesop
@@ -152,8 +148,8 @@ def Homeomorph.sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
 def Homeomorph.pUnitPiEquiv (f : PUnit → Type*) [∀ x, TopologicalSpace (f x)]: ((t : PUnit) → (f t)) ≃ₜ f () where
   toFun a := a ()
   invFun a _t := a
-  left_inv x := by aesop
-  right_inv x := by aesop
+  left_inv x := rfl
+  right_inv x := rfl
   continuous_toFun := by simp; fun_prop
   continuous_invFun := by simp; fun_prop
 
@@ -163,10 +159,10 @@ def LinearEquiv.pUnitPiEquiv (f : PUnit → Type*) [∀ x, AddCommMonoid (f x)]
     ((t : PUnit) → (f t)) ≃ₗ[R] f () where
   toFun a := a ()
   invFun a _t := a
-  left_inv x := by aesop
-  right_inv x := by aesop
-  map_add' f g := rfl
-  map_smul' r f := rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 -- elsewhere
 theorem finsum_apply {α ι N : Type*} [AddCommMonoid N] [Finite ι]

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -129,10 +129,10 @@ theorem diamond_fix :
   conv_lhs => rw [← @bracketBilin_apply_apply R _ _ _ _]
   rw [← @bracketBilin_apply_apply R _ _ _ (_) (.ofAssociativeAlgebra) _ _ (_) (_) x y]
   rotate_left
-  exact @lieAlgebraSelfModule _ _ _ (_) (_)
+  exact @lieAlgebraSelfModule ..
   refine LinearMap.congr_fun₂ ?_ x y
   ext xa xb ya yb
-  change @Bracket.bracket _ _ (_) (xa ⊗ₜ[R] xb) (ya ⊗ₜ[R] yb) = _
+  change @Bracket.bracket _ _ _ (xa ⊗ₜ[R] xb) (ya ⊗ₜ[R] yb) = _
   dsimp [Ring.lie_def]
   rw [TensorProduct.tmul_sub, mul_comm]
 
@@ -168,9 +168,9 @@ variable (G : Type) [TopologicalSpace G] [Group G]
 def action :
     LeftInvariantDerivation 𝓘(ℝ, E) G →ₗ⁅ℝ⁆ (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; ℝ⟯) where
   toFun l := Derivation.toLinearMap l
-  map_add' := by simp
-  map_smul' := by simp
-  map_lie' {x y} := rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  map_lie' {_ _} := rfl
 
 open scoped TensorProduct
 
@@ -284,8 +284,8 @@ noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
   ρ := {
     toFun := fun A ↦ {
       toFun := fun x ↦ (w.rho A).1 *ᵥ x
-      map_add' := fun _ _ ↦ Matrix.mulVec_add _ _ _
-      map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul _ _ _ }
+      map_add' := fun _ _ ↦ Matrix.mulVec_add ..
+      map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul .. }
     map_one' := by aesop
     map_mul' := fun _ _ ↦ by
       simp only [obj_carrier, MonCat.mul_of, _root_.map_mul, Units.val_mul, ← Matrix.mulVec_mulVec]

FLT/HIMExperiments/flatness.lean

@@ -92,8 +92,7 @@ noncomputable def _root_.Ideal.isoBaseOfIsPrincipal {I : Ideal R} [IsDomain R]
     rw [LinearMap.mem_ker] at h
     apply (AddSubmonoid.mk_eq_zero _).mp at h
     rw [Ideal.mem_bot]
-    refine eq_zero_of_ne_zero_of_mul_right_eq_zero ?_ h
-    refine mt (fun h3 ↦ ?_) hI
+    refine eq_zero_of_ne_zero_of_mul_right_eq_zero (mt (fun h3 ↦ ?_) hI) h
     rwa [Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero I])
   (by
     rintro ⟨i, hi⟩

FLT/MathlibExperiments/IsFrobenius.lean

@@ -110,12 +110,8 @@ lemma IsMaximal_not_eq_bot [NumberField K] (Q : Ideal (𝓞 K)) [Ideal.IsMaximal
   Ring.ne_bot_of_isMaximal_of_not_isField inferInstance (RingOfIntegers.not_isField K)
 
 lemma NumberField_Ideal_IsPrime_iff_IsMaximal  [NumberField K]
-    (Q : Ideal (𝓞 K)) (h1: Q ≠ ⊥) : Ideal.IsPrime Q ↔ Ideal.IsMaximal Q := by
-  constructor
-  · intro h
-    exact Ideal.IsPrime.isMaximal h h1
-  · intro h
-    exact Ideal.IsMaximal.isPrime h
+    (Q : Ideal (𝓞 K)) (h1: Q ≠ ⊥) : Ideal.IsPrime Q ↔ Ideal.IsMaximal Q :=
+  ⟨fun h => Ideal.IsPrime.isMaximal h h1, fun h => Ideal.IsMaximal.isPrime h⟩
 
 instance Fintype_Quot_of_IsMaximal [NumberField K] (P : Ideal (𝓞 K)) [Ideal.IsMaximal P] : Fintype ((𝓞 K) ⧸ P) := by
   sorry

blueprint/src/chapter/AdeleMiniproject.tex

@@ -132,7 +132,8 @@ \section{Results about finite adeles which we can work on now}
   \lean{IsDedekindDomain.HeightOneSpectrum.valuation_comap}
 \end{lemma}
 \begin{proof}
-   Standard.
+  \leanok
+  Standard.
 \end{proof}
 
 \begin{definition}