Norms between levels, and the ground-level norm of a restriction

Let T : LayerRestriction small big be a restriction of finite normal layers, the layer K/F restricted to K/E for an intermediate field F ⊆ E ⊆ K, with ground subgroups U' ≤ U. On ground levels a restriction has the inclusion A^U ⊆ A^{U'} (LayerRestriction.groundInclusion) and, in the other direction, the norm N_{U/U'} : A^{U'} → A^U, the sum of the translates of an element by representatives of the cosets U/U'. It is the map the Artin–Tate functoriality diagram artinMap_groundNorm is stated against.

The norm is not a new construction. The level A^W of an open subgroup is the degree-zero cohomology H⁰(W, A) of W acting on the coefficient module (Formation.levelEquivH0), and the norm Formation.levelNorm between the levels of any open subgroups W' ≤ W is Tau Ceti's relative degree-zero corestriction ContCohomology.explicitCor0Le along W' ≤ W, read on levels. The ground-level norm of a restriction is its instance W = U, W' = U'.

Main definitions

• TauCeti.ClassFieldTheory.Formation.levelNorm: the norm A^{W'} → A^W between the levels of open subgroups W' ≤ W.
• TauCeti.ClassFieldTheory.LayerRestriction.groundNorm: the norm A^{U'} → A^U between the ground levels of a restriction.

Main statements

• TauCeti.ClassFieldTheory.Formation.levelNorm_top_apply_coe: the norm to the level of G is the sum of the translates by representatives of the cosets in G.
• TauCeti.ClassFieldTheory.Formation.levelNorm_inclusion: the norm of an element of the larger level A^W is its multiple by the index [W : W'].
• TauCeti.ClassFieldTheory.Formation.levelNorm_trans: norms between levels compose along a tower of open subgroups.
• TauCeti.ClassFieldTheory.NormalLayer.toAddMonoidHom_norm: the norm of a layer is the norm Formation.levelNorm between its top and ground levels.
• TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_apply_coe: the norm is the sum of the translates by coset representatives.
• TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_groundInclusion: the norm of an element of the ground level A^U is its multiple by the relative degree.
• TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_trans: ground-level norms compose along a tower of restrictions.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1–2.
• J. S. Milne, Class Field Theory, Chapter II, 1.29–1.30 (the norm along a subgroup).

The norm between two levels

noncomputable def TauCeti.ClassFieldTheory.Formation.levelNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W W' : OpenSubgroup G} (h : W' ≤ W) : ↥(F.level W') →+ ↥(F.level W)

The norm N_{W/W'} : A^{W'} → A^W between the levels of open subgroups W' ≤ W: the relative degree-zero corestriction ContCohomology.explicitCor0Le along W' ≤ W, read on levels (levelEquivH0_levelNorm) and evaluated by levelNorm_apply_coe. The subgroup W' need not be normal in W.

theorem TauCeti.ClassFieldTheory.Formation.levelEquivH0_levelNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W W' : OpenSubgroup G} (h : W' ≤ W) (x : ↥(F.level W')) : (F.levelEquivH0 W) ((F.levelNorm h) x) = (ContCohomology.explicitCor0Le G ↑F.toRep ↑W ↑W' ⋯) ((F.levelEquivH0 W') x)

Read in degree-zero cohomology, the norm between two levels is the relative corestriction ContCohomology.explicitCor0Le.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelNorm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W W' : OpenSubgroup G} (h : W' ≤ W) (x : ↥(F.level W')) : ↑((F.levelNorm h) x) = ∑ᶠ (q : ↥↑W ⧸ (↑W').subgroupOf ↑W), (F.toRep.ρ ↑(Quotient.out q)) ↑x

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

theorem TauCeti.ClassFieldTheory.Formation.levelNorm_top_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W' : OpenSubgroup G} (h : W' ≤ ⊤) (x : ↥(F.level W')) : ↑((F.levelNorm h) x) = ∑ᶠ (q : G ⧸ ↑W'), (F.toRep.ρ (Quotient.out q)) ↑x

The norm from a level to the level of the whole group G is the sum of the translates by representatives of the cosets of W' in G: N_{G/W'} x = ∑ ρ(g) x over the representatives g = q.out of the cosets q ∈ G/W'.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelNorm_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W : OpenSubgroup G} (h : W ≤ W) : F.levelNorm h = AddMonoidHom.id ↥(F.level W)

The norm from a level to itself is the identity.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelNorm_inclusion {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W W' : OpenSubgroup G} (h : W' ≤ W) (x : ↥(F.level W)) : (F.levelNorm h) ((Submodule.inclusion ⋯) x) = (↑W').relIndex ↑W • x

The norm of an element of the larger level A^W is its multiple by the index [W : W'].

theorem TauCeti.ClassFieldTheory.Formation.levelNorm_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {W W' W'' : OpenSubgroup G} (h : W' ≤ W) (h' : W'' ≤ W') : F.levelNorm ⋯ = (F.levelNorm h).comp (F.levelNorm h')

Norms between levels compose along a tower W'' ≤ W' ≤ W of open subgroups.

The norm of a layer as a level norm

theorem TauCeti.ClassFieldTheory.NormalLayer.toAddMonoidHom_norm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : (L.norm F).toAddMonoidHom = F.levelNorm ⋯

The norm N_{U/V} : A^V → A^U of a layer is the norm Formation.levelNorm between its top and ground levels.

The norm between the ground levels of a restriction

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.groundNorm {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) : ↥(F.level small.ground) →+ ↥(F.level big.ground)

The norm N_{U/U'} : A^{U'} → A^U along a restriction U' ≤ U of ground subgroups: the norm Formation.levelNorm between the two ground levels, evaluated by groundNorm_apply_coe. The subgroup U' need not be normal in U, so this is not the norm of a layer.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(F.level small.ground)) : ↑((T.groundNorm F) x) = ∑ᶠ (q : ↥↑big.ground ⧸ (↑small.ground).subgroupOf ↑big.ground), (F.toRep.ρ ↑(Quotient.out q)) ↑x

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

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_groundInclusion {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↥(F.level big.ground)) : (T.groundNorm F) ((T.groundInclusion F) x) = T.relativeDegree • x

The norm of an element of the ground level A^U is its multiple by the relative degree.

Towers

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRestriction L L) (F : Formation G) : T.groundNorm F = AddMonoidHom.id ↥(F.level L.ground)

The norm along the trivial layer restriction is the identity.

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundNorm_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) : ⋯.groundNorm F = (T'.groundNorm F).comp (T.groundNorm F)

Ground-level norms compose along a tower of layer restrictions.