Restrictions of a finite normal layer, and its finite quotient system

Let V ◁ U be a finite normal layer of a formation, the layer K/F in field notation. Raising the ground field to an intermediate field F ⊆ E ⊆ K leaves a layer K/E, again normal because V stays normal in the smaller ground subgroup. Two layers are related by a restriction when they have the same top subgroup and the ground subgroup of the first lies in the ground subgroup of the second; LayerRestriction small big is that relation. Its relative degree is [U : U'], the degree [E : F] of the new ground field over the old one. This convention is intended to support the corestriction normalisation cor ∘ res = [E : F]; ⚠ it is the index of the subgroup U' in U, not the other way round.

Restrictions of a fixed layer are the same thing as subgroups of its Galois group: U' is recovered from H = U'/V ≤ Γ, and this finite quotient system H ↦ subgroupLayer H is what Tate's theorem quantifies over. The two directions of the correspondence appear below as NormalLayer.subgroupGround, which builds the intermediate subgroup out of H, and NormalLayer.subgroupGalEquiv, which identifies the Galois group of the resulting layer with H again.

Three facts make the system usable in the cohomological arguments downstream. The Galois group of the smaller layer maps to the Galois group of the bigger one (LayerRestriction.galHom), and does so injectively; the degrees multiply along the restriction (LayerRestriction.degree_mul_relativeDegree); and — because the two layers have the same top subgroup, hence the same coefficient module A^V — the coefficient module of the smaller layer is the coefficient module of the bigger one, restricted along galHom (LayerRestriction.repIso). It is that last identification which lets a cohomology class of the layer be restricted to a subgroup of its Galois group at all, and it is what LayerRestriction.cohomologyRes feeds to Mathlib's change-of-group map to obtain

H^n(U/V, A^V) ⟶ H^n(U'/V, A^V).

In degree zero this map is the inclusion A^U ⊆ A^{U'} of ground levels (LayerRestriction.groundLevelEquiv_cohomologyRes_zero_apply), which is what fixes its direction.

Restrictions compose (LayerRestriction.trans), and along a tower F ⊆ E ⊆ E' ⊆ K the relative degree is multiplicative, the homomorphisms of Galois groups compose, and restriction of cohomology is functorial. Inside the finite quotient system the same tower structure is indexed by an inclusion K ≤ H of subgroups of Γ, and a subgroup of the Galois group of the layer of H gives back a layer of the system (NormalLayer.subgroupLayer_subgroupLayer), so a statement quantified over all subgroups of Γ can be applied inside the layer of any one of them — which is how Tate's theorem is used downstream.

Main definitions

• TauCeti.ClassFieldTheory.LayerRestriction: the relation small is big with its ground field raised to an intermediate field.
• TauCeti.ClassFieldTheory.LayerRestriction.relativeDegree: the relative degree [U : U'].
• TauCeti.ClassFieldTheory.LayerRestriction.galHom: the induced homomorphism U'/V → U/V.
• TauCeti.ClassFieldTheory.LayerRestriction.repIso: the coefficient module of the smaller layer is the coefficient module of the bigger layer, restricted along galHom.
• TauCeti.ClassFieldTheory.LayerRestriction.trans: the composite of two restrictions.
• TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes: restriction of the cohomology of a layer along a restriction of layers.
• TauCeti.ClassFieldTheory.LayerRestriction.groundInclusion: the inclusion A^U ⊆ A^{U'} of ground levels, the degree-zero shadow of cohomologyRes.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupGround: the intermediate open subgroup attached to a subgroup of the Galois group.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer: the layer of a subgroup of the Galois group, and TauCeti.ClassFieldTheory.NormalLayer.subgroupRestriction, the restriction relating it to the layer it comes from.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupGalEquiv: the Galois group of that layer is the chosen subgroup.

Main statements

• TauCeti.ClassFieldTheory.LayerRestriction.galHom_injective: the Galois group of the smaller layer embeds in the Galois group of the bigger one.
• TauCeti.ClassFieldTheory.LayerRestriction.degree_mul_relativeDegree: [U' : V] * [U : U'] = [U : V].
• TauCeti.ClassFieldTheory.NormalLayer.degree_subgroupLayer: the layer of H has degree #H.
• TauCeti.ClassFieldTheory.NormalLayer.relativeDegree_subgroupRestriction: its relative degree is the index of H.
• TauCeti.ClassFieldTheory.NormalLayer.galHom_subgroupRestriction: the homomorphism of Galois groups it induces is the inclusion of H.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer_top: the layer of the whole Galois group is the layer itself.
• TauCeti.ClassFieldTheory.LayerRestriction.relativeDegree_trans and TauCeti.ClassFieldTheory.LayerRestriction.galHom_trans: the relative degree is multiplicative and the homomorphisms of Galois groups compose along a tower of restrictions.
• TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_trans: restriction of cohomology is functorial along a tower of restrictions.
• TauCeti.ClassFieldTheory.LayerRestriction.groundInclusion_trans: ground-level inclusions compose along a tower of restrictions.
• TauCeti.ClassFieldTheory.LayerRestriction.groundLevelEquiv_cohomologyRes_zero_apply: in degree zero, restriction of cohomology is the ground-level inclusion.
• TauCeti.ClassFieldTheory.LayerRestriction.exists_refinement: a refinement of a layer restricts to a refinement of each of its restrictions.
• TauCeti.ClassFieldTheory.LayerRestriction.cohomologyInfl_comp_cohomologyRes: restriction to an intermediate ground field commutes with inflation to a larger top field.
• TauCeti.ClassFieldTheory.NormalLayer.relativeDegree_subgroupLayerRestriction: the relative degree of a tower K ≤ H inside the finite quotient system is the relative index of K in H.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer_subgroupLayer: the layer of a subgroup of the Galois group of the layer of H is again a layer of the system.
• TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer_range_galHom: conversely, every restriction of L is the layer of a subgroup of its Galois group.

Implementation notes

LayerRestriction is a relation between two layers that already exist, not a bundle carrying a layer and constructing a second one. This is what lets the downstream restriction and corestriction maps be stated for an arbitrary pair small, big of layers, and it makes towers of restrictions compose without transporting a layer along an equality. Because it is a Prop, the relative degree cannot be read off the datum itself: relativeDegree is a function of the two layers, and takes the restriction proof to make that dependency explicit and support the notation T.relativeDegree.

NormalLayer.subgroupGround is the correspondence-theorem preimage of H — the subgroup QuotientGroup.comapMk'OrderIso attaches to H — pushed from U into the ambient group G, so that it can be an OpenSubgroup G and be compared with the other subgroups of a formation.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1–2.
• J. Neukirch, Class Field Theory, Chapter III, §1.
• J. Tate, The higher dimensional cohomology groups of class field theory, Ann. of Math. 56 (1952), 294–297.

Restrictions

structure TauCeti.ClassFieldTheory.LayerRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (small big : NormalLayer G) : Prop

A restriction of finite normal layers: small is big with its ground field raised to an intermediate field. In field notation, F ⊆ E ⊆ K takes the layer K/F to the layer K/E, so the top subgroup is unchanged and the ground subgroup shrinks.

• same_top : small.top = big.top

  a restriction does not move the top subgroup

• ground_le : small.ground ≤ big.ground

  a restriction shrinks the ground subgroup

theorem TauCeti.ClassFieldTheory.LayerRestriction.ground_toSubgroup_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : ↑small.ground ≤ ↑big.ground

The ground subgroups of a restriction, compared as subgroups of the ambient group.

theorem TauCeti.ClassFieldTheory.LayerRestriction.same_top_toSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : ↑small.top = ↑big.top

The top subgroups of a restriction, compared as subgroups of the ambient group.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.relativeDegree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (_T : LayerRestriction small big) : ℕ

The relative degree [U : U'] of a restriction, the degree of the new ground field over the old one. ⚠ U' is the subgroup, so the relative degree is the index of U' in U.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.relativeDegree_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : T.relativeDegree = (↑small.ground).relIndex ↑big.ground

The relative degree is the relative index of the two ground subgroups.

theorem TauCeti.ClassFieldTheory.LayerRestriction.degree_mul_relativeDegree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : small.degree * T.relativeDegree = big.degree

The degree of a layer is multiplicative along a restriction: [U' : V] * [U : U'] = [U : V].

theorem TauCeti.ClassFieldTheory.LayerRestriction.relativeDegree_pos {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : 0 < T.relativeDegree

The relative degree of a restriction is positive: the Galois groups involved are finite.

def TauCeti.ClassFieldTheory.LayerRestriction.galHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : small.Gal →* big.Gal

The homomorphism U'/V → U/V of Galois groups induced by a restriction. It is injective (galHom_injective), and its image is the subgroup of U/V that the intermediate subgroup U' cuts out.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.galHom_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (w : ↥small.ground) : T.galHom ↑w = ↑((Subgroup.inclusion ⋯) w)

The homomorphism of Galois groups is induced by the inclusion of ground subgroups.

theorem TauCeti.ClassFieldTheory.LayerRestriction.galHom_injective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : Function.Injective ⇑T.galHom

The Galois group of the smaller layer of a restriction embeds in the Galois group of the bigger one. Both are quotients of subgroups of U by the same top subgroup V.

theorem TauCeti.ClassFieldTheory.LayerRestriction.mk_mem_range_galHom_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (u : ↥big.ground) : ↑u ∈ T.galHom.range ↔ ↑u ∈ small.ground

An element of Gal(K/F) lies in the image of Gal(K/E) exactly when its representatives lie in the ground subgroup U' of K/E.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.repIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) : small.rep F ≅ Rep.res T.galHom (big.rep F)

The coefficient module of the smaller layer of a restriction is the coefficient module of the bigger one, read as a representation of the smaller Galois group along galHom. The two modules are the level A^V of one and the same top subgroup — a restriction does not move the top subgroup — so this isomorphism moves no element of the ambient module.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.repIso_hom_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.top)) : ↑((Rep.Hom.hom (T.repIso F).hom) x) = ↑x

The identification of coefficient modules moves no element of the ambient module.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.repIso_inv_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 big.top)) : ↑((Rep.Hom.hom (T.repIso F).inv) x) = ↑x

The inverse of the identification of coefficient modules moves no element of the ambient module either.

theorem TauCeti.ClassFieldTheory.LayerRestriction.repIso_inv_comm_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (g : ↥T.galHom.range) (x : ↥(F.level big.top)) : (Rep.Hom.hom (T.repIso F).inv).toLinearMap (((MonoidHom.comp (big.rep F).ρ T.galHom.range.subtype) g) x) = ((small.rep F).ρ ((MonoidHom.ofInjective ⋯).symm g)) ((Rep.Hom.hom (T.repIso F).inv).toLinearMap x)

The inverse identification of coefficient modules intertwines the action of the image of the smaller Galois group with the action of the smaller layer.

Towers of restrictions

theorem TauCeti.ClassFieldTheory.LayerRestriction.refl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : LayerRestriction L L

Every layer is a restriction of itself.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.galHom_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRestriction L L) : T.galHom = MonoidHom.id L.Gal

The homomorphism of Galois groups attached to the trivial restriction is the identity.

theorem TauCeti.ClassFieldTheory.LayerRestriction.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) : LayerRestriction a c

Restrictions compose: raising the ground field twice is one restriction. In field notation this is the tower F ⊆ E ⊆ E' ⊆ K.

theorem TauCeti.ClassFieldTheory.LayerRestriction.relativeDegree_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) : ⋯.relativeDegree = T.relativeDegree * T'.relativeDegree

The relative degree is multiplicative along a tower of restrictions.

theorem TauCeti.ClassFieldTheory.LayerRestriction.galHom_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) : ⋯.galHom = T'.galHom.comp T.galHom

The homomorphisms of Galois groups compose along a tower of restrictions.

theorem TauCeti.ClassFieldTheory.LayerRestriction.galHom_range_trans_le {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) : ⋯.galHom.range ≤ T'.galHom.range

Along a tower, the image of the smallest Galois group sits inside the image of the middle one.

theorem TauCeti.ClassFieldTheory.LayerRestriction.galHom_range_map_ofInjective {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) : Subgroup.map (↑(MonoidHom.ofInjective ⋯)) T.galHom.range = ⋯.galHom.range.subgroupOf T'.galHom.range

Along a tower, the image of the middle Galois group inside the largest one carries the image of the smallest to the expected subgroup.

theorem TauCeti.ClassFieldTheory.LayerRestriction.repIso_inv_hom_trans_apply {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) (x : ↥(F.level c.top)) : (Rep.Hom.hom (⋯.repIso F).inv) x = (Rep.Hom.hom (T.repIso F).inv) ((Rep.Hom.hom (T'.repIso F).inv) x)

The identifications of coefficient modules compose along a tower of restrictions. All three are the identity on the ambient module, so this is an equation between three inclusions of one and the same level.

Restriction of layer cohomology

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : big.H F n ⟶ small.H F n

Restriction of cohomology along a restriction of layers, the map

H^n(U/V, A^V) ⟶ H^n(U'/V, A^V)

induced by the inclusion U'/V ↪ U/V of Galois groups and the identification of the two coefficient modules. Both layers have the same top subgroup, so no coefficient actually moves: the map is Mathlib's change-of-group map for the inclusion.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (n : ℕ) : T.cohomologyRes F n = groupCohomology.map T.galHom (T.repIso F).inv n

Layer restriction is the group-cohomology map for the inclusion of Galois groups, with the canonical identification of coefficients.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRestriction L L) (F : Formation G) (n : ℕ) : T.cohomologyRes F n = CategoryTheory.CategoryStruct.id (L.H F n)

Restricting along the trivial restriction does nothing.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyRes_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) (n : ℕ) : ⋯.cohomologyRes F n = CategoryTheory.CategoryStruct.comp (T'.cohomologyRes F n) (T.cohomologyRes F n)

Restriction of cohomology is functorial along a tower of restrictions. Restricting from K/F to K/E and then to K/E' is restricting from K/F to K/E'.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.groundInclusion {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 big.ground) →ₗ[ℤ] ↥(F.level small.ground)

The ground-level inclusion of a restriction: raising the ground field from F to E enlarges the ground level, A^U ⊆ A^{U'}. It is the degree-zero shadow of cohomologyRes.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundInclusion_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 big.ground)) : ↑((T.groundInclusion F) x) = ↑x

The ground-level inclusion moves no element of the ambient module.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundInclusion_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRestriction L L) (F : Formation G) : T.groundInclusion F = LinearMap.id

The ground-level inclusion along the trivial layer restriction is the identity.

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundInclusion_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) : ⋯.groundInclusion F = T.groundInclusion F ∘ₗ T'.groundInclusion F

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

theorem TauCeti.ClassFieldTheory.LayerRestriction.groundLevelEquiv_cohomologyRes_zero_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (F : Formation G) (x : ↑(big.H F 0)) : (small.groundLevelEquiv F) ((ModuleCat.Hom.hom (groupCohomology.H0Iso (small.rep F)).hom) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F 0)) x)) = (T.groundInclusion F) ((big.groundLevelEquiv F) ((ModuleCat.Hom.hom (groupCohomology.H0Iso (big.rep F)).hom) x))

In degree zero, restriction of cohomology is the ground-level inclusion. Read through the identification of H⁰(U/V, A^V) with the ground level A^U, restricting a class from the layer K/F to the layer K/E is the inclusion A^U ⊆ A^{U'}. This is what fixes the direction of cohomologyRes.

Restriction and refinement

theorem TauCeti.ClassFieldTheory.LayerRestriction.exists_refinement {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big big' : NormalLayer G} (R : LayerRestriction small big) (T : LayerRefinement big big') : ∃ (small' : NormalLayer G), LayerRefinement small small' ∧ LayerRestriction small' big'

A refinement of a layer restricts to a refinement of its restriction. In field notation, for F ⊆ E ⊆ K ⊆ L with K/F and L/F Galois, the layer L/E refines K/E and is a restriction of L/F.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyInfl_comp_cohomologyRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big small' big' : NormalLayer G} (R : LayerRestriction small big) (R' : LayerRestriction small' big') (T : LayerRefinement big big') (T' : LayerRefinement small small') (F : Formation G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (R'.cohomologyRes F n) = CategoryTheory.CategoryStruct.comp (R.cohomologyRes F n) (T'.cohomologyInfl F n)

Restriction commutes with inflation. For layers K/F, K/E, L/F and L/E related by the restrictions R, R' and the refinements T, T', inflating from K/F to L/F and then restricting to L/E is restricting to K/E and then inflating to L/E.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyInfl_comp_cohomologyRes_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big small' big' : NormalLayer G} (R : LayerRestriction small big) (R' : LayerRestriction small' big') (T : LayerRefinement big big') (T' : LayerRefinement small small') (F : Formation G) (n : ℕ) {Z : ModuleCat ℤ} (h : small'.H F n ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (CategoryTheory.CategoryStruct.comp (R'.cohomologyRes F n) h) = CategoryTheory.CategoryStruct.comp (R.cohomologyRes F n) (CategoryTheory.CategoryStruct.comp (T'.cohomologyInfl F n) h)

Restriction commutes with inflation. For layers K/F, K/E, L/F and L/E related by the restrictions R, R' and the refinements T, T', inflating from K/F to L/F and then restricting to L/E is restricting to K/E and then inflating to L/E.

theorem TauCeti.ClassFieldTheory.LayerRestriction.cohomologyInfl_comp_cohomologyRes_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big small' big' : NormalLayer G} (R : LayerRestriction small big) (R' : LayerRestriction small' big') (T : LayerRefinement big big') (T' : LayerRefinement small small') (F : Formation G) (n : ℕ) (x : ↑(big.H F n)) : (CategoryTheory.ConcreteCategory.hom (R'.cohomologyRes F n)) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F n)) x) = (CategoryTheory.ConcreteCategory.hom (T'.cohomologyInfl F n)) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F n)) x)

Restriction commutes with inflation. For layers K/F, K/E, L/F and L/E related by the restrictions R, R' and the refinements T, T', inflating from K/F to L/F and then restricting to L/E is restricting to K/E and then inflating to L/E.

The finite quotient system

def TauCeti.ClassFieldTheory.NormalLayer.subgroupGround {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : Subgroup G

The intermediate subgroup V ≤ W ≤ U attached to a subgroup H of the Galois group U ⧸ V: the preimage of H in U, read inside G.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mem_subgroupGround {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) {g : G} : g ∈ L.subgroupGround H ↔ ∃ (hg : g ∈ L.ground), ↑⟨g, hg⟩ ∈ H

Membership in the intermediate subgroup: an element of U lies in it exactly when its class in the Galois group lies in H.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupGround_eq_map_comap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : L.subgroupGround H = Subgroup.map (↑L.ground).subtype (Subgroup.comap (QuotientGroup.mk' L.relativeTop) H)

The intermediate subgroup of H, written without the correspondence theorem: it is the preimage of H under the quotient map U → U ⧸ V, pushed into G. This is the form in which relative indices transport along subgroupGround.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupGround_le_ground {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : L.subgroupGround H ≤ ↑L.ground

The intermediate subgroup lies in the ground subgroup.

theorem TauCeti.ClassFieldTheory.NormalLayer.top_le_subgroupGround {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : ↑L.top ≤ L.subgroupGround H

The intermediate subgroup contains the top subgroup, which is where the layer of H gets its normality from.

def TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : NormalLayer G

The layer of a subgroup H ≤ U ⧸ V: the finite normal layer V ◁ W whose ground subgroup is the preimage W of H. The family H ↦ subgroupLayer H is the finite quotient system that Tate's theorem quantifies over.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.ground_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : ↑(L.subgroupLayer H).ground = L.subgroupGround H

The ground subgroup of the layer of H is the preimage of H.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.top_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : (L.subgroupLayer H).top = L.top

The layer of H has the same top subgroup, hence the same coefficient module, as the layer it comes from.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : LayerRestriction (L.subgroupLayer H) L

The layer of H is a restriction of the layer it comes from: it has the same top field and a smaller ground field. This is the datum through which cohomology of the layer restricts to the layer of H.

theorem TauCeti.ClassFieldTheory.NormalLayer.range_galHom_subgroupRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : ⋯.galHom.range = H

The image of the Galois group of the layer of H is H.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.subgroupGalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : (L.subgroupLayer H).Gal ≃* ↥H

The Galois group of the layer of H is H.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupGalEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) (γ : (L.subgroupLayer H).Gal) : ↑((L.subgroupGalEquiv H) γ) = ⋯.galHom γ

The identification of the Galois group of the layer of H with H is the homomorphism of Galois groups of the restriction.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : (L.subgroupLayer H).degree = Nat.card ↥H

The degree of the layer of H is the order of H.

theorem TauCeti.ClassFieldTheory.NormalLayer.galHom_subgroupRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : ⋯.galHom = H.subtype.comp (L.subgroupGalEquiv H).toMonoidHom

The homomorphism of Galois groups attached to the restriction to H is the inclusion of H, read through subgroupGalEquiv.

theorem TauCeti.ClassFieldTheory.NormalLayer.relativeDegree_subgroupRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (H : Subgroup L.Gal) : ⋯.relativeDegree = H.index

The relative degree of the restriction to H is the index of H.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupGround_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : L.subgroupGround ⊤ = ↑L.ground

The intermediate subgroup of the whole Galois group is the ground subgroup.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer_top {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : L.subgroupLayer ⊤ = L

The layer of the whole Galois group is the layer itself.

Towers inside the finite quotient system

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupGround_mono {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : Monotone L.subgroupGround

The intermediate subgroup attached to a subgroup of the Galois group grows with it.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupLayerRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {H K : Subgroup L.Gal} (h : K ≤ H) : LayerRestriction (L.subgroupLayer K) (L.subgroupLayer H)

The layer of a smaller subgroup is a restriction of the layer of a bigger one. Together with NormalLayer.subgroupRestriction this makes the finite quotient system a system of towers: K ≤ H ≤ U/V is the tower of ground fields F ⊆ E ⊆ E' ⊆ K.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupGalEquiv_galHom_subgroupLayerRestriction_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {H K : Subgroup L.Gal} (h : K ≤ H) (γ : (L.subgroupLayer K).Gal) : (L.subgroupGalEquiv H) (⋯.galHom γ) = (Subgroup.inclusion h) ((L.subgroupGalEquiv K) γ)

The homomorphism of Galois groups of a tower inside the finite quotient system is the inclusion of subgroups, read through subgroupGalEquiv.

theorem TauCeti.ClassFieldTheory.NormalLayer.relativeDegree_subgroupLayerRestriction {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {H K : Subgroup L.Gal} (h : K ≤ H) : ⋯.relativeDegree = K.relIndex H

The relative degree of a tower inside the finite quotient system is the relative index of the two subgroups.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {H : Subgroup L.Gal} (H' : Subgroup (L.subgroupLayer H).Gal) : (L.subgroupLayer H).subgroupLayer H' = L.subgroupLayer (Subgroup.map ⋯.galHom H')

The finite quotient system is closed under passing to a sublayer. The layer of a subgroup H' of the Galois group of the layer of H is the layer of the image of H' in U/V. This is what lets a statement quantified over all subgroups of U/V be applied inside the layer of one of them.

theorem TauCeti.ClassFieldTheory.NormalLayer.subgroupLayer_range_galHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) {small : NormalLayer G} (T : LayerRestriction small L) : L.subgroupLayer T.galHom.range = small

Every restriction of a layer is the layer of a subgroup of its Galois group. Together with NormalLayer.subgroupRestriction and NormalLayer.range_galHom_subgroupRestriction this is the correspondence between restrictions of L and subgroups of U ⧸ V.

The layer of a quotient of the Galois group

def TauCeti.ClassFieldTheory.NormalLayer.quotientLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (N : Subgroup L.Gal) [N.Normal] : NormalLayer G

The layer of a quotient (U ⧸ V) ⧸ N of the Galois group by a normal subgroup N: the finite normal layer W ◁ U with the same ground subgroup whose top subgroup is the preimage W of N. In field notation it is the subextension K^N / F of K / F, which L refines (NormalLayer.quotientRefinement).

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.ground_quotientLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (N : Subgroup L.Gal) [N.Normal] : (L.quotientLayer N).ground = L.ground

The layer of a quotient has the ground subgroup of the layer it comes from.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.top_quotientLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (N : Subgroup L.Gal) [N.Normal] : ↑(L.quotientLayer N).top = L.subgroupGround N

The top subgroup of the layer of (U ⧸ V) ⧸ N is the preimage of N.

theorem TauCeti.ClassFieldTheory.NormalLayer.quotientRefinement {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (N : Subgroup L.Gal) [N.Normal] : LayerRefinement (L.quotientLayer N) L

A layer refines the layer of each quotient of its Galois group: it has the same ground field and a bigger top field.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.ker_galHom_quotientRefinement {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (N : Subgroup L.Gal) [N.Normal] : ⋯.galHom.ker = N

The homomorphism of Galois groups of the refinement L of the layer of (U ⧸ V) ⧸ N has kernel N.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_quotientLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (N : Subgroup L.Gal) [N.Normal] : (L.quotientLayer N).degree = N.index

The degree of the layer of (U ⧸ V) ⧸ N is the index of N.