The Galois action on the semi-local algebra

Let L/K be an extension of number fields and v a finite place of K. An automorphism σ of L/K acts on the semi-local algebra K_v ⊗[K] L through the second factor, by id ⊗ σ; this is the base change TauCeti.Algebra.TensorProduct.baseChangeAutHom of σ to K_v. Under the semi-local decomposition K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w it permutes the factors: the component at σ • w of (id ⊗ σ) z is the component of z at w, transported along the isomorphism of completions L_w ≃ L_{σ • w} induced by σ (semilocalEquiv_baseChangeAutHom). This is the action under which the adelic Galois action of L/K restricts to the components above v (TauCeti.finiteAdeleSemilocalHom_finiteAdeleEquiv).

When L/K is Galois, the Galois group permutes the places above v transitively, and the stabilizer of one place w — its decomposition group — acts on L_w. The units of the semi-local algebra are then coinduced from the decomposition group: as integral representations of Gal(L/K),

(K_v ⊗[K] L)ˣ ≅ Coind_{D_w}^{Gal(L/K)} L_wˣ,

the map sending y to the function g ↦ ((id ⊗ g) y)_w (semilocalUnitsCoindIso); its bijectivity is an instance of TauCeti.resCoindToHom_bijective_of_transport. Shapiro's lemma therefore computes the cohomology of the semi-local units from the local Galois cohomology of L_wˣ.

Main definitions

• TauCeti.semilocalUnitsRep: the units of K_v ⊗[K] L, as an integral representation of Aut(L/K).
• TauCeti.decompositionUnitsRep: the units of L_w, as an integral representation of the decomposition group of w.
• TauCeti.semilocalUnitsToCoind: the map y ↦ (g ↦ ((id ⊗ g) y)_w) into the coinduced representation.
• TauCeti.semilocalUnitsCoindIso: for L/K Galois, that map as an isomorphism of representations.

Main results

• TauCeti.semilocalEquiv_baseChangeAutHom: under the semi-local decomposition, id ⊗ σ carries the factor at w to the factor at σ • w by the isomorphism of completions.
• TauCeti.semilocalUnitsCoindIso: the semi-local units are coinduced from one completion.

References

• J. S. Milne, Class Field Theory, Chapter VII, §2 (the cohomology of ∏_{w ∣ v} L_wˣ).
• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition (8.3) and Chapter VI, §2.

theorem TauCeti.semilocalEquiv_baseChangeAutHom {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (σ : Gal(L/K)) {w w' : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }} (h : (↑w').asIdeal = σ • (↑w).asIdeal) (z : TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) : (semilocalEquiv L v) (((Algebra.TensorProduct.baseChangeAutHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) σ) z) w' = (v.completionCongr σ h) ((semilocalEquiv L v) z w)

The Galois action permutes the semi-local factors. If σ carries the place w above v to w', then the component at w' of (id ⊗ σ) z is the component of z at w, transported along the isomorphism of completions L_w ≃ L_{w'} induced by σ.

@[reducible, inline]

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

The units of the semi-local algebra K_v ⊗[K] L, as an integral representation of Aut(L/K) acting through Algebra.TensorProduct.baseChangeAutHom.

@[reducible, inline]

noncomputable abbrev TauCeti.decompositionUnitsRep {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : Rep.{u, 0, u} ℤ ↥(MulAction.stabilizer Gal(L/K) w.asIdeal)

The units of the completion L_w, as an integral representation of the decomposition group of w acting through decompositionHom.

noncomputable def TauCeti.semilocalUnitsToCoind {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : semilocalUnitsRep L v ⟶ Rep.coind.{0, u, u, u} (MulAction.stabilizer Gal(L/K) w.asIdeal).subtype (decompositionUnitsRep v w)

The map y ↦ (g ↦ ((id ⊗ g) y)_w) from the semi-local units to the representation coinduced from the units of L_w. It is the morphism adjoint to the projection to the factor at w, which is equivariant for the decomposition group of w.

theorem TauCeti.semilocalUnitsToCoind_apply {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (y : (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ) (g : Gal(L/K)) : ↑(Additive.toMul (↑((Rep.Hom.hom (semilocalUnitsToCoind v w)) (Additive.ofMul y)) g)) = (semilocalEquiv L v) (((Algebra.TensorProduct.baseChangeAutHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) g) ↑y) ⟨w, inst✝⟩

The value of semilocalUnitsToCoind at g is the component at w of (id ⊗ g) y.

noncomputable def TauCeti.semilocalUnitsCoindIso {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] : semilocalUnitsRep L v ≅ Rep.coind.{0, u, u, u} (MulAction.stabilizer Gal(L/K) w.asIdeal).subtype (decompositionUnitsRep v w)

The semi-local units are coinduced. For L/K Galois and w a place above v, the units of K_v ⊗[K] L are, as an integral representation of Gal(L/K), coinduced from the units of L_w as a representation of the decomposition group of w.

@[simp]

theorem TauCeti.semilocalUnitsCoindIso_hom {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] : (semilocalUnitsCoindIso v w).hom = semilocalUnitsToCoind v w

The coinduction isomorphism is semilocalUnitsToCoind.