Maps of coefficient modules on finite normal layers

A G-equivariant map φ : A → A' between the coefficient modules of two formations on G carries every level A^U into the level A'^U. On a finite normal layer V ◁ U it therefore induces a map A^V → A'^V of the coefficient modules of the layer, equivariant for the Galois group U ⧸ V; this is NormalLayer.repMap, through which a map of formations acts on the cohomology L.H F n of the layer.

Taking V-invariants is only left exact. A short exact sequence 0 → A → A' → A'' → 0 of coefficient modules gives a short exact sequence 0 → A^V → A'^V → A''^V → 0 on the layer exactly when every V-invariant element of A'' lifts to a V-invariant element of A', which is NormalLayer.shortExact_repMap. For the sequence 0 → (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ} → 0 of a number field this lifting is Hilbert 90 for the top subgroup, and the resulting sequence 0 → Lˣ → I_L → C_L → 0 is the source of the long exact sequence relating the cohomology of the multiplicative, idele and idele-class formations of a layer.

Main definitions

• TauCeti.ClassFieldTheory.NormalLayer.repMap: the map of layer coefficient modules induced by an equivariant map of coefficient modules.

Main statements

• TauCeti.ClassFieldTheory.Formation.map_mem_level: an equivariant map preserves levels.
• TauCeti.ClassFieldTheory.NormalLayer.shortExact_repMap: a short exact sequence of coefficient modules stays short exact on a layer once invariants of the top subgroup lift.
• TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_map_repMap, TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_comp_map_repMap and TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_hom_comp_map_repMap: inflation, restriction and conjugation of layer cohomology commute with the maps of cohomology induced by a map of coefficient modules.

theorem TauCeti.ClassFieldTheory.Formation.map_mem_level {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) {U : OpenSubgroup G} {x : ↑F.toRep} (hx : x ∈ F.level U) : (Rep.Hom.hom φ) x ∈ F'.level U

An equivariant map of coefficient modules preserves levels: it carries an element fixed by U to an element fixed by U.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.repMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (L : NormalLayer G) (φ : F.toRep ⟶ F'.toRep) : L.rep F ⟶ L.rep F'

The map of layer coefficient modules induced by a map of coefficient modules: an equivariant map A → A' restricts to a map A^V → A'^V of top levels, equivariant for the Galois group of the layer. Composing with groupCohomology.map or groupCohomology.functor makes a map of formations act on the cohomology of the layer.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.repMap_hom_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (L : NormalLayer G) (φ : F.toRep ⟶ F'.toRep) (x : ↥(F.level L.top)) : ↑((Rep.Hom.hom (L.repMap φ)) x) = (Rep.Hom.hom φ) ↑x

repMap φ applies φ to an element of the top level.

theorem TauCeti.ClassFieldTheory.NormalLayer.repMap_comp {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' F'' : Formation G} (L : NormalLayer G) (φ : F.toRep ⟶ F'.toRep) (ψ : F'.toRep ⟶ F''.toRep) : L.repMap (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (L.repMap φ) (L.repMap ψ)

repMap is functorial: it carries a composite to the composite.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.repMap_id {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (L : NormalLayer G) : L.repMap (CategoryTheory.CategoryStruct.id F.toRep) = CategoryTheory.CategoryStruct.id (L.rep F)

repMap carries the identity to the identity.

theorem TauCeti.ClassFieldTheory.NormalLayer.repMap_comp_eq_zero {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' F'' : Formation G} (L : NormalLayer G) {φ : F.toRep ⟶ F'.toRep} {ψ : F'.toRep ⟶ F''.toRep} (hφψ : Function.Exact ⇑(Rep.Hom.hom φ) ⇑(Rep.Hom.hom ψ)) : CategoryTheory.CategoryStruct.comp (L.repMap φ) (L.repMap ψ) = 0

The maps of layer coefficient modules induced by an exact pair of coefficient maps compose to zero.

theorem TauCeti.ClassFieldTheory.NormalLayer.shortExact_repMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' F'' : Formation G} (L : NormalLayer G) {φ : F.toRep ⟶ F'.toRep} {ψ : F'.toRep ⟶ F''.toRep} (hφ : Function.Injective ⇑(Rep.Hom.hom φ)) (hφψ : Function.Exact ⇑(Rep.Hom.hom φ) ⇑(Rep.Hom.hom ψ)) (hψ : ∀ y ∈ F''.level L.top, ∃ x ∈ F'.level L.top, (Rep.Hom.hom ψ) x = y) : { X₁ := L.rep F, X₂ := L.rep F', X₃ := L.rep F'', f := L.repMap φ, g := L.repMap ψ, zero := ⋯ }.ShortExact

A short exact sequence of coefficient modules stays short exact on a layer V ◁ U once every V-invariant element of the third module lifts to a V-invariant element of the second. Injectivity and exactness in the middle pass to the top levels unconditionally; the lifting hypothesis is exactly the surjectivity of A'^V → A''^V, which in general is obstructed by H¹(V, A).

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_map_repMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} {old new : NormalLayer G} (T : LayerRefinement old new) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) : CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (groupCohomology.map (MonoidHom.id new.Gal) (new.repMap φ) n) = CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id old.Gal) (old.repMap φ) n) (T.cohomologyInfl F' n)

Inflation commutes with maps of coefficient modules: for a refinement V' ◁ U of a layer V ◁ U and an equivariant map φ : A → A' of coefficient modules, inflating from H^n(U/V, A^V) to H^n(U/V', A^{V'}) and then applying φ is applying φ and then inflating from H^n(U/V, A'^V).

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_map_repMap_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} {old new : NormalLayer G} (T : LayerRefinement old new) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) {Z : ModuleCat ℤ} (h : groupCohomology (new.rep F') n ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id new.Gal) (new.repMap φ) n) h) = CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id old.Gal) (old.repMap φ) n) (CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F' n) h)

Inflation commutes with maps of coefficient modules: for a refinement V' ◁ U of a layer V ◁ U and an equivariant map φ : A → A' of coefficient modules, inflating from H^n(U/V, A^V) to H^n(U/V', A^{V'}) and then applying φ is applying φ and then inflating from H^n(U/V, A'^V).

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_map_repMap_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} {old new : NormalLayer G} (T : LayerRefinement old new) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) (x : ↑(old.H F n)) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id new.Gal) (new.repMap φ) n)) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F n)) x) = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F' n)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id old.Gal) (old.repMap φ) n)) x)

Inflation commutes with maps of coefficient modules: for a refinement V' ◁ U of a layer V ◁ U and an equivariant map φ : A → A' of coefficient modules, inflating from H^n(U/V, A^V) to H^n(U/V', A^{V'}) and then applying φ is applying φ and then inflating from H^n(U/V, A'^V).

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_comp_map_repMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} {small big : NormalLayer G} (R : LayerRestriction small big) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) : CategoryTheory.CategoryStruct.comp (R.cohomologyRes F n) (groupCohomology.map (MonoidHom.id small.Gal) (small.repMap φ) n) = CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id big.Gal) (big.repMap φ) n) (R.cohomologyRes F' n)

Restriction commutes with maps of coefficient modules: for a restriction K/E of a layer K/F and an equivariant map φ : A → A' of coefficient modules, restricting a class of H^n(Gal(K/F), A^V) and then applying φ is applying φ and then restricting.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_comp_map_repMap_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} {small big : NormalLayer G} (R : LayerRestriction small big) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) {Z : ModuleCat ℤ} (h : groupCohomology (small.rep F') n ⟶ Z) : CategoryTheory.CategoryStruct.comp (R.cohomologyRes F n) (CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id small.Gal) (small.repMap φ) n) h) = CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id big.Gal) (big.repMap φ) n) (CategoryTheory.CategoryStruct.comp (R.cohomologyRes F' n) h)

Restriction commutes with maps of coefficient modules: for a restriction K/E of a layer K/F and an equivariant map φ : A → A' of coefficient modules, restricting a class of H^n(Gal(K/F), A^V) and then applying φ is applying φ and then restricting.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_comp_map_repMap_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} {small big : NormalLayer G} (R : LayerRestriction small big) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) (x : ↑(big.H F n)) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id small.Gal) (small.repMap φ) n)) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F n)) x) = (CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F' n)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id big.Gal) (big.repMap φ) n)) x)

Restriction commutes with maps of coefficient modules: for a restriction K/E of a layer K/F and an equivariant map φ : A → A' of coefficient modules, restricting a class of H^n(Gal(K/F), A^V) and then applying φ is applying φ and then restricting.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_hom_comp_map_repMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (L : NormalLayer G) (g : G) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) : CategoryTheory.CategoryStruct.comp (L.conjugateCohomologyIso F g n).hom (groupCohomology.map (MonoidHom.id (L.conjugate g).Gal) ((L.conjugate g).repMap φ) n) = CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) n) (L.conjugateCohomologyIso F' g n).hom

Conjugation commutes with maps of coefficient modules: for g in the ambient group and an equivariant map φ : A → A' of coefficient modules, conjugating a class of H^n(U/V, A^V) by g and then applying φ is applying φ and then conjugating, since φ (g • x) = g • φ x.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_hom_comp_map_repMap_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (L : NormalLayer G) (g : G) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) {Z : ModuleCat ℤ} (h : groupCohomology ((L.conjugate g).rep F') n ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.conjugateCohomologyIso F g n).hom (CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id (L.conjugate g).Gal) ((L.conjugate g).repMap φ) n) h) = CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) n) (CategoryTheory.CategoryStruct.comp (L.conjugateCohomologyIso F' g n).hom h)

Conjugation commutes with maps of coefficient modules: for g in the ambient group and an equivariant map φ : A → A' of coefficient modules, conjugating a class of H^n(U/V, A^V) by g and then applying φ is applying φ and then conjugating, since φ (g • x) = g • φ x.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_hom_comp_map_repMap_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (L : NormalLayer G) (g : G) (φ : F.toRep ⟶ F'.toRep) (n : ℕ) (x : ↑(L.H F n)) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id (L.conjugate g).Gal) ((L.conjugate g).repMap φ) n)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g n).hom) x) = (CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F' g n).hom) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) n)) x)

Conjugation commutes with maps of coefficient modules: for g in the ambient group and an equivariant map φ : A → A' of coefficient modules, conjugating a class of H^n(U/V, A^V) by g and then applying φ is applying φ and then conjugating, since φ (g • x) = g • φ x.