Coinduction of semi-local integral units

For a finite Galois extension L/K and a finite place v of K, the subgroup of (K_v ⊗[K] L)ˣ integral and invertible in every component is coinduced from 𝒪[L_w]ˣ for any place w above v. The decomposition group acts on that component through its canonical action on L_w.

The subgroup is defined using the depth-zero unit filtrations in the actual completions. Its coinduction isomorphism is the restriction of TauCeti.semilocalUnitsCoindIso. This comparison lets Shapiro's lemma compute the integral factors outside a finite set of places in the cohomology of ideles, rather than replacing those factors by L_wˣ.

References

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

noncomputable def TauCeti.semilocalIntegralUnits {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Subgroup (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ

The units of K_v ⊗[K] L whose components belong to the integer-unit groups of every completion above v.

@[simp]

theorem TauCeti.mem_semilocalIntegralUnits_iff {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (y : (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ) : y ∈ semilocalIntegralUnits L v ↔ ∀ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Valued.v ((semilocalEquiv L v) (↑y) w) = 1

A semi-local unit is integral and invertible exactly when every component has valuation one.

theorem TauCeti.baseChangeAutHom_mem_semilocalIntegralUnits {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Gal(L/K)) {y : (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ} (hy : y ∈ semilocalIntegralUnits L v) : (Units.map ↑((Algebra.TensorProduct.baseChangeAutHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) g)) y ∈ semilocalIntegralUnits L v

The Galois action preserves the group of semi-local integral units.

@[instance_reducible]

noncomputable instance TauCeti.semilocalIntegralUnitsMulDistribMulAction {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : MulDistribMulAction Gal(L/K) ↥(semilocalIntegralUnits L v)

The Galois action on the group of semi-local integral units.

@[simp]

theorem TauCeti.coe_smul_semilocalIntegralUnits {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Gal(L/K)) (y : ↥(semilocalIntegralUnits L v)) : ↑(g • y) = (Units.map ↑((Algebra.TensorProduct.baseChangeAutHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) g)) ↑y

The restricted Galois action agrees with the action on the semi-local algebra.

@[reducible, inline]

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

The integral representation on the semi-local integer-unit group.

noncomputable def TauCeti.semilocalIntegralUnitsIncl {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : semilocalIntegralUnitsRep L v ⟶ semilocalUnitsRep L v

Inclusion of the integral semi-local units in the full semi-local unit representation.

@[simp]

theorem TauCeti.semilocalIntegralUnitsIncl_apply {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (y : Additive ↥(semilocalIntegralUnits L v)) : (Rep.Hom.hom (semilocalIntegralUnitsIncl L v)) y = Additive.ofMul ↑(Additive.toMul y)

The semi-local representation inclusion evaluates to the subgroup inclusion.

@[reducible, inline]

noncomputable abbrev TauCeti.decompositionIntegralUnitsRep {K L : Type u} [Field K] [NumberField K] [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 integer-unit group of L_w, with the action of its decomposition group.

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

The coinduction map sends an integral semi-local unit y to the function g ↦ ((id ⊗ g)y)_w, now valued in the integer-unit group of L_w.

theorem TauCeti.semilocalIntegralUnitsToCoind_apply {K L : Type u} [Field K] [NumberField K] [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 : ↥(semilocalIntegralUnits L v)) (g : Gal(L/K)) : ↑↑(Additive.toMul (↑((Rep.Hom.hom (semilocalIntegralUnitsToCoind v w)) (Additive.ofMul y)) g)) = (semilocalEquiv L v) (((Algebra.TensorProduct.baseChangeAutHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) g) ↑↑y) ⟨w, inst✝⟩

The coinduction map evaluated at an automorphism is its component at w.

noncomputable def TauCeti.integralUnitsCoindIncl {K L : Type u} [Field K] [NumberField K] [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.coind.{0, u, u, u} (MulAction.stabilizer Gal(L/K) w.asIdeal).subtype (decompositionIntegralUnitsRep v w) ⟶ Rep.coind.{0, u, u, u} (MulAction.stabilizer Gal(L/K) w.asIdeal).subtype (decompositionUnitsRep v w)

Coinduction of the inclusion of local integer units into the full local unit group.

@[simp]

theorem TauCeti.integralUnitsCoindIncl_apply {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (F : ↑(Rep.coind.{0, u, u, u} (MulAction.stabilizer Gal(L/K) w.asIdeal).subtype (decompositionIntegralUnitsRep v w))) (g : Gal(L/K)) : ↑((Rep.Hom.hom (integralUnitsCoindIncl v w)) F) g = Additive.ofMul ↑(Additive.toMul (↑F g))

The coinduced inclusion applies the local subgroup inclusion at each automorphism.

theorem TauCeti.semilocalIntegralUnitsToCoind_comp_incl {K L : Type u} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : CategoryTheory.CategoryStruct.comp (semilocalIntegralUnitsToCoind v w) (integralUnitsCoindIncl v w) = CategoryTheory.CategoryStruct.comp (semilocalIntegralUnitsIncl L v) (semilocalUnitsToCoind v w)

Integral coinduction is the restriction of full coinduction: the canonical inclusion square commutes as a square of Galois representations.

noncomputable def TauCeti.semilocalIntegralUnitsCoindIso {K L : Type u} [Field K] [NumberField K] [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] : semilocalIntegralUnitsRep L v ≅ Rep.coind.{0, u, u, u} (MulAction.stabilizer Gal(L/K) w.asIdeal).subtype (decompositionIntegralUnitsRep v w)

Semi-local integral units are coinduced from local integral units. For a Galois extension, projection to one completion identifies the representation on all integral semi-local units with coinduction from the decomposition group of that completion.

@[simp]

theorem TauCeti.semilocalIntegralUnitsCoindIso_hom {K L : Type u} [Field K] [NumberField K] [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] : (semilocalIntegralUnitsCoindIso v w).hom = semilocalIntegralUnitsToCoind v w

The coinduction isomorphism is the map obtained by projection to w.