The finite S-ideles as a product of semi-local factors

Let L/K be an extension of number fields and S a finite set of finite places of K. The finite S-ideles of L are the finite ideles whose component at every finite place w of L not above S is a unit of 𝒪_w:

I_{L,S}^f = ∏_{v ∈ S} ∏_{w ∣ v} L_wˣ × ∏_{v ∉ S} ∏_{w ∣ v} 𝒪_wˣ.

A finite idele is determined by its semi-local components in the units of K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w (TauCeti.finiteIdeleSemilocalHom), and taking components is equivariant for the Galois action of Aut(L/K) on finite adeles (GlobalNumberFields.finiteAdeleGaloisAction) and on the semi-local algebras (Algebra.TensorProduct.baseChangeAutHom). Together with the assembly of a finite idele from semi-local units (TauCeti.finiteIdeleOfSemilocalUnits), these identify the finite S-ideles, as an integral representation of Aut(L/K), with the product over the places of K of the semi-local unit groups (K_v ⊗[K] L)ˣ for v ∈ S and of the integral semi-local unit groups for v ∉ S (finiteSIdelesPiIso). This is the form in which the Tate cohomology of the S-ideles is computed one place at a time, through Shapiro's lemma for each semi-local factor.

Main definitions

• TauCeti.finiteSIdeles L S: the finite S-ideles of L, as a subgroup of the finite ideles.
• TauCeti.finiteSIdelesRep L S: the finite S-ideles, as an integral representation of Aut(L/K).
• TauCeti.finiteSIdelesPiRep L S: the product of the semi-local factors of the finite S-ideles.
• TauCeti.finiteSIdelesPiIso L S: the isomorphism of representations between the two.

Main results

• TauCeti.finiteSIdeles_eq_sIntegralUnits: the finite S-ideles are the S-integral finite ideles of L (IsDedekindDomain.FiniteAdeleRing.sIntegralUnits) for the places above S.
• TauCeti.mem_finiteSIdeles_iff_valued_eq_one: a finite idele is an S-idele exactly when its components at the places not above S have valuation one.
• TauCeti.toFiniteIdele_mem_finiteSIdeles_iff: an idele is an S-idele exactly when its finite part is a finite S-idele.

References

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

The finite S-ideles

def TauCeti.finiteSIdeles {K : Type u} [Field K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Subgroup (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ

The finite S-ideles. For a finite set S of finite places of K, the finite ideles of L whose semi-local component at every finite place v ∉ S of K is integral, that is, whose component at every place of L not above S is a unit of 𝒪_w.

theorem TauCeti.finiteSIdeles_eq_sIntegralUnits {K : Type u} [Field K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : finiteSIdeles L S = IsDedekindDomain.FiniteAdeleRing.sIntegralUnits (NumberField.RingOfIntegers L) L {w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) | IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∈ S}

The finite S-ideles of L are the S'-integral finite ideles of L, for S' the set of places of L above S.

theorem TauCeti.mem_finiteSIdeles_iff_valued_eq_one {K : Type u} [Field K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {a : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ} : a ∈ finiteSIdeles L S ↔ ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Valued.v (↑a w) = 1

A finite idele is an S-idele exactly when its component at every place of L not above S has valuation one.

@[simp]

theorem TauCeti.mem_finiteSIdeles_iff {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {a : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ} : a ∈ finiteSIdeles L S ↔ ∀ v ∉ S, (finiteIdeleSemilocalHom L v) a ∈ semilocalIntegralUnits L v

A finite idele is an S-idele exactly when its semi-local components outside S are integral.

theorem TauCeti.toFiniteIdele_mem_finiteSIdeles_iff {K : Type u} [Field K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L} : (NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers L) L) x ∈ finiteSIdeles L S ↔ x ∈ GlobalNumberFields.sIdeles L ↑S

An idele is an S-idele exactly when its finite part is a finite S-idele.

theorem TauCeti.map_finiteAdeleGaloisAction_mem_finiteSIdeles {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (σ : Gal(L/K)) {a : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ} (ha : a ∈ finiteSIdeles L S) : (Units.map ↑((GlobalNumberFields.finiteAdeleGaloisAction K L) σ)) a ∈ finiteSIdeles L S

The Galois action on finite ideles preserves the finite S-ideles.

@[instance_reducible]

noncomputable instance TauCeti.finiteSIdelesMulDistribMulAction {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : MulDistribMulAction Gal(L/K) ↥(finiteSIdeles L S)

The Galois action of Aut(L/K) on the finite S-ideles, through the Galois action on finite adeles.

@[simp]

theorem TauCeti.coe_smul_finiteSIdeles {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (σ : Gal(L/K)) (a : ↥(finiteSIdeles L S)) : ↑(σ • a) = (Units.map ↑((GlobalNumberFields.finiteAdeleGaloisAction K L) σ)) ↑a

The Galois action on a finite S-idele is the Galois action on the underlying finite idele.

@[reducible, inline]

noncomputable abbrev TauCeti.finiteSIdelesRep {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Rep.{u, 0, u} ℤ Gal(L/K)

The finite S-ideles, as an integral representation of Aut(L/K).

@[reducible, inline]

noncomputable abbrev TauCeti.finiteSIdelesPiRep {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Rep.{u, 0, u} ℤ Gal(L/K)

The product, over the finite places v of K, of the semi-local units (K_v ⊗[K] L)ˣ for v ∈ S and of the integral semi-local units ∏_{w ∣ v} 𝒪_wˣ for v ∉ S, as an integral representation of Aut(L/K).

noncomputable def TauCeti.finiteSIdelesPiIso {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : finiteSIdelesRep L S ≅ finiteSIdelesPiRep L S

The finite S-ideles are the product of their semi-local factors. As integral representations of Aut(L/K), I_{L,S}^f ≅ ∏_{v ∈ S} (K_v ⊗[K] L)ˣ × ∏_{v ∉ S} ∏_{w ∣ v} 𝒪_wˣ, by taking semi-local components.

@[simp]

theorem TauCeti.finiteSIdelesPiIso_hom_apply_inl {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (a : ↥(finiteSIdeles L S)) (v : ↥S) : (Rep.Hom.hom (finiteSIdelesPiIso L S).hom) (Additive.ofMul a) (Sum.inl v) = Additive.ofMul ((finiteIdeleSemilocalHom L ↑v) ↑a)

The factor of finiteSIdelesPiIso at a place v ∈ S is the semi-local component.

@[simp]

theorem TauCeti.finiteSIdelesPiIso_hom_apply_inr {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (a : ↥(finiteSIdeles L S)) (v : { v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) // v ∉ S }) : (Rep.Hom.hom (finiteSIdelesPiIso L S).hom) (Additive.ofMul a) (Sum.inr v) = Additive.ofMul ⟨(finiteIdeleSemilocalHom L ↑v) ↑a, ⋯⟩

The factor of finiteSIdelesPiIso at a place v ∉ S is the semi-local component, which is integral.