From d6c13d0a0e47969b21d1dca8480e25aedb383907 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 30 Nov 2024 14:53:27 +0100 Subject: [PATCH] Bump mathlib (#248) --- FLT/Basic/Reductions.lean | 46 +++--- FLT/EllipticCurve/Torsion.lean | 30 ++-- FLT/GlobalLanglandsConjectures/GLnDefs.lean | 5 +- lake-manifest.json | 148 ++++++++++---------- lean-toolchain | 2 +- 5 files changed, 120 insertions(+), 111 deletions(-) diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean index c429cef5..a44b68e5 100644 --- 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 index 5769e186..32c5ddf6 100644 --- 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 index 46dda2bb..d51c8134 100644 --- 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 index 157887f8..cc7dc15c 100644 --- 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 index 57a4710c..6d9e70f7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0-rc3