The ideles and idele classes of a separable closure of a number field

Let K be a number field with separable closure Kˢ and absolute Galois group G_K = Gal(Kˢ/K). This file builds the two discrete G_K-modules on which the global class formations are built: the ideles of Kˢ,

I_{Kˢ} = colim_E I_E,

the direct limit of the idele groups of the finite Galois subextensions E of Kˢ/K along the extension maps I_E → I_{E'} for E ≤ E', and the idele classes C_{Kˢ} = I_{Kˢ} / (Kˢ)ˣ, the quotient by the principal ideles. Both are written additively, as IdeleCoeff K and IdeleClassCoeff K, in the same way as TauCeti.UnitsCoeff K writes (Kˢ)ˣ.

An element g ∈ G_K acts on I_E through its restriction to Gal(E/K) and the Galois action TauCeti.GlobalNumberFields.adeleGaloisAction on adeles. These actions commute with the extension maps (adeleTransition_adeleGaloisAction), so they pass to the direct limit. The ideles of E are fixed by the open subgroup of G_K fixing E (smul_ideleCoeffOf_of_mem_fixingSubgroup), so both modules are discrete with open point stabilizers.

Conversely, the ideles of E embed in I_{Kˢ} (ideleCoeffOf_injective). More generally, the ideles of any finite subextension E of Kˢ/K, Galois over K or not, embed in I_{Kˢ} through the normal closure of E (ideleCoeffOfIntermediateField, ideleCoeffOfIntermediateField_coe), and they are exactly the ideles of Kˢ fixed by the subgroup G_E of G_K fixing E (mem_range_ideleCoeffOfIntermediateField_iff): (I_{Kˢ})^{G_E} = I_E. A fixed idele is defined over a finite Galois subextension M ⊇ E; every element of Gal(M/E) lifts to G_E, so it is fixed by Gal(M/E) and descends to E by Galois descent for the ideles of number fields (TauCeti.GlobalNumberFields.mem_range_ideleExtension_iff). An element of G_K that restricts to an automorphism e of E acts on these ideles by transport along e (smul_ideleCoeffOfIntermediateField).

A unit of Kˢ lies in a finite Galois subextension E, and its principal idele in I_E does not depend on the choice of E; this is the equivariant embedding principalIdele : (Kˢ)ˣ → I_{Kˢ} (principalIdele_ofMul_map_algebraMap, principalIdele_injective). The sequence

0 → (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ} → 0

is exact by principalIdele_injective, ideleClassMk_eq_zero_iff and ideleClassMk_surjective.

Main definitions

• TauCeti.ClassFieldTheory.adeleTransition, ideleTransition: the extension maps of adeles and ideles along an inclusion of finite Galois subextensions of Kˢ/K.
• TauCeti.ClassFieldTheory.IdeleCoeff K: the ideles of Kˢ, written additively.
• TauCeti.ClassFieldTheory.ideleCoeffOf E: the ideles of E as ideles of Kˢ.
• TauCeti.ClassFieldTheory.ideleCoeffOfIntermediateField K E: the ideles of a finite subextension E, not necessarily Galois over K, as ideles of Kˢ.
• TauCeti.ClassFieldTheory.IdeleCoeff.lift: the homomorphism out of the ideles of Kˢ induced by compatible homomorphisms out of the ideles of the finite Galois subextensions.
• TauCeti.ClassFieldTheory.principalIdele K: the principal ideles (Kˢ)ˣ → I_{Kˢ}.
• TauCeti.ClassFieldTheory.IdeleClassCoeff K: the idele classes of Kˢ, written additively.
• TauCeti.ClassFieldTheory.ideleClassMk K: the quotient map I_{Kˢ} → C_{Kˢ}.
• TauCeti.ClassFieldTheory.IdeleClassCoeff.lift: the homomorphism out of the idele classes of Kˢ induced by a homomorphism out of the ideles of Kˢ vanishing on the principal ideles.

Main results

• TauCeti.ClassFieldTheory.exists_ideleCoeffOf_eq: every idele of Kˢ comes from some I_E.
• TauCeti.ClassFieldTheory.smul_ideleCoeffOf: the action of G_K on the ideles of E.
• TauCeti.ClassFieldTheory.ideleCoeffOf_injective: the ideles of E embed in the ideles of Kˢ.
• TauCeti.ClassFieldTheory.ideleCoeffOf_ideleExtension: ideleCoeffOfIntermediateField may be computed through any finite Galois subextension containing E.
• TauCeti.ClassFieldTheory.ideleCoeffOfIntermediateField_ideleExtension: extending an idele from F to a larger finite subextension E does not change it as an idele of Kˢ.
• TauCeti.ClassFieldTheory.smul_ideleCoeffOfIntermediateField: the action of G_K on the ideles of a finite subextension, through the automorphisms of E it restricts to.
• TauCeti.ClassFieldTheory.mem_range_ideleCoeffOfIntermediateField_iff: Galois descent, an idele of Kˢ is an idele of the finite subextension E exactly when it is fixed by the subgroup of G_K fixing E.
• TauCeti.ClassFieldTheory.principalIdele_injective: the principal ideles embed (Kˢ)ˣ.

Implementation notes

The direct limit is indexed by FiniteGaloisIntermediateField K (SeparableClosure K), the finite Galois subextensions. Each of them is stable under G_K, so G_K acts on every level separately and on the direct limit through Mathlib's DirectLimit instances; indexing by all finite subextensions would instead move I_E to I_{g E}. Both the transition maps and the level actions are continuous ring homomorphisms of adele rings, and identities between their composites are proved by NumberField.AdeleRing.ringHom_ext, from their values on the diagonal field and on the idempotent (1, 0).

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1 and §2.

The transition maps

noncomputable def TauCeti.ClassFieldTheory.adeleTransition {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') : NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField →+* NumberField.AdeleRing (NumberField.RingOfIntegers ↥E'.toIntermediateField) ↥E'.toIntermediateField

The extension map of adele rings 𝔸_E → 𝔸_{E'} along an inclusion E ≤ E' of finite Galois subextensions of Kˢ/K.

theorem TauCeti.ClassFieldTheory.adeleTransition_apply {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (a : NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : (adeleTransition h) a = (NumberField.adeleExtension (NumberField.RingOfIntegers ↥E.toIntermediateField) (↥E.toIntermediateField) (NumberField.RingOfIntegers ↥E'.toIntermediateField) ↥E'.toIntermediateField) a

The extension map of adele rings along E ≤ E' is the extension map of adeles along the inclusion E → E'.

theorem TauCeti.ClassFieldTheory.continuous_adeleTransition {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') : Continuous ⇑(adeleTransition h)

The extension map of adele rings is continuous.

@[simp]

theorem TauCeti.ClassFieldTheory.adeleTransition_algebraMap {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (x : ↥E.toIntermediateField) : (adeleTransition h) ((algebraMap (↥E.toIntermediateField) (NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField)) x) = (algebraMap (↥E'.toIntermediateField) (NumberField.AdeleRing (NumberField.RingOfIntegers ↥E'.toIntermediateField) ↥E'.toIntermediateField)) ((IntermediateField.inclusion h) x)

The extension map of adele rings extends the inclusion E ≤ E' on the diagonal fields.

theorem TauCeti.ClassFieldTheory.adeleTransition_fst {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (a : NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : ((adeleTransition h) a).1 = (NumberField.infiniteAdeleExtension ↥E.toIntermediateField ↥E'.toIntermediateField) a.1

The infinite component of the extension of an adele is the extension of its infinite component.

theorem TauCeti.ClassFieldTheory.adeleTransition_snd {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (a : NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : ((adeleTransition h) a).2 = (IsDedekindDomain.finiteAdeleExtension (NumberField.RingOfIntegers ↥E.toIntermediateField) (↥E.toIntermediateField) (NumberField.RingOfIntegers ↥E'.toIntermediateField) ↥E'.toIntermediateField) a.2

The finite component of the extension of an adele is the extension of its finite component.

@[simp]

theorem TauCeti.ClassFieldTheory.adeleTransition_self {K : Type u_1} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) : adeleTransition ⋯ = RingHom.id (NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField)

The extension map along E ≤ E is the identity.

@[simp]

theorem TauCeti.ClassFieldTheory.adeleTransition_comp {K : Type u_1} [Field K] [NumberField K] {E E' E'' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (h' : E' ≤ E'') : (adeleTransition h').comp (adeleTransition h) = adeleTransition ⋯

The extension maps compose along a tower E ≤ E' ≤ E''.

theorem TauCeti.ClassFieldTheory.adeleTransition_adeleGaloisAction {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (g : AbsoluteGaloisGroup K) (a : NumberField.AdeleRing (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : (adeleTransition h) (((GlobalNumberFields.adeleGaloisAction K ↥E.toIntermediateField) (AlgEquiv.restrictNormal g ↥E.toIntermediateField)) a) = ((GlobalNumberFields.adeleGaloisAction K ↥E'.toIntermediateField) (AlgEquiv.restrictNormal g ↥E'.toIntermediateField)) ((adeleTransition h) a)

The extension maps are Galois equivariant: for g ∈ G_K, extending from E to E' and then acting by the restriction of g to E' is acting by the restriction of g to E and then extending.

@[reducible, inline]

noncomputable abbrev TauCeti.ClassFieldTheory.ideleGroupMulDistribMulAction (K : Type u_1) [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) : MulDistribMulAction (AbsoluteGaloisGroup K) (NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField)

The action of G_K on the ideles of a finite Galois subextension E, through the restriction G_K → Gal(E/K) and the Galois action on adeles. It is a definition rather than an instance, so that it does not compete with other actions on idele groups; it is the action for which the transition maps of ideles are equivariant. See note [reducible non-instances].

theorem TauCeti.ClassFieldTheory.coe_ideleGroupMulDistribMulAction_smul {K : Type u_1} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) (g : AbsoluteGaloisGroup K) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : ↑(g • a) = ((GlobalNumberFields.adeleGaloisAction K ↥E.toIntermediateField) (AlgEquiv.restrictNormal g ↥E.toIntermediateField)) ↑a

In ideleGroupMulDistribMulAction, g ∈ G_K acts on the underlying adele of an idele of E by the Galois action of its restriction to Gal(E/K).

noncomputable def TauCeti.ClassFieldTheory.ideleTransition (K : Type u_1) [Field K] [NumberField K] (E E' : FiniteGaloisIntermediateField K (SeparableClosure K)) (h : E ≤ E') : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField →*[AbsoluteGaloisGroup K] NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E'.toIntermediateField) ↥E'.toIntermediateField

The extension map of ideles I_E → I_{E'} along an inclusion E ≤ E' of finite Galois subextensions, as a G_K-equivariant homomorphism. These are the transition maps of the direct system whose limit is IdeleCoeff K.

@[simp]

theorem TauCeti.ClassFieldTheory.coe_ideleTransition {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : ↑((ideleTransition K E E' h) a) = (adeleTransition h) ↑a

The underlying adele of the extension of an idele is the extension of its underlying adele.

theorem TauCeti.ClassFieldTheory.ideleTransition_unitEmbedding {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (u : (↥E.toIntermediateField)ˣ) : (ideleTransition K E E' h) ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) u) = (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers ↥E'.toIntermediateField) ↥E'.toIntermediateField) ((Units.map ↑(IntermediateField.inclusion h)) u)

The extension of a principal idele is the principal idele of the same field element.

instance TauCeti.ClassFieldTheory.instDirectedSystemFiniteGaloisIntermediateFieldSeparableClosureIdeleGroupRingOfIntegersSubtypeMemIntermediateFieldCoeMulDistribMulActionHomAbsoluteGaloisGroupIdIdeleTransition {K : Type u_1} [Field K] [NumberField K] : DirectedSystem (fun (E : FiniteGaloisIntermediateField K (SeparableClosure K)) => NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) fun (x1 x2 : FiniteGaloisIntermediateField K (SeparableClosure K)) (x3 : x1 ≤ x2) => ⇑(ideleTransition K x1 x2 x3)

The idele groups of the finite Galois subextensions of Kˢ/K form a directed system along the extension maps.

The ideles of the separable closure

def TauCeti.ClassFieldTheory.IdeleCoeff (K : Type u_1) [Field K] [NumberField K] : Type u_1

The ideles of Kˢ, written additively: the direct limit of the idele groups of the finite Galois subextensions of Kˢ/K along the extension maps. Its elements are read through ideleCoeffOf (exists_ideleCoeffOf_eq).

@[instance_reducible]

noncomputable instance TauCeti.ClassFieldTheory.instAddCommGroupIdeleCoeff {K : Type u_1} [Field K] [NumberField K] : AddCommGroup (IdeleCoeff K)

@[instance_reducible]

noncomputable instance TauCeti.ClassFieldTheory.instDistribMulActionAbsoluteGaloisGroupIdeleCoeff {K : Type u_1} [Field K] [NumberField K] : DistribMulAction (AbsoluteGaloisGroup K) (IdeleCoeff K)

@[instance_reducible]

instance TauCeti.ClassFieldTheory.instTopologicalSpaceIdeleCoeff {K : Type u_1} [Field K] [NumberField K] : TopologicalSpace (IdeleCoeff K)

instance TauCeti.ClassFieldTheory.instDiscreteTopologyIdeleCoeff {K : Type u_1} [Field K] [NumberField K] : DiscreteTopology (IdeleCoeff K)

noncomputable def TauCeti.ClassFieldTheory.ideleCoeffOf (K : Type u_1) [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) : Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) →+ IdeleCoeff K

The ideles of a finite Galois subextension E as ideles of Kˢ, written additively.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleCoeffOf_ideleTransition {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : (ideleCoeffOf K E') (Additive.ofMul ((ideleTransition K E E' h) a)) = (ideleCoeffOf K E) (Additive.ofMul a)

An idele of E and its extension to E' are the same idele of Kˢ.

theorem TauCeti.ClassFieldTheory.exists_ideleCoeffOf_eq {K : Type u_1} [Field K] [NumberField K] (x : IdeleCoeff K) : ∃ (E : FiniteGaloisIntermediateField K (SeparableClosure K)) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField), (ideleCoeffOf K E) (Additive.ofMul a) = x

Every idele of Kˢ is an idele of a finite Galois subextension.

theorem TauCeti.ClassFieldTheory.ideleCoeffOf_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {E : FiniteGaloisIntermediateField K (SeparableClosure K)} {a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField} : (ideleCoeffOf K E) (Additive.ofMul a) = 0 ↔ ∃ (E' : FiniteGaloisIntermediateField K (SeparableClosure K)) (h : E ≤ E'), (ideleTransition K E E' h) a = 1

An idele of E vanishes in the ideles of Kˢ exactly when its extension to some larger finite Galois subextension is trivial.

theorem TauCeti.ClassFieldTheory.IdeleCoeff.hom_ext {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddMonoid M] {φ ψ : IdeleCoeff K →+ M} (h : ∀ (E : FiniteGaloisIntermediateField K (SeparableClosure K)), φ.comp (ideleCoeffOf K E) = ψ.comp (ideleCoeffOf K E)) : φ = ψ

Two homomorphisms out of the ideles of Kˢ agree once they agree on the ideles of every finite Galois subextension.

theorem TauCeti.ClassFieldTheory.IdeleCoeff.hom_ext_iff {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddMonoid M] {φ ψ : IdeleCoeff K →+ M} : φ = ψ ↔ ∀ (E : FiniteGaloisIntermediateField K (SeparableClosure K)), φ.comp (ideleCoeffOf K E) = ψ.comp (ideleCoeffOf K E)

noncomputable def TauCeti.ClassFieldTheory.IdeleCoeff.lift (K : Type u_1) [Field K] [NumberField K] {M : Type u_2} [AddCommMonoid M] (φ : (E : FiniteGaloisIntermediateField K (SeparableClosure K)) → Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) →+ M) (hφ : ∀ (E E' : FiniteGaloisIntermediateField K (SeparableClosure K)) (h : E ≤ E') (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField), (φ E') (Additive.ofMul ((ideleTransition K E E' h) a)) = (φ E) (Additive.ofMul a)) : IdeleCoeff K →+ M

The universal property of the ideles of Kˢ: homomorphisms out of the ideles of the finite Galois subextensions of Kˢ/K that are compatible with the extension maps induce a homomorphism out of the ideles of Kˢ (IdeleCoeff.lift_ideleCoeffOf).

@[simp]

theorem TauCeti.ClassFieldTheory.IdeleCoeff.lift_ideleCoeffOf {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddCommMonoid M] (φ : (E : FiniteGaloisIntermediateField K (SeparableClosure K)) → Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) →+ M) (hφ : ∀ (E E' : FiniteGaloisIntermediateField K (SeparableClosure K)) (h : E ≤ E') (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField), (φ E') (Additive.ofMul ((ideleTransition K E E' h) a)) = (φ E) (Additive.ofMul a)) (E : FiniteGaloisIntermediateField K (SeparableClosure K)) (a : Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField)) : (lift K φ hφ) ((ideleCoeffOf K E) a) = (φ E) a

The homomorphism induced by compatible homomorphisms out of the ideles of the finite Galois subextensions restricts to each of them on the ideles of that subextension.

@[simp]

theorem TauCeti.ClassFieldTheory.smul_ideleCoeffOf {K : Type u_1} [Field K] [NumberField K] (g : AbsoluteGaloisGroup K) (E : FiniteGaloisIntermediateField K (SeparableClosure K)) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : g • (ideleCoeffOf K E) (Additive.ofMul a) = (ideleCoeffOf K E) (Additive.ofMul ((Units.map ↑((GlobalNumberFields.adeleGaloisAction K ↥E.toIntermediateField) (AlgEquiv.restrictNormal g ↥E.toIntermediateField))) a))

The Galois action on the ideles of Kˢ: g ∈ G_K acts on the ideles of E through its restriction to Gal(E/K).

theorem TauCeti.ClassFieldTheory.smul_ideleCoeffOf_of_mem_fixingSubgroup {K : Type u_1} [Field K] [NumberField K] {g : AbsoluteGaloisGroup K} {E : FiniteGaloisIntermediateField K (SeparableClosure K)} (hg : g ∈ E.fixingSubgroup) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E.toIntermediateField) ↥E.toIntermediateField) : g • (ideleCoeffOf K E) (Additive.ofMul a) = (ideleCoeffOf K E) (Additive.ofMul a)

The subgroup of G_K fixing E fixes the ideles of E.

instance TauCeti.ClassFieldTheory.instContinuousSMulAbsoluteGaloisGroupIdeleCoeff {K : Type u_1} [Field K] [NumberField K] : ContinuousSMul (AbsoluteGaloisGroup K) (IdeleCoeff K)

The ideles of Kˢ are a discrete G_K-module: the stabilizer of an idele of E contains the open subgroup fixing E.

Galois descent for the ideles of Kˢ

theorem TauCeti.ClassFieldTheory.ideleTransition_injective {K : Type u_1} [Field K] [NumberField K] {E E' : FiniteGaloisIntermediateField K (SeparableClosure K)} (h : E ≤ E') : Function.Injective ⇑(ideleTransition K E E' h)

The extension map of ideles along an inclusion of finite Galois subextensions of Kˢ/K is injective.

theorem TauCeti.ClassFieldTheory.ideleCoeffOf_injective {K : Type u_1} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) : Function.Injective ⇑(ideleCoeffOf K E)

The ideles of a finite Galois subextension E embed in the ideles of Kˢ.

The ideles of a finite subextension

noncomputable def TauCeti.ClassFieldTheory.ideleCoeffOfIntermediateField (K : Type u_1) [Field K] [NumberField K] (E : IntermediateField K (SeparableClosure K)) [NumberField ↥E] : Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E) ↥E) →+ IdeleCoeff K

The ideles of a finite subextension E of Kˢ/K as ideles of Kˢ: an idele of E is extended to the normal closure of E and read in the ideles of Kˢ. It may be computed through any finite Galois subextension containing E (ideleCoeffOf_ideleExtension), it is ideleCoeffOf K E when E is itself Galois over K (ideleCoeffOfIntermediateField_coe), and its image is the set of ideles of Kˢ fixed by the subgroup of G_K fixing E (mem_range_ideleCoeffOfIntermediateField_iff).

theorem TauCeti.ClassFieldTheory.ideleCoeffOf_ideleExtension {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] (M : FiniteGaloisIntermediateField K (SeparableClosure K)) (h : E ≤ M.toIntermediateField) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E) ↥E) : (ideleCoeffOf K M) (Additive.ofMul ((GlobalNumberFields.ideleExtension ↥E ↥M.toIntermediateField) a)) = (ideleCoeffOfIntermediateField K E) (Additive.ofMul a)

ideleCoeffOfIntermediateField through any finite Galois subextension: for E ≤ M, the extension to M of an idele of E is, as an idele of Kˢ, the idele of E itself.

theorem TauCeti.ClassFieldTheory.ideleCoeffOfIntermediateField_ideleExtension {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] {F : IntermediateField K (SeparableClosure K)} [NumberField ↥F] [Algebra ↥F ↥E] [IsScalarTower (↥F) (↥E) (SeparableClosure K)] (b : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥F) ↥F) : (ideleCoeffOfIntermediateField K E) (Additive.ofMul ((GlobalNumberFields.ideleExtension ↥F ↥E) b)) = (ideleCoeffOfIntermediateField K F) (Additive.ofMul b)

ideleCoeffOfIntermediateField is compatible with extension of ideles: if F and E are finite subextensions of Kˢ/K with E an algebra over F compatibly with Kˢ, then the extension to E of an idele of F is, as an idele of Kˢ, the idele of F itself.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleCoeffOfIntermediateField_coe {K : Type u_1} [Field K] [NumberField K] (E : FiniteGaloisIntermediateField K (SeparableClosure K)) : ideleCoeffOfIntermediateField K E.toIntermediateField = ideleCoeffOf K E

For a finite Galois subextension E, ideleCoeffOfIntermediateField is ideleCoeffOf.

theorem TauCeti.ClassFieldTheory.ideleCoeffOfIntermediateField_injective {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] : Function.Injective ⇑(ideleCoeffOfIntermediateField K E)

The ideles of a finite subextension E embed in the ideles of Kˢ.

theorem TauCeti.ClassFieldTheory.smul_ideleCoeffOfIntermediateField {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] (g : AbsoluteGaloisGroup K) (e : ↥E ≃+* ↥E) (he : ∀ (x : ↥E), ↑(e x) = g ↑x) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E) ↥E) : g • (ideleCoeffOfIntermediateField K E) (Additive.ofMul a) = (ideleCoeffOfIntermediateField K E) (Additive.ofMul ((Units.map (GlobalNumberFields.adeleEquiv (↥E) (↥E) e).toMonoidHom) a))

The Galois action on the ideles of a finite subextension E: if g ∈ G_K restricts on E to the automorphism e of E, then g acts on the ideles of E, read in the ideles of Kˢ, by transport of adeles along e.

theorem TauCeti.ClassFieldTheory.smul_ideleCoeffOfIntermediateField_of_normal {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] [Normal K ↥E] (g : AbsoluteGaloisGroup K) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E) ↥E) : g • (ideleCoeffOfIntermediateField K E) (Additive.ofMul a) = (ideleCoeffOfIntermediateField K E) (Additive.ofMul ((Units.map ↑((GlobalNumberFields.adeleGaloisAction K ↥E) (AlgEquiv.restrictNormal g ↥E))) a))

The Galois action on the ideles of a normal finite subextension E: g ∈ G_K acts on the ideles of E, read in the ideles of Kˢ, through its restriction to Gal(E/K).

theorem TauCeti.ClassFieldTheory.smul_ideleCoeffOfIntermediateField_of_mem_fixingSubgroup {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] {g : AbsoluteGaloisGroup K} (hg : g ∈ E.fixingSubgroup) (a : NumberField.IdeleGroup (NumberField.RingOfIntegers ↥E) ↥E) : g • (ideleCoeffOfIntermediateField K E) (Additive.ofMul a) = (ideleCoeffOfIntermediateField K E) (Additive.ofMul a)

The subgroup of G_K fixing a finite subextension E fixes the ideles of E.

theorem TauCeti.ClassFieldTheory.mem_range_ideleCoeffOfIntermediateField_iff {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] {x : IdeleCoeff K} : x ∈ (ideleCoeffOfIntermediateField K E).range ↔ ∀ g ∈ E.fixingSubgroup, g • x = x

Galois descent for the ideles of Kˢ: an idele of Kˢ is an idele of the finite subextension E exactly when it is fixed by the subgroup of G_K fixing E.

The principal ideles

noncomputable def TauCeti.ClassFieldTheory.principalIdele (K : Type u_1) [Field K] [NumberField K] : UnitsCoeff K →+[AbsoluteGaloisGroup K] IdeleCoeff K

The principal ideles of Kˢ: a unit x of Kˢ lies in a finite Galois subextension E and is sent to its principal idele in the ideles of E, independently of E (principalIdele_ofMul_map_algebraMap). This is the G_K-equivariant embedding (Kˢ)ˣ → I_{Kˢ} (principalIdele_injective).

theorem TauCeti.ClassFieldTheory.principalIdele_ofMul_map_algebraMap {K : Type u_1} [Field K] [NumberField K] {E : IntermediateField K (SeparableClosure K)} [NumberField ↥E] (u : (↥E)ˣ) : (principalIdele K) (Additive.ofMul ((Units.map ↑(algebraMap (↥E) (SeparableClosure K))) u)) = (ideleCoeffOfIntermediateField K E) (Additive.ofMul ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers ↥E) ↥E) u))

The principal idele of a unit of a finite subextension E is its principal idele in the ideles of E.

theorem TauCeti.ClassFieldTheory.principalIdele_injective {K : Type u_1} [Field K] [NumberField K] : Function.Injective ⇑(principalIdele K)

The principal ideles embed (Kˢ)ˣ in the ideles of Kˢ: a field element is a unit of some adele ring only through its diagonal image, which is injective.

theorem TauCeti.ClassFieldTheory.smul_mem_range_principalIdele {K : Type u_1} [Field K] [NumberField K] (g : AbsoluteGaloisGroup K) (x : IdeleCoeff K) (hx : x ∈ (principalIdele K).toAddMonoidHom.range) : g • x ∈ (principalIdele K).toAddMonoidHom.range

The principal ideles form a G_K-stable subgroup of the ideles of Kˢ.

The idele classes of the separable closure

def TauCeti.ClassFieldTheory.IdeleClassCoeff (K : Type u_1) [Field K] [NumberField K] : Type u_1

The idele classes of Kˢ, written additively: the ideles of Kˢ modulo the principal ideles. Its elements are read through ideleClassMk (ideleClassMk_surjective).

@[instance_reducible]

noncomputable instance TauCeti.ClassFieldTheory.instAddCommGroupIdeleClassCoeff {K : Type u_1} [Field K] [NumberField K] : AddCommGroup (IdeleClassCoeff K)

@[instance_reducible]

noncomputable instance TauCeti.ClassFieldTheory.instDistribMulActionAbsoluteGaloisGroupIdeleClassCoeff {K : Type u_1} [Field K] [NumberField K] : DistribMulAction (AbsoluteGaloisGroup K) (IdeleClassCoeff K)

@[instance_reducible]

instance TauCeti.ClassFieldTheory.instTopologicalSpaceIdeleClassCoeff {K : Type u_1} [Field K] [NumberField K] : TopologicalSpace (IdeleClassCoeff K)

instance TauCeti.ClassFieldTheory.instDiscreteTopologyIdeleClassCoeff {K : Type u_1} [Field K] [NumberField K] : DiscreteTopology (IdeleClassCoeff K)

noncomputable def TauCeti.ClassFieldTheory.ideleClassMk (K : Type u_1) [Field K] [NumberField K] : IdeleCoeff K →+[AbsoluteGaloisGroup K] IdeleClassCoeff K

The G_K-equivariant quotient map from the ideles of Kˢ to its idele classes.

theorem TauCeti.ClassFieldTheory.ideleClassMk_surjective {K : Type u_1} [Field K] [NumberField K] : Function.Surjective ⇑(ideleClassMk K)

Every idele class of Kˢ is the class of an idele.

theorem TauCeti.ClassFieldTheory.ideleClassMk_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : IdeleCoeff K} : (ideleClassMk K) x = 0 ↔ ∃ (y : UnitsCoeff K), (principalIdele K) y = x

The kernel of the quotient map is the principal ideles.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleClassMk_principalIdele {K : Type u_1} [Field K] [NumberField K] (y : UnitsCoeff K) : (ideleClassMk K) ((principalIdele K) y) = 0

The class of a principal idele vanishes.

noncomputable def TauCeti.ClassFieldTheory.IdeleClassCoeff.lift (K : Type u_1) [Field K] [NumberField K] {M : Type u_2} [AddCommGroup M] (φ : IdeleCoeff K →+ M) (hφ : ∀ (y : UnitsCoeff K), φ ((principalIdele K) y) = 0) : IdeleClassCoeff K →+ M

The universal property of the idele classes of Kˢ: a homomorphism out of the ideles of Kˢ vanishing on the principal ideles induces a homomorphism out of the idele classes (IdeleClassCoeff.lift_ideleClassMk).

@[simp]

theorem TauCeti.ClassFieldTheory.IdeleClassCoeff.lift_ideleClassMk {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddCommGroup M] (φ : IdeleCoeff K →+ M) (hφ : ∀ (y : UnitsCoeff K), φ ((principalIdele K) y) = 0) (x : IdeleCoeff K) : (lift K φ hφ) ((ideleClassMk K) x) = φ x

The homomorphism induced on the idele classes of Kˢ sends the class of an idele to the value of the original homomorphism on it.

theorem TauCeti.ClassFieldTheory.IdeleClassCoeff.hom_ext {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddMonoid M] {φ ψ : IdeleClassCoeff K →+ M} (h : φ.comp (ideleClassMk K).toAddMonoidHom = ψ.comp (ideleClassMk K).toAddMonoidHom) : φ = ψ

Two homomorphisms out of the idele classes of Kˢ agree once they agree on the classes of ideles.

theorem TauCeti.ClassFieldTheory.IdeleClassCoeff.hom_ext_iff {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddMonoid M] {φ ψ : IdeleClassCoeff K →+ M} : φ = ψ ↔ φ.comp (ideleClassMk K).toAddMonoidHom = ψ.comp (ideleClassMk K).toAddMonoidHom

instance TauCeti.ClassFieldTheory.instContinuousSMulAbsoluteGaloisGroupIdeleClassCoeff {K : Type u_1} [Field K] [NumberField K] : ContinuousSMul (AbsoluteGaloisGroup K) (IdeleClassCoeff K)

The idele classes of Kˢ are a discrete G_K-module: the stabilizer of the class of an idele contains the stabilizer of the idele.