The local invariant of the carry class of an unramified character

Let F be a nonarchimedean local field, E/F a finite unramified Galois extension inside Fˢ with arithmetic Frobenius φ, χ : Gal(E/F) → ℚ/ℤ a character and a ∈ Fˣ. Read on G_F through restriction to E, the character has open kernel (IntermediateField.isOpen_ker_comp_restrictNormalHom), and its carry cocycle with the invariant a ∈ ((Fˢ)ˣ)^{G_F},

(g, h) ↦ a ^ ⌊χ'(g|_E) + χ'(h|_E)⌋,

is a class of Br F: classically, the cup product a ∪ δχ, the class of the cyclic algebra of a and χ. Its local invariant is

inv_F (a ∪ δχ) = v_F(a) · χ(φ)       (invMap_characterCarryCocycle).

For the character with χ(φ) = 1 / [E : F], the Frobenius character TauCeti.ClassFieldTheory.frobeniusCharacter read on Gal(E/F), the carry cocycle is the inflation of the carry cocycle of a at φ, which represents the unramified class unramifiedClass F E a of invariant v_F(a) / [E : F] (TauCeti.ClassFieldTheory.unramifiedInv_unramifiedClass). Every character of the cyclic group Gal(E/F) is an integer multiple of that one, and the class of the carry cocycle is additive in the character (TauCeti.ContCohomology.characterCarryCocycle_zsmul_character).

This is the local computation behind the global classes with prescribed local invariants: the carry cocycle of a global character and an idele localizes, by naturality along the decomposition maps (TauCeti.ContCohomology.explicitMap2_characterCarryCocycle), to the carry classes of the local characters and the components of the idele.

Main results

• TauCeti.ClassFieldTheory.invMap_characterCarryCocycle: the local invariant of the carry class of an unramified character χ and a ∈ Fˣ is v_F(a) · χ(φ).

References

• J.-P. Serre, Local Fields, Chapter XIV, §1, Proposition 2.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI (Serre, Local Class Field Theory), §1.

theorem TauCeti.ClassFieldTheory.invMap_characterCarryCocycle {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (E : IntermediateField F (SeparableClosure F)) [FiniteDimensional F ↥E] [IsGalois F ↥E] [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension F ↥E] [IsUnramified F ↥E] (χ : Additive Gal(↥E/F) →+ AddCircle 1) (a : Fˣ) : (invMap F) ((unitsRepH2Equiv F) ↑((ContCohomology.characterCarryCocycle (χ.comp (MonoidHom.toAdditive (AlgEquiv.restrictNormalHom ↥E))) ⋯) ((baseUnitsEquivInvariants F) (Additive.ofMul a)))) = Multiplicative.toAdd ((normalizedValuation F) a) • χ (Additive.ofMul frobeniusAlgEquiv)

The local invariant of the carry class of an unramified character. For a character χ of the Galois group of a finite unramified Galois extension E/F inside Fˢ, read on G_F, and a ∈ Fˣ, the class in Br F of the carry cocycle of χ and a, classically the cup product a ∪ δχ, has invariant v_F(a) · χ(φ), where φ is arithmetic Frobenius.