Restriction of trivial coefficients in a tower

For a tower of finite normal layers, restriction on integral Tate cohomology composes in every integer degree. This supplies the trivial-coefficient side of the tower compatibility used by the Tate isomorphism of a class formation.

In positive degrees these maps agree with ordinary group-cohomology restriction along the inclusion of Galois groups, and below degree minus one with the transfer in group homology. In degree zero the map is the identity on integral representatives, while degree minus one vanishes for integral coefficients.

Main results

• TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRes_trans: trivial-coefficient Tate restriction is functorial along a tower of restrictions, in every integer degree.

Implementation notes

The case split by degree follows the corestriction counterpart LayerRestriction.trivialTateCor_trans in Formation/Tate/TrivialCorestrictionTrans.lean. Below degree minus one the argument follows tateRes_negSucc_succ_trans in Formation/Tate/Restriction.lean, the same step with formation coefficients.

References

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

Positive degrees

Degrees below minus one

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRes_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRestriction a b) (T' : LayerRestriction b c) (r : ℤ) : ⋯.trivialTateRes r = CategoryTheory.CategoryStruct.comp (T'.trivialTateRes r) (T.trivialTateRes r)

Trivial-coefficient Tate restriction is functorial along a tower of restrictions, in every integer degree. For fields F ⊆ E ⊆ E' ⊆ K, with T' restricting K/F to K/E and T restricting K/E to K/E', restricting Tate cohomology with trivial integral coefficients directly from K/F to K/E' agrees with restricting from K/F to K/E and then to K/E'.

This is the trivial-coefficient counterpart of tateRes_trans_eq_comp.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRes_trans_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRestriction a b) (T' : LayerRestriction b c) (r : ℤ) {Z : ModuleCat ℤ} (h : a.TrivialTateH r ⟶ Z) : CategoryTheory.CategoryStruct.comp (⋯.trivialTateRes r) h = CategoryTheory.CategoryStruct.comp (T'.trivialTateRes r) (CategoryTheory.CategoryStruct.comp (T.trivialTateRes r) h)

Trivial-coefficient Tate restriction is functorial along a tower of restrictions, in every integer degree. For fields F ⊆ E ⊆ E' ⊆ K, with T' restricting K/F to K/E and T restricting K/E to K/E', restricting Tate cohomology with trivial integral coefficients directly from K/F to K/E' agrees with restricting from K/F to K/E and then to K/E'.

This is the trivial-coefficient counterpart of tateRes_trans_eq_comp.