Norms along a refinement and the norm limitation theorem

Let F ⊆ K ⊆ L be a tower inside a formation, so that the layer L/F refines the layer K/F: both have ground subgroup U = G_F, and the top subgroup shrinks from V = G_K to V' = G_L. The norm of the larger layer factors through the smaller one,

N_{L/F} = N_{K/F} ∘ N_{L/K},

where N_{L/K} : A^{V'} → A^V is the norm between the two top levels (LayerRefinement.topNorm). Consequently every norm from the larger layer is a norm from the smaller one (LayerRefinement.normSubgroup_le_map). The same factorization through the norm Formation.levelNorm from an intermediate level, which need not be normal, shows that a norm from L is a norm from every intermediate field F ⊆ E ⊆ L (NormalLayer.normSubgroup_le_range_levelNorm).

The layers V ◁ G of the open normal subgroups V of G all have the ground level A^G, the level of the ground field. Reading their norm subgroups there gives one family Formation.normSubgroup F V of subgroups of A^G, indexed by V, which is monotone in V (Formation.normSubgroup_mono) and equal to A^G for V = G (Formation.normSubgroup_top).

For a class formation the two norm subgroups have finite index equal to the orders of the abelianized Galois groups (ClassFormation.natCard_normQuotient_eq_natCard_abelianization), so the inclusion is an equality exactly when those orders agree (ClassFormation.map_normSubgroup_eq_iff). Applied to an open normal subgroup V and its maximal abelian sublayer V · closure [G, G], whose Galois group G ⧸ (V · closure [G, G]) has the same order as (G ⧸ V)^ab (OpenNormalSubgroup.natCard_abelianization_gal_eq_degree_maximalAbelianLayer), this is the norm limitation theorem (ClassFormation.normSubgroup_maximalAbelianLayer): a layer and its maximal abelian sublayer have the same norm subgroup in A^G. It is a consequence of reciprocity, not of an existence theorem, and it is why a norm subgroup can only determine an abelian layer.

Main definitions

• TauCeti.ClassFieldTheory.LayerRefinement.topNorm: the norm A^{V'} → A^V between the top levels of a refinement.
• TauCeti.ClassFieldTheory.Formation.normSubgroup: the norm subgroup of the layer V ◁ G, read in the level A^G.

Main statements

• TauCeti.ClassFieldTheory.NormalLayer.norm_apply_coe_eq_explicitCor0Le: the norm of a layer is relative degree-zero corestriction from its top subgroup to its ground subgroup.
• TauCeti.ClassFieldTheory.LayerRefinement.topNorm_trans: top-level norms compose along a tower of refinements.
• TauCeti.ClassFieldTheory.LayerRefinement.groundEquiv_norm_topNorm: transitivity of the norm along a refinement.
• TauCeti.ClassFieldTheory.LayerRefinement.normSubgroup_le_map: refining a layer shrinks its norm subgroup.
• TauCeti.ClassFieldTheory.Formation.mem_normSubgroup_iff_mem_map: the norm subgroup of V ◁ G read in the ground level of a refinement V' ◁ G.
• TauCeti.ClassFieldTheory.Formation.normSubgroup_mono: the norm subgroup of V ◁ G is monotone in V.
• TauCeti.ClassFieldTheory.NormalLayer.normSubgroup_le_range_levelNorm and TauCeti.ClassFieldTheory.Formation.normSubgroup_le_range_levelNorm: a norm from a layer is a norm from every intermediate level, normal or not.
• TauCeti.ClassFieldTheory.ClassFormation.map_normSubgroup_eq_iff: in a class formation a refinement keeps the norm subgroup exactly when it keeps the order of the abelianized Galois group.
• TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_maximalAbelianLayer: norm limitation.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.
• J. Neukirch, Class Field Theory, Chapter III, Theorem 5.5 (Corollary).
• J.-P. Serre, Local Fields, Chapter XI, §3.

The norm of a layer as a level norm

theorem TauCeti.ClassFieldTheory.NormalLayer.norm_apply_coe_eq_explicitCor0Le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (x : ↥(F.level L.top)) : ↑((L.norm F) x) = ↑((ContCohomology.explicitCor0Le G ↑F.toRep ↑L.ground ↑L.top ⋯) ((F.levelEquivH0 L.top) x))

The norm N_{U/V} : A^V → A^U of a layer is Tau Ceti's relative degree-zero corestriction ContCohomology.explicitCor0Le from the top subgroup V to the ground subgroup U, read on levels.

theorem TauCeti.ClassFieldTheory.NormalLayer.normSubgroup_le_range_levelNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) {W : OpenSubgroup G} (hT : L.top ≤ W) (hW : W ≤ L.ground) : (L.normSubgroup F).toAddSubgroup ≤ (F.levelNorm hW).range

A norm from a layer is a norm from every intermediate level. If V ≤ W ≤ U for the layer V ◁ U, then N_{U/V}(A^V) ⊆ N_{U/W}(A^W), the subgroup W not being required to be normal in U: in field notation, for F ⊆ E ⊆ K with K/F Galois, a norm from K is a norm from E.

The norm between the top levels of a refinement

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.topNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) : ↥(F.level new.top) →+ ↥(F.level old.top)

The norm N_{V/V'} : A^{V'} → A^V between the top levels of a refinement, whose top subgroup shrinks from V to V': the norm Formation.levelNorm between the two top levels, evaluated by topNorm_apply_coe. In field notation it is the norm N_{L/K} for F ⊆ K ⊆ L.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.topNorm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (x : ↥(F.level new.top)) : ↑((T.topNorm F) x) = ∑ᶠ (q : ↥↑old.top ⧸ (↑new.top).subgroupOf ↑old.top), (F.toRep.ρ ↑(Quotient.out q)) ↑x

The norm between the top levels of a refinement is the sum of the translates by coset representatives, read in the ambient module: N_{V/V'} x = ∑ ρ(g) x over the representatives g = q.out of the cosets q ∈ V/V'.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.topNorm_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {L : NormalLayer G} (T : LayerRefinement L L) : T.topNorm F = AddMonoidHom.id ↥(F.level L.top)

The norm along the trivial refinement is the identity.

theorem TauCeti.ClassFieldTheory.LayerRefinement.topNorm_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) : ⋯.topNorm F = (T.topNorm F).comp (T'.topNorm F)

Top-level norms compose along a tower of refinements.

theorem TauCeti.ClassFieldTheory.LayerRefinement.groundEquiv_norm_topNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (x : ↥(F.level new.top)) : (T.groundEquiv F) ((old.norm F) ((T.topNorm F) x)) = (new.norm F) x

Transitivity of the norm along a refinement: N_{L/F} = N_{K/F} ∘ N_{L/K}, the two ground levels being identified by groundEquiv.

theorem TauCeti.ClassFieldTheory.LayerRefinement.normSubgroup_le_map {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) : new.normSubgroup F ≤ Submodule.map (↑(T.groundEquiv F)) (old.normSubgroup F)

Refining a layer shrinks its norm subgroup: a norm from the larger top level A^{V'} is a norm from the smaller top level A^V, so N_{L/F}(L) ⊆ N_{K/F}(K) for F ⊆ K ⊆ L.

The norm subgroups of the layers of open normal subgroups

noncomputable def TauCeti.ClassFieldTheory.Formation.normSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (V : OpenNormalSubgroup G) : Submodule ℤ ↥(F.level ⊤)

The norm subgroup of the layer V ◁ G of an open normal subgroup V, read in the level A^G of the whole group through NormalLayer.groundEquivOfOpenNormal. In field notation it is N_{L/K}(A_L) ⊆ A_K for the finite Galois extension L/K cut out by V. Unlike NormalLayer.normSubgroup, which lives in the ground level of its own layer, these subgroups share one carrier, so the norm subgroups of different V can be compared.

theorem TauCeti.ClassFieldTheory.Formation.mem_normSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} {V : OpenNormalSubgroup G} {a : ↥(F.level ⊤)} : a ∈ F.normSubgroup V ↔ (NormalLayer.groundEquivOfOpenNormal F V) a ∈ (NormalLayer.ofOpenNormal V).normSubgroup F

An element of A^G lies in the norm subgroup of V exactly when, read in the ground level of the layer V ◁ G, it lies in the norm subgroup of that layer.

theorem TauCeti.ClassFieldTheory.Formation.mem_normSubgroup_iff_mem_map {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} {V V' : OpenNormalSubgroup G} (h : V' ≤ V) {a : ↥(F.level ⊤)} : a ∈ F.normSubgroup V ↔ (NormalLayer.groundEquivOfOpenNormal F V') a ∈ Submodule.map (↑(⋯.groundEquiv F)) ((NormalLayer.ofOpenNormal V).normSubgroup F)

For V' ≤ V, an element of A^G lies in the norm subgroup of V exactly when, read in the ground level of the finer layer V' ◁ G, it lies in the norm subgroup of V ◁ G moved there by the ground-level identification of the refinement.

theorem TauCeti.ClassFieldTheory.Formation.normSubgroup_mono {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : Monotone F.normSubgroup

Norm subgroups are monotone in the open normal subgroup. If V' ≤ V, then the extension cut out by V' contains the one cut out by V, and every norm from the larger extension is a norm from the smaller one.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.normSubgroup_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : F.normSubgroup ⊤ = ⊤

The layer of the whole group has the whole level A^G as its norm subgroup: it cuts out the ground field itself, whose norm to itself is the identity.

theorem TauCeti.ClassFieldTheory.Formation.normSubgroup_le_range_levelNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {V : OpenNormalSubgroup G} {W : OpenSubgroup G} (h : V.toOpenSubgroup ≤ W) : (F.normSubgroup V).toAddSubgroup ≤ (F.levelNorm ⋯).range

A norm from the layer of V is a norm from every open subgroup containing V. For an open subgroup W ≥ V, not necessarily normal, the norm subgroup of V ◁ G lies in the image of the norm N_{G/W} : A^W → A^G: in field notation, for a finite extension E/K inside the Galois extension L/K cut out by V, N_{L/K}(A_L) ⊆ N_{E/K}(A_E).

Norm limitation

theorem TauCeti.ClassFieldTheory.ClassFormation.map_normSubgroup_eq_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {old new : NormalLayer G} (T : LayerRefinement old new) : Submodule.map (↑(T.groundEquiv F)) (old.normSubgroup F) = new.normSubgroup F ↔ Nat.card (Abelianization old.Gal) = Nat.card (Abelianization new.Gal)

In a class formation, a refinement keeps the norm subgroup exactly when it keeps the order of the abelianized Galois group. By reciprocity the two norm quotients have the orders of the two abelianized Galois groups, and the norm subgroup of the refined layer lies in that of the original one.

theorem TauCeti.ClassFieldTheory.ClassFormation.normSubgroup_maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (V : OpenNormalSubgroup G) : F.normSubgroup V.maximalAbelianLayer = F.normSubgroup V

Norm limitation. In a class formation, the layer V ◁ G of an open normal subgroup and its maximal abelian sublayer V · closure [G, G] have the same norm subgroup in A^G: the norm group of a finite Galois extension is the norm group of its maximal abelian subextension.