ImperialCollegeLondon / FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Apache License 2.0
262 stars 48 forks source link

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

Open kbuzzard opened 3 days ago

kbuzzard commented 3 days ago

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 Lw 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 OL tensor{O_K} O_v for almost all v by a previous result. 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).