The character formula on carry classes

Let K be a field with absolute Galois group G_K = Gal(Kˢ/K), let χ : G_K → ℚ/ℤ be a character with open kernel and a ∈ Kˣ. The carry cocycle TauCeti.ContCohomology.characterCarryCocycle of χ and a represents the Brauer class usually written a ∪ δχ. This file proves the character formula for it: for a class formation on the units formation of K whose invariant on every layer is a map ι : Br K → ℚ/ℤ after inflation,

ι (a ∪ δχ) = χ (Art a),

where Art is the Artin map of the class formation (ClassFormation.apply_characterCarryCocycle_of_mk_eq_fieldArtinMap). For a nonarchimedean local field this is inv_K (a ∪ δχ) = χ (Art_K a) for the local invariant invMap and the absolute local Artin map artinMap (invMap_characterCarryCocycle_of_mk_eq_artinMap), with no hypothesis on the ramification of χ; at an infinite place it is the same formula for the archimedean invariant infiniteInvMap and Artin map infiniteArtinAt (infiniteInvMap_characterCarryCocycle_of_mk_eq_infiniteArtinAt).

The local formula holds on every open subgroup H of G_K, read by its invariant subgroupInvMap, the local invariant of its corestriction to G_K. Such a subgroup is the subgroup Gal(Kˢ/σ(L)) fixing the image of a finite extension L/K under a K-embedding σ : L → Kˢ, and for a character ψ of it and b ∈ Lˣ,

inv_H (σ b ∪ δψ) = ψ (Art_L b),

the Artin symbol being read in H along G_L ≃ Gal(Kˢ/σ(L)) (subgroupInvMap_characterCarryCocycle_of_mk_eq_artinMap). Since the local Artin symbols are dense in G_L^ab, every value of ψ is the invariant of a carry class of ψ (exists_subgroupInvMap_characterCarryCocycle_eq). These evaluate the summands of the Mackey formula for the invariant of a corestricted idele class (TauCeti.ClassFieldTheory.invMap_ideleBrLocalization_explicitCor2) on carry classes: by naturality (TauCeti.ContCohomology.explicitMap2_characterCarryCocycle), each summand is the invariant of a carry class over an open subgroup of a local absolute Galois group.

The proof compares the carry class with the class a₀ ∪ δχ in the character formula ClassFormation.character_artinMap of a finite layer. On the layer V ◁ G_K of an open normal subgroup V on which χ vanishes, the cup product a₀ ∪ δχ is represented by the carry cocycle of the character of G_K / V induced by χ (TauCeti.ClassFieldTheory.NormalLayer.artinCharacterCup_groundLevelEquiv_eq_H2π), whose inflation to G_K is the carry cocycle of χ (brInfl_artinCharacterCup).

These are the local factors of a sum of local invariants of a global carry class: the global class localizes to the carry classes of the restricted characters (TauCeti.ClassFieldTheory.ideleBrLocalization_characterCarryCocycle), and the character formula turns the sum of their invariants into the value of the character on a product of local Artin symbols.

Main results

• TauCeti.ClassFieldTheory.brInfl_artinCharacterCup: on the layer of an open normal subgroup, the inflation of a₀ ∪ δχ is the carry class of the character read on G_K.
• TauCeti.ClassFieldTheory.ClassFormation.apply_characterCarryCocycle_of_mk_eq_fieldArtinMap: the character formula on carry classes for a class formation on the units formation.
• TauCeti.ClassFieldTheory.invMap_characterCarryCocycle_of_mk_eq_artinMap: the local character formula inv_K (a ∪ δχ) = χ (Art_K a).
• TauCeti.ClassFieldTheory.infiniteInvMap_characterCarryCocycle_of_mk_eq_infiniteArtinAt: the archimedean character formula inv_w (a ∪ δχ) = χ (Art_w a).
• TauCeti.ClassFieldTheory.subgroupInvMap_characterCarryCocycle_of_mk_eq_artinMap: the local character formula inv_H (σ b ∪ δψ) = ψ (Art_L b) on the open subgroup H = Gal(Kˢ/σ(L)).
• TauCeti.ClassFieldTheory.exists_subgroupInvMap_characterCarryCocycle_eq: every value of a character of an open subgroup is the invariant of one of its carry classes.

References

• J.-P. Serre, Local Fields, Chapter XI, §3, and Chapter XIV, §1.
• J. S. Milne, Class Field Theory, Chapter VII, §8.

The carry class on a layer of the units formation

theorem TauCeti.ClassFieldTheory.brInfl_artinCharacterCup {K : Type} [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (χ : Additive (Abelianization (NormalLayer.ofOpenNormal V).Gal) →+ AddCircle 1) (ψ : Additive (AbsoluteGaloisGroup K) →+ AddCircle 1) (hχψ : ∀ (g : AbsoluteGaloisGroup K), ψ (Additive.ofMul g) = χ (Additive.ofMul (Abelianization.of ((NormalLayer.galOfOpenNormalEquiv V).symm ↑g)))) (a : Kˣ) : (brInfl V) ((((NormalLayer.ofOpenNormal V).artinCharacterCup (unitsFormation K)) ((localGroundEquiv K V) (Additive.ofMul a))) χ) = (unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle ψ ⋯) ((baseUnitsEquivInvariants K) (Additive.ofMul a)))

The inflation of the Artin character cup is the carry class. Let χ be a character of the abelianized Galois group of the layer V ◁ G_K, and let ψ : G_K → ℚ/ℤ be the same character read on G_K. Then for a ∈ Kˣ the inflation to Br K of the class a₀ ∪ δχ of the character formula is the Brauer class of the carry cocycle of ψ and a.

The character formula on carry classes

theorem TauCeti.ClassFieldTheory.ClassFormation.apply_characterCarryCocycle_of_mk_eq_fieldArtinMap {K : Type} [Field K] (cf : ClassFormation (unitsFormation K)) (ι : Br K →+ AddCircle 1) (hι : ∀ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (x : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation K) 2)), (cf.inv (NormalLayer.ofOpenNormal V)) x = ι ((brInfl V) x)) (χ : Additive (AbsoluteGaloisGroup K) →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : Kˣ) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = cf.fieldArtinMap a) : ι ((unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle χ hχ) ((baseUnitsEquivInvariants K) (Additive.ofMul a)))) = χ (Additive.ofMul ((absoluteGaloisGroupRestrictEquiv K) σ))

The character formula on carry classes. Let cf be a class formation on the units formation of K whose invariant on the layer of every open normal subgroup V is ι ∘ brInfl V for a homomorphism ι : Br K → ℚ/ℤ. Let χ : G_K → ℚ/ℤ be a character with open kernel and a ∈ Kˣ. If σ ∈ Gal(AlgebraicClosure K/K) represents the Artin symbol cf.fieldArtinMap a, then ι (a ∪ δχ) = χ(σ), where a ∪ δχ is the Brauer class of the carry cocycle of χ and a.

theorem TauCeti.ClassFieldTheory.invMap_characterCarryCocycle_of_mk_eq_artinMap {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (χ : Additive (AbsoluteGaloisGroup K) →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : Kˣ) (σ : Field.absoluteGaloisGroup K) (hσ : ↑σ = (artinMap K) a) : (invMap K) ((unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle χ hχ) ((baseUnitsEquivInvariants K) (Additive.ofMul a)))) = χ (Additive.ofMul ((absoluteGaloisGroupRestrictEquiv K) σ))

The local character formula inv_K (a ∪ δχ) = χ (Art_K a). For a nonarchimedean local field K, a character χ : G_K → ℚ/ℤ with open kernel and a ∈ Kˣ, if σ ∈ Gal(AlgebraicClosure K/K) represents the absolute local Artin symbol artinMap K a, then the local invariant of the Brauer class of the carry cocycle of χ and a is χ(σ).

theorem TauCeti.ClassFieldTheory.infiniteInvMap_characterCarryCocycle_of_mk_eq_infiniteArtinAt {K : Type} [Field K] (w : NumberField.InfinitePlace K) (χ : Additive (AbsoluteGaloisGroup w.Completion) →+ AddCircle 1) (a : w.Completionˣ) (σ : Field.absoluteGaloisGroup w.Completion) (hσ : ↑σ = (infiniteArtinAt w) a) : (infiniteInvMap w) ((unitsRepH2Equiv w.Completion) ↑((ContCohomology.characterCarryCocycle χ ⋯) ((baseUnitsEquivInvariants w.Completion) (Additive.ofMul a)))) = χ (Additive.ofMul ((absoluteGaloisGroupRestrictEquiv w.Completion) σ))

The archimedean character formula inv_w (a ∪ δχ) = χ (Art_w a). For an infinite place w of a field K, a character χ : G_{K_w} → ℚ/ℤ and a ∈ K_wˣ, if σ ∈ Gal(AlgebraicClosure K_w/K_w) represents the archimedean Artin symbol infiniteArtinAt w a, then the archimedean invariant of the Brauer class of the carry cocycle of χ and a is χ(σ). No hypothesis on χ is needed: G_{K_w} is finite, so the kernel of χ is open.

Open subgroups of a local absolute Galois group

theorem TauCeti.ClassFieldTheory.subgroupInvMap_characterCarryCocycle_of_mk_eq_artinMap {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (ψ : Additive ↥σ.fieldRange.fixingSubgroup →+ AddCircle 1) (hψ : IsOpen ↑ψ.ker) (b : Lˣ) (ρ : Field.absoluteGaloisGroup L) (hρ : ↑ρ = (artinMap L) b) : (subgroupInvMap K σ.fieldRange.fixingSubgroup ⋯) ↑((ContCohomology.characterCarryCocycle ψ hψ) (embeddedUnitsInvariants K L σ b)) = ψ (Additive.ofMul ((absoluteGaloisGroupEquivFixingSubgroup K L σ) ((absoluteGaloisGroupRestrictEquiv L) ρ)))

The local character formula on an open subgroup inv_H (σ b ∪ δψ) = ψ (Art_L b). Let L/K be a finite extension of nonarchimedean local fields, embedded in Kˢ by σ, so that H = Gal(Kˢ/σ(L)) is an open subgroup of G_K. For a character ψ : H → ℚ/ℤ with open kernel and b ∈ Lˣ, if ρ ∈ Gal(AlgebraicClosure L/L) represents the absolute local Artin symbol artinMap L b, then the invariant of H of the carry class of ψ and of the invariant σ b is ψ of the image of ρ in H along G_L ≃ H.

theorem TauCeti.ClassFieldTheory.exists_subgroupInvMap_characterCarryCocycle_eq {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (H : Subgroup (AbsoluteGaloisGroup K)) [H.FiniteIndex] (hH : IsOpen ↑H) (ψ : Additive ↥H →+ AddCircle 1) (hψ : IsOpen ↑ψ.ker) (h : ↥H) : ∃ (b : ↥(ContCohomology.H0 (↥H) (UnitsCoeff K))), (subgroupInvMap K H hH) ↑((ContCohomology.characterCarryCocycle ψ hψ) b) = ψ (Additive.ofMul h)

Every value of a character of an open subgroup is the invariant of a carry class. For an open subgroup H of G_K, a character ψ : H → ℚ/ℤ with open kernel and h ∈ H, some invariant b ∈ ((Kˢ)ˣ)^H has inv_H (b ∪ δψ) = ψ(h).