Range comparisons for finite-layer Tate cohomology

For a restriction of finite normal layers K/E inside K/F, the Galois group of K/E is identified with the image of its inclusion into the Galois group of K/F. This file transports Tate cohomology of the smaller layer along that identification, both with formation coefficients (LayerRestriction.tateRangeIso) and with trivial integral coefficients (LayerRestriction.trivialTateRangeIso). These comparisons are shared by Tate restriction and Tate corestriction between finite layers.

For a subgroup H of the Galois group of a finite normal layer L, the layer L.subgroupLayer H of H has Galois group H and the coefficient module of L; its Tate cohomology is Tate cohomology of H with coefficients in the restricted module (NormalLayer.subgroupLayerTateIso).

Main definitions

• TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso: Tate cohomology of the smaller layer as Tate cohomology of the image subgroup.
• TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso: the same comparison with trivial integral coefficients.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupLayerTateIso: Tate cohomology of the layer of a subgroup, as Tate cohomology of that subgroup.

Main results

• TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso_hom and TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom: each range comparison is the Tate map of its compatible pair, in every degree.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupLayerTateIso_hom: the subgroup-layer comparison is the Tate map of its compatible pair isIntertwiningMap_repIso_subgroupLayer.
• TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso_inv_H0π: in degree zero, the inverse comparison sends the class of an invariant element to the class of the same element.
• TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso_inv_HNegOneπ: in degree minus one, the inverse comparison sends the class of a norm-zero element to the class of its image under the inverse coefficient identification.

@[instance_reducible]

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.instFintypeRange {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : Fintype ↥T.galHom.range

The range of the inclusion between finite layer Galois groups is finite.

theorem TauCeti.ClassFieldTheory.LayerRestriction.isIntertwiningMap_repIso_range {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) : (small.rep F).ρ.IsIntertwiningMap (MonoidHom.comp (Rep.res T.galHom.range.subtype (big.rep F)).ρ ↑(MonoidHom.ofInjective ⋯)) ↑(Representation.equivOfIso (T.repIso F)).toLinearEquiv

The identification of coefficient modules intertwines the Galois action of the smaller layer with the action of the image of its Galois group in the larger one. This is the compatible pair along which tateRangeIso transports Tate cohomology.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (r : ℤ) : small.TateH F r ≅ tateCohomology (Rep.res T.galHom.range.subtype (big.rep F)) r

Tate cohomology of the smaller layer, identified with Tate cohomology of the image of its Galois group in the larger one. The coefficient identification is repIso.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso_hom {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.tateRangeIso F r).hom = TateCohomology.map ⋯ r

The range comparison is the Tate map attached to the compatible pair isIntertwiningMap_repIso_range.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso_inv_H0π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(Rep.res T.galHom.range.subtype (big.rep F)).ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (T.tateRangeIso F 0).inv) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (Rep.res T.galHom.range.subtype (big.rep F)))) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (small.rep F))) ⟨(Rep.Hom.hom (T.repIso F).inv) ↑x, ⋯⟩

In degree zero, the inverse range comparison sends the class of an invariant of the image subgroup to the class of the same element, read through repIso, in the smaller layer.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateRangeIso_inv_HNegOneπ {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(LinearMap.ker (Rep.res T.galHom.range.subtype (big.rep F)).ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (T.tateRangeIso F (-1)).inv) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.HNegOneπ (Rep.res T.galHom.range.subtype (big.rep F)))) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.HNegOneπ (small.rep F))) ((TateCohomology.mapKerNorm ⋯) x)

In degree minus one, the inverse range comparison sends the class of a norm-zero element of the image subgroup to the class of its image under the inverse coefficient identification.

Trivial coefficients

theorem TauCeti.ClassFieldTheory.LayerRestriction.isIntertwiningMap_trivial_range {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : (Rep.trivial ℤ small.Gal ℤ).ρ.IsIntertwiningMap (MonoidHom.comp (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)).ρ ↑(MonoidHom.ofInjective ⋯)) ↑(LinearEquiv.refl ℤ ℤ)

The identity on ℤ intertwines the trivial action of the smaller Galois group with the trivial action of the image of its Galois group in the larger one. This is the compatible pair along which trivialTateRangeIso transports Tate cohomology.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (r : ℤ) : small.TrivialTateH r ≅ tateCohomology (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)) r

Tate cohomology with trivial integral coefficients on the smaller Galois group, identified with the restriction of the trivial representation on the larger Galois group to the image of the inclusion.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (r : ℤ) : (T.trivialTateRangeIso r).hom = TateCohomology.map ⋯ r

The trivial-coefficient range comparison is the Tate map attached to the compatible pair isIntertwiningMap_trivial_range.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_H0π {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↥(Rep.trivial ℤ small.Gal ℤ).ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (T.trivialTateRangeIso 0).hom) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (Rep.trivial ℤ small.Gal ℤ))) x) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.H0π (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)))) ⟨↑x, ⋯⟩

In degree zero, the trivial-coefficient range comparison preserves the integral invariant representing a Tate class.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupCohomology_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso ↑n).hom ((TateCohomology.isoGroupCohomology n).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupCohomology.mapIso (MonoidHom.ofInjective ⋯) (LinearEquiv.refl ℤ ℤ) ⋯ n).hom

In positive degrees, the trivial-coefficient range comparison agrees with the ordinary group-cohomology change-of-group isomorphism.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupCohomology_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) [NeZero n] {Z : ModuleCat ℤ} (h : (groupCohomology.functor ℤ (↥T.galHom.range) n).obj (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso ↑n).hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology n).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupCohomology.mapIso (MonoidHom.ofInjective ⋯) (LinearEquiv.refl ℤ ℤ) ⋯ n).hom) h

In positive degrees, the trivial-coefficient range comparison agrees with the ordinary group-cohomology change-of-group isomorphism.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.trivialRangeRepHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : Rep.trivial ℤ small.Gal ℤ ⟶ Rep.res (↑(MonoidHom.ofInjective ⋯)) (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))

The identity on ℤ as an equivariant map from the smaller Galois group's trivial representation to the range-comparison representation.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialRangeRepHom_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ℤ) : (CategoryTheory.ConcreteCategory.hom T.trivialRangeRepHom) x = x

The trivial range comparison fixes each integer coefficient.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialRangeRepHom_hom_toLinearMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : (Rep.Hom.hom T.trivialRangeRepHom).toLinearMap = LinearMap.id

The coefficient map in the trivial range comparison is the identity linear map.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupHomology_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) : CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (Int.negSucc (n + 1))).hom ((TateCohomology.isoGroupHomology (Int.negSucc (n + 1)) (n + 1) ⋯).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (Int.negSucc (n + 1)) (n + 1) ⋯).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupHomology.map (↑(MonoidHom.ofInjective ⋯)) T.trivialRangeRepHom (n + 1))

Below degree minus one, the trivial-coefficient range comparison agrees with the group-homology change-of-group isomorphism.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupHomology_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (n : ℕ) {Z : ModuleCat ℤ} (h : (groupHomology.functor ℤ (↥T.galHom.range) (n + 1)).obj (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (Int.negSucc (n + 1))).hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (Int.negSucc (n + 1)) (n + 1) ⋯).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (Int.negSucc (n + 1)) (n + 1) ⋯).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupHomology.map (↑(MonoidHom.ofInjective ⋯)) T.trivialRangeRepHom (n + 1))) h

Below degree minus one, the trivial-coefficient range comparison agrees with the group-homology change-of-group isomorphism.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupHomology_hom_neg_two {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (-2)).hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupHomology.map (↑(MonoidHom.ofInjective ⋯)) T.trivialRangeRepHom 1)

In degree -2, the trivial-coefficient range comparison agrees with change of group on first homology.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupHomology_hom_neg_two_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) {Z : ModuleCat ℤ} (h : (groupHomology.functor ℤ (↥T.galHom.range) 1).obj (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.trivialTateRangeIso (-2)).hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupHomology.map (↑(MonoidHom.ofInjective ⋯)) T.trivialRangeRepHom 1)) h

In degree -2, the trivial-coefficient range comparison agrees with change of group on first homology.

theorem TauCeti.ClassFieldTheory.LayerRestriction.trivialTateRangeIso_hom_comp_isoGroupHomology_hom_neg_two_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↑(small.TrivialTateH (-2))) : (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ)))) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateRangeIso (-2)).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.trivial ℤ small.Gal ℤ)) (groupHomology.map (↑(MonoidHom.ofInjective ⋯)) T.trivialRangeRepHom 1))) x

In degree -2, the trivial-coefficient range comparison agrees with change of group on first homology.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tensorProduct_map_trivialRangeRepHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : TensorProduct.map (MonoidHom.toAdditive (Abelianization.map ↑(MonoidHom.ofInjective ⋯))).toIntLinearMap (Rep.Hom.hom T.trivialRangeRepHom).toLinearMap = LinearMap.rTensor ℤ (MonoidHom.toAdditive (Abelianization.map ↑(MonoidHom.ofInjective ⋯))).toIntLinearMap

Tensoring with the coefficient map for the trivial range comparison is right tensoring by the induced map on abelianizations.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.HNegTwoAddEquivAbelianization_trivialTateRangeIso_hom_neg_two {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↑(small.TrivialTateH (-2))) : (TensorProduct.rid ℤ (Additive (Abelianization ↥T.galHom.range))) ((TateCohomology.HNegTwoAddEquivTensorOfIsTrivial (Rep.res T.galHom.range.subtype (Rep.trivial ℤ big.Gal ℤ))) ((CategoryTheory.ConcreteCategory.hom (T.trivialTateRangeIso (-2)).hom) x)) = (MonoidHom.toAdditive (Abelianization.map ↑(MonoidHom.ofInjective ⋯))) (TateCohomology.HNegTwoAddEquivAbelianization x)

In degree -2, the trivial range comparison becomes the map induced on abelianizations under the generic low-degree identifications.

theorem TauCeti.ClassFieldTheory.NormalLayer.isIntertwiningMap_repIso_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (H : Subgroup L.Gal) : ((L.subgroupLayer H).rep F).ρ.IsIntertwiningMap (MonoidHom.comp (Rep.res H.subtype (L.rep F)).ρ ↑(L.subgroupGalEquiv H)) ↑(Representation.equivOfIso (⋯.repIso F)).toLinearEquiv

The identification of the coefficient module of the layer of H with the coefficient module of L intertwines the action of the Galois group of the layer of H with the action of H on the restricted module. This is the compatible pair along which subgroupLayerTateIso transports Tate cohomology.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.subgroupLayerTateIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (H : Subgroup L.Gal) [Fintype ↥H] (r : ℤ) : (L.subgroupLayer H).TateH F r ≅ tateCohomology (Rep.res H.subtype (L.rep F)) r

Tate cohomology of the layer of H is Tate cohomology of H with coefficients in the restriction of the coefficient module of L.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupLayerTateIso_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (H : Subgroup L.Gal) [Fintype ↥H] (r : ℤ) : (L.subgroupLayerTateIso F H r).hom = TateCohomology.map ⋯ r

The comparison subgroupLayerTateIso is the Tate map attached to the compatible pair isIntertwiningMap_repIso_subgroupLayer.