Inflation, the Tate isomorphism and character classes of a class formation

A refinement LayerRefinement old new enlarges the top field of a finite normal layer from K to L over the same ground field F. Inflation of positive-degree Tate cohomology along it, with formation coefficients (LayerRefinement.tateInfl) and with trivial integral coefficients (LayerRefinement.trivialTateInfl), is change of group along the quotient map of Galois groups Gal(L/F) → Gal(K/F) (LayerRefinement.tateInfl_eq_posMap, LayerRefinement.trivialTateInfl_eq_posMap). Since change of group preserves the Tate cup product, inflating cup product with a degree-two class is cup product of the inflated classes (LayerRefinement.cupClass_infl).

For a class formation the fundamental class does not inflate to the fundamental class: inf u_{K/F} = [L : K] • u_{L/F} (ClassFormation.fundamentalClass_infl). Hence Tate's isomorphism H^r(Gal(K/F), ℤ) ≃ H^{r+2}(Gal(K/F), A^{V}) satisfies the scaled inflation formula

inf (x ∪ u_{K/F}) = [L : K] • (inf x ∪ u_{L/F})

in every positive degree r (ClassFormation.tateIso_infl). Inflation is not defined in Tate degrees at most zero, so the formula has no counterpart there. The restriction and corestriction squares of ClassFormation.tateIso_res and ClassFormation.tateIso_cor commute without a factor; the inflation square differs from them exactly by the relative degree.

The classes through which Artin and Tate characterize the Artin map behave without such a factor. A character χ of Gal(K/F)^ab inflates to the character χ ∘ π of Gal(L/F)^ab, where π : Gal(L/F)^ab → Gal(K/F)^ab is the quotient map, and inflation carries the connecting class δχ ∈ H²(Gal(K/F), ℤ) to δ(χ ∘ π) (LayerRefinement.trivialTateInfl_characterConnectingClass). Cup product with the degree-zero class of a ∈ A^U is induced by the coefficient map n ↦ n • a, which inflation does not see, so inflation carries the Artin character cup a₀ ∪ δχ of K/F to that of L/F (LayerRefinement.cohomologyInfl_artinCharacterCup). Since inflation preserves invariants, inv_{L/F}(a₀ ∪ δ(χ ∘ π)) = inv_{K/F}(a₀ ∪ δχ) (ClassFormation.inv_artinCharacterCup_comp_quotientHom). By the character formula of Artin and Tate, χ(artinMap a) = inv(a₀ ∪ δχ), this is the statement that the Artin maps of K/F and L/F are compatible with the quotient map π.

Main statements

• TauCeti.ClassFieldTheory.LayerRefinement.cupClass_infl: inflation preserves cup product with a degree-two class.
• TauCeti.ClassFieldTheory.ClassFormation.tateIso_infl: the scaled inflation formula for the Tate isomorphism.
• TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_characterConnectingClass: inflation of the connecting class of a character is the connecting class of the inflated character.
• TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_artinCharacterCup: inflation of the Artin character cup is the Artin character cup of the inflated character.
• TauCeti.ClassFieldTheory.ClassFormation.inv_artinCharacterCup_comp_quotientHom: the invariant of the Artin character cup does not change under inflation.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1–4.
• J.-P. Serre, Local Fields, Chapter XI, §§1–3.

theorem TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_eq_posMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (r : ℕ) [NeZero r] : T.tateInfl F r = TateCohomology.posMap T.galHom (T.repHom F) r

Inflation of positive-degree Tate cohomology along a refinement is the change of group along the quotient map of Galois groups and the inclusion of coefficient modules.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_eq_posMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (r : ℕ) [NeZero r] : T.trivialTateInfl r = TateCohomology.posMap T.galHom T.trivialRepHom r

Inflation of positive-degree Tate cohomology with trivial integral coefficients is the change of group along the quotient map of Galois groups.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cupClass_infl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (u : ↑(old.H F 2)) (r : ℕ) [NeZero r] (x : ↑(old.TrivialTateH ↑r)) : (CategoryTheory.ConcreteCategory.hom (T.tateInfl F (r + 2))) ((cupClass F old u ↑r) x) = (cupClass F new ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) u) ↑r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateInfl r)) x)

Inflating cup product with a degree-two class gives cup product of the inflated classes, in every positive degree.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_characterConnectingClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (χ : Additive (Abelianization old.Gal) →+ AddCircle 1) : (CategoryTheory.ConcreteCategory.hom (T.trivialTateInfl 2)) (old.characterConnectingClass χ) = new.characterConnectingClass (χ.comp T.quotientHom)

Inflation of the connecting class of a character. Inflating δχ ∈ H²(Gal(K/F), ℤ) to the refinement L/F gives the connecting class of the inflated character χ ∘ π, where π : Gal(L/F)^ab → Gal(K/F)^ab is the quotient map.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_artinCharacterCup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (a : ↥(F.level old.ground)) (χ : Additive (Abelianization old.Gal) →+ AddCircle 1) : (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) (((old.artinCharacterCup F) a) χ) = ((new.artinCharacterCup F) ((T.groundEquiv F) a)) (χ.comp T.quotientHom)

Inflation of the Artin character cup. Inflating the class a₀ ∪ δχ ∈ H²(Gal(K/F), A^V) of a ∈ A^U and a character χ of Gal(K/F)^ab to the refinement L/F gives the class a₀ ∪ δ(χ ∘ π) ∈ H²(Gal(L/F), A^{V'}) of the same element a of the common ground level and the inflated character.

theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso_infl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} {old new : NormalLayer G} (cf : ClassFormation F) (T : LayerRefinement old new) (r : ℕ) [NeZero r] (x : ↑(old.TrivialTateH ↑r)) : (CategoryTheory.ConcreteCategory.hom (T.tateInfl F (r + 2))) ((cf.tateIso old ↑r) x) = T.relativeDegree • (cf.tateIso new ↑r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateInfl r)) x)

The scaled inflation formula for the Tate isomorphism. Under a refinement of the top field from K to L, inflating x ∪ u_{K/F} gives [L : K] times the cup product of the inflation of x with u_{L/F}, in every positive degree. Unlike restriction and corestriction, the inflation square commutes only up to the relative degree, because inf u_{K/F} = [L : K] • u_{L/F}.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.inv_artinCharacterCup_comp_quotientHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} {old new : NormalLayer G} (cf : ClassFormation F) (T : LayerRefinement old new) (a : ↥(F.level old.ground)) (χ : Additive (Abelianization old.Gal) →+ AddCircle 1) : (cf.inv new) (((new.artinCharacterCup F) ((T.groundEquiv F) a)) (χ.comp T.quotientHom)) = (cf.inv old) (((old.artinCharacterCup F) a) χ)

The invariant of the Artin character cup is unchanged by inflation. For a ∈ A^U and a character χ of Gal(K/F)^ab, the invariant over the refinement L/F of a₀ ∪ δ(χ ∘ π) is the invariant over K/F of a₀ ∪ δχ, where π : Gal(L/F)^ab → Gal(K/F)^ab is the quotient map.