Norm quotients under a base change of coprime degree

Let V ◁ U be a finite normal layer of a formation A, the layer L/K in field notation, and let V' ◁ U' be a layer with U' ≤ U and V' ≤ V, the layer L'/K' for fields K ⊆ K' and L ⊆ L'. If the degree [K' : K] = [U : U'] is prime to the degree [L : K] = [U : V], then an element of A^U that is a norm from A^{V'} is already a norm from A^V (NormalLayer.mem_normSubgroup_of_coprime). Indeed, if x = N_{L'/K'}(y), then [K' : K] x = N_{K'/K}(x) = N_{L/K}(N_{L'/L}(y)), while [L : K] x = N_{L/K}(x), and some integer combination of the two degrees is 1. So A^U / N_{L/K}(A^V) is a quotient of a subgroup of A^{U'} / N_{L'/K'}(A^{V'}), and the order of the first norm quotient divides that of the second (NormalLayer.natCard_normQuotient_dvd_of_coprime).

The base change used in practice is the compositum with the fixed field E of an open subgroup W: the layer LE/KE, which is (V ⊓ W) ◁ (U ⊓ W) (NormalLayer.compositum). When [U : U ⊓ W] is prime to [U : V], the compositum has the same degree as the layer (NormalLayer.degree_compositum_of_coprime).

For a formation on an absolute Galois group G_K and a prime p, adjoining the p-th roots of unity is a step of degree prime to p. So a bound #(A^U / N_{U/V}(A^V)) ∣ p for the layers of degree p whose ground field contains the p-th roots of unity gives the same bound for every layer of degree p (NormalLayer.natCard_normQuotient_dvd_prime_of_adjoin_nth_roots). For the idele-class formation of a number field this is the reduction, in the proof of the second fundamental inequality for cyclic layers of prime degree, to the case where Kummer theory applies.

Restriction and corestriction between the layer and its compositum are explicit linear maps (NormalLayer.normQuotientRes and NormalLayer.normQuotientCor). Their composite multiplies by the relative ground index, and restriction is injective at coprime index. When the degrees agree, NormalLayer.compositumGalEquiv bundles the corresponding Galois-group equivalence.

Main definitions

• TauCeti.ClassFieldTheory.NormalLayer.compositum: the layer LE/KE, that is, (V ⊓ W) ◁ (U ⊓ W).

Main statements

• TauCeti.ClassFieldTheory.NormalLayer.mem_normSubgroup_of_coprime: under a base change of degree prime to the degree of the layer, an element of the ground level that becomes a norm is a norm.
• TauCeti.ClassFieldTheory.NormalLayer.natCard_normQuotient_dvd_of_coprime: the order of the norm quotient divides that of the base-changed layer.
• TauCeti.ClassFieldTheory.NormalLayer.degree_compositum_of_coprime: a compositum of coprime degree keeps the degree of the layer.
• TauCeti.ClassFieldTheory.NormalLayer.natCard_normQuotient_dvd_prime_of_adjoin_nth_roots: the reduction of the bound #(A^U / N(A^V)) ∣ p on layers of prime degree p to layers whose ground field contains the p-th roots of unity.

References

• J. S. Milne, Class Field Theory, Chapter VII, §5 (the proof of the second inequality, reduction to the case that the ground field contains the p-th roots of unity).
• J. Neukirch, Algebraic Number Theory, Chapter VI, §4 (proof of Theorem 4.4).

Base change of coprime degree

theorem TauCeti.ClassFieldTheory.NormalLayer.mem_normSubgroup_of_coprime {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {L L' : NormalLayer G} (hg : L'.ground ≤ L.ground) (ht : L'.top ≤ L.top) (hcop : ((↑L'.ground).relIndex ↑L.ground).Coprime L.degree) {x : ↥(F.level L.ground)} (hx : (Submodule.inclusion ⋯) x ∈ L'.normSubgroup F) : x ∈ L.normSubgroup F

Under a base change of coprime degree, a norm is a norm. Let L'/K' be a layer over the layer L/K, with K ⊆ K' and L ⊆ L'. If [K' : K] is prime to [L : K], an element of the ground level A^U that is a norm from the top level A^{V'} of L'/K' is a norm from A^V.

theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_normQuotient_dvd_of_coprime {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) {L L' : NormalLayer G} (hg : L'.ground ≤ L.ground) (ht : L'.top ≤ L.top) (hcop : ((↑L'.ground).relIndex ↑L.ground).Coprime L.degree) : Nat.card (L.NormQuotient F) ∣ Nat.card (L'.NormQuotient F)

The norm quotient divides under a base change of coprime degree. If L'/K' lies over the layer L/K and [K' : K] is prime to [L : K], the order of A^U / N_{L/K}(A^V) divides the order of A^{U'} / N_{L'/K'}(A^{V'}). The first is a quotient of the image of A^U in the second. Both orders are read with Nat.card, so the divisibility is vacuous when the second norm quotient is infinite.

The compositum with the fixed field of an open subgroup

def TauCeti.ClassFieldTheory.NormalLayer.compositum {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : NormalLayer G

The compositum LE/KE of the layer L/K with the fixed field E of an open subgroup W: the layer (V ⊓ W) ◁ (U ⊓ W). Normality of V ⊓ W in U ⊓ W comes from that of V in U alone; W need not be normal.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.compositum_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : (L.compositum W).ground = L.ground ⊓ W

The ground subgroup of the compositum LE/KE is U ⊓ W, cutting out KE.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.compositum_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : (L.compositum W).top = L.top ⊓ W

The top subgroup of the compositum LE/KE is V ⊓ W, cutting out LE.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_compositum_of_coprime {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (hcop : ((↑W).relIndex ↑L.ground).Coprime L.degree) : (L.compositum W).degree = L.degree

A compositum of coprime degree keeps the degree. If [U : U ⊓ W] is prime to the degree [U : V] of the layer, then the compositum (V ⊓ W) ◁ (U ⊓ W) has degree [U : V] too.

theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_normQuotient_dvd_compositum {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (hcop : ((↑W).relIndex ↑L.ground).Coprime L.degree) : Nat.card (L.NormQuotient F) ∣ Nat.card ((L.compositum W).NormQuotient F)

The norm quotient divides that of a compositum of coprime degree.

Galois groups and norm-quotient maps of a compositum

theorem TauCeti.ClassFieldTheory.NormalLayer.compositum_ground_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : (L.compositum W).ground ≤ L.ground

The ground subgroup of a compositum is contained in the original ground subgroup.

theorem TauCeti.ClassFieldTheory.NormalLayer.compositum_top_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : (L.compositum W).top ≤ L.top

The top subgroup of a compositum is contained in the original top subgroup.

def TauCeti.ClassFieldTheory.NormalLayer.compositumGalHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : (L.compositum W).Gal →* L.Gal

The homomorphism (U ⊓ W) ⧸ (V ⊓ W) → U ⧸ V from the Galois group of the base change to that of the layer, induced by the inclusion U ⊓ W ≤ U: in field notation, the restriction Gal(LE/KE) → Gal(L/K).

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.compositumGalHom_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (u : ↥(L.compositum W).ground) : (L.compositumGalHom W) ↑u = ↑((Subgroup.inclusion ⋯) u)

The homomorphism of Galois groups is induced by the inclusion U ⊓ W ≤ U.

theorem TauCeti.ClassFieldTheory.NormalLayer.compositumGalHom_injective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : Function.Injective ⇑(L.compositumGalHom W)

The Galois group of the base change embeds in the Galois group of the layer: an element of U ⊓ W that lies in V lies in V ⊓ W.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_compositum_dvd {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) : (L.compositum W).degree ∣ L.degree

The degree of the base change divides the degree of the layer.

theorem TauCeti.ClassFieldTheory.NormalLayer.compositumGalHom_bijective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (hdeg : (L.compositum W).degree = L.degree) : Function.Bijective ⇑(L.compositumGalHom W)

When the base change has the same degree as the layer, the homomorphism of Galois groups is an isomorphism.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.compositumGalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (hdeg : (L.compositum W).degree = L.degree) : (L.compositum W).Gal ≃* L.Gal

When the compositum has the same degree, restriction is an equivalence of Galois groups.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.compositumGalEquiv_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (hdeg : (L.compositum W).degree = L.degree) (u : ↥(L.compositum W).ground) : (L.compositumGalEquiv W hdeg) ↑u = ↑((Subgroup.inclusion ⋯) u)

The Galois-group equivalence restricts a quotient representative by subgroup inclusion.

Restriction and corestriction of norm quotients

theorem TauCeti.ClassFieldTheory.NormalLayer.coe_norm_compositum {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (hdeg : (L.compositum W).degree = L.degree) (a : ↥(F.level L.top)) : ↑(((L.compositum W).norm F) ((Submodule.inclusion ⋯) a)) = ↑((L.norm F) a)

When the base change has the same degree as the layer, the norm of an element of A^V along the compositum is its norm along the layer: the cosets of V ⊓ W in U ⊓ W are those of V in U.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.normQuotientRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (hdeg : (L.compositum W).degree = L.degree) : L.NormQuotient F →ₗ[ℤ] (L.compositum W).NormQuotient F

The restriction A^U / N_{U/V}(A^V) → A^{U ⊓ W} / N_{(U ⊓ W)/(V ⊓ W)}(A^{V ⊓ W}) of norm quotients to the compositum, induced by the inclusion A^U ⊆ A^{U ⊓ W}. It is defined when the compositum has the same degree as the layer, which makes every norm of the layer a norm of its compositum.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.normQuotientRes_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (hdeg : (L.compositum W).degree = L.degree) (x : ↥(F.level L.ground)) : (L.normQuotientRes W F hdeg) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((Submodule.inclusion ⋯) x)

Restriction sends the class of x ∈ A^U to the class of x in A^{U ⊓ W}.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.normQuotientCor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) : (L.compositum W).NormQuotient F →ₗ[ℤ] L.NormQuotient F

The corestriction A^{U ⊓ W} / N_{(U ⊓ W)/(V ⊓ W)}(A^{V ⊓ W}) → A^U / N_{U/V}(A^V) of norm quotients from the compositum, induced by N_{U/(U ⊓ W)} : A^{U ⊓ W} → A^U, which carries norms of the compositum to norms of the layer by transitivity of norms.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.normQuotientCor_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (y : ↥(F.level (L.compositum W).ground)) : (L.normQuotientCor W F) (Submodule.Quotient.mk y) = Submodule.Quotient.mk ((F.levelNorm ⋯) y)

Corestriction sends the class of y ∈ A^{U ⊓ W} to the class of N_{U/(U ⊓ W)} y.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.normQuotientCor_normQuotientRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (hdeg : (L.compositum W).degree = L.degree) (x : L.NormQuotient F) : (L.normQuotientCor W F) ((L.normQuotientRes W F hdeg) x) = (↑(L.compositum W).ground).relIndex ↑L.ground • x

Corestriction after restriction is multiplication by the index [U : U ⊓ W].

theorem TauCeti.ClassFieldTheory.NormalLayer.normQuotientRes_injective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (W : OpenSubgroup G) (F : Formation G) (hcop : ((↑W).relIndex ↑L.ground).Coprime L.degree) : Function.Injective ⇑(L.normQuotientRes W F ⋯)

Restriction to a compositum of coprime index is injective: a class that becomes a norm already was a norm, by mem_normSubgroup_of_coprime.

Adjoining the p-th roots of unity

theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_normQuotient_dvd_prime_of_adjoin_nth_roots {K : Type} [Field K] (F : Formation (AbsoluteGaloisGroup K)) {p : ℕ} (hp : Nat.Prime p) (h : ∀ (L' : NormalLayer (AbsoluteGaloisGroup K)), L'.degree = p → ↑L'.ground ≤ (IntermediateField.adjoin K {x : SeparableClosure K | x ^ p = 1}).fixingSubgroup → Nat.card (L'.NormQuotient F) ∣ p) (L : NormalLayer (AbsoluteGaloisGroup K)) (hL : L.degree = p) : Nat.card (L.NormQuotient F) ∣ p

Reduction to a ground field containing the p-th roots of unity. Let F be a formation on the absolute Galois group G_K and p a prime. If the norm quotient of every layer of degree p whose ground field contains the p-th roots of unity has order dividing p, then so does the norm quotient of every layer of degree p. The layer L/K is replaced by L(μ_p)/K(μ_p): the degree [K(μ_p) : K] is prime to p, so this compositum still has degree p, and the order of the norm quotient of L/K divides that of L(μ_p)/K(μ_p).