From cce118255c5e743609bb9060708679be0f0c5838 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 8 Dec 2024 09:18:54 +0000 Subject: [PATCH] Bump mathlib --- .../FiniteAdeleRing/BaseChange.lean | 15 +++++++++------ FLT/FLT_files.lean | 9 +++++---- FLT/GlobalLanglandsConjectures/GLnDefs.lean | 2 +- .../NumberTheory/NumberField/Completion.lean | 8 ++++++++ FLT/MathlibExperiments/FrobeniusRiou.lean | 16 +++------------- FLT/NumberField/AdeleRing.lean | 7 ------- lake-manifest.json | 14 +++++++------- 7 files changed, 33 insertions(+), 38 deletions(-) create mode 100644 FLT/Mathlib/NumberTheory/NumberField/Completion.lean diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index 4ebba11d..7288388b 100644 --- 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 index ee8017b8..3baff8d0 100644 --- 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 index d57b2193..38918d70 100644 --- 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 new file mode 100644 index 00000000..c96d512c --- /dev/null +++ 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 index a26924a8..d3c1e87a 100644 --- 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 index 94f4f3f5..92993466 100644 --- 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 index 56490466..7208ae67 100644 --- 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",