Merge branch 'main' of https://github.com/smmercuri/FLT

.github/dependabot.yml

@@ -0,0 +1,9 @@
+version: 2  # Specifies the version of the Dependabot configuration file format
+
+updates:
+  # Configuration for dependency updates
+  - package-ecosystem: "github-actions"  # Specifies the ecosystem to check for updates
+    directory: "/"  # Specifies the directory to check for dependencies; "/" means the root directory
+    schedule:
+      # Check for updates to GitHub Actions every month
+      interval: "monthly"

.github/workflows/01-claim-issue.yml

@@ -6,7 +6,7 @@ on:
 
 jobs:
   claim_issue:
-    if: github.event.issue.pull_request == null && contains(github.event.comment.body, 'claim')
+    if: github.event.issue.pull_request == null && contains(github.event.comment.body, 'claim') && !contains(github.event.comment.body, 'disclaim')
     runs-on: ubuntu-latest
 
     steps:

.github/workflows/blueprint.yml

@@ -75,13 +75,7 @@ jobs:
         uses: actions/cache@v4
         with:
           path: |
-            .lake/build/doc/Init
-            .lake/build/doc/Lake
-            .lake/build/doc/Lean
-            .lake/build/doc/Std
-            .lake/build/doc/Mathlib
-            .lake/build/doc/declarations
-            !.lake/build/doc/declarations/declaration-data-FLT*
+            .lake/build/doc
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             MathlibDoc-

.github/workflows/update-dependencies.yml

@@ -2,7 +2,7 @@ name: Update Dependencies
 
 on:
   schedule:             # Sets a schedule to trigger the workflow
-  - cron: "0 8 */3 * *" # Every 3 days at 08:00 AM UTC (for more info on the cron syntax see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule)
+  - cron: "0 8 */7 * *" # Every 7 days at 08:00 AM UTC (for more info on the cron syntax see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule)
   workflow_dispatch:    # Allows the workflow to be triggered manually via the GitHub interface
 
 jobs:

FLT/Basic/Reductions.lean

@@ -1,8 +1,8 @@
 import Mathlib.Data.PNat.Basic
 import Mathlib.NumberTheory.FLT.Four
 import Mathlib.NumberTheory.FLT.Three
-import Mathlib.Tactic
 import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
+import Mathlib.Tactic.ModCases
 import Mathlib.RepresentationTheory.Basic
 import Mathlib.RingTheory.SimpleModule
 import FLT.EllipticCurve.Torsion

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -1,10 +1,11 @@
-import Mathlib -- **TODO** fix when finished or if `exact?` is too slow
---import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
---import Mathlib.NumberTheory.NumberField.Basic
---import Mathlib.NumberTheory.RamificationInertia
-import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
-import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import Mathlib.FieldTheory.Separable
+import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
+import Mathlib.RingTheory.DedekindDomain.IntegralClosure
+import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import FLT.Mathlib.Algebra.Order.Hom.Monoid
 
 /-!
 
@@ -17,6 +18,10 @@ are defined. In this file we define the natural `K`-algebra map `𝔸_K^∞ →
 the natural `L`-algebra map `𝔸_K^∞ ⊗[K] L → 𝔸_L^∞`, and show that the latter map
 is an isomorphism.
 
+## Main definition
+
+* `FiniteAdeleRing.baseChangeEquiv : L ⊗[K] FiniteAdeleRing A K ≃ₐ[L] FiniteAdeleRing B L`
+
 -/
 
 open scoped Multiplicative
@@ -48,10 +53,6 @@ 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^∞` .
--/
-
 -- We start by filling in some holes in the API for finite extensions of Dedekind domains.
 namespace IsDedekindDomain
 
@@ -275,6 +276,7 @@ noncomputable def adicCompletionTensorComapAlgHom (v : HeightOneSpectrum A) :
       Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 :=
   Algebra.TensorProduct.lift (Algebra.ofId _ _) (adicCompletionComapAlgHom' A K L B v) fun _ _ ↦ .all _ _
 
+omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] in
 lemma adicCompletionComapAlgIso_tmul_apply (v : HeightOneSpectrum A) (x y i) :
   adicCompletionTensorComapAlgHom A K L B v (x ⊗ₜ y) i =
     x • adicCompletionComapAlgHom A K L B v i.1 i.2 y := by
@@ -302,6 +304,7 @@ noncomputable def tensorAdicCompletionIntegersTo (v : HeightOneSpectrum A) :
     ((Algebra.TensorProduct.includeRight.restrictScalars A).comp (IsScalarTower.toAlgHom _ _ _))
     (fun _ _ ↦ .all _ _)
 
+omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] in
 set_option linter.deprecated false in -- `map_zero` and `map_add` time-outs
 theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
     (v : HeightOneSpectrum A) :
@@ -390,11 +393,26 @@ variable [Algebra K (ProdAdicCompletions B L)]
 noncomputable def ProdAdicCompletions.baseChange :
     ProdAdicCompletions A K →ₐ[K] ProdAdicCompletions B L where
   toFun kv w := (adicCompletionComapAlgHom A K L B _ w rfl (kv (comap A w)))
-  map_one' := sorry -- #232 is this and the next few sorries. There is probably a cleverer way to do this.
-  map_mul' := sorry
-  map_zero' := sorry
-  map_add' := sorry
-  commutes' := sorry
+  map_one' := by
+    dsimp only
+    exact funext fun w => by rw [Pi.one_apply, Pi.one_apply, map_one]
+  map_mul' x y := by
+    dsimp only
+    exact funext fun w => by rw [Pi.mul_apply, Pi.mul_apply, map_mul]
+  map_zero' := by
+    dsimp only
+    exact funext fun w => by rw [Pi.zero_apply, Pi.zero_apply, map_zero]
+  map_add' x y := by
+    dsimp only
+    funext w
+    letI : Module K (adicCompletion L w) := Algebra.toModule
+    rw [Pi.add_apply, Pi.add_apply, map_add]
+  commutes' r := by
+    funext w
+    rw [IsScalarTower.algebraMap_apply K L (ProdAdicCompletions B L)]
+    dsimp only [algebraMap_apply']
+    exact adicCompletionComapAlgHom_coe A K L B _ w _ r
+
 
 -- Note that this is only true because L/K is finite; in general tensor product doesn't
 -- commute with infinite products, but it does here.
@@ -421,12 +439,17 @@ theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff
     ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChangeEquiv A K L B (1 ⊗ₜ x)) :=
   sorry -- #240
 
--- Easy consequence of the previous result
-theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff'
-    (x : ProdAdicCompletions A K) :
-    ProdAdicCompletions.IsFiniteAdele x ↔
-    ∀ (l : L), ProdAdicCompletions.IsFiniteAdele
-      (ProdAdicCompletions.baseChangeEquiv A K L B (l ⊗ₜ x)) := sorry -- #241
+theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff' (x : ProdAdicCompletions A K) :
+    ProdAdicCompletions.IsFiniteAdele x ↔ ∀ (l : L), ProdAdicCompletions.IsFiniteAdele
+    (ProdAdicCompletions.baseChangeEquiv A K L B (l ⊗ₜ x)) := by
+  constructor
+  · simp_rw [ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff A K L B, baseChangeEquiv,
+      AlgEquiv.coe_ofBijective, Algebra.TensorProduct.lift_tmul, map_one, one_mul]
+    intro h l
+    exact ProdAdicCompletions.IsFiniteAdele.mul (ProdAdicCompletions.IsFiniteAdele.algebraMap' l) h
+  · intro h
+    rw [ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff A K L B]
+    exact h 1
 
 -- Make ∏_w L_w into a K-algebra in a way compatible with the L-algebra structure
 variable [Algebra K (FiniteAdeleRing B L)]
@@ -436,11 +459,37 @@ variable [Algebra K (FiniteAdeleRing B L)]
 noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] FiniteAdeleRing B L where
   toFun ak := ⟨ProdAdicCompletions.baseChange A K L B ak.1,
     (ProdAdicCompletions.baseChange_isFiniteAdele_iff A K L B ak).1 ak.2⟩
-  map_one' := sorry
-  map_mul' := sorry
-  map_zero' := sorry
-  map_add' := sorry
-  commutes' := sorry
+  map_one' := by
+    ext
+    have h : (1 : FiniteAdeleRing A K) = (1 : ProdAdicCompletions A K) := rfl
+    have t : (1 : FiniteAdeleRing B L) = (1 : ProdAdicCompletions B L) := rfl
+    simp_rw [h, t, map_one]
+  map_mul' x y := by
+    have h : (x * y : FiniteAdeleRing A K) =
+      (x : ProdAdicCompletions A K) * (y : ProdAdicCompletions A K) := rfl
+    simp_rw [h, map_mul]
+    rfl
+  map_zero' := by
+    ext
+    have h : (0 : FiniteAdeleRing A K) = (0 : ProdAdicCompletions A K) := rfl
+    have t : (0 : FiniteAdeleRing B L) = (0 : ProdAdicCompletions B L) := rfl
+    simp_rw [h, t, map_zero]
+  map_add' x y:= by
+    have h : (x + y : FiniteAdeleRing A K) =
+      (x : ProdAdicCompletions A K) + (y : ProdAdicCompletions A K) := rfl
+    simp_rw [h, map_add]
+    rfl
+  commutes' r := by
+    ext
+    have h : (((algebraMap K (FiniteAdeleRing A K)) r) : ProdAdicCompletions A K) =
+      (algebraMap K (ProdAdicCompletions A K)) r := rfl
+    have i : algebraMap K (FiniteAdeleRing B L) r =
+      algebraMap L (FiniteAdeleRing B L) (algebraMap K L r) :=
+      IsScalarTower.algebraMap_apply K L (FiniteAdeleRing B L) r
+    have j (p : L) : (((algebraMap L (FiniteAdeleRing B L)) p) : ProdAdicCompletions B L) =
+      (algebraMap L (ProdAdicCompletions B L)) p := rfl
+    simp_rw [h, AlgHom.commutes, i, j]
+    exact IsScalarTower.algebraMap_apply K L (ProdAdicCompletions B L) r
 
 -- Presumably we have this?
 noncomputable def bar {K L AK AL : Type*} [CommRing K] [CommRing L]

FLT/Deformations/RepresentationTheory/Irreducible.lean

@@ -0,0 +1,30 @@
+import FLT.Deformations.RepresentationTheory.Subrepresentation
+import FLT.Mathlib.RepresentationTheory.Basic
+
+namespace Representation
+
+variable {G : Type*} [Group G]
+
+variable {k : Type*} [Field k]
+
+variable {W : Type*} [AddCommMonoid W] [Module k W]
+
+/-!
+  `IsIrreducible ρ` is the statement that a given Representation ρ is irreducible (also known as simple),
+  meaning that any subrepresentation must be either the full one (⊤) or zero (⊥)
+
+  This notion is only well behaved when the representation is over a field k. If it were defined over
+  a ring A with a nontrivial ideal J, the subrepresentation JW would often be a non trivial subrepresentation,
+  so ρ would rarely be irreducible.
+-/
+class IsIrreducible (ρ : Representation k G W) : Prop where
+  irreducible : IsSimpleOrder (Subrepresentation ρ)
+
+/-!
+  `IsAbsolutelyIrreducible ρ` states that a given Representation ρ over a field k
+  is absolutely irreducible, meaning that all the possible base change extensions are irreducible.
+-/
+class IsAbsolutelyIrreducible (ρ : Representation k G W) : Prop where
+  absolutelyIrreducible : ∀ k', ∀ _ : Field k', ∀ _ : Algebra k k', IsIrreducible (k' ⊗ᵣ' ρ)
+
+end Representation

FLT/Deformations/RepresentationTheory/Subrepresentation.lean

@@ -0,0 +1,74 @@
+import Mathlib.RepresentationTheory.Basic
+import FLT.Mathlib.LinearAlgebra.Span.Defs
+
+open Pointwise
+
+universe u
+
+variable {A : Type*} [CommRing A]
+
+variable {G : Type*} [Group G]
+
+variable {W : Type*} [AddCommMonoid W] [Module A W]
+
+variable {ρ : Representation A G W}
+
+variable (ρ) in
+structure Subrepresentation where
+  toSubmodule : Submodule A W
+  apply_mem_toSubmodule (g : G) ⦃v : W⦄ : v ∈ toSubmodule → ρ g v ∈ toSubmodule
+
+namespace Subrepresentation
+
+lemma toSubmodule_injective : Function.Injective (toSubmodule : Subrepresentation ρ → Submodule A W) := by
+  rintro ⟨_,_⟩
+  congr!
+
+instance : SetLike (Subrepresentation ρ) W where
+  coe ρ' := ρ'.toSubmodule
+  coe_injective' := SetLike.coe_injective.comp toSubmodule_injective
+
+def toRepresentation (ρ' : Subrepresentation ρ): Representation A G ρ'.toSubmodule where
+  toFun g := (ρ g).restrict (ρ'.apply_mem_toSubmodule g)
+  map_one' := by ext; simp
+  map_mul' x y := by ext; simp
+
+instance : Max (Subrepresentation ρ) where
+  max ρ₁ ρ₂ := .mk (ρ₁.toSubmodule ⊔ ρ₂.toSubmodule) <| by
+      simp only [Submodule.forall_mem_sup, map_add]
+      intro g x₁ hx₁ x₂ hx₂
+      exact Submodule.mem_sup.mpr
+        ⟨ρ g x₁, ρ₁.apply_mem_toSubmodule g hx₁, ρ g x₂, ρ₂.apply_mem_toSubmodule g hx₂, rfl⟩
+
+instance : Min (Subrepresentation ρ) where
+  min ρ₁ ρ₂ := .mk (ρ₁.toSubmodule ⊓ ρ₂.toSubmodule) <| by
+      simp only [Submodule.mem_inf, and_imp]
+      rintro g x hx₁ hx₂
+      exact ⟨ρ₁.apply_mem_toSubmodule g hx₁, ρ₂.apply_mem_toSubmodule g hx₂⟩
+
+
+@[simp, norm_cast]
+lemma coe_sup (ρ₁ ρ₂ : Subrepresentation ρ) : ↑(ρ₁ ⊔ ρ₂) = (ρ₁ : Set W) + (ρ₂ : Set W) :=
+  Submodule.coe_sup ρ₁.toSubmodule ρ₂.toSubmodule
+
+@[simp, norm_cast]
+lemma coe_inf (ρ₁ ρ₂ : Subrepresentation ρ) : ↑(ρ₁ ⊓ ρ₂) = (ρ₁ ∩ ρ₂ : Set W) := rfl
+
+@[simp]
+lemma toSubmodule_sup (ρ₁ ρ₂ : Subrepresentation ρ) :
+  (ρ₁ ⊔ ρ₂).toSubmodule = ρ₁.toSubmodule ⊔ ρ₂.toSubmodule := rfl
+
+@[simp]
+lemma toSubmodule_inf (ρ₁ ρ₂ : Subrepresentation ρ) :
+  (ρ₁ ⊓ ρ₂).toSubmodule = ρ₁.toSubmodule ⊓ ρ₂.toSubmodule := rfl
+
+instance : Lattice (Subrepresentation ρ) :=
+  toSubmodule_injective.lattice _ toSubmodule_sup toSubmodule_inf
+
+instance : BoundedOrder (Subrepresentation ρ) where
+  top := ⟨⊤, by simp⟩
+  le_top _ _ := by simp
+  bot := ⟨⊥, by simp⟩
+  bot_le _ _ := by simp +contextual
+
+end Subrepresentation

FLT/DivisionAlgebra/Finiteness.lean

@@ -8,7 +8,7 @@ import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import FLT.ForMathlib.ActionTopology
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.NumberField.IsTotallyReal
 import FLT.NumberField.AdeleRing
 import Mathlib.GroupTheory.DoubleCoset
@@ -34,14 +34,14 @@ variable (K : Type*) [Field K] [NumberField K]
 variable (D : Type*) [DivisionRing D] [Algebra K D]
 
 local instance : TopologicalSpace (FiniteAdeleRing (𝓞 K) K ⊗[K] D) :=
-  actionTopology (FiniteAdeleRing (𝓞 K) K) _
-local instance : IsActionTopology (FiniteAdeleRing (𝓞 K) K) ((FiniteAdeleRing (𝓞 K) K) ⊗[K] D) :=
+  moduleTopology (FiniteAdeleRing (𝓞 K) K) _
+local instance : IsModuleTopology (FiniteAdeleRing (𝓞 K) K) ((FiniteAdeleRing (𝓞 K) K) ⊗[K] D) :=
   ⟨rfl⟩
 
 variable [FiniteDimensional K D]
 
 instance : TopologicalRing ((FiniteAdeleRing (𝓞 K) K) ⊗[K] D) :=
-  ActionTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _
+  IsModuleTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _
 
 variable [Algebra.IsCentral K D]
 

FLT/EllipticCurve/Torsion.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard
 -/
+import Mathlib.Algebra.Module.Torsion
 import Mathlib.AlgebraicGeometry.EllipticCurve.Group
 import Mathlib.FieldTheory.IsSepClosed
 import Mathlib.RepresentationTheory.Basic
@@ -29,12 +30,9 @@ abbrev WeierstrassCurve.n_torsion (n : ℕ) : Type u := Submodule.torsionBy ℤ
 --variable (n : ℕ) in
 --#synth AddCommGroup (E.n_torsion n)
 
-def ZMod.module (A : Type*) [AddCommGroup A] (n : ℕ) (hn : ∀ a : A, n • a = 0) :
-    Module (ZMod n) A :=
-  sorry
-
 -- not sure if this instance will cause more trouble than it's worth
-instance (n : ℕ) : Module (ZMod n) (E.n_torsion n) := sorry -- shouldn't be too hard
+noncomputable instance (n : ℕ) : Module (ZMod n) (E.n_torsion n) :=
+  AddCommGroup.zmodModule sorry -- shouldn't be too hard
 
 -- 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.