Extension of ideles and its global norm

Extension of adeles induces a continuous homomorphism on units, with the units topology, and carries principal ideles to principal ideles. It therefore descends to idele classes. Both maps compose in towers and raise the global norm to the field degree. This is extension of scalars, not the norm map in the opposite direction.

The norm formula combines the local degree formulas for finite and infinite completions, regrouping the local factors by the place below. In particular, a complex place above a real place contributes degree two. No Galois hypothesis is used.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter VI, §1.

noncomputable def TauCeti.GlobalNumberFields.ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K →* NumberField.IdeleGroup (NumberField.RingOfIntegers L) L

Extension of ideles along a number-field extension, induced by extension of adeles.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : ↑((ideleExtension K L) x) = (NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) ↑x

The underlying adele of the extended idele is the extended adele.

theorem TauCeti.GlobalNumberFields.continuous_ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Continuous ⇑(ideleExtension K L)

Extension is continuous for the units topology on ideles.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleExtension_unitEmbedding (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : Kˣ) : (ideleExtension K L) ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) x) = (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers L) L) ((Units.map ↑(algebraMap K L)) x)

Extension carries a principal idele to the principal idele of the same element in L.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleExtension_self (K : Type u_1) [Field K] [NumberField K] : ideleExtension K K = MonoidHom.id (NumberField.IdeleGroup (NumberField.RingOfIntegers K) K)

Extension of ideles along the identity extension is the identity.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleExtension_comp (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] : (ideleExtension L M).comp (ideleExtension K L) = ideleExtension K M

Extension of ideles composes in a tower.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleInfiniteCoord_ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (w : NumberField.InfinitePlace L) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : w.ideleInfiniteCoord ((ideleExtension K L) x) = (Units.map ↑(NumberField.LiesOver.completionMap (w.comap (algebraMap K L)) w)) ((w.comap (algebraMap K L)).ideleInfiniteCoord x)

The infinite coordinate of an extended idele is the image of the source coordinate at the place below under the completion map.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleFiniteCoord_ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : w.ideleFiniteCoord ((ideleExtension K L) x) = (Units.map ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension K L (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w) w)) ((IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w).ideleFiniteCoord x)

The finite coordinate of an extended idele is the image of the source coordinate at the place below under the adic completion extension.

@[simp]

theorem TauCeti.GlobalNumberFields.toFiniteIdele_ideleExtension {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : (NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers L) L) ((ideleExtension K L) x) = (Units.map ↑(IsDedekindDomain.finiteAdeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L)) ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) x)

Taking the finite component commutes with extension of ideles.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleNorm_ideleExtension {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : ideleNorm ((ideleExtension K L) x) = ideleNorm x ^ Module.finrank K L

Extension of ideles raises the global norm to the field degree.

theorem TauCeti.GlobalNumberFields.principalSubgroup_le_comap_ideleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K ≤ Subgroup.comap (ideleExtension K L) (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers L) L)

Extension sends the principal subgroup into the principal subgroup.

noncomputable def TauCeti.GlobalNumberFields.ideleClassExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K →* NumberField.IdeleClassGroup (NumberField.RingOfIntegers L) L

The map on idele classes induced by extension of ideles.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassExtension_mk (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : (ideleClassExtension K L) ↑x = ↑((ideleExtension K L) x)

On an idele class, extension is represented by the extended idele.

theorem TauCeti.GlobalNumberFields.continuous_ideleClassExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Continuous ⇑(ideleClassExtension K L)

The extension map on idele classes is continuous.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassExtension_self (K : Type u_1) [Field K] [NumberField K] : ideleClassExtension K K = MonoidHom.id (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)

Extension of idele classes along the identity extension is the identity.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassExtension_comp (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] : (ideleClassExtension L M).comp (ideleClassExtension K L) = ideleClassExtension K M

Extension of idele classes composes in a tower.

@[simp]

theorem TauCeti.GlobalNumberFields.ideleClassNorm_ideleClassExtension {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : ideleClassNorm ((ideleClassExtension K L) x) = ideleClassNorm x ^ Module.finrank K L

Extension of idele classes raises the class norm to the field degree.