restricted products

Stream: maths

[Kevin Buzzard]

I've only really ever seen restricted products defined in mathematics when dealing with adeles and situations related to adeles. Typically the books say that if $G_i$ are groups (or rings or top spaces or top rings or...) for $i$ running through some index set, and if $H_i$ are subgroups (resp subrings etc) of $G_i$ for all but finitely many $i$ (i.e. allowing $H_i$ not to be defined for some $i$) then the restricted product of the $G_i$ wrt the $H_i$ is the elements in $\prod_i G_i$ whose $$i$$th component is in $H_i$ for all but finitely many $i$.

Right now, as far as I know, we only have one instance of this construction in mathlib, which is the finite adeles, where $H_i$ exist for all $i$. The adeles of a number field are now in mathlib but defined explicitly as the product (not restricted product) of the finite adeles and the infinite adeles. In particular we don't need to worry about defining $H_i$ when $i$ is an infinite place. But even if we did, we could just define it to be \top for the finitely many $i$ for which the literature doesn't want to define an $H_i$.

I think we need some API for restricted products. For example I need for FLT the assertion that the adeles are locally compact, and I propose to prove this by showing that the product of two locally compact spaces is locally compact (which we might well have) and then showing that the restricted product of $G_i$ where $H_i$ are compact open has a restricted product topology making it locally compact. Right now we're doing all this by hand for finite adeles but it's going to be useful later on to know things like $GL_n(\mathbb{A_f})$ is a restricted direct product of $GL_n(\mathbb{Q}_p)$ with respect to $GL_n(\Z_p)$. So I propose making a general restricted product API but making it so that all of the $G_i$ are equipped with subobjects $H_i$, as opposed to "all but finitely many" as in the literature, and in any future situation where we really don't have $H_i$ for some $i$, we just let those $H_i$ be top or bot or whatever (it doesn't matter, because changing finitely many $H_i$ makes no difference to the restricted product).

Does anyone see any reason why this might be a bad idea?

I'm proposing a definition like this

import Mathlib

variable (I : Type*) (G : I → Type*) (H : I → Type*) [∀ i, SetLike (H i) (G i)]

def RestrictedProduct := {x : ∀ i, G i // ∀ᶠ i : I in Filter.cofinite, x i ∈ (H i : Set (G i))}

and hopefully it can be extended to the case where H_i is a subgroup/subring etc of G_i, but right now the definition doesn't compile because I am incompetent at SetLike.

[Thomas Browning]

Maybe the variables line should be something more like this?
variable (I : Type*) (G : I → Type*) {Ht : I → Type*} (H : ∀ i, Ht i) [∀ i, SetLike (Ht i) (G i)]

[Thomas Browning]

But I don't see an obvious problem with requiring $H_i$ for all $i$.

[Adam Topaz]

This makes me wonder whether we could use a Sort-valued analogue of docs#Filter.Eventually

[Adam Topaz]

Namely I'm envisioning something like this:

import Mathlib

variable
  {I : Type*}
  {dom : Set I}
  {F : Filter I}
  (h : dom ∈ F)
  (G : I → Type*)
  (H : I → Type*)
  [∀ i, SetLike (H i) (G i)]
  (𝒪 : (i : I) → i ∈ dom → H i)

def restrictedProduct := {x : (i : I) → G i | {j : I | ∃ (h : j ∈ dom), (x j ∈ 𝒪 j h) } ∈ F }

[Adam Topaz]

Thinking more carefully the assumption that dom is in F is redundant, since this is implied whenever restrictedProduct is nonempty.

[Anatole Dedecker]

I'm not at all used to that area of maths, but I would definitely just define $H_i$ for all $i$, I don't see how that could be a problem.

[Adam Topaz]

Yeah I agree that one could define H i for all i with no issues. But defining terms of H i for all i could be a problem. E.g. in the usual case I is the set of primes of a number field, G i is the completion at the place, H i is the type of subrings of the completion, and the terms of H i are the rings of integers at the finite places only.

[Kevin Buzzard]

My proposal is to set H i = ⊤ as a junk value when in the books they have H i undefined.

The only problem I've run into so far is the following. If G i are topological spaces and H i are open subspaces, then you can put a topology on the restricted product by saying that a basis of open sets in the restricted product is $\prod_i U_i$ where $U_i=H_i$ for all but finitely many $i$. Then you can prove that if all the $H_i$ are compact then the restricted product is locally compact. However at the infinite places the $H_i$ really aren't locally compact.

But I claim that this doesn't matter. Right now in the definition of the adele we do not define the full adeles as being a restricted product, we define it as a product of finite and infinite adeles, with the finite adeles being (what will be defeq to, when I'm done) a restricted product. So the proof of local compactness of adeles will go: product of two locally compact spaces is locally compact, infinite adeles are locally compact, finite adeles are locally compact because of the machinery above.

[Kevin Buzzard]

Archimedean and nonarchimedean norms sometimes live happily together, but most of the time when formalising you simply deal with the two situations using different techniques. You see this in Jacquet-Langlands. They make a valliant effort to do everything in "full generality" but they do things like talking about Schwarz space, and the definition is "if it's archimedean do this, and if it's nonarchimedean then do that", and then when they start proving theorems about Schwarz space it's "if it's archimedean do this, and if it's nonarchimedean then do that". In practice if you look at the definition of the adeles of a number field, we have adopted the pragmatic approach, i.e. confess up front that archimedean and nonarchimedean norms just need to be dealt with separately, and probably it's best if we continue this way. One reason for doing it like this is that the nonarchimedean adele part of the story makes sense for all Dedekind domains (no finiteness hypotheses required, and one can imagine doing Riemann-Roch using these ideas a la Serre for curves over the complexes) whereas the archimedean story is specifically for number fields.

[Adam Topaz]

I think in this case Using junk values will make things more annoying

[Adam Topaz]

The elements of the restricted product are the actual “functions” and they don’t have any restrictions on where they can be evaluated. OTOH they also satisfy some property that involves the filter, but i see no reason to use junk values in the definition of that property. In practice we would have assumptions that some unrestricted sequence satisfies that property, which will behave in the same way as saying that “this is not a junk value”. But if we have junk values in the definition of the property then we will have to split ifs in proofs and potentially add additional hypotheses to theorems.

[Kevin Buzzard]

I don't buy it. By the very nature of the definition, changing finitely many H_i (or pretending they're undefined, or pretending they're defined) doesn't even change the definition. I searched the literature (what little I could find of it) but the only filter I could ever find being used was the cofinite filter. All the proofs already split on whether you're in H_i or whether you're in the finite set of exceptions.

[Adam Topaz]

Some other filters are used for adeles in higher dimensions

[Anatole Dedecker]

I'm tempted to agree with Kevin (again, without real experience in working with these objects) : it sounds like you are going to assume things for all but finitely many $$H_i$$s anyway, which means you shouldn't care about junk values for finitely many of thems (e.g probably the solution to Kevin's problem is simply to assume that, eventually, the $$H_i$$s are compact). The obvious issue is then that typeclass inference doesn't know how to deal with docs#Filter.Eventually, but that shouldn't cause that much troubles (?).

[Adam Topaz]

One could imagine situations where H i is empty (e.g. maybe we want to consider the type of compact subrings, which is empty for the reals but nonempty for the p-adics). But that’s a contrived example, i admit. Anyway, my feeling is that junk values in the property defining restricted products will not be any easier to use when compared with the bounded approach i suggest above, but the easiest way to find out is to just do it in one way or another.