Galois descent for adeles

For an extension of number fields L/K, the extension map 𝔸_K → 𝔸_L is injective (adeleExtension_injective). When L/K is Galois, its image is the set of adeles of L fixed by Gal(L/K) (mem_range_adeleExtension_iff):

𝔸_K = (𝔸_L)^{Gal(L/K)}.

Both statements are read off the base change 𝔸_K ⊗[K] L ≃ 𝔸_L (adeleBaseChangeHom_bijective). For injectivity, 𝔸_K → 𝔸_K ⊗[K] L is injective because L is flat over K. For the image, Gal(L/K) acts semilinearly on 𝔸_L, fixes the extended adeles, and the scalar extension L ⊗[K] 𝔸_K → 𝔸_L of the extension map is surjective, so its image is all the invariants by TauCeti.GaloisDescent.range_eq_invariants_of_liftBaseChange_surjective.

These are the adelic input to Galois descent for the ideles of a separable closure, where the ideles of a finite Galois subextension are recovered as the fixed points of its Galois group.

Main results

• TauCeti.GlobalNumberFields.adeleExtension_injective: the extension map of adeles is injective.
• TauCeti.GlobalNumberFields.mem_range_adeleExtension_iff: for L/K Galois, an adele of L is extended from K exactly when it is fixed by Gal(L/K).

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §2.

theorem TauCeti.GlobalNumberFields.adeleExtension_injective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Function.Injective ⇑(NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L)

The extension map of adeles is injective.

theorem TauCeti.GlobalNumberFields.mem_range_adeleExtension_iff (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {a : NumberField.AdeleRing (NumberField.RingOfIntegers L) L} : a ∈ (NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L).range ↔ ∀ (σ : Gal(L/K)), ((adeleGaloisAction K L) σ) a = a

Galois descent for adeles: for a Galois extension L/K, an adele of L is extended from an adele of K exactly when it is fixed by every element of Gal(L/K).