The infinite ideles as a Galois representation

Let L/K be an extension of number fields. The infinite ideles of L are the units L_∞ˣ = ∏_w L_wˣ of its infinite adele ring, the product running over the infinite places w of L. The automorphisms of L/K act on them through the Galois action on infinite adeles (TauCeti.GlobalNumberFields.infiniteAdeleGaloisAction), which permutes the places of L.

Grouping the places of L by the infinite place v of K below them identifies the infinite ideles, as an integral representation of Aut(L/K), with the product over v of the units of the semi-local algebras K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w:

L_∞ˣ ≅ ∏_v (K_v ⊗[K] L)ˣ

(infiniteIdelesPiIso). Each factor is coinduced from the units of a single completion (TauCeti.GlobalNumberFields.infiniteSemilocalUnitsCoindIso), so this decomposition is how the Tate cohomology of the infinite ideles reduces to the Galois cohomology of the archimedean local fields. The infinite ideles are the archimedean factor of the S-ideles I_{L,S} = L_∞ˣ × ∏_{w ∈ S} L_wˣ × ∏_{w ∉ S} 𝒪_wˣ.

Main definitions

• TauCeti.GlobalNumberFields.infiniteIdeleMulDistribMulAction: the Galois action on the infinite ideles, an instance in the scope AdeleGaloisAction.
• TauCeti.GlobalNumberFields.infiniteIdelesRep: the infinite ideles of L as an integral representation of Aut(L/K).
• TauCeti.GlobalNumberFields.infiniteIdelesPiIso: its decomposition as the product over the infinite places of K of the semi-local units.

References

• J. S. Milne, Class Field Theory, Chapter VII, §2.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §2.

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.infiniteIdeleMulDistribMulAction (K L : Type u) [Field K] [Field L] [Algebra K L] : MulDistribMulAction Gal(L/K) (NumberField.InfiniteAdeleRing L)ˣ

The Galois action on infinite ideles: σ ∈ Aut(L/K) acts on the units of the infinite adele ring of L by the ring automorphism infiniteAdeleGaloisAction K L σ. It is a definition rather than a global instance, available as an instance in the scope AdeleGaloisAction.

theorem TauCeti.GlobalNumberFields.coe_infiniteIdele_smul {K L : Type u} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (x : (NumberField.InfiniteAdeleRing L)ˣ) : ↑(σ • x) = ((infiniteAdeleGaloisAction K L) σ) ↑x

The Galois action on an infinite idele is the Galois action on the underlying infinite adele.

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.infiniteIdelesRep (K L : Type u) [Field K] [Field L] [Algebra K L] : Rep.{u, 0, u} ℤ Gal(L/K)

The infinite ideles of L, the units of its infinite adele ring, as an integral representation of Aut(L/K).

noncomputable def TauCeti.GlobalNumberFields.infiniteIdelesPiIso (K L : Type u) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] : infiniteIdelesRep K L ≅ Rep.pi fun (v : NumberField.InfinitePlace K) => infiniteSemilocalUnitsRep L v

The infinite ideles are the product of the semi-local units. As integral representations of Aut(L/K), the infinite ideles of L are the product over the infinite places v of K of the units of K_v ⊗[K] L, by the semi-local components above each v.

theorem TauCeti.GlobalNumberFields.coe_infiniteIdelesPiIso_hom_apply {K L : Type u} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (x : Additive (NumberField.InfiniteAdeleRing L)ˣ) (v : NumberField.InfinitePlace K) : ↑(Additive.toMul ((Rep.Hom.hom (infiniteIdelesPiIso K L).hom) x v)) = (infiniteAdeleSemilocalHom L v) ↑(Additive.toMul x)

The component at v of the image of an infinite idele under infiniteIdelesPiIso is its semi-local component above v.