Galois descent for ideles

For an extension of number fields L/K, the extension map of ideles I_K → I_L is injective (ideleExtension_injective). When L/K is Galois, its image is the set of ideles of L fixed by Gal(L/K) (mem_range_ideleExtension_iff):

I_K = (I_L)^{Gal(L/K)}.

Both are the corresponding statements for adeles (adeleExtension_injective, mem_range_adeleExtension_iff), applied to an idele and to its inverse.

Main results

• TauCeti.GlobalNumberFields.ideleExtension_injective: the extension map of ideles is injective.
• TauCeti.GlobalNumberFields.mem_range_ideleExtension_iff: for L/K Galois, an idele of L is extended from K exactly when it is fixed by Gal(L/K).
• TauCeti.GlobalNumberFields.ideleClassExtension_bijective: when algebraMap K L is surjective, extension of idele classes is bijective.

References

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

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

The extension map of ideles is injective.

theorem TauCeti.GlobalNumberFields.mem_range_ideleExtension_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.IdeleGroup (NumberField.RingOfIntegers L) L} : a ∈ (ideleExtension K L).range ↔ ∀ (σ : Gal(L/K)), ((adeleGaloisAction K L) σ) ↑a = ↑a

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

theorem TauCeti.GlobalNumberFields.ideleClassExtension_bijective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (h : Function.Surjective ⇑(algebraMap K L)) : Function.Bijective ⇑(ideleClassExtension K L)

Extension of idele classes along a surjective algebraMap is bijective: when every element of L comes from K, a principal idele of L extended from K is the extension of a principal idele of K, and every idele of L is fixed by the trivial group Gal(L/K), so it descends to K.