Corestriction between finite normal layers

For a restriction of layers K/E inside K/F, corestriction carries Hⁿ(Gal(K/E), A^V) to Hⁿ(Gal(K/F), A^V). The smaller Galois group is identified with the image of its inclusion into the larger one, and the coefficient identification repIso then transports the generic group-cohomology corestriction to the layer cohomology groups.

The comparison with subgroup restriction is explicit. It gives the normalization cor ∘ res = [E : F], with precisely the relative degree of the restriction of layers. This is the normalization used to compare invariants and fundamental classes under corestriction.

Along a tower F ⊆ E ⊆ E' ⊆ K, corestricting from K/E' to K/E and then to K/F is corestricting from K/E' to K/F (cohomologyCor_trans). This is the transitivity of group-cohomology corestriction, TauCeti.groupCohomology.corestriction_trans, read through the coefficient identifications repIso.

For the restriction of a layer to the layer of its whole Galois group, the relative degree is 1, so restriction is injective on cohomology (NormalLayer.cohomologyRes_subgroupRestriction_top_injective); a class whose restriction generates the cohomology of that layer therefore generates the cohomology of the original layer.

References

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

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRangeIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : small.H F n ≅ groupCohomology (Rep.res T.galHom.range.subtype (big.rep F)) n

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

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRangeIso_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : T.cohomologyRangeIso F n = groupCohomology.mapIso (MonoidHom.ofInjective ⋯) (Representation.equivOfIso (T.repIso F)).toLinearEquiv ⋯ n

The range comparison is the canonical change-of-group isomorphism, with the coefficient equivalence underlying repIso.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.map_subtype_comp_cohomologyRangeIso_inv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.map T.galHom.range.subtype (CategoryTheory.CategoryStruct.id (Rep.res T.galHom.range.subtype (big.rep F))) n) (T.cohomologyRangeIso F n).inv = T.cohomologyRes F n

Restriction to the image subgroup followed by the inverse coefficient and group identification is the existing restriction between layer cohomology groups.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.map_subtype_comp_cohomologyRangeIso_inv_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) {Z : ModuleCat ℤ} (h : small.H F n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.map T.galHom.range.subtype (CategoryTheory.CategoryStruct.id (Rep.res T.galHom.range.subtype (big.rep F))) n) (CategoryTheory.CategoryStruct.comp (T.cohomologyRangeIso F n).inv h) = CategoryTheory.CategoryStruct.comp (T.cohomologyRes F n) h

Restriction to the image subgroup followed by the inverse coefficient and group identification is the existing restriction between layer cohomology groups.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : small.H F n ⟶ big.H F n

Corestriction between the cohomology groups of finite normal layers. This is subgroup corestriction transported along the inclusion of Galois groups and repIso.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : T.cohomologyCor F n = CategoryTheory.CategoryStruct.comp (T.cohomologyRangeIso F n).hom (groupCohomology.corestriction T.galHom.range (big.rep F) n)

Layer corestriction is the range comparison followed by subgroup corestriction.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRangeIso_inv_comp_cohomologyCor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (T.cohomologyRangeIso F n).inv (T.cohomologyCor F n) = groupCohomology.corestriction T.galHom.range (big.rep F) n

Under the canonical identification with the image subgroup, layer corestriction is generic group-cohomology corestriction.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRangeIso_inv_comp_cohomologyCor_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) {Z : ModuleCat ℤ} (h : big.H F n ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.cohomologyRangeIso F n).inv (CategoryTheory.CategoryStruct.comp (T.cohomologyCor F n) h) = CategoryTheory.CategoryStruct.comp (groupCohomology.corestriction T.galHom.range (big.rep F) n) h

Under the canonical identification with the image subgroup, layer corestriction is generic group-cohomology corestriction.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor_cohomologyRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (T.cohomologyRes F n) (T.cohomologyCor F n) = T.relativeDegree • CategoryTheory.CategoryStruct.id (big.H F n)

Corestriction after restriction multiplies every cohomology class by the relative degree [E : F].

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor_cohomologyRes_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) {Z : ModuleCat ℤ} (h : big.H F n ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.cohomologyRes F n) (CategoryTheory.CategoryStruct.comp (T.cohomologyCor F n) h) = CategoryTheory.CategoryStruct.comp (T.relativeDegree • CategoryTheory.CategoryStruct.id (big.H F n)) h

Corestriction after restriction multiplies every cohomology class by the relative degree [E : F].

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor_cohomologyRes_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) (x : ↑(big.H F n)) : (CategoryTheory.ConcreteCategory.hom (T.cohomologyCor F n)) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F n)) x) = (↑small.ground).relIndex ↑big.ground • x

Corestriction after restriction multiplies every cohomology class by the relative degree [E : F].

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRestriction L L) (F : Formation G) (n : ℕ) : T.cohomologyCor F n = CategoryTheory.CategoryStruct.id (L.H F n)

Corestriction along the trivial restriction is the identity.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyCor_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) (F : Formation G) (n : ℕ) : ⋯.cohomologyCor F n = CategoryTheory.CategoryStruct.comp (T.cohomologyCor F n) (T'.cohomologyCor F n)

Corestriction of cohomology is functorial along a tower of restrictions. Corestricting from K/E' to K/E and then to K/F is corestricting from K/E' to K/F.

theorem TauCeti.ClassFieldTheory.NormalLayer.cohomologyRes_subgroupRestriction_top_injective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (n : ℕ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F n))

Restriction to the layer of the whole Galois group is injective on cohomology: corestriction splits it, the relative degree being 1.

theorem TauCeti.ClassFieldTheory.NormalLayer.exists_zsmul_eq_of_cohomologyRes_subgroupRestriction_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) {n : ℕ} (u : ↑(L.H F n)) (hgen : ∀ (x : ↑((L.subgroupLayer ⊤).H F n)), ∃ (m : ℤ), x = m • (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F n)) u) (y : ↑(L.H F n)) : ∃ (m : ℤ), m • u = y

If the restriction of u to the layer of the whole Galois group generates the cohomology of that layer, then u generates the cohomology of L.