The inflation-restriction sequence of a refinement of layers

Let T : LayerRefinement old new enlarge the top field of a finite normal layer: in field notation old is K/F and new is L/F for a tower F ⊆ K ⊆ L of fields Galois over F, with Galois groups U/V and U/V'. The kernel V/V' of the quotient map T.galHom : U/V' → U/V is a subgroup of the Galois group of new, and its layer new.subgroupLayer T.galHom.ker is the layer L/K, a restriction of new.

This file proves that inflation from K/F and restriction to L/K form an exact sequence

Hⁿ⁺¹(U/V, A^V) ⟶ Hⁿ⁺¹(U/V', A^{V'}) ⟶ Hⁿ⁺¹(V/V', A^{V'})

as soon as Hⁱ(V/V', A^{V'}) vanishes for 0 < i ≤ n (LayerRefinement.range_cohomologyInfl_eq_ker_cohomologyRes). For a class formation H¹ of every layer vanishes, so in degree two a class of L/F is inflated from K/F exactly when its restriction to L/K vanishes. This is the finite-layer form of the statement that the classes of H² split by K are those inflated from K/F.

Main statements

• TauCeti.ClassFieldTheory.LayerRefinement.range_cohomologyInfl_eq_ker_cohomologyRes: the inflation-restriction sequence of a refinement is exact.
• TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_injective: inflation is injective when the layer of the kernel has no cohomology in lower positive degrees.
• TauCeti.ClassFieldTheory.LayerRefinement.exists_cohomologyInfl_eq_of_cohomologyRes_eq_zero: in degree two, if H¹(V/V', A^{V'}) vanishes, a class restricting to zero on L/K is inflated.
• TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree_subgroupRestriction_ker: the restriction to L/K has relative degree [K : F].

References

• J. S. Milne, Class Field Theory, v4.03, Chapter II, Proposition 1.34.
• J.-P. Serre, Local Fields, Chapter VII, §6, Proposition 5.

theorem TauCeti.ClassFieldTheory.LayerRefinement.range_cohomologyInfl_eq_ker_cohomologyRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (n : ℕ) (hH : ∀ i < n, Subsingleton ↑((new.subgroupLayer T.galHom.ker).H F (i + 1))) : (ModuleCat.Hom.hom (T.cohomologyInfl F (n + 1))).range = (ModuleCat.Hom.hom (⋯.cohomologyRes F (n + 1))).ker

The inflation-restriction sequence of a refinement of layers. For a refinement T : LayerRefinement old new, the tower F ⊆ K ⊆ L with Galois groups U/V and U/V', if Hⁱ(V/V', A^{V'}) vanishes for 0 < i ≤ n, then a class of Hⁿ⁺¹(U/V', A^{V'}) is inflated from Hⁿ⁺¹(U/V, A^V) exactly when its restriction to the layer L/K of the kernel V/V' vanishes.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_injective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (n : ℕ) (hH : ∀ i < n, Subsingleton ↑((new.subgroupLayer T.galHom.ker).H F (i + 1))) : Function.Injective ⇑(ModuleCat.Hom.hom (T.cohomologyInfl F (n + 1)))

Inflation along a refinement of layers is injective when the layer of the kernel has no cohomology below the degree. For a refinement T : LayerRefinement old new, the tower F ⊆ K ⊆ L with Galois groups U/V and U/V', if Hⁱ(V/V', A^{V'}) vanishes for 0 < i ≤ n, then inflation Hⁿ⁺¹(U/V, A^V) ⟶ Hⁿ⁺¹(U/V', A^{V'}) is injective. In degree two this needs only the vanishing of H¹ on the layer L/K.

theorem TauCeti.ClassFieldTheory.LayerRefinement.exists_cohomologyInfl_eq_of_cohomologyRes_eq_zero {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (hH : Subsingleton ↑((new.subgroupLayer T.galHom.ker).H F 1)) {y : ↑(new.H F 2)} (hy : (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F 2)) y = 0) : ∃ (x : ↑(old.H F 2)), (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) x = y

Degree-two inflation-restriction. For a refinement T : LayerRefinement old new, the tower F ⊆ K ⊆ L, if H¹ of the layer L/K vanishes, then a class of H²(L/F) whose restriction to L/K vanishes is inflated from H²(K/F).

theorem TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree_subgroupRestriction_ker {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : ⋯.relativeDegree = old.degree

The restriction to the layer L/K has relative degree [K : F]: for a refinement T : LayerRefinement old new, the index of the kernel V/V' of T.galHom in U/V' is the degree of old.