Refinements of a finite normal layer, and inflation

Let V ◁ U be a finite normal layer of a formation, the layer K/F in field notation. Enlarging the top field to a field K ⊆ L that is still Galois over F gives a layer L/F: its top subgroup V' ≤ V is again normal in the same ground subgroup U. Two layers are related by a refinement when they have the same ground subgroup and the top subgroup of the second lies in the top subgroup of the first; LayerRefinement old new is that relation. Its relative degree is [V : V'], the degree [L : K] of the new top field over the old one.

A refinement is the dual of a restriction (LayerRestriction): there the top subgroup is fixed and the ground subgroup shrinks. Where a restriction induces an injection of Galois groups and leaves the coefficient module alone, a refinement induces the surjection

LayerRefinement.galHom : U/V' → U/V,

whose kernel is V/V' (LayerRefinement.galHom_mk_eq_one_iff), and a genuine enlargement of coefficient modules, the inclusion A^V ⊆ A^{V'} of levels. That inclusion is equivariant along galHom (LayerRefinement.repHom), and Mathlib's change-of-group map for the pair is inflation

LayerRefinement.cohomologyInfl : H^n(U/V, A^V) ⟶ H^n(U/V', A^{V'}),

the map along the quotient U/V' → U/V which reads a cochain on U/V with values in (A^{V'})^{V/V'} = A^V as a cochain on U/V'. In degree zero it is the identity of the common ground level A^U (LayerRefinement.groundLevelEquiv_cohomologyInfl_zero_apply).

Refinements compose (LayerRefinement.trans): along a tower F ⊆ K ⊆ L ⊆ M of top fields the relative degree is multiplicative, the Galois-group quotients compose, and inflation is functorial. In positive degree the Tate groups are the ordinary cohomology groups, and inflation of Tate cohomology, LayerRefinement.tateInfl, is cohomologyInfl read through that identification. The parallel maps trivialCohomologyInfl and trivialTateInfl inflate the trivial integral coefficients that form the source of Tate's class-formation isomorphism. Both kinds of inflation compose along towers. Any two layers over the same ground, in particular any two refinements of one layer, have a common refinement, the compositum of the two top fields, whose top subgroup is the intersection of the two top subgroups (LayerRefinement.exists_commonRefinement). This is what lets the invariant of a class, defined by inflating it to some refinement, be compared across refinements.

Main definitions

• TauCeti.ClassFieldTheory.LayerRefinement: the relation new is old with its top field enlarged.
• TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree: the relative degree [V : V'].
• TauCeti.ClassFieldTheory.LayerRefinement.galHom: the quotient map U/V' → U/V.
• TauCeti.ClassFieldTheory.LayerRefinement.repHom: the inclusion A^V ⊆ A^{V'} of coefficient modules, equivariant along galHom.
• TauCeti.ClassFieldTheory.LayerRefinement.groundEquiv: the identity of the common ground level.
• TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl: inflation of layer cohomology.
• TauCeti.ClassFieldTheory.LayerRefinement.tateInfl: inflation of layer Tate cohomology, in positive degrees.
• TauCeti.ClassFieldTheory.LayerRefinement.trivialCohomologyInfl and TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl: the corresponding inflation maps for trivial integral coefficients.

Main statements

• TauCeti.ClassFieldTheory.LayerRefinement.galHom_surjective and TauCeti.ClassFieldTheory.LayerRefinement.galHom_mk_eq_one_iff: the map of Galois groups is the quotient by V/V'.
• TauCeti.ClassFieldTheory.LayerRefinement.galHom_ofOpenNormal_mk_eq_one_iff: for the layers of open normal subgroups V' ≤ V, the kernel of G ⧸ V' → G ⧸ V is V ⧸ V'.
• TauCeti.ClassFieldTheory.LayerRefinement.degree_mul_relativeDegree: [U : V] * [V : V'] = [U : V'].
• TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree_trans, TauCeti.ClassFieldTheory.LayerRefinement.galHom_trans, TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_trans and TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_trans, together with their trivialCohomologyInfl_trans and trivialTateInfl_trans counterparts: towers of refinements.
• TauCeti.ClassFieldTheory.LayerRefinement.groundLevelEquiv_cohomologyInfl_zero_apply: in degree zero, inflation is the identity of the ground level.
• TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_comp_tateHIsoH_hom: in positive degree, Tate inflation is ordinary inflation.
• TauCeti.ClassFieldTheory.LayerRefinement.exists_commonRefinement: two layers over the same ground have a common refinement.

Implementation notes

As for LayerRestriction, a refinement is a Prop-valued relation between two layers that already exist, so refinements of arbitrary pairs of layers can be composed without transporting a layer along an equality. The two ground subgroups are equal but their coercions to types are not the same type, which is why galHom is Mathlib's QuotientGroup.quotientMapSubgroupOfOfLe rather than a quotient map on one fixed group.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§1–2.
• J. Neukirch, Class Field Theory, Chapter III, §1.
• J.-P. Serre, Local Fields, Chapter VII, §5, and Chapter XI, §1.

Refinements

structure TauCeti.ClassFieldTheory.LayerRefinement {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (old new : NormalLayer G) : Prop

A refinement of finite normal layers: new is old with its top field enlarged. In field notation, F ⊆ K ⊆ L takes the layer K/F to the layer L/F, so the ground subgroup is unchanged and the top subgroup shrinks.

• same_ground : old.ground = new.ground

  a refinement does not move the ground subgroup

• top_le : new.top ≤ old.top

  a refinement shrinks the top subgroup

theorem TauCeti.ClassFieldTheory.LayerRefinement.same_ground_toSubgroup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : ↑old.ground = ↑new.ground

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

theorem TauCeti.ClassFieldTheory.LayerRefinement.top_toSubgroup_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : ↑new.top ≤ ↑old.top

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

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (_T : LayerRefinement old new) : ℕ

The relative degree [V : V'] of a refinement, the degree of the new top field over the old one.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : T.relativeDegree = (↑new.top).relIndex ↑old.top

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

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

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

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

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

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

The homomorphism U/V' → U/V of Galois groups induced by a refinement. It is surjective (galHom_surjective) with kernel V/V' (galHom_mk_eq_one_iff).

@[simp]

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

The homomorphism of Galois groups sends the class of an element of U to its class.

theorem TauCeti.ClassFieldTheory.LayerRefinement.galHom_surjective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : Function.Surjective ⇑T.galHom

The Galois group of the old layer is a quotient of the Galois group of the new one.

theorem TauCeti.ClassFieldTheory.LayerRefinement.galHom_mk_eq_one_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (w : ↥new.ground) : T.galHom ↑w = 1 ↔ ↑w ∈ old.top

The kernel of the homomorphism of Galois groups is V/V': the class of an element of U dies in U/V exactly when the element lies in the old top subgroup.

theorem TauCeti.ClassFieldTheory.LayerRefinement.level_top_le {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 old.top ≤ F.level new.top

The old top level sits inside the new one: a smaller subgroup fixes more elements.

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.repHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) : Rep.res T.galHom (old.rep F) ⟶ new.rep F

The inclusion A^V ⊆ A^{V'} of coefficient modules, equivariant along the quotient map galHom of Galois groups: an element of U acts on an element of A^V in the same way whether the element is read in A^V or in A^{V'}.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.repHom_hom_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 old.top)) : ↑((Rep.Hom.hom (T.repHom F)) x) = ↑x

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

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.groundEquiv {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 old.ground) ≃ₗ[ℤ] ↥(F.level new.ground)

The ground-level identification of a refinement: both layers have the same ground subgroup U, hence the same ground level A^U.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.groundEquiv_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 old.ground)) : ↑((T.groundEquiv F) x) = ↑x

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

theorem TauCeti.ClassFieldTheory.LayerRefinement.ofOpenNormal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V V' : OpenNormalSubgroup G} (h : V' ≤ V) : LayerRefinement (NormalLayer.ofOpenNormal V) (NormalLayer.ofOpenNormal V')

The layers V ◁ ⊤ of two nested open normal subgroups V' ≤ V form a refinement: the finite Galois extension cut out by V' contains the one cut out by V.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.groundEquiv_groundEquivOfOpenNormal {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 ⊤)) : (⋯.groundEquiv F) ((NormalLayer.groundEquivOfOpenNormal F V) a) = (NormalLayer.groundEquivOfOpenNormal F V') a

For nested open normal subgroups V' ≤ V, the identifications of A^G with the ground levels of the layers V ◁ G and V' ◁ G agree along the refinement of the first layer by the second.

theorem TauCeti.ClassFieldTheory.LayerRefinement.galHom_ofOpenNormal_mk_eq_one_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V V' : OpenNormalSubgroup G} (h : V' ≤ V) (w : ↥(NormalLayer.ofOpenNormal V').ground) : ⋯.galHom ↑w = 1 ↔ ↑w ∈ V

For nested open normal subgroups V' ≤ V, the class of w ∈ G in the Galois group G ⧸ V' dies in G ⧸ V exactly when w ∈ V.

Towers of refinements

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

Every layer is a refinement of itself.

@[simp]

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

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

theorem TauCeti.ClassFieldTheory.LayerRefinement.repHom_self_toLinearMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRefinement L L) (F : Formation G) : (Rep.Hom.hom (T.repHom F)).toLinearMap = (Rep.Hom.hom (CategoryTheory.CategoryStruct.id (L.rep F))).toLinearMap

The coefficient map attached to the trivial refinement is the identity on underlying linear maps.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) : LayerRefinement a c

Refinements compose: enlarging the top field twice is one refinement. In field notation this is the tower F ⊆ K ⊆ L ⊆ M.

theorem TauCeti.ClassFieldTheory.LayerRefinement.relativeDegree_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) : ⋯.relativeDegree = T.relativeDegree * T'.relativeDegree

The relative degree is multiplicative along a tower of refinements: [V : V''] = [V : V'] * [V' : V''].

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

The quotient maps of Galois groups compose along a tower of refinements.

theorem TauCeti.ClassFieldTheory.LayerRefinement.repHom_trans_toLinearMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) (F : Formation G) : (Rep.Hom.hom (⋯.repHom F)).toLinearMap = (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor T'.galHom).map (T.repHom F)) (T'.repHom F))).toLinearMap

The coefficient inclusions compose along a tower of refinements, on underlying linear maps.

Inflation of layer cohomology

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (n : ℕ) : old.H F n ⟶ new.H F n

Inflation of cohomology along a refinement of layers, the map

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

induced by the quotient map U/V' → U/V of Galois groups and the inclusion A^V ⊆ A^{V'} of coefficient modules: Mathlib's change-of-group map for that pair. It has the shape of Mathlib's inflation groupCohomology.infNatTrans, the change-of-group map along G → G ⧸ S and the inclusion of S-invariants, with U/V' → U/V in place of G → G ⧸ S and A^V = (A^{V'})^{V/V'} in place of the invariants.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (n : ℕ) : T.cohomologyInfl F n = groupCohomology.map T.galHom (T.repHom F) n

Inflation is Mathlib's cohomology map for the quotient homomorphism and coefficient inclusion attached to the refinement.

@[simp]

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

Inflating along the trivial refinement does nothing.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) (F : Formation G) (n : ℕ) : ⋯.cohomologyInfl F n = CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (T'.cohomologyInfl F n)

Inflation of cohomology is functorial along a tower of refinements. Inflating from K/F to L/F and then to M/F is inflating from K/F to M/F.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_trans_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) (F : Formation G) (n : ℕ) (x : ↑(a.H F n)) : (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyInfl F n)) x = (CategoryTheory.ConcreteCategory.hom (T'.cohomologyInfl F n)) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F n)) x)

Inflation of cohomology is functorial along a tower of refinements. Inflating from K/F to L/F and then to M/F is inflating from K/F to M/F.

Inflation with trivial coefficients

def TauCeti.ClassFieldTheory.LayerRefinement.trivialRepHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : Rep.res T.galHom (Rep.trivial ℤ old.Gal ℤ) ⟶ Rep.trivial ℤ new.Gal ℤ

The identity of ℤ as a morphism from the restriction of the trivial representation of the old Galois group to the trivial representation of the new Galois group.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialRepHom_hom_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (x : ℤ) : (Rep.Hom.hom T.trivialRepHom) x = x

The trivial-coefficient morphism moves no integer.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialRepHom_self_toLinearMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRefinement L L) : (Rep.Hom.hom T.trivialRepHom).toLinearMap = (Rep.Hom.hom (CategoryTheory.CategoryStruct.id (Rep.trivial ℤ L.Gal ℤ))).toLinearMap

The trivial-coefficient morphism of a trivial refinement is the identity on underlying linear maps.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialRepHom_trans_toLinearMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) : (Rep.Hom.hom ⋯.trivialRepHom).toLinearMap = (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor T'.galHom).map T.trivialRepHom) T'.trivialRepHom)).toLinearMap

Trivial-coefficient morphisms compose along a tower, on underlying linear maps.

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.trivialCohomologyInfl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (n : ℕ) : old.TrivialH n ⟶ new.TrivialH n

Inflation of ordinary cohomology with trivial integral coefficients along a refinement of layers.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialCohomologyInfl_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (n : ℕ) : T.trivialCohomologyInfl n = groupCohomology.map T.galHom T.trivialRepHom n

Trivial-coefficient inflation is the ordinary change-of-group map along the quotient homomorphism of a refinement.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialCohomologyInfl_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRefinement L L) (n : ℕ) : T.trivialCohomologyInfl n = CategoryTheory.CategoryStruct.id (L.TrivialH n)

Inflating trivial-coefficient cohomology along the trivial refinement does nothing.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialCohomologyInfl_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) (n : ℕ) : ⋯.trivialCohomologyInfl n = CategoryTheory.CategoryStruct.comp (T.trivialCohomologyInfl n) (T'.trivialCohomologyInfl n)

Inflation of ordinary cohomology with trivial coefficients is functorial along a tower of refinements.

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (r : ℕ) [NeZero r] : old.TrivialTateH ↑r ⟶ new.TrivialTateH ↑r

Inflation of positive-degree Tate cohomology with trivial integral coefficients along a refinement of layers.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (r : ℕ) [NeZero r] : T.trivialTateInfl r = CategoryTheory.CategoryStruct.comp (old.trivialTateHIsoH r).hom (CategoryTheory.CategoryStruct.comp (T.trivialCohomologyInfl r) (new.trivialTateHIsoH r).inv)

Trivial-coefficient Tate inflation is ordinary inflation transported across the canonical positive-degree comparisons.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_comp_trivialTateHIsoH_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (r : ℕ) [NeZero r] : CategoryTheory.CategoryStruct.comp (T.trivialTateInfl r) (new.trivialTateHIsoH r).hom = CategoryTheory.CategoryStruct.comp (old.trivialTateHIsoH r).hom (T.trivialCohomologyInfl r)

Trivial-coefficient Tate inflation is ordinary inflation read through the canonical positive-degree comparisons with ordinary cohomology.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_comp_trivialTateHIsoH_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (r : ℕ) [NeZero r] {Z : ModuleCat ℤ} (h : new.TrivialH r ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.trivialTateInfl r) (CategoryTheory.CategoryStruct.comp (new.trivialTateHIsoH r).hom h) = CategoryTheory.CategoryStruct.comp (old.trivialTateHIsoH r).hom (CategoryTheory.CategoryStruct.comp (T.trivialCohomologyInfl r) h)

Trivial-coefficient Tate inflation is ordinary inflation read through the canonical positive-degree comparisons with ordinary cohomology.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRefinement L L) (r : ℕ) [NeZero r] : T.trivialTateInfl r = CategoryTheory.CategoryStruct.id (L.TrivialTateH ↑r)

Inflating positive-degree Tate cohomology with trivial coefficients along the trivial refinement does nothing.

theorem TauCeti.ClassFieldTheory.LayerRefinement.trivialTateInfl_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) (r : ℕ) [NeZero r] : ⋯.trivialTateInfl r = CategoryTheory.CategoryStruct.comp (T.trivialTateInfl r) (T'.trivialTateInfl r)

Inflation of positive-degree Tate cohomology with trivial coefficients is functorial along a tower of refinements.

theorem TauCeti.ClassFieldTheory.LayerRefinement.groundLevelEquiv_cohomologyInfl_zero_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (x : ↑(old.H F 0)) : (new.groundLevelEquiv F) ((ModuleCat.Hom.hom (groupCohomology.H0Iso (new.rep F)).hom) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 0)) x)) = (T.groundEquiv F) ((old.groundLevelEquiv F) ((ModuleCat.Hom.hom (groupCohomology.H0Iso (old.rep F)).hom) x))

In degree zero, inflation of cohomology is the identity of the ground level. Read through the identification of H⁰(U/V, A^V) with the ground level A^U, inflating a class from the layer K/F to the layer L/F does not move it.

noncomputable def TauCeti.ClassFieldTheory.LayerRefinement.tateInfl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (r : ℕ) [NeZero r] : old.TateH F ↑r ⟶ new.TateH F ↑r

Inflation of Tate cohomology along a refinement of layers, in positive degrees only: Ĥ^r(U/V, A^V) ⟶ Ĥ^r(U/V', A^{V'}) for r ≠ 0. In positive degree the Tate groups of a layer are its ordinary cohomology groups (NormalLayer.tateHIsoH), and Tate inflation is cohomologyInfl read through that identification at both layers.

theorem TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (r : ℕ) [NeZero r] : T.tateInfl F r = CategoryTheory.CategoryStruct.comp (old.tateHIsoH F r).hom (CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F r) (new.tateHIsoH F r).inv)

Tate inflation is ordinary inflation read through the identifications tateHIsoH of positive-degree Tate cohomology with ordinary cohomology at the two layers.

theorem TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_comp_tateHIsoH_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (r : ℕ) [NeZero r] : CategoryTheory.CategoryStruct.comp (T.tateInfl F r) (new.tateHIsoH F r).hom = CategoryTheory.CategoryStruct.comp (old.tateHIsoH F r).hom (T.cohomologyInfl F r)

Tate inflation commutes with the identifications of positive-degree Tate cohomology with ordinary cohomology: inflating a Tate class and reading it as an ordinary class is inflating the ordinary class.

theorem TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_comp_tateHIsoH_hom_assoc {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (r : ℕ) [NeZero r] {Z : ModuleCat ℤ} (h : new.H F r ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.tateInfl F r) (CategoryTheory.CategoryStruct.comp (new.tateHIsoH F r).hom h) = CategoryTheory.CategoryStruct.comp (old.tateHIsoH F r).hom (CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F r) h)

Tate inflation commutes with the identifications of positive-degree Tate cohomology with ordinary cohomology: inflating a Tate class and reading it as an ordinary class is inflating the ordinary class.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRefinement L L) (F : Formation G) (r : ℕ) [NeZero r] : T.tateInfl F r = CategoryTheory.CategoryStruct.id (L.TateH F ↑r)

Inflating Tate cohomology along the trivial refinement does nothing.

theorem TauCeti.ClassFieldTheory.LayerRefinement.tateInfl_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) (F : Formation G) (r : ℕ) [NeZero r] : ⋯.tateInfl F r = CategoryTheory.CategoryStruct.comp (T.tateInfl F r) (T'.tateInfl F r)

Inflation of Tate cohomology is functorial along a tower of refinements, in every positive degree.

Common refinements

theorem TauCeti.ClassFieldTheory.LayerRefinement.exists_commonRefinement {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L₁ L₂ : NormalLayer G} (h : L₁.ground = L₂.ground) : ∃ (newer : NormalLayer G), LayerRefinement L₁ newer ∧ LayerRefinement L₂ newer

Two layers over the same ground have a common refinement. In field notation, two Galois extensions L₁/F and L₂/F are both contained in their compositum, whose layer has top subgroup V₁ ⊓ V₂. Applied to two refinements of one layer, this is what lets a construction made at "some refinement" of a layer be compared across refinements.