microproject: restricted products

Stream: FLT

[Kevin Buzzard]

After the sterling work of @Salvatore Mercuri , @Madison Crim and @Matthew Jasper we are now much of the way towards a proof that $L\otimes_K\mathbb{A}_K=\mathbb{A}_L$ both algebraically and topologically. There is one mathematically tricky step left, which is $L\otimes_KK_v=\prod_{w|v}L_w$, which Salvatore has recently PRed in the infinite case but which we still need in the finite case. The blueprint has details of a proof which I propose to formalize https://imperialcollegelondon.github.io/FLT/blueprint/Adele_miniproject.html#IsDedekindDomain.HeightOneSpectrum.adicCompletionComapAlgEquiv but I was slightly unhappy with the precision and I tinkered with it in FLT#399, which should hopefully be merged soon.

I think that after the adele refactor is merged, then modulo $L\otimes_KK_v=\prod_wL_w$ what we will need to finish the job is some more API for docs#RestrictedProduct . Let me go through what I think we need to finish the job.

[Kevin Buzzard]

First we need a variant of some work of Maddy. When adeles were a subset of ProdAdicCompletions we needed some API for ProdAdicCompletions and Maddy proved that the construction commuted with $L\otimes_K(*)$ if $L/K$ is a finite extension of fields. Now we seem to need the analogous result for restricted products (here everything is a commutative ring):

1) Say $K_i$ are a bunch of $A$-algebras, and $C_i$ are sub-$A$-algebras, Let $\prod'[K_i;C_i]$ denote the restricted product of the $K_i$ wrt the $C_i$. If $B$ is an $A$-algebra which is finite as an $A$-module, then I claim $B\otimes_A\prod'[K_i;C_i]=\prod'[B\otimes_AK_i;B\otimes_AC_i].$

[Kevin Buzzard]

I think this can be broken down into two claims.
1a) Tensor products with finite modules commutes with arbitrary products (e.g. $B\otimes_A\prod_i C_i=\prod_i (B\otimes C_i)$; Maddy you must have essentially done this?)
1b) Some form of "tensor products commute with filtered colimits" (because the restricted tensor product is just a filtered colimit of things defined in 1a).

[Kevin Buzzard]

Then we need some way of writing down maps between restricted products. I've started on this in the file FLT/Mathlib/Topology/Algebra/RestrictedProduct.lean in FLT#399. The point is that the restricted products might be over different types (for example the finite places of $K$ and the finite places of $L$) but we want to prove that things are isomorphic.

The kind of results which we need are:

2) Say $M_v$ are types with subsets $C_v$ indexed by $v\in V$ and say $L_v$ are types with subsets $B_v$ indexed by $w\in W$. Say we have a map $c$ from $W$ to $V$ (corestriction, in the application) and for every $w$ we have a map $M_{f(w)}\to L_w$ which takes $C_{f(w)}$ into $B_w.$

Say that for each $v\in V$ the set $c^{-1}(v)$ is finite, and the map from $M_v$ to $\prod_{w\in c^{-1}(v)}L_w$ is an isomorphism, sending $C_v$ to $\prod_{w\in c^{-1}(b)}B_w.$

Then there's an induced map $\prod'_v[M_v;C_v]\to\prod'_w[L_w;B_w]$ and the claim is that it's a bijection.

In the application $M_v=L\otimes_KK_v=B\otimes_AK_v$ and $C_v=B\otimes_AA_v.$

[Kevin Buzzard]

Plus variants when everything is a ring or a $B$-algebra, when it's an isomorphism of rings.

[Kevin Buzzard]

Finally we need that if everything is topological, then the induced map is a homeomorphism.

[Kevin Buzzard]

We will also need the canonical isomorphism $L\otimes_KX=B\otimes_AX$ if $X$ is a $K$-module.

[Kevin Buzzard]

Javier Lopez had claimed $L\otimes_KK_v=\prod_wL_w$ but unfortunately he now has a new job so has little time for mathlib; he's now unclaimed this issue, which is FLT#231 .

[Matthew Jasper]

I think that we also need the map $B \otimes_A A_v \rightarrow B \otimes_A K_v \cong L \otimes_K K_v$ is injective (i.e., FLT#400 actually proves the thing that it claims to).

[Rebecca Bellovin]

I'm happy to take a stab at FLT#231

[Kevin Buzzard]

It might be the case that it's better breaking it up into smaller pieces first. Maybe it's too big to be an issue? But feel free! Make sure you look at the WIP PR by Javier first, there will be some useful stuff there

[Kevin Buzzard]

I feel like I'm missing a trick here. I want to split this argument into two or more pieces. Here's what it looks like to me.

The claim is the following. The set-up: say $A$ is a Dedekind domain, $K$ is its field of fractions, $L/K$ is a finite separable extension, $B$ is the integral closure of $A$ in $L$. Then for $v$ a nonzero maximal ideal of $A$ the claim is that the canonical map $K_v\to\prod_{w|v}L_w$ induces an isomorphism $L\otimes_KK_v=\prod_{w|v}L_w$.

The proof firstly depends on a choice; choose $\alpha\in L$ such that $L=K(\alpha)$. Using this write $L\otimes_KK_v=\prod_{i\in I}L_i$ where $I$ is some auxiliary finite set that depends on $\alpha$ and the isomorphism is a map which also depends on $\alpha$. Then say "oh well the $L_i$ match up with the $L_v$ so we're done"

[Kevin Buzzard]

I want to prove the first statement (about the $L_i$) as an independent lemma but I'm a bit confused about what the statement should say. Is there a statement which is independent of $\alpha$ and useful? For example one could prove $L\otimes_KK_v$ is a finite sum of fields. But does one need more control over the index set in order to finish the job?

[Matthew Jasper]

The map $\{w : w|v\} \rightarrow \mathrm{spec} (L \otimes_K K_v)$ given by the maps $L \otimes_K K_v \rightarrow L_w$ is bijective. Then show $L \otimes K_v$ is a finite sum of fields?

[Kevin Buzzard]

I agree that the map is a bijection (although this might need "if the valuation $v$ on $K$ comes from a nonzero maximal ideal of $A$ then every nonarchimedean norm on $L$ which restricts to $v$ on $K$ must come from a nonzero maximal ideal of $B$" and I'm not entirely clear on how hard this is). But I'm a bit less clear right now about how that gives "the obvious map $L\otimes_KK_v\to\oplus_wL_w$ is a bijection", as opposed to just "there is an isomorphism".

[Matthew Jasper]

So, letting $\phi : L \otimes K_v \rightarrow \prod_w L_w$ be the obvious map and $\pi_u : \prod_w L_w \rightarrow L_u$ the projection, I was thinking $\ker \phi = \bigcap_w \ker (\pi_w \circ \phi) = \bigcap_{\frak{m}} \frak{m} = 0$ to show injectivity and a density approach (using the results from my last PR) to show surjectivity. Maybe CRT could be used instead though.

[Kevin Buzzard]

Yes, it occurred to me also that maybe one just tries to prove directly that the obvious map $\phi$ is an injection and a surjection. You've got very good at density arguments, perhaps your PR about the integral level extends easily to show that $L$ is dense in $\prod_w L_w$?

[Rebecca Bellovin]

Can we just take the integral statement and invert $\pi_K$? But I guess showing that $(\mathcal{O}_L\otimes \mathcal{O}_{K_v})[1/\pi_K]\cong L\otimes K_v$ could be tricky.

[Kevin Buzzard]

The integral statement assumes the rational one to get injectivity

[Kevin Buzzard]

I think there are two approaches to this.

1) The approach in the blueprint. Here is a concrete statement which is certainly true but I'm unclear about how far we are from it.

We're in the usual AKLB set-up which I outlined above (K field of fractions of Ded domain A, L/K finite separable, B integral closure of A in L), with $v$ a nonzero maximal ideal of $A$ (i.e. A isn't a field!). Say $M$ is a field and an $L\otimes_KK_v$-algebra (e.g. $M=L_w$ for some $w|v$). Say $M$ is finite-dimensional as a $K_v$-vector space. Then

(i) $M$ inherits a norm, extending the norm on $K_v$ (@María Inés de Frutos Fernández do we have this in mathlib yet?)

(ii) The restriction of this norm to $L$ is equivalent to the $w$-adic norm on $L$, for some $w|v.$

That is one way to make progress on this $L\otimes_KK_v$ business. Here is a completely different approach, but I don't know how feasible it is: (1) prove that the map $L\otimes_KK_v\to\prod_{w|v}L_w$ is surjective and $K_v$-linear using the ideas which @Matthew Jasper has recently formalized. Then (2) deduce it's an isomorphism by a dimension-count. For this we'll just need $[L_w:K_v]=e_if_i$ because we have $\sum_i e_if_i=[L:K]$. Here $e_i$ and $f_i$ are defined globally, so if one were to approach this via a local definition of $e$ and $f$ then one would have to relate the local $e$ and $f$ to the global one.

[Matthew Jasper]

#23333 is open for now

[Kevin Buzzard]

I'd better get reviewing!

[María Inés de Frutos Fernández]

Kevin Buzzard said:

(i) $M$ inherits a norm, extending the norm on $K_v$ (@María Inés de Frutos Fernández do we have this in mathlib yet?)

It is not in Mathlib, but I have PR'd the whole proof: see #23178, #23184, #23251, #23252, #23254, #23266, #23301 and #23333.

[Madison Crim]

Kevin Buzzard said:

I think this can be broken down into two claims.
1a) Tensor products with finite modules commutes with arbitrary products (e.g. $B\otimes_A\prod_i C_i=\prod_i (B\otimes C_i)$; Maddy you must have essentially done this?)
1b) Some form of "tensor products commute with filtered colimits" (because the restricted tensor product is just a filtered colimit of things defined in 1a).

This is proven in TensorPi.lean for a finite free module

[Andrew Yang]

Tensor products with finite modules commutes with arbitrary products

I think you need finitely presented.

[Madison Crim]

I haven't proved it for finitely presented, but yes this condition is more general and does give the desired result.

[Kevin Buzzard]

I think free isn't good enough any more because we need it for $\mathcal{O}_L/\mathcal{O}_K$ which isn't always free :-/

[Kevin Buzzard]

The problem is that I don't really know how to make sense of $L\otimes_K\mathbb{A}_K$ as a restricted product, because $L\otimes_KK_v$ is fine but $A_v$ isn't an $K$-module.

[Matthew Jasper]

I might try that second approach for showing that the $L \otimes K_v$ map is an isomorphism.

[Kevin Buzzard]

Note that both approaches will need that the map is a surjection

[Matthew Jasper]

Ok, I'll pr that separately then.

[Kevin Buzzard]

@Madison Crim are you interested in beefing up your result about tensor products with finite modules commuting with arbitrary products from the finite free case to the general finitely presented case?

[Kevin Buzzard]

I think we must be a long way off the dimension counting argument right now. I should ask some of the global fields experts about it

[Madison Crim]

Absolutely, I actually started to think about this when I first took on my previous task.

[Kevin Buzzard]

Andrew Yang said:

Tensor products with finite modules commutes with arbitrary products

I think you need finitely presented.

Do you have a reference for this?

[Andrew Yang]

One proof is "It is true for $R^n$, and tensor product is right exact, so look at $R^n \to R^m \to M \to 0$ and you're done". I think the converse is also true and there seems to be a proof here.

[Kevin Buzzard]

Aha so Maddy your work in the free case will be an essential ingredient!

[Kevin Buzzard]

I talked about this $L\otimes_KK_v=\prod_wL_w$ issue at LLL and after some discussions I'm really coming around to the dimension count idea. The sorry in FLT#231 says that the canonical map $L\otimes_KK_v\to\prod_{w|v}L_w$ is bijective. I think/hope Matthew's work will show that it's surjective. The dimension count argument to finish is that it's a $K_v$-linear surjection between two finite-dimensional $K_v$-vector spaces of the same dimension so if it's a surjection then it must be a bijection.

The reason I think that we might be closer to this than I'd realised, is that already in the repo we have that if $w|v$ then the restriction of $w$ to $K$ is $v$ scaled by a factor of $e$. After the adele refactor bump we have a new sorry saying that the same is true for the restriction of $w$ on $L_w$ to $K_v$, but this is precisely the statement that "local e is global e". The statement that "local f is global f" should just follow from the claim that the residue field of $K_v$ is $A/P_v$ which sounds very doable (indeed I suspect that Matthew has introduced all the tools necessary, if it's not there already). So all that is missing is the statement that for a finite extension of nonarch local fields, the degree is $ef$, and this sounds very doable.

I'm still confused about the Ostrowski approach. I've had it in my head for years that to prove Ostrowski for number fields (every nonarch valuation comes from a max ideal of the ring of integers) it suffices to prove it for the rationals and then everything is obvious. I'm no longer sure that everything is obvious but maybe what's actually happened is that I've forgotten the proof of Ostrowski and it's got some key technique in it which makes it easy. But one reason I like the local approach is that the dimension being $ef$ just sounds like an important and useful result in general, and I want to build up the theory of local fields in mathlib. Right now we are still bickering about the definition but I feel like things are converging.

[Matthew Jasper]

The dim = local $e f$ is the global result once you show that $\mathcal{O}_w/\mathcal{O}_v$ is a finite extension of DVRs (depending on what exactly you mean by "local $e$")

[Alex Kontorovich]

In case it's useful, here's a quick exposition over $\mathbb Q$: https://youtu.be/bCziMZ8tkHQ?si=tnak6ZkTXB2tca7z&t=2297

[Matthew Jasper]

FLT#432 is the surjective "half" of this