Galois action on adeles

A field isomorphism transports finite and infinite adeles by restriction of places and the induced maps of completions. The resulting ring equivalences are continuous in both directions and commute with the diagonal embeddings. Their composition laws give the Galois action on the finite adele ring and on the full adele ring, with the discrete topology on the finite automorphism group; the former is the finite component of the latter.

The construction uses finiteAdeleExtension and infiniteAdeleExtension with the algebra structure induced by the field isomorphism. In particular, it preserves the restricted-product condition, rather than merely permuting the ambient unrestricted product.

References

• Neukirch, Algebraic Number Theory, Chapter VI, §1.

noncomputable def TauCeti.GlobalNumberFields.infiniteAdeleEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] (e : K ≃+* L) : NumberField.InfiniteAdeleRing K ≃+* NumberField.InfiniteAdeleRing L

The transport of infinite adeles along a field isomorphism. The component at w uses the completion map from the place obtained by pulling w back along the isomorphism.

theorem TauCeti.GlobalNumberFields.continuous_infiniteAdeleEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] (e : K ≃+* L) : Continuous ⇑(infiniteAdeleEquiv K L e)

Transport of infinite adeles is continuous.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleEquiv_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] (e : K ≃+* L) (x : K) : (infiniteAdeleEquiv K L e) ((algebraMap K (NumberField.InfiniteAdeleRing K)) x) = (algebraMap L (NumberField.InfiniteAdeleRing L)) (e x)

Transport of infinite adeles commutes with the diagonal field embeddings.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleEquiv_symm (K : Type u_1) (L : Type u_2) [Field K] [Field L] (e : K ≃+* L) : (infiniteAdeleEquiv K L e).symm = infiniteAdeleEquiv L K e.symm

The inverse transport of infinite adeles is transport along the inverse field isomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleEquiv_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] (e : K ≃+* L) (a : NumberField.InfiniteAdeleRing K) (w : NumberField.InfinitePlace L) : (infiniteAdeleEquiv K L e) a w = (NumberField.LiesOver.completionMap (w.comap (algebraMap K L)) w) (a (w.comap (algebraMap K L)))

The placewise formula for transport of infinite adeles. The local map uses the algebra structure induced by e, not any pre-existing algebra structure on L over K.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleEquiv_refl (K : Type u_1) [Field K] : infiniteAdeleEquiv K K (RingEquiv.refl K) = RingEquiv.refl (NumberField.InfiniteAdeleRing K)

Transport of infinite adeles along the identity field isomorphism is the identity.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleEquiv_trans (K : Type u_1) (L : Type u_2) [Field K] [Field L] (M : Type u_3) [Field M] (e : K ≃+* L) (f : L ≃+* M) : (infiniteAdeleEquiv K L e).trans (infiniteAdeleEquiv L M f) = infiniteAdeleEquiv K M (e.trans f)

Transport of infinite adeles respects composition of field isomorphisms.

noncomputable def TauCeti.GlobalNumberFields.infiniteAdeleGaloisAction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Gal(L/K) →* NumberField.InfiniteAdeleRing L ≃+* NumberField.InfiniteAdeleRing L

The action of the field automorphism group on infinite adeles, by ring automorphisms. It is the infinite component of adeleGaloisAction (adeleGaloisAction_fst).

theorem TauCeti.GlobalNumberFields.infiniteAdeleGaloisAction_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (a : NumberField.InfiniteAdeleRing L) : ((infiniteAdeleGaloisAction K L) σ) a = (infiniteAdeleEquiv L L σ.toRingEquiv) a

Evaluation of the Galois action on infinite adeles uses transport along the underlying field automorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleGaloisAction_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (x : L) : ((infiniteAdeleGaloisAction K L) σ) ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = (algebraMap L (NumberField.InfiniteAdeleRing L)) (σ x)

The Galois action on infinite adeles extends the action on the diagonally embedded number field.

noncomputable def TauCeti.GlobalNumberFields.finiteAdeleEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K ≃+* IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L

The transport of finite adeles along a field isomorphism, including preservation of integrality at all but finitely many places.

theorem TauCeti.GlobalNumberFields.continuous_finiteAdeleEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) : Continuous ⇑(finiteAdeleEquiv K L e)

Transport of finite adeles is continuous.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleEquiv_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) (x : K) : (finiteAdeleEquiv K L e) ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)) x) = (algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) (e x)

Transport of finite adeles commutes with the diagonal field embeddings.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleEquiv_symm (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) : (finiteAdeleEquiv K L e).symm = finiteAdeleEquiv L K e.symm

The inverse transport of finite adeles is transport along the inverse field isomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleEquiv_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : ((finiteAdeleEquiv K L e) a) w = (IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension K L (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w) w) (a (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w))

The placewise formula for transport of finite adeles. The prime below w is its comap under the induced isomorphism of rings of integers.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleEquiv_refl (K : Type u_1) [Field K] [NumberField K] : finiteAdeleEquiv K K (RingEquiv.refl K) = RingEquiv.refl (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)

Transport of finite adeles along the identity field isomorphism is the identity.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleEquiv_trans (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (M : Type u_3) [Field M] [NumberField M] (e : K ≃+* L) (f : L ≃+* M) : (finiteAdeleEquiv K L e).trans (finiteAdeleEquiv L M f) = finiteAdeleEquiv K M (e.trans f)

Transport of finite adeles respects composition of field isomorphisms.

noncomputable def TauCeti.GlobalNumberFields.adeleEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) : NumberField.AdeleRing (NumberField.RingOfIntegers K) K ≃+* NumberField.AdeleRing (NumberField.RingOfIntegers L) L

The ring equivalence of full adele rings induced by a field isomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleEquiv_fst (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : ((adeleEquiv K L e) a).1 = (infiniteAdeleEquiv K L e) a.1

@[simp]

theorem TauCeti.GlobalNumberFields.adeleEquiv_snd (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : ((adeleEquiv K L e) a).2 = (finiteAdeleEquiv K L e) a.2

theorem TauCeti.GlobalNumberFields.continuous_adeleEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) : Continuous ⇑(adeleEquiv K L e)

Transport of full adeles is continuous. Its inverse is the transport along e.symm.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleEquiv_symm (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) : (adeleEquiv K L e).symm = adeleEquiv L K e.symm

The inverse transport of full adeles is transport along the inverse field isomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleEquiv_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (e : K ≃+* L) (x : K) : (adeleEquiv K L e) ((algebraMap K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) x) = (algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) (e x)

Field isomorphisms commute with the diagonal embeddings into the full adele rings.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleEquiv_refl (K : Type u_1) [Field K] [NumberField K] : adeleEquiv K K (RingEquiv.refl K) = RingEquiv.refl (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)

Transport of full adeles along the identity field isomorphism is the identity.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleEquiv_trans (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] (M : Type u_3) [Field M] [NumberField M] (e : K ≃+* L) (f : L ≃+* M) : (adeleEquiv K L e).trans (adeleEquiv L M f) = adeleEquiv K M (e.trans f)

Transport of full adeles respects composition of field isomorphisms.

noncomputable def TauCeti.GlobalNumberFields.finiteAdeleGaloisAction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] : Gal(L/K) →* IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L ≃+* IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L

The action of the field automorphism group on finite adeles, by ring automorphisms. It is the finite component of adeleGaloisAction (adeleGaloisAction_snd).

theorem TauCeti.GlobalNumberFields.finiteAdeleGaloisAction_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) : ((finiteAdeleGaloisAction K L) σ) a = (finiteAdeleEquiv L L σ.toRingEquiv) a

Evaluation of the Galois action on finite adeles uses transport along the underlying field automorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleGaloisAction_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (x : L) : ((finiteAdeleGaloisAction K L) σ) ((algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) (σ x)

The Galois action on finite adeles extends the action on the diagonally embedded number field.

noncomputable def TauCeti.GlobalNumberFields.adeleGaloisAction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] : Gal(L/K) →* NumberField.AdeleRing (NumberField.RingOfIntegers L) L ≃+* NumberField.AdeleRing (NumberField.RingOfIntegers L) L

The action of the field automorphism group on full adeles, by continuous ring automorphisms. No normality hypothesis is needed to act; for a Galois extension this is the Galois action.

theorem TauCeti.GlobalNumberFields.adeleGaloisAction_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (a : NumberField.AdeleRing (NumberField.RingOfIntegers L) L) : ((adeleGaloisAction K L) σ) a = (adeleEquiv L L σ.toRingEquiv) a

Evaluation of the Galois action uses transport along the underlying field automorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleGaloisAction_snd (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (a : NumberField.AdeleRing (NumberField.RingOfIntegers L) L) : (((adeleGaloisAction K L) σ) a).2 = ((finiteAdeleGaloisAction K L) σ) a.2

The finite component of the Galois action on full adeles is the Galois action on finite adeles.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleGaloisAction_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (x : L) : ((adeleGaloisAction K L) σ) ((algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) (σ x)

The Galois action extends the action on the diagonally embedded number field.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleGaloisAction_fst (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (a : NumberField.AdeleRing (NumberField.RingOfIntegers L) L) : (((adeleGaloisAction K L) σ) a).1 = ((infiniteAdeleGaloisAction K L) σ) a.1

The infinite component of the Galois action on full adeles is the Galois action on infinite adeles.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleGaloisAction_adeleExtension (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] [NumberField K] (σ : Gal(L/K)) (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : ((adeleGaloisAction K L) σ) ((NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a) = (NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a

The Galois action fixes every adele extended from the base field, not only principal adeles.

theorem TauCeti.GlobalNumberFields.continuous_adeleGaloisAction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) : Continuous ⇑((adeleGaloisAction K L) σ)

Every automorphism acts continuously on full adeles.

theorem TauCeti.GlobalNumberFields.continuous_adeleGaloisAction_uncurry (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace Gal(L/K)] [DiscreteTopology Gal(L/K)] : Continuous fun (p : Gal(L/K) × NumberField.AdeleRing (NumberField.RingOfIntegers L) L) => ((adeleGaloisAction K L) p.1) p.2

The action is jointly continuous when the automorphism group has its discrete topology, as is appropriate for a finite extension.

@[reducible]

noncomputable def TauCeti.GlobalNumberFields.adeleMulSemiringAction (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] : MulSemiringAction Gal(L/K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)

The Galois action as a semiring action, available in the AdeleGaloisAction scope. It is not a global instance, so competing actions on an adele ring remain available.

@[simp]

theorem TauCeti.GlobalNumberFields.adele_smul_def (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (a : NumberField.AdeleRing (NumberField.RingOfIntegers L) L) : σ • a = ((adeleGaloisAction K L) σ) a

The scoped Galois action is evaluation of adeleGaloisAction.

instance TauCeti.GlobalNumberFields.instContinuousSMulAlgEquivAdeleRingRingOfIntegersOfDiscreteTopology_tauCeti (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace Gal(L/K)] [DiscreteTopology Gal(L/K)] : ContinuousSMul Gal(L/K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)

With the discrete topology on field automorphisms, the scoped Galois action is continuous.