An element of prod_v K_v is a finite adele iff its image in prod_w L_w is a finite adele

[kbuzzard]

If L/K is a finite extension of number fields (or fields of fractions of Dedekind domains etc etc) then an element of prod_v K_v is integral at almost all places iff its image in prod_w L_w is. One implication is easy. To get the reverse, say the image of (x_v) in prod_w L_w is a finite adele. Then locally it's in prod_{w|v} O_w for almost all v, so 1 tensor x_v is in O_L tensor_{O_K} O_v for almost all v by a previous result (my instinct is that this is where the hard work is; this work is blocked on #229 though). This surely is enough (for example one can take traces to deduce that nx_v is integral, and n is a unit for almost all v).

Status: blocked on #229

[WilliamCoram]

claim