Bump mathlib (#248)

ImperialCollegeLondon · Nov 30, 2024 · d6c13d0 · d6c13d0
1 parent 0e154d2
commit d6c13d0
Show file tree

Hide file tree

Showing 5 changed files with 120 additions and 111 deletions.
diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean
@@ -205,23 +205,30 @@ upon a Frey package guarantee that the running hypotheses in
 Section 4.1 of [Serre] all hold. We put the curve into the form where the
 equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
 The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. -/
-def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := {
-    a₁ := 1
-    -- a₂ is (or should be) an integer because of the congruences assumed e.g. P.ha4
-    a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4
-    a₃ := 0
-    a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 16 -- this should also be an integer
-    a₆ := 0
-    Δ' := Units.mk0 ((P.a ^ P.p) ^ 2 * (P.b ^ P.p) ^ 2 * (P.c ^ P.p) ^ 2 / 2 ^ 8) <| by
-      field_simp
-      norm_cast
-      simp_rw [← mul_pow]
-      refine pow_ne_zero 2 <| pow_ne_zero P.p <| (mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0)
-    coe_Δ' := by
-      simp only [Units.val_mk0, ← Int.cast_pow P.c, ← P.hFLT]
-      field_simp [EllipticCurve.Δ', WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄,
-        WeierstrassCurve.b₆, WeierstrassCurve.b₈]
-      ring }
+def FreyCurve (P : FreyPackage) : WeierstrassCurve ℚ where
+  a₁ := 1
+  -- a₂ is (or should be) an integer because of the congruences assumed e.g. P.ha4
+  a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4
+  a₃ := 0
+  a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 16 -- this should also be an integer
+  a₆ := 0
+
+lemma FreyCurve.Δ (P : FreyPackage) : P.FreyCurve.Δ = (P.a*P.b*P.c)^(2*P.p) / 2 ^ 8 := by
+  trans (P.a ^ P.p) ^ 2 * (P.b ^ P.p) ^ 2 * (P.c ^ P.p) ^ 2 / 2 ^ 8
+  · field_simp
+    norm_cast
+    simp [← P.hFLT, WeierstrassCurve.Δ, FreyCurve, WeierstrassCurve.b₂, WeierstrassCurve.b₄,
+      WeierstrassCurve.b₆, WeierstrassCurve.b₈]
+    ring
+  · simp [← mul_pow, ← pow_mul, mul_comm 2]
+
+instance (P : FreyPackage) : WeierstrassCurve.IsElliptic (FreyCurve P) where
+  isUnit := by
+    rw [FreyCurve.Δ, isUnit_iff_ne_zero]
+    apply div_ne_zero
+    · norm_cast
+      exact pow_ne_zero _ <| mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0
+    · norm_num
 
 lemma FreyCurve.b₂ (P : FreyPackage) :
     P.FreyCurve.b₂ = P.b ^ P.p - P.a ^ P.p := by
@@ -246,12 +253,11 @@ lemma FreyCurve.c₄' (P : FreyPackage) :
 
 lemma FreyCurve.Δ'inv (P : FreyPackage) :
     (↑(P.FreyCurve.Δ'⁻¹) : ℚ) = 2 ^ 8 / (P.a*P.b*P.c)^(2*P.p) := by
-  simp [FreyCurve]
-  ring
+  simp [FreyCurve.Δ]
 
 lemma FreyCurve.j (P : FreyPackage) :
     P.FreyCurve.j = 2^8*(P.c^(2*P.p)-(P.a*P.b)^P.p) ^ 3 /(P.a*P.b*P.c)^(2*P.p) := by
-  rw [mul_div_right_comm, EllipticCurve.j, FreyCurve.Δ'inv, FreyCurve.c₄']
+  rw [mul_div_right_comm, WeierstrassCurve.j, FreyCurve.Δ'inv, FreyCurve.c₄']
 
 private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b := by
   rify

diff --git a/FLT/EllipticCurve/Torsion.lean b/FLT/EllipticCurve/Torsion.lean
@@ -20,11 +20,11 @@ could talk to David first. Note that he has already made substantial progress.
 
 universe u
 
-variable {k : Type u} [Field k] (E : EllipticCurve k)
+variable {k : Type u} [Field k] (E : WeierstrassCurve k) [E.IsElliptic]
 
 open WeierstrassCurve WeierstrassCurve.Affine
 
-abbrev EllipticCurve.n_torsion (n : ℕ) : Type u := Submodule.torsionBy ℤ (E.toWeierstrassCurve ⟮k⟯) n
+abbrev WeierstrassCurve.n_torsion (n : ℕ) : Type u := Submodule.torsionBy ℤ (E ⟮k⟯) n
 
 --variable (n : ℕ) in
 --#synth AddCommGroup (E.n_torsion n)
@@ -38,11 +38,11 @@ instance (n : ℕ) : Module (ZMod n) (E.n_torsion n) := sorry -- shouldn't be to
 
 -- This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata.
 -- Please do not work on it without talking to KB and David first.
-theorem EllipticCurve.n_torsion_finite {n : ℕ} (hn : 0 < n) : Finite (E.n_torsion n) := sorry
+theorem WeierstrassCurve.n_torsion_finite {n : ℕ} (hn : 0 < n) : Finite (E.n_torsion n) := sorry
 
 -- This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata.
 -- Please do not work on it without talking to KB and David first.
-theorem EllipticCurve.n_torsion_card [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
+theorem WeierstrassCurve.n_torsion_card [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
     Nat.card (E.n_torsion n) = n^2 := sorry
 
 set_option autoImplicit true in -- TODO: fix statement
@@ -53,27 +53,27 @@ theorem group_theory_lemma {A : Type*} [AddCommGroup A] {n : ℕ} (hn : 0 < n) (
 -- I only need this if n is prime but there's no harm thinking about it in general I guess.
 -- It follows from the previous theorem using pure group theory (possibly including the
 -- structure theorem for finite abelian groups)
-theorem EllipticCurve.n_torsion_dimension [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
+theorem WeierstrassCurve.n_torsion_dimension [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
     ∃ φ : E.n_torsion n ≃+ (ZMod n) × (ZMod n), True := sorry
 
 -- This should be a straightforward but perhaps long unravelling of the definition
 /-- The map on points for an elliptic curve over `k` induced by a morphism of `k`-algebras
 is a group homomorphism. -/
-def EllipticCurve.Points.map {K L : Type u} [Field K] [Field L] [Algebra k K] [Algebra k L]
-    (f : K →ₐ[k] L) : E.toWeierstrassCurve ⟮K⟯ →+ E.toWeierstrassCurve ⟮L⟯ := sorry
+def WeierstrassCurve.Points.map {K L : Type u} [Field K] [Field L] [Algebra k K] [Algebra k L]
+    (f : K →ₐ[k] L) : E ⟮K⟯ →+ E ⟮L⟯ := sorry
 
-lemma EllipticCurve.Points.map_id (K : Type u) [Field K] [Algebra k K] :
-    EllipticCurve.Points.map E (AlgHom.id k K) = AddMonoidHom.id _ := sorry
+lemma WeierstrassCurve.Points.map_id (K : Type u) [Field K] [Algebra k K] :
+    WeierstrassCurve.Points.map E (AlgHom.id k K) = AddMonoidHom.id _ := sorry
 
-lemma EllipticCurve.Points.map_comp (K L M : Type u) [Field K] [Field L] [Field M]
+lemma WeierstrassCurve.Points.map_comp (K L M : Type u) [Field K] [Field L] [Field M]
     [Algebra k K] [Algebra k L] [Algebra k M] (f : K →ₐ[k] L) (g : L →ₐ[k] M) :
-    (EllipticCurve.Points.map E g).comp (EllipticCurve.Points.map E f) =
-    EllipticCurve.Points.map E (g.comp f) := sorry
+    (WeierstrassCurve.Points.map E g).comp (WeierstrassCurve.Points.map E f) =
+    WeierstrassCurve.Points.map E (g.comp f) := sorry
 
 /-- The Galois action on the points of an elliptic curve. -/
-def EllipticCurve.galoisRepresentation (K : Type u) [Field K] [Algebra k K] :
-    DistribMulAction (K ≃ₐ[k] K) (E.toWeierstrassCurve ⟮K⟯) := sorry
+def WeierstrassCurve.galoisRepresentation (K : Type u) [Field K] [Algebra k K] :
+    DistribMulAction (K ≃ₐ[k] K) (E ⟮K⟯) := sorry
 
 /-- The Galois action on the n-torsion points of an elliptic curve. -/
-def EllipticCurve.torsionGaloisRepresentation (n : ℕ) (K : Type u) [Field K] [Algebra k K] :
+def WeierstrassCurve.torsionGaloisRepresentation (n : ℕ) (K : Type u) [Field K] [Algebra k K] :
     Representation (ZMod n) (K ≃ₐ[k] K) (E.n_torsion n) := sorry
diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
@@ -30,6 +30,9 @@ of the `GL_n` functor. There's notation `GL (Fin n)` for this.
 -/
 
 open scoped Manifold
+/- Next line is necessary while the manifold smoothness class is not extended to `ω`.
+Later, replace with `open scoped ContDiff`. -/
+local notation "∞" => (⊤ : ℕ∞)
 
 namespace DedekindDomain
 
@@ -256,7 +259,7 @@ structure IsSmooth (f : GL (Fin n) (FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ
   loc_cst (y : GL (Fin n) ℝ) :
     IsLocallyConstant (fun x ↦ f (x, y))
   smooth (x : GL (Fin n) (FiniteAdeleRing ℤ ℚ)) :
-    Smooth 𝓘(ℝ, Matrix (Fin n) (Fin n) ℝ) 𝓘(ℝ, ℂ) (fun y ↦ f (x, y))
+    ContMDiff 𝓘(ℝ, Matrix (Fin n) (Fin n) ℝ) 𝓘(ℝ, ℂ) ∞ (fun y ↦ f (x, y))
 
 open Matrix
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,62 +1,82 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276",
-   "name": "batteries",
+   "scope": "",
+   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
+   "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
-   "name": "Qq",
+   "scope": "",
+   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
+   "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
+   "inputRev": null,
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
-   "name": "aesop",
+   "scope": "",
+   "rev": "cee87aa25cfbd8e4c3cd89bc26cce86e927e36dc",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
-   "name": "proofwidgets",
+   "scope": "",
+   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
+   "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/dupuisf/BibtexQuery",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
-   "name": "Cli",
+   "scope": "",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
-   "name": "importGraph",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -71,75 +91,55 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/plausible",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
-   "name": "plausible",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "f28fa7213f2fe9065a3a12f88d256ea7dd006d7e",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/PatrickMassot/checkdecls.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
-   "name": "checkdecls",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
-   "name": "MD4Lean",
+   "scope": "leanprover-community",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
-   "name": "UnicodeBasic",
+   "scope": "leanprover-community",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
-   "name": "BibtexQuery",
+   "scope": "leanprover-community",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
-   "name": "«doc-gen4»",
+   "scope": "leanprover-community",
+   "rev": "f46c0445cc86ad2bc973edf8c5b2bd88bd91913b",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "FLT",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.14.0-rc3
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0-rc2
		leanprover/lean4:v4.14.0-rc3