The local invariants of an idele layer and their sum

Let K be a number field and L/F a finite Galois layer inside Kˢ, cut out by open subgroups V ◁ U of G_K. This file attaches to every class x ∈ H²(Gal(L/F), I_L) of the idele formation ideleFormation K a local invariant at every place of K, and their sum. The class is carried to the continuous cohomology of G_K by inflation to U = G_F and corestriction to G_K,

ideleLayerCorInfl K L : H²(Gal(L/F), I_L) → H²(G_F, I_{Kˢ}) → H²(G_K, I_{Kˢ}),

and there it is localized at the places of K (ideleBrLocalization, ideleInfiniteBrLocalization) and evaluated by the local invariants invMap and infiniteInvMap:

• ideleLocalInvAt K L v x ∈ ℚ/ℤ at a finite place v, nonzero only at the finitely many places of ideleSupport K L x;
• ideleInfiniteInvAt K L w x ∈ ℚ/ℤ at an infinite place w;
• ideleSumLocalInv K L x, the sum of all of them: the sum of the local invariants sumLocalInv K of the family ideleLocalization K (ideleLayerCorInfl K L x) of local Brauer classes, computed over any finite set of finite places containing ideleSupport K L x (ideleSumLocalInv_eq_sum).

Inflation to a refinement L'/F of the layer does not change the class over G_K (ideleLayerCorInfl_cohomologyInfl), so all of these are inflation-invariant (ideleSumLocalInv_infl). Corestriction is what makes the invariants of a layer over F those of places of K: classically, the invariant at v of a corestricted class is the sum of the invariants at the places of F above v, so ideleSumLocalInv K L is the sum of the local invariants over all places of F.

The sum of the local invariants behaves under the operations on layers as the invariant of a class formation must. Restriction to an intermediate ground field E multiplies the class over G_K by [E : F] (ideleLayerCorInfl_cohomologyRes), because corestriction from G_E to G_K factors through G_F and corestriction after restriction is multiplication by the index; hence Σ inv (res x) = [E : F] • Σ inv x (ideleSumLocalInv_res). Conjugation by g ∈ G_K does not change the class over G_K (ideleLayerCorInfl_conjugateCohomologyIso), so it preserves every local invariant and their sum (ideleSumLocalInv_conj).

Main definitions

• TauCeti.ClassFieldTheory.ideleLayerCorInfl K L: the class over G_K of an idele-layer class.
• TauCeti.ClassFieldTheory.ideleLocalInvAt K L v, TauCeti.ClassFieldTheory.ideleInfiniteInvAt K L w: the local invariants of an idele-layer class at a finite place v and an infinite place w.
• TauCeti.ClassFieldTheory.ideleSupport K L x: the finite set of finite places where the local invariant of x is nonzero.
• TauCeti.ClassFieldTheory.ideleSumLocalInv K L: the sum of the local invariants.

Main results

• TauCeti.ClassFieldTheory.ideleLayerCorInfl_cohomologyInfl: inflation to a refinement does not change the class over G_K.
• TauCeti.ClassFieldTheory.ideleSumLocalInv_eq_sum: the sum of the local invariants is a finite sum over any set of finite places containing the support, plus the archimedean invariants.
• TauCeti.ClassFieldTheory.ideleSumLocalInv_infl: the sum of the local invariants is inflation-invariant.
• TauCeti.ClassFieldTheory.ideleLayerCorInfl_cohomologyRes, TauCeti.ClassFieldTheory.ideleSumLocalInv_res: restriction to an intermediate ground field multiplies the class over G_K, and so the sum of the local invariants, by the relative degree.
• TauCeti.ClassFieldTheory.ideleLayerCorInfl_conjugateCohomologyIso, TauCeti.ClassFieldTheory.ideleSumLocalInv_conj: conjugation preserves the class over G_K, and so the sum of the local invariants.

References

• J. S. Milne, Class Field Theory, Chapter VII, §2 and Chapter VIII, §4.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII (Tate, Global Class Field Theory), §11.

The class over the absolute Galois group

noncomputable def TauCeti.ClassFieldTheory.ideleLayerCorInfl (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ↑(L.H (ideleFormation K) 2) →+ ContCohomology.H2 (AbsoluteGaloisGroup K) (IdeleCoeff K)

The class over G_K of an idele-layer class: for a layer V ◁ U of the idele formation, inflation H²(U ⧸ V, I_{Kˢ}^V) → H²(U, I_{Kˢ}) followed by corestriction from the open subgroup U to G_K.

theorem TauCeti.ClassFieldTheory.ideleLayerCorInfl_apply (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (ideleFormation K) 2)) : (ideleLayerCorInfl K L) x = (ContCohomology.explicitCor2 (AbsoluteGaloisGroup K) (IdeleCoeff K) ↑L.ground ⋯) ((L.explicitInfl2 (ideleCoeffEquivIdeleFormation K) ⋯) x)

The class over G_K of an idele-layer class is the corestriction of its inflation.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLayerCorInfl_cohomologyInfl (K : Type) [Field K] [NumberField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (x : ↑(old.H (ideleFormation K) 2)) : (ideleLayerCorInfl K new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (ideleFormation K) 2)) x) = (ideleLayerCorInfl K old) x

Inflation to a refinement does not change the class over G_K. Both layers have the same ground subgroup U, and corestriction from U does not see the identification of the two copies of U.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLayerCorInfl_cohomologyRes (K : Type) [Field K] [NumberField K] {small big : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRestriction small big) (x : ↑(big.H (ideleFormation K) 2)) : (ideleLayerCorInfl K small) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes (ideleFormation K) 2)) x) = T.relativeDegree • (ideleLayerCorInfl K big) x

Restriction multiplies the class over G_K by the relative degree: for a restriction of a layer L/F to an intermediate ground field E, the class over G_K of the restricted class is [E : F] times the class over G_K of the original one.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLayerCorInfl_conjugateCohomologyIso (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (x : ↑(L.H (ideleFormation K) 2)) : (ideleLayerCorInfl K (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (ideleFormation K) g 2).hom) x) = (ideleLayerCorInfl K L) x

Conjugation does not change the class over G_K: for g : G_K, the conjugate class in the conjugate layer gL/gF has the same class over G_K.

The local invariants

noncomputable def TauCeti.ClassFieldTheory.ideleLocalInvAt (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ↑(L.H (ideleFormation K) 2) →+ AddCircle 1

The local invariant at a finite place v of an idele-layer class: the invariant of the nonarchimedean local field K_v of the localization at v of its class over G_K.

theorem TauCeti.ClassFieldTheory.ideleLocalInvAt_apply (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : ↑(L.H (ideleFormation K) 2)) : (ideleLocalInvAt K L v) x = (invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((ideleBrLocalization v) ((ideleLayerCorInfl K L) x))

The local invariant at a finite place is the invariant of the localization of the class over G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLocalInvAt_eq_zero_iff (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : ↑(L.H (ideleFormation K) 2)) : (ideleLocalInvAt K L v) x = 0 ↔ (ideleBrLocalization v) ((ideleLayerCorInfl K L) x) = 0

The local invariant at a finite place vanishes exactly when the localization does.

noncomputable def TauCeti.ClassFieldTheory.ideleInfiniteInvAt (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (w : NumberField.InfinitePlace K) : ↑(L.H (ideleFormation K) 2) →+ AddCircle 1

The local invariant at an infinite place w of an idele-layer class: the archimedean invariant of the localization at w of its class over G_K.

theorem TauCeti.ClassFieldTheory.ideleInfiniteInvAt_apply (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (w : NumberField.InfinitePlace K) (x : ↑(L.H (ideleFormation K) 2)) : (ideleInfiniteInvAt K L w) x = (infiniteInvMap w) ((ideleInfiniteBrLocalization w) ((ideleLayerCorInfl K L) x))

The local invariant at an infinite place is the archimedean invariant of the localization of the class over G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleInfiniteInvAt_eq_zero_iff (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (w : NumberField.InfinitePlace K) (x : ↑(L.H (ideleFormation K) 2)) : (ideleInfiniteInvAt K L w) x = 0 ↔ (ideleInfiniteBrLocalization w) ((ideleLayerCorInfl K L) x) = 0

The local invariant at an infinite place vanishes exactly when the localization does.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLocalInvAt_infl (K : Type) [Field K] [NumberField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : ↑(old.H (ideleFormation K) 2)) : (ideleLocalInvAt K new v) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (ideleFormation K) 2)) x) = (ideleLocalInvAt K old v) x

Inflation preserves the local invariants at the finite places.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleInfiniteInvAt_infl (K : Type) [Field K] [NumberField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (w : NumberField.InfinitePlace K) (x : ↑(old.H (ideleFormation K) 2)) : (ideleInfiniteInvAt K new w) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (ideleFormation K) 2)) x) = (ideleInfiniteInvAt K old w) x

Inflation preserves the local invariants at the infinite places.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLocalInvAt_res (K : Type) [Field K] [NumberField K] {small big : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRestriction small big) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : ↑(big.H (ideleFormation K) 2)) : (ideleLocalInvAt K small v) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes (ideleFormation K) 2)) x) = T.relativeDegree • (ideleLocalInvAt K big v) x

Restriction multiplies the local invariants at the finite places by the relative degree.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleInfiniteInvAt_res (K : Type) [Field K] [NumberField K] {small big : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRestriction small big) (w : NumberField.InfinitePlace K) (x : ↑(big.H (ideleFormation K) 2)) : (ideleInfiniteInvAt K small w) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes (ideleFormation K) 2)) x) = T.relativeDegree • (ideleInfiniteInvAt K big w) x

Restriction multiplies the local invariants at the infinite places by the relative degree.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleLocalInvAt_conj (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : ↑(L.H (ideleFormation K) 2)) : (ideleLocalInvAt K (L.conjugate g) v) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (ideleFormation K) g 2).hom) x) = (ideleLocalInvAt K L v) x

Conjugation preserves the local invariants at the finite places.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleInfiniteInvAt_conj (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (w : NumberField.InfinitePlace K) (x : ↑(L.H (ideleFormation K) 2)) : (ideleInfiniteInvAt K (L.conjugate g) w) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (ideleFormation K) g 2).hom) x) = (ideleInfiniteInvAt K L w) x

Conjugation preserves the local invariants at the infinite places.

Finite support

theorem TauCeti.ClassFieldTheory.hasFiniteSupport_ideleLocalInvAt (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (ideleFormation K) 2)) : Function.HasFiniteSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (ideleLocalInvAt K L v) x

An idele-layer class is unramified almost everywhere: its local invariant vanishes at all but finitely many finite places.

noncomputable def TauCeti.ClassFieldTheory.ideleSupport (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (ideleFormation K) 2)) : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The ramification set of an idele-layer class: the finite set of the finite places where its local invariant is nonzero: the support of the finite-place part of the localization ideleLocalization K of its class over G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_ideleSupport (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) {x : ↑(L.H (ideleFormation K) 2)} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} : v ∈ ideleSupport K L x ↔ (ideleLocalInvAt K L v) x ≠ 0

A finite place lies in the ramification set of x exactly when the local invariant of x there is nonzero.

theorem TauCeti.ClassFieldTheory.ideleLocalInvAt_eq_zero_of_notMem_ideleSupport (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) {x : ↑(L.H (ideleFormation K) 2)} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v ∉ ideleSupport K L x) : (ideleLocalInvAt K L v) x = 0

Outside its ramification set, the local invariant of an idele-layer class vanishes.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleSupport_infl (K : Type) [Field K] [NumberField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (x : ↑(old.H (ideleFormation K) 2)) : ideleSupport K new ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (ideleFormation K) 2)) x) = ideleSupport K old x

Inflation preserves the ramification set.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleSupport_conj (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (x : ↑(L.H (ideleFormation K) 2)) : ideleSupport K (L.conjugate g) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (ideleFormation K) g 2).hom) x) = ideleSupport K L x

Conjugation preserves the ramification set.

The sum of the local invariants

noncomputable def TauCeti.ClassFieldTheory.ideleSumLocalInv (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ↑(L.H (ideleFormation K) 2) →+ AddCircle 1

The sum of the local invariants of an idele-layer class: the sum sumLocalInv K of the local invariants of the family ideleLocalization K of local Brauer classes of its class over G_K. It is the sum of the invariants ideleLocalInvAt at the finitely many finite places of ideleSupport and of the invariants ideleInfiniteInvAt at the infinite places (ideleSumLocalInv_eq_sum).

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_apply (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (ideleFormation K) 2)) : (ideleSumLocalInv K L) x = (sumLocalInv K) ((ideleLocalization K) ((ideleLayerCorInfl K L) x))

The sum of the local invariants is sumLocalInv K of the localizations of the class over G_K.

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_eq_sum (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (ideleFormation K) 2)) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : ideleSupport K L x ⊆ S) : (ideleSumLocalInv K L) x = ∑ v ∈ S, (ideleLocalInvAt K L v) x + ∑ w : NumberField.InfinitePlace K, (ideleInfiniteInvAt K L w) x

The sum of the local invariants of an idele-layer class may be computed over any finite set of finite places containing its ramification set, together with all the infinite places.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_infl (K : Type) [Field K] [NumberField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (x : ↑(old.H (ideleFormation K) 2)) : (ideleSumLocalInv K new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (ideleFormation K) 2)) x) = (ideleSumLocalInv K old) x

The sum of the local invariants is inflation-invariant: inflating an idele-layer class to a refinement of its layer does not change the sum of its local invariants.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_res (K : Type) [Field K] [NumberField K] {small big : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRestriction small big) (x : ↑(big.H (ideleFormation K) 2)) : (ideleSumLocalInv K small) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes (ideleFormation K) 2)) x) = T.relativeDegree • (ideleSumLocalInv K big) x

Restriction multiplies the sum of the local invariants by the relative degree: for a restriction of a layer L/F to an intermediate ground field E, Σ inv (res x) = [E : F] • Σ inv x.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_conj (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (x : ↑(L.H (ideleFormation K) 2)) : (ideleSumLocalInv K (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (ideleFormation K) g 2).hom) x) = (ideleSumLocalInv K L) x

Conjugation preserves the sum of the local invariants: for g : G_K, the conjugate class in the conjugate layer gL/gF has the same sum of local invariants.