Restriction and corestriction of the Tate isomorphism of a class formation

Restriction to an intermediate ground field preserves cup product with a degree-two class. Since the fundamental class restricts to the fundamental class of the smaller layer, the Tate isomorphism commutes with restriction in every integer degree. In degree minus two this is the square relating inclusion of ground levels to transfer of abelianized Galois groups.

Dually, the projection formula cor (x ∪ res u) = cor x ∪ u shows that corestriction from an intermediate ground field carries cup product with the restricted fundamental class to cup product with the fundamental class, so the Tate isomorphism also commutes with corestriction in every integer degree. In degree minus two this is the square relating the norm between ground levels to inclusion of Galois groups.

The range comparisons identify a layer's Galois group with its image in the larger group. The restriction and corestriction maps defined branchwise by degree agree with generic Tate restriction and corestriction through these comparisons, so the generic cup-product restriction law and projection formula apply to the existing finite-layer maps.

Main statements

• TauCeti.ClassFieldTheory.LayerRestriction.cupClass_res, TauCeti.ClassFieldTheory.ClassFormation.tateIso_res: compatibility with restriction.
• TauCeti.ClassFieldTheory.LayerRestriction.cupClass_cor, TauCeti.ClassFieldTheory.ClassFormation.tateIso_cor: compatibility with corestriction.
• TauCeti.ClassFieldTheory.ClassFormation.tateIso_res_trans: compatibility with restriction along a tower of ground fields.

References

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

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.cupClass_res {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (u : ↑(big.H F 2)) (r : ℤ) (x : ↑(big.TrivialTateH r)) : (CategoryTheory.ConcreteCategory.hom (T.tateRes F (r + 2))) ((cupClass F big u r) x) = (cupClass F small ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F 2)) u) r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateRes r)) x)

Restricting cup product with a degree-two layer class gives cup product of the restricted classes, in every integer degree.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.cupClass_cor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (u : ↑(big.H F 2)) (r : ℤ) (x : ↑(small.TrivialTateH r)) : (CategoryTheory.ConcreteCategory.hom (T.tateCor F (r + 2))) ((cupClass F small ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F 2)) u) r) x) = (cupClass F big u r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateCor r)) x)

The projection formula for layer classes: corestricting cup product with the restriction of a degree-two class u of the larger layer is cup product with u of the corestricted class, in every integer degree.

theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso_res {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} {small big : NormalLayer G} (cf : ClassFormation F) (T : LayerRestriction small big) (r : ℤ) (x : ↑(big.TrivialTateH r)) : (CategoryTheory.ConcreteCategory.hom (T.tateRes F (r + 2))) ((cf.tateIso big r) x) = (cf.tateIso small r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateRes r)) x)

The Tate isomorphism of a class formation commutes with restriction to an intermediate ground field, in every integer degree.

theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso_res_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {a b c : NormalLayer G} (T : LayerRestriction a b) (T' : LayerRestriction b c) (r : ℤ) (x : ↑(c.TrivialTateH r)) : (CategoryTheory.ConcreteCategory.hom (T.tateRes F (r + 2))) ((CategoryTheory.ConcreteCategory.hom (T'.tateRes F (r + 2))) ((cf.tateIso c r) x)) = (cf.tateIso a r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateRes r)) ((CategoryTheory.ConcreteCategory.hom (T'.trivialTateRes r)) x))

The Tate isomorphism commutes with iterated restriction along a tower of ground fields.

theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso_cor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} {small big : NormalLayer G} (cf : ClassFormation F) (T : LayerRestriction small big) (r : ℤ) (x : ↑(small.TrivialTateH r)) : (CategoryTheory.ConcreteCategory.hom (T.tateCor F (r + 2))) ((cf.tateIso small r) x) = (cf.tateIso big r) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateCor r)) x)

The Tate isomorphism of a class formation commutes with corestriction from an intermediate ground field, in every integer degree.