Finite-layer corestriction and generic Tate corestriction

The corestriction maps of finite normal layers agree, in every integer degree, with generic subgroup corestriction after the range comparison identifying the smaller Galois group with its image in the larger one. This holds both for formation coefficients and for trivial integral coefficients.

These comparisons let the generic Tate cup-product projection formula apply to the existing finite-layer maps, for use in establishing compatibility of finite-layer Tate isomorphisms with corestriction and norm compatibility of Artin maps.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
• K. S. Brown, Cohomology of Groups, Chapter III, §9 and Chapter VI, §5.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_eq_cor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (r : ℤ) : T.tateCor F r = CategoryTheory.CategoryStruct.comp (T.tateRangeIso F r).hom (TateCohomology.cor (big.rep F) T.galHom.range r)

Layer Tate corestriction is the range comparison followed by generic subgroup corestriction, in every integer degree. The subgroup carrier uses Subgroup.fintypeOfFinite, as fixed by the generic map TauCeti.TateCohomology.cor.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateCor_eq_cor_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (r : ℤ) {Z : ModuleCat ℤ} (h : big.TateH F r ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.tateCor F r) h = CategoryTheory.CategoryStruct.comp (T.tateRangeIso F r).hom (CategoryTheory.CategoryStruct.comp (TateCohomology.cor (big.rep F) T.galHom.range r) h)

Layer Tate corestriction is the range comparison followed by generic subgroup corestriction, in every integer degree. The subgroup carrier uses Subgroup.fintypeOfFinite, as fixed by the generic map TauCeti.TateCohomology.cor.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_eq_cor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (r : ℤ) : T.trivialTateCor r = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso r).hom (TateCohomology.cor (Rep.trivial ℤ big.Gal ℤ) T.galHom.range r)

With trivial integral coefficients, layer Tate corestriction is the range comparison followed by generic subgroup corestriction, in every integer degree. The subgroup carrier uses the Subgroup.fintypeOfFinite instance fixed by the generic corestriction map.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateCor_eq_cor_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (r : ℤ) {Z : ModuleCat ℤ} (h : big.TrivialTateH r ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.trivialTateCor r) h = CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso r).hom (CategoryTheory.CategoryStruct.comp (TateCohomology.cor (Rep.trivial ℤ big.Gal ℤ) T.galHom.range r) h)

With trivial integral coefficients, layer Tate corestriction is the range comparison followed by generic subgroup corestriction, in every integer degree. The subgroup carrier uses the Subgroup.fintypeOfFinite instance fixed by the generic corestriction map.