From 0e154d2d09f21ae50667c5027bd899b8013f930d Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 26 Nov 2024 09:29:45 +0000 Subject: [PATCH] Document a bunch of adele-related issues (#244) * document locations of a ton of new issues in the file * Iso -> Equiv --- .../FiniteAdeleRing/BaseChange.lean | 77 +++++++++++++++---- blueprint/lean_decls | 6 +- blueprint/src/chapter/AdeleMiniproject.tex | 18 ++--- 3 files changed, 72 insertions(+), 29 deletions(-) diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index aa975754..a7ffce65 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -193,6 +193,7 @@ noncomputable def adicCompletionComapRingHom -- So we need to be careful making L_w into a K-algebra -- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/beef.20up.20smul.20on.20completion.20to.20algebra.20instance/near/484166527 +-- Hopefully resolved in https://github.com/leanprover-community/mathlib4/pull/19466 variable (w : HeightOneSpectrum B) in noncomputable instance : Algebra K (adicCompletion L w) where toFun k := algebraMap L (adicCompletion L w) (algebraMap K L k) @@ -211,7 +212,7 @@ instance : IsScalarTower K L (adicCompletion L w) := IsScalarTower.of_algebraMap noncomputable def adicCompletionComapAlgHom (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) : - (HeightOneSpectrum.adicCompletion K v) →ₐ[K] + (HeightOneSpectrum.adicCompletion K v) →A[K] (HeightOneSpectrum.adicCompletion L w) where __ := adicCompletionComapRingHom A K v w hvw commutes' r := by @@ -226,17 +227,26 @@ noncomputable def adicCompletionComapAlgHom rw [show (r : adicCompletion K (comap A w)) = @UniformSpace.Completion.coe' K this r from rfl] apply UniformSpace.Completion.extensionHom_coe rw [this, ← IsScalarTower.algebraMap_apply K L] + cont := sorry -- #235 +-- this name is surely wrong lemma v_adicCompletionComapAlgHom (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) (x) : Valued.v (adicCompletionComapAlgHom A K L B v w hvw x) ^ (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) = Valued.v x := sorry + -- #234 noncomputable def adicCompletionComapAlgHom' (v : HeightOneSpectrum A) : (HeightOneSpectrum.adicCompletion K v) →ₐ[K] (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) := Pi.algHom _ _ fun i ↦ adicCompletionComapAlgHom A K L B v i.1 i.2 +noncomputable def adicCompletionContinuousComapAlgHom (v : HeightOneSpectrum A) : + (HeightOneSpectrum.adicCompletion K v) →A[K] + (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) where + __ := adicCompletionComapAlgHom' A K L B v + cont := sorry -- #236 + open scoped TensorProduct -- ⊗ notation for tensor product noncomputable def adicCompletionTensorComapAlgHom (v : HeightOneSpectrum A) : @@ -244,14 +254,32 @@ 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 _ _ -noncomputable def adicCompletionComapAlgIso (v : HeightOneSpectrum A) : +attribute [local instance] Algebra.TensorProduct.rightAlgebra in +variable (v : HeightOneSpectrum A) in +instance : TopologicalSpace (L ⊗[K] adicCompletion K v) := moduleTopology (adicCompletion K v) _ + +noncomputable def adicCompletionTensorComapContinuousAlgHom (v : HeightOneSpectrum A) : + L ⊗[K] adicCompletion K v →A[L] + Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 where + __ := adicCompletionTensorComapAlgHom A K L B v + cont := sorry -- #237 + +noncomputable def adicCompletionComapAlgEquiv (v : HeightOneSpectrum A) : (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃ₐ[L] (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) := - AlgEquiv.ofBijective (adicCompletionTensorComapAlgHom A K L B v) sorry + AlgEquiv.ofBijective (adicCompletionTensorComapAlgHom A K L B v) sorry --#231 -theorem adicCompletionComapAlgIso_integral : ∃ S : Finset (HeightOneSpectrum A), ∀ v ∉ S, +-- Can't state this properly because ≃[A]L doesn't exist yet -- #238 +noncomputable def adicCompletionComapContinuousAlgEquiv (v : HeightOneSpectrum A) : + sorry +-- (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃A[L] +-- (∀ w : {w : HeightOneSpectrum B // v = comap A w}, HeightOneSpectrum.adicCompletion L w.1) + := sorry + +theorem adicCompletionComapAlgEquiv_integral : ∃ S : Finset (HeightOneSpectrum A), ∀ v ∉ S, -- image of B ⊗[A] (integer ring at v) = (product of integer rings at w's) under above iso - sorry := sorry -- stated properly in #229 + sorry := sorry -- stated properly in #229. Can't make progress + -- until actual statement is merged. end IsDedekindDomain.HeightOneSpectrum @@ -268,37 +296,49 @@ 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 for this and the next few. There is probably a cleverer way to do this. + 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 -noncomputable def ProdAdicCompletions.baseChangeIso : +-- 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. +noncomputable def ProdAdicCompletions.baseChangeEquiv : L ⊗[K] ProdAdicCompletions A K ≃ₐ[L] ProdAdicCompletions B L := AlgEquiv.ofBijective - (Algebra.TensorProduct.lift (Algebra.ofId _ _) (ProdAdicCompletions.baseChange A K L B) sorry) sorry + (Algebra.TensorProduct.lift (Algebra.ofId _ _) + (ProdAdicCompletions.baseChange A K L B) fun _ _ ↦ mul_comm _ _) sorry -- #239 +-- I am unclear about whether these next two sorries are in the right order. +-- One direction of `baseChange_isFiniteAdele_iff` below (->) is easy, but perhaps the other way +-- should be deduced from the result after this one. See #240. +-- (`ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff`). theorem ProdAdicCompletions.baseChange_isFiniteAdele_iff (x : ProdAdicCompletions A K) : - ProdAdicCompletions.IsFiniteAdele x ↔ - ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChange A K L B x) := sorry + ProdAdicCompletions.IsFiniteAdele x ↔ + ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChange A K L B x) := sorry --#240 -theorem ProdAdicCompletions.baseChangeIso_isFiniteAdele_iff +-- This theorem and the one before are probably equivalent, I'm not sure which one to prove first. +-- See #240 +theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff (x : ProdAdicCompletions A K) : - ProdAdicCompletions.IsFiniteAdele x ↔ - ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChangeIso A K L B (1 ⊗ₜ x)) := sorry + ProdAdicCompletions.IsFiniteAdele x ↔ + ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChangeEquiv A K L B (1 ⊗ₜ x)) := + sorry -- #240 -theorem ProdAdicCompletions.baseChangeIso_isFiniteAdele_iff' +-- Easy consequence of the previous result +theorem ProdAdicCompletions.baseChangeEquiv_isFiniteAdele_iff' (x : ProdAdicCompletions A K) : ProdAdicCompletions.IsFiniteAdele x ↔ ∀ (l : L), ProdAdicCompletions.IsFiniteAdele - (ProdAdicCompletions.baseChangeIso A K L B (l ⊗ₜ x)) := sorry + (ProdAdicCompletions.baseChangeEquiv A K L B (l ⊗ₜ x)) := sorry -- #241 -- Make ∏_w L_w into a K-algebra in a way compatible with the L-algebra structure variable [Algebra K (FiniteAdeleRing B L)] [IsScalarTower K L (FiniteAdeleRing B L)] +-- Restriction of an algebra map is an algebra map; these should be easy. #242 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⟩ @@ -308,13 +348,16 @@ noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] Fin map_add' := sorry commutes' := sorry +-- Presumably we have this? noncomputable def bar {K L AK AL : Type*} [CommRing K] [CommRing L] [CommRing AK] [CommRing AL] [Algebra K AK] [Algebra K AL] [Algebra K L] [Algebra L AL] [IsScalarTower K L AL] (f : AK →ₐ[K] AL) : L ⊗[K] AK →ₐ[L] AL := Algebra.TensorProduct.lift (Algebra.ofId _ _) f <| fun l ak ↦ mul_comm (Algebra.ofId _ _ l) (f ak) -noncomputable def FiniteAdeleRing.baseChangeIso : L ⊗[K] FiniteAdeleRing A K ≃ₐ[L] FiniteAdeleRing B L := - AlgEquiv.ofBijective (bar <| FiniteAdeleRing.baseChange A K L B) sorry +-- Follows from the above. Should be a continuous L-alg equiv but we don't have continuous +-- alg equivs yet so can't even state it properly. +noncomputable def FiniteAdeleRing.baseChangeEquiv : L ⊗[K] FiniteAdeleRing A K ≃ₐ[L] FiniteAdeleRing B L := + AlgEquiv.ofBijective (bar <| FiniteAdeleRing.baseChange A K L B) sorry -- #243 end DedekindDomain diff --git a/blueprint/lean_decls b/blueprint/lean_decls index b3472763..4780827a 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -79,11 +79,11 @@ Bourbaki52222.separableClosure_finrank_le NumberField.AdeleRing.locallyCompactSpace IsDedekindDomain.HeightOneSpectrum.valuation_comap IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgHom -IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso -IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso_integral +IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv +IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral DedekindDomain.ProdAdicCompletions.baseChange DedekindDomain.FiniteAdeleRing.baseChange -DedekindDomain.FiniteAdeleRing.baseChangeIso +DedekindDomain.FiniteAdeleRing.baseChangeEquiv Rat.AdeleRing.zero_discrete Rat.AdeleRing.discrete NumberField.AdeleRing.discrete diff --git a/blueprint/src/chapter/AdeleMiniproject.tex b/blueprint/src/chapter/AdeleMiniproject.tex index 3102ba99..80384ff7 100644 --- a/blueprint/src/chapter/AdeleMiniproject.tex +++ b/blueprint/src/chapter/AdeleMiniproject.tex @@ -129,8 +129,8 @@ \subsection{Base change for finite adeles} primes of $B$ which pull back to $v$. \begin{theorem} - \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso} - \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso} + \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv} + \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv} \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgHom} The induced continuous $L$-algebra homomorphism $L\otimes_KK_v\to\prod_{w|v}L_w$ is an isomorphism. \end{theorem} @@ -140,9 +140,9 @@ \subsection{Base change for finite adeles} \end{proof} \begin{theorem} - \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso_integral} - \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso_integral} - \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso} + \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral} + \label{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral} + \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv} The isomorphism $L\otimes_KK_v\to\prod_{w|v}L_w$ induces a topological isomorphism $B\otimes_AA_v\to \prod_{w|v}B_w$ for all but finitely many $v$ in the height one spectrum of $A$. @@ -191,9 +191,9 @@ \subsection{Base change for finite adeles} \end{proof} \begin{theorem} - \label{DedekindDomain.FiniteAdeleRing.baseChangeIso} - \lean{DedekindDomain.FiniteAdeleRing.baseChangeIso} - \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso_integral} + \label{DedekindDomain.FiniteAdeleRing.baseChangeEquiv} + \lean{DedekindDomain.FiniteAdeleRing.baseChangeEquiv} + \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral} \leanok If we give $L\otimes_K\A_{A,K}^\infty$ the ``module topology'', coming from the fact that $L\otimes_K\A_{A,K}^\infty$ is an $\A_{A,K}^\infty$-module, then the induced @@ -201,7 +201,7 @@ \subsection{Base change for finite adeles} $L\otimes_K\A_{A,K}^\infty\to\A_{B,L}^\infty$ is a topological isomorphism. \end{theorem} \begin{proof} - Follows from theorem~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgIso_integral}. + Follows from theorem~\ref{IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv_integral}. \end{proof} \subsection{Base change for infinite adeles}