Bump mathlib

ImperialCollegeLondon · Dec 10, 2024 · cce1182 · cce1182
1 parent f7c20d3
commit cce1182
Show file tree

Hide file tree

Showing 7 changed files with 33 additions and 38 deletions.
diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/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
 
 /-!
 
@@ -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) :

diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -12,15 +12,19 @@ import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.flatness
 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.Mathlib.NumberTheory.NumberField.Completion
+import FLT.Mathlib.RingTheory.Norm.Defs
+import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
+import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct
@@ -30,9 +34,6 @@ import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
-import FLT.Mathlib.RingTheory.Norm.Defs
-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/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
@@ -285,7 +285,7 @@ noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
     FDRep ℂ (orthogonalGroup (Fin n) ℝ) where
   V := FGModuleCat.of ℂ (Fin w.d → ℂ)
   ρ := {
-    toFun := fun A ↦ {
+    toFun := fun A ↦ ModuleCat.ofHom {
       toFun := fun x ↦ (w.rho A).1 *ᵥ x
       map_add' := fun _ _ ↦ Matrix.mulVec_add ..
       map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul .. }

diff --git a/FLT/Mathlib/NumberTheory/NumberField/Completion.lean b/FLT/Mathlib/NumberTheory/NumberField/Completion.lean
@@ -0,0 +1,8 @@
+import Mathlib.NumberTheory.NumberField.Completion
+
+/-!
+# TODO
+
+Rename `InfinitePlace.Completion.Rat.norm_infinitePlace_completion` to
+`Rat.norm_infinitePlace_completion`
+-/
diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -3,15 +3,8 @@ Copyright (c) 2024 Jou Glasheen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard
 -/
-import Mathlib.FieldTheory.Cardinality
-import Mathlib.RingTheory.DedekindDomain.Ideal
-import Mathlib.RingTheory.Ideal.Pointwise
-import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
-import Mathlib.RingTheory.Ideal.Pointwise
-import Mathlib.RingTheory.Ideal.Over
-import Mathlib.FieldTheory.Normal
 import Mathlib.FieldTheory.SeparableClosure
-import Mathlib.RingTheory.OreLocalization.Ring
+import Mathlib.RingTheory.Ideal.Over
 
 /-!
 
@@ -21,7 +14,7 @@ This file proves a general result in commutative algebra which can be used to de
 elements of Galois groups of local or fields (for example number fields).
 
 KB was alerted to this very general result (which needs no Noetherian or finiteness assumptions
-on the rings, just on the Galois group) by Joel Riou
+on the rings, just on the Galois group) by Joël Riou
 here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Uses.20of.20Frobenius.20elements.20in.20mathematics/near/448934112
 
 ## Mathematical details
@@ -696,9 +689,6 @@ open scoped algebraMap
 noncomputable local instance : Algebra A[X] B[X] :=
   RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom))
 
-theorem IsAlgebraic.mul {R K : Type*} [CommRing R] [CommRing K] [Algebra R K] {x y : K}
-  (hx : IsAlgebraic R x) (hy : IsAlgebraic R y) : IsAlgebraic R (x * y) := sorry
-
 theorem IsAlgebraic.invLoc {R S K : Type*} [CommRing R] {M : Submonoid R} [CommRing S] [Algebra R S]
     [IsLocalization M S] {x : M} [CommRing K] [Algebra K S] (h : IsAlgebraic K ((x : R) : S)):
     IsAlgebraic K (IsLocalization.mk' S 1 x) := by
@@ -734,7 +724,7 @@ theorem algebraMap_algebraMap {R S T : Type*} [CommRing R] [CommRing S] [CommRin
   exact Eq.symm (IsScalarTower.algebraMap_apply R S T r)
 
 theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R] [CommRing k]
-    [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K]
+    [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K] [NoZeroDivisors k]
     (h : ∀ x : R, IsAlgebraic k (x : K)) : Algebra.IsAlgebraic k K := by
   rw [Algebra.isAlgebraic_def]
   let M := nonZeroDivisors R

diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
@@ -22,13 +22,6 @@ section Discrete
 
 open NumberField DedekindDomain
 
--- mathlib PR #19644
-lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
-    ‖(x : v.completion)‖ = |x| := sorry -- this will be done when the mathlib PR is merged
-
--- mathlib PR #19644
-noncomputable def Rat.infinitePlace : InfinitePlace ℚ := .mk (Rat.castHom _)
-
 theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
     IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {0} := by
   use {f | ∀ v, f v ∈ (Metric.ball 0 1)} ×ˢ

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "099b90e374ba73983c3fda87595be625f1931669",
+   "rev": "82c0223cfb0ba31bcf8bef02519adb92fecf4421",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8e459c606cbf19248c6a59956570f051f05e6067",
+   "rev": "7edf946a4217aa3aa911290811204096e8464ada",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "41ff1f7899c971f91362710d4444e338b8acd644",
+   "rev": "965bd1ea790c952273326d1c99f55f88114de87b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -115,10 +115,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e",
+   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -135,10 +135,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83",
+   "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",