Merge branch 'main' into MC_prod

ImperialCollegeLondon · Dec 8, 2024 · 0f3b24b · 0f3b24b
2 parents 8b49014 + 39b6469
commit 0f3b24b
Show file tree

Hide file tree

Showing 8 changed files with 64 additions and 255 deletions.
diff --git a/.github/workflows/01-claim-issue.yml b/.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:

diff --git a/FLT/DivisionAlgebra/Finiteness.lean b/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]
 

diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -5,11 +5,8 @@ import FLT.Basic.Reductions
 import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
 import FLT.DivisionAlgebra.Finiteness
 import FLT.EllipticCurve.Torsion
-import FLT.ForMathlib.ActionTopology
-import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
 import FLT.ForMathlib.MiscLemmas
-import FLT.FromMathlib.Algebra
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
@@ -18,6 +15,12 @@ import FLT.GroupScheme.FiniteFlat
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Hard.Results
 import FLT.HIMExperiments.flatness
+import FLT.Junk.Algebra
+import FLT.Junk.Algebra2
+import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+import FLT.Mathlib.Data.ENNReal.Inv
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct
@@ -27,6 +30,8 @@ import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal

diff --git a/FLT/ForMathlib/MiscLemmas.lean b/FLT/ForMathlib/MiscLemmas.lean
@@ -27,6 +27,7 @@ theorem isOpenMap_of_coinduced (φ : A →+ B) (hφc : Continuous φ)
     rw [AddMonoidHom.map_add, hk, add_zero]
 
 -- **TODO** ask Yury how to golf
+-- Answer: `IsOpenQuotientMap.prodMap`
 open TopologicalSpace in
 theorem coinduced_prod_eq_prod_coinduced {X Y S T : Type*} [AddCommGroup X] [AddCommGroup Y]
     [AddCommGroup S] [AddCommGroup T] (f : X →+ S) (g : Y →+ T)

diff --git a/FLT/FromMathlib/Algebra.lean → FLT/Junk/Algebra.lean b/FLT/FromMathlib/Algebra.lean → FLT/Junk/Algebra.lean
@@ -1,3 +1,4 @@
+#exit
 /-
 Copyright (c) 2024 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

diff --git a/FLT/ForMathlib/Algebra.lean → FLT/Junk/Algebra2.lean b/FLT/ForMathlib/Algebra.lean → FLT/Junk/Algebra2.lean
@@ -1,5 +1,5 @@
-import Mathlib.RingTheory.OreLocalization.Ring
 #exit
+import Mathlib.RingTheory.OreLocalization.Ring
 
 -- extend localization theory to algebras
 -- I should only be doing this in the commutative case

diff --git a/FLT/ForMathlib/Topology/Algebra/Algebra.lean → .../Topology/Algebra/ContinuousAlgEquiv.lean b/FLT/ForMathlib/Topology/Algebra/Algebra.lean → .../Topology/Algebra/ContinuousAlgEquiv.lean