Conjugation of a finite normal layer

An element g of the ambient group carries a finite normal layer V ◁ U of a formation to the layer gVg⁻¹ ◁ gUg⁻¹. In field notation g is an automorphism of the big extension, and the conjugate layer is the layer gK/gF obtained by transporting K/F along it. This file builds that layer and the maps it induces, on the levels of the formation and on the cohomology of the layer.

The conjugate subgroups are obtained by pulling U and V back along x ↦ g⁻¹xg, which is continuous, so the conjugate layer is again a layer of open subgroups (NormalLayer.conjugate). Conjugation is an action: it is trivial at 1 and composes (NormalLayer.conjugate_one, NormalLayer.conjugate_conjugate). Unlike a restriction or a refinement, conjugation moves both subgroups of the layer, so it changes neither the Galois group nor the coefficient module up to isomorphism: NormalLayer.conjugateGalEquiv identifies U/V with gUg⁻¹/gVg⁻¹, and the degree of the layer is unchanged (NormalLayer.degree_conjugate).

On the coefficient side the map is the action of g itself. If x is fixed by U then g · x is fixed by gUg⁻¹, so acting by g is an isomorphism A^U ≃ A^{gUg⁻¹} of levels (Formation.levelConjEquiv); applied to the top and ground subgroups of a layer this gives NormalLayer.conjugateCoefficientEquiv and NormalLayer.conjugateGroundLevelEquiv. The two isomorphisms intertwine: g · (u · x) = (gug⁻¹) · (g · x). That single identity (NormalLayer.conjugateCoefficientEquiv_rep_apply) is what feeds both

• NormalLayer.conjugateCohomologyIso, conjugation on ordinary group cohomology H^n(U/V, A^V) ≅ H^n(gUg⁻¹/gVg⁻¹, A^{gVg⁻¹}), obtained from Mathlib's change-of-group isomorphism; and
• NormalLayer.conjugateTateIso, conjugation on the Tate groups in every integer degree, obtained from TauCeti.TateCohomology.mapIso, the functoriality of Tate cohomology in a compatible pair.

Three compatibilities fix the direction of these maps and let conjugation be read on the norm quotient A^U / N_{U/V}(A^V), the group the Artin map of a class formation lands in: in degree zero the cohomological map is the action of g on the ground level (NormalLayer.groundLevelEquiv_conjugateCohomologyIso_zero_apply), and conjugation carries the norm of a layer to the norm of the conjugate layer (NormalLayer.norm_conjugateCoefficientEquiv), hence its norm subgroup onto the norm subgroup there (NormalLayer.map_normSubgroup_conjugateGroundLevelEquiv). Finally, NormalLayer.tateHZeroEquivNormQuotient_conjugateTateIso_apply identifies degree-zero Tate conjugation with the resulting map on norm quotients.

Main definitions

• TauCeti.ClassFieldTheory.NormalLayer.conjugate: the conjugate layer gVg⁻¹ ◁ gUg⁻¹.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv: the induced isomorphism U/V ≃* gUg⁻¹/gVg⁻¹ of Galois groups.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundHom: inverse conjugation gUg⁻¹ → U, as a continuous homomorphism of ground subgroups.
• TauCeti.ClassFieldTheory.Formation.levelConjEquiv: acting by g is an isomorphism A^U ≃ A^{gUg⁻¹} of levels.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv and TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundLevelEquiv: that isomorphism at the top and at the ground subgroup of a layer.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso and TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso: conjugation on the ordinary and Tate cohomology of a layer.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv: conjugation on the norm quotient of a layer.

Main statements

• TauCeti.ClassFieldTheory.NormalLayer.conjugate_one and TauCeti.ClassFieldTheory.NormalLayer.conjugate_conjugate: conjugation of layers is an action of the ambient group.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_one, TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_trans_conjugateCohomologyIso, TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_one and TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_trans_conjugateTateIso: the induced maps on ordinary and Tate cohomology satisfy the same action laws, up to transport along conjugate_one and conjugate_conjugate; the Galois-group and norm-quotient equivalences satisfy matching transported laws, while the maps on ground subgroups, coefficient modules and ground levels satisfy them on underlying elements.
• TauCeti.ClassFieldTheory.NormalLayer.degree_conjugate: a conjugate layer has the same degree.
• TauCeti.ClassFieldTheory.NormalLayer.card_gal_conjugate: its simp-normal form, on the orders of the Galois groups.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv_rep_apply: the isomorphisms of Galois groups and of coefficient modules intertwine, restated as TauCeti.ClassFieldTheory.NormalLayer.isIntertwiningMap_conjugateCoefficientEquiv.
• TauCeti.ClassFieldTheory.NormalLayer.groundLevelEquiv_conjugateCohomologyIso_zero_apply: in degree zero, conjugation of cohomology is the action of g on the ground level.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_hom_tateHIsoH_inv: in positive degrees, conjugation of Tate cohomology is conjugation of ordinary cohomology.
• TauCeti.ClassFieldTheory.NormalLayer.norm_conjugateCoefficientEquiv and TauCeti.ClassFieldTheory.NormalLayer.map_normSubgroup_conjugateGroundLevelEquiv: conjugation commutes with the norm of a layer and carries its norm subgroup onto that of the conjugate layer.
• TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv_mk: conjugation on norm quotients sends the class of a representative to the class of its conjugate.
• TauCeti.ClassFieldTheory.NormalLayer.tateHZeroEquivNormQuotient_conjugateTateIso_apply: conjugation commutes with the canonical identification of degree-zero Tate cohomology with the norm quotient.
• TauCeti.ClassFieldTheory.LayerRefinement.conjugate and TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_conjugateCohomologyIso_hom: conjugation carries refinements to refinements and commutes with inflation.

Implementation notes

NormalLayer.conjugate takes the comap of x ↦ g⁻¹xg rather than the image of x ↦ gxg⁻¹, so that membership in the conjugate subgroups is definitionally the membership condition g⁻¹xg ∈ U and needs no image lemma to use.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Chapter I, §5.

Conjugation of levels

theorem TauCeti.ClassFieldTheory.Formation.ρ_mem_level_conj {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (g : G) {U U' : OpenSubgroup G} (h : ∀ (x : G), g * x * g⁻¹ ∈ U' → x ∈ U) {a : ↑F.toRep} (ha : a ∈ F.level U) : (F.toRep.ρ g) a ∈ F.level U'

Conjugation carries a level into the level of the conjugate subgroup. If U' is the conjugate gUg⁻¹ then acting by g takes an element fixed by U to an element fixed by U'.

def TauCeti.ClassFieldTheory.Formation.levelConjEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (g : G) {U U' : OpenSubgroup G} (h : ∀ (x : G), g * x * g⁻¹ ∈ U' ↔ x ∈ U) : ↥(F.level U) ≃ₗ[ℤ] ↥(F.level U')

Conjugation of levels: acting by g is an isomorphism A^U ≃ A^{gUg⁻¹}. The hypothesis says that U' is the conjugate gUg⁻¹.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelConjEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (g : G) {U U' : OpenSubgroup G} (h : ∀ (x : G), g * x * g⁻¹ ∈ U' ↔ x ∈ U) (a : ↥(F.level U)) : ↑((F.levelConjEquiv g h) a) = (F.toRep.ρ g) ↑a

levelConjEquiv acts by g on underlying elements.

@[simp]

theorem TauCeti.ClassFieldTheory.Formation.levelConjEquiv_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (g : G) {U U' : OpenSubgroup G} (h : ∀ (x : G), g * x * g⁻¹ ∈ U' ↔ x ∈ U) (b : ↥(F.level U')) : ↑((F.levelConjEquiv g h).symm b) = (F.toRep.ρ g⁻¹) ↑b

The inverse of levelConjEquiv acts by g⁻¹ on underlying elements.

theorem TauCeti.ClassFieldTheory.Formation.levelConjEquiv_comp_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (g h : G) {U₁ U₂ U₃ U₄ : OpenSubgroup G} (hh : ∀ (x : G), h * x * h⁻¹ ∈ U₂ ↔ x ∈ U₁) (hg : ∀ (x : G), g * x * g⁻¹ ∈ U₃ ↔ x ∈ U₂) (hgh : ∀ (x : G), g * h * x * (g * h)⁻¹ ∈ U₄ ↔ x ∈ U₁) (a : ↥(F.level U₁)) : ↑((F.levelConjEquiv g hg) ((F.levelConjEquiv h hh) a)) = ↑((F.levelConjEquiv (g * h) hgh) a)

Conjugating a level by h and then by g agrees on underlying elements with conjugating by g * h.

The conjugate layer

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

The conjugate layer gVg⁻¹ ◁ gUg⁻¹ of a finite normal layer V ◁ U. In field notation it is the layer gK/gF obtained by transporting K/F along the automorphism g of the big extension.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mem_ground_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) {x : G} : x ∈ (L.conjugate g).ground ↔ g⁻¹ * x * g ∈ L.ground

Membership in the ground subgroup of the conjugate layer.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.mem_top_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) {x : G} : x ∈ (L.conjugate g).top ↔ g⁻¹ * x * g ∈ L.top

Membership in the top subgroup of the conjugate layer.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugate_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : L.conjugate 1 = L

Conjugating by 1 does nothing.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugate_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g h : G) : (L.conjugate h).conjugate g = L.conjugate (g * h)

Conjugation of layers composes, so it is an action of the ambient group on the layers of a formation. The later conjugating element g occurs on the left in the product g * h.

theorem TauCeti.ClassFieldTheory.NormalLayer.conj_mem_ground_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) {x : G} : g * x * g⁻¹ ∈ (L.conjugate g).ground ↔ x ∈ L.ground

The conjugate gug⁻¹ of an element of the ground subgroup lies in the ground subgroup of the conjugate layer, and only then.

theorem TauCeti.ClassFieldTheory.NormalLayer.conj_mem_top_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) {x : G} : g * x * g⁻¹ ∈ (L.conjugate g).top ↔ x ∈ L.top

The conjugate gvg⁻¹ of an element of the top subgroup lies in the top subgroup of the conjugate layer, and only then.

theorem TauCeti.ClassFieldTheory.NormalLayer.toSubgroup_ground_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : ↑(L.conjugate g).ground = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ↑L.ground

The ground subgroup of the conjugate layer is the conjugate gUg⁻¹ of the ground subgroup, read as the image of U under conjugation by g.

The Galois group of a conjugate layer

def TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : ↥L.ground ≃* ↥(L.conjugate g).ground

Conjugation by g as an isomorphism U ≃* gUg⁻¹ of the ground subgroups of a layer and its conjugate.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (u : ↥L.ground) : ↑((L.conjugateGroundEquiv g) u) = g * ↑u * g⁻¹

On elements of G, the ground-subgroup equivalence is conjugation u ↦ g * u * g⁻¹.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundEquiv_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (v : ↥(L.conjugate g).ground) : ↑((L.conjugateGroundEquiv g).symm v) = g⁻¹ * ↑v * g

On elements of G, the inverse ground-subgroup equivalence is conjugation v ↦ g⁻¹ * v * g.

def TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : ↥↑(L.conjugate g).ground →ₜ* ↥↑L.ground

Inverse conjugation v ↦ g⁻¹ v g, the inverse ground-subgroup equivalence, as a continuous homomorphism from the ground subgroup gUg⁻¹ of the conjugate layer to the ground subgroup U of the layer.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundHom_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (v : ↥↑(L.conjugate g).ground) : ↑((L.conjugateGroundHom g) v) = g⁻¹ * ↑v * g

On elements of G, the inverse-conjugation homomorphism is v ↦ g⁻¹ * v * g.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundHom_smul {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) {M : Type} [AddMonoid M] [DistribMulAction G M] (v : ↥↑(L.conjugate g).ground) (m : M) : (DistribSMul.toAddMonoidHom M g) ((L.conjugateGroundHom g) v • m) = v • (DistribSMul.toAddMonoidHom M g) m

The action of g on M and inverse conjugation form a compatible pair.

theorem TauCeti.ClassFieldTheory.NormalLayer.map_relativeTop_conjugateGroundEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : Subgroup.map (↑(L.conjugateGroundEquiv g)) L.relativeTop = (L.conjugate g).relativeTop

Conjugation carries the top subgroup of a layer, read inside its ground subgroup, onto the corresponding subgroup of the conjugate layer. This is what lets it descend to Galois groups.

def TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : L.Gal ≃* (L.conjugate g).Gal

Conjugation by g as an isomorphism U/V ≃* gUg⁻¹/gVg⁻¹ of Galois groups.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (u : ↥L.ground) : (L.conjugateGalEquiv g) ↑u = ↑((L.conjugateGroundEquiv g) u)

The Galois-group equivalence sends the class of a representative u to the class of its conjugate g * u * g⁻¹.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv_symm_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) (v : ↥(L.conjugate g).ground) : (L.conjugateGalEquiv g).symm ↑v = ↑((L.conjugateGroundEquiv g).symm v)

The inverse Galois-group equivalence sends the class of a representative to the class of its inverse-conjugate.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.card_gal_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : Fintype.card (L.conjugate g).Gal = Fintype.card L.Gal

A conjugate layer has a Galois group of the same order. This is the simp-normal form of degree_conjugate: simp rewrites degree to Fintype.card of the Galois group via degree_eq_natCard_gal, and this lemma then identifies the two cardinalities.

theorem TauCeti.ClassFieldTheory.NormalLayer.degree_conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g : G) : (L.conjugate g).degree = L.degree

A conjugate layer has the same degree. Not @[simp], since its left-hand side is not in simp-normal form; simp proves it through card_gal_conjugate.

Conjugation of the levels and the coefficient module of a layer

def TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) : ↥(F.level L.top) ≃ₗ[ℤ] ↥(F.level (L.conjugate g).top)

Conjugation on the coefficient module of a layer: acting by g is an isomorphism A^V ≃ A^{gVg⁻¹}.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (x : ↥(F.level L.top)) : ↑((L.conjugateCoefficientEquiv F g) x) = (F.toRep.ρ g) ↑x

The coefficient equivalence acts by g on underlying elements.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (y : ↥(F.level (L.conjugate g).top)) : ↑((L.conjugateCoefficientEquiv F g).symm y) = (F.toRep.ρ g⁻¹) ↑y

The inverse coefficient equivalence acts by g⁻¹ on underlying elements.

def TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundLevelEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) : ↥(F.level L.ground) ≃ₗ[ℤ] ↥(F.level (L.conjugate g).ground)

Conjugation on the ground level of a layer: acting by g is an isomorphism A^U ≃ A^{gUg⁻¹}. This is the map the Artin map of a class formation is conjugated by.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundLevelEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (x : ↥(F.level L.ground)) : ↑((L.conjugateGroundLevelEquiv F g) x) = (F.toRep.ρ g) ↑x

The ground-level equivalence acts by g on underlying elements.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundLevelEquiv_symm_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (y : ↥(F.level (L.conjugate g).ground)) : ↑((L.conjugateGroundLevelEquiv F g).symm y) = (F.toRep.ρ g⁻¹) ↑y

The inverse ground-level equivalence acts by g⁻¹ on underlying elements.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv_rep_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (γ : L.Gal) (x : ↥(F.level L.top)) : (L.conjugateCoefficientEquiv F g) (((L.rep F).ρ γ) x) = (((L.conjugate g).rep F).ρ ((L.conjugateGalEquiv g) γ)) ((L.conjugateCoefficientEquiv F g) x)

The isomorphisms of Galois groups and of coefficient modules intertwine: g · (γ · x) = (gγg⁻¹) · (g · x).

theorem TauCeti.ClassFieldTheory.NormalLayer.isIntertwiningMap_conjugateCoefficientEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) : (L.rep F).ρ.IsIntertwiningMap (MonoidHom.comp ((L.conjugate g).rep F).ρ ↑(L.conjugateGalEquiv g)) ↑(L.conjugateCoefficientEquiv F g)

Conjugation is a compatible pair of a group isomorphism and an isomorphism of coefficient modules, the datum TauCeti.TateCohomology.mapIso consumes.

Conjugation of the cohomology of a layer

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (n : ℕ) : L.H F n ≅ (L.conjugate g).H F n

Conjugation on the ordinary cohomology of a layer, the isomorphism

H^n(U/V, A^V) ≅ H^n(gUg⁻¹/gVg⁻¹, A^{gVg⁻¹})

induced by the isomorphism of Galois groups and the action of g on the coefficients.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_def {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (n : ℕ) : L.conjugateCohomologyIso F g n = groupCohomology.mapIso (L.conjugateGalEquiv g) (L.conjugateCoefficientEquiv F g) ⋯ n

Conjugation on ordinary cohomology is Mathlib's groupCohomology.mapIso of the isomorphism of Galois groups and the action of g on the coefficients.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (r : ℤ) : L.TateH F r ≅ (L.conjugate g).TateH F r

Conjugation on the Tate cohomology of a layer, in every integer degree. In the degrees where Mathlib compares Tate cohomology with ordinary cohomology or homology, it is the ordinary change-of-group map of that theory, by TauCeti.TateCohomology.map_comp_isoGroupCohomology_hom and TauCeti.TateCohomology.map_comp_isoGroupHomology_hom.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (r : ℤ) : (L.conjugateTateIso F g r).hom = TateCohomology.map ⋯ r

Conjugation on Tate cohomology is the Tate map of the compatible pair isIntertwiningMap_conjugateCoefficientEquiv.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_hom_tateHIsoH_inv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (n : ℕ) [NeZero n] (u : ↑(L.H F n)) : (CategoryTheory.ConcreteCategory.hom (L.conjugateTateIso F g ↑n).hom) ((CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F n).inv) u) = (CategoryTheory.ConcreteCategory.hom ((L.conjugate g).tateHIsoH F n).inv) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g n).hom) u)

In positive degrees, conjugation of Tate cohomology is conjugation of ordinary cohomology, through the identifications tateHIsoH of a layer and its conjugate.

theorem TauCeti.ClassFieldTheory.NormalLayer.groundLevelEquiv_conjugateCohomologyIso_zero_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (x : ↑(L.H F 0)) : ((L.conjugate g).groundLevelEquiv F) ((ModuleCat.Hom.hom (groupCohomology.H0Iso ((L.conjugate g).rep F)).hom) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 0).hom) x)) = (L.conjugateGroundLevelEquiv F g) ((L.groundLevelEquiv F) ((ModuleCat.Hom.hom (groupCohomology.H0Iso (L.rep F)).hom) x))

In degree zero, conjugation of cohomology is the action of g on the ground level. Read through the identification of H⁰(U/V, A^V) with A^U, conjugating a class is applying g to the corresponding element of the ground level. This is what fixes the direction of conjugateCohomologyIso.

Conjugation and the norm of a layer

theorem TauCeti.ClassFieldTheory.NormalLayer.norm_conjugateCoefficientEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (x : ↥(F.level L.top)) : ((L.conjugate g).norm F) ((L.conjugateCoefficientEquiv F g) x) = (L.conjugateGroundLevelEquiv F g) ((L.norm F) x)

Conjugation commutes with the norm of a layer: the isomorphism of Galois groups permutes the summands of N_{U/V}.

theorem TauCeti.ClassFieldTheory.NormalLayer.map_normSubgroup_conjugateGroundLevelEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) : Submodule.map (↑(L.conjugateGroundLevelEquiv F g)) (L.normSubgroup F) = (L.conjugate g).normSubgroup F

Conjugation carries the norm subgroup of a layer onto the norm subgroup of the conjugate layer, so it descends to an isomorphism of the norm quotients the Artin map of a class formation is read on.

noncomputable def TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) : L.NormQuotient F ≃+ (L.conjugate g).NormQuotient F

Conjugation on the norm quotient: acting by g on the ground level descends through the norm subgroups of a layer and its conjugate.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (x : ↥(F.level L.ground)) : (L.conjugateNormQuotientEquiv F g) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((L.conjugateGroundLevelEquiv F g) x)

Conjugation on norm quotients sends the class of a ground-level element to the class of its conjugate.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv_symm_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (y : ↥(F.level (L.conjugate g).ground)) : (L.conjugateNormQuotientEquiv F g).symm (Submodule.Quotient.mk y) = Submodule.Quotient.mk ((L.conjugateGroundLevelEquiv F g).symm y)

The inverse norm-quotient equivalence sends the class of a ground-level element to the class of its inverse conjugate.

theorem TauCeti.ClassFieldTheory.NormalLayer.tateHZeroEquivNormQuotient_conjugateTateIso_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g : G) (x : ↑(L.TateH F 0)) : ((L.conjugate g).tateHZeroEquivNormQuotient F) ((CategoryTheory.ConcreteCategory.hom (L.conjugateTateIso F g 0).hom) x) = (L.conjugateNormQuotientEquiv F g) ((L.tateHZeroEquivNormQuotient F) x)

In degree zero, conjugation on Tate cohomology is conjugation on the norm quotient.

Conjugation by 1 and by a product

conjugate_one and conjugate_conjugate make conjugation an action on layers. The maps it induces satisfy the matching laws. On subgroups and levels these are stated on underlying elements, where no transport is needed; on cohomology they are stated up to the eqToIso along those two equalities of layers.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundEquiv_conjugateGroundEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g h : G) (u : ↥L.ground) : ↑(((L.conjugate h).conjugateGroundEquiv g) ((L.conjugateGroundEquiv h) u)) = ↑((L.conjugateGroundEquiv (g * h)) u)

Conjugating the ground subgroup by h and then by g is conjugating it by g * h.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCoefficientEquiv_conjugateCoefficientEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g h : G) (x : ↥(F.level L.top)) : ↑(((L.conjugate h).conjugateCoefficientEquiv F g) ((L.conjugateCoefficientEquiv F h) x)) = ↑((L.conjugateCoefficientEquiv F (g * h)) x)

Conjugating the coefficient module of a layer by h and then by g is conjugating it by g * h.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGroundLevelEquiv_conjugateGroundLevelEquiv_apply_coe {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g h : G) (x : ↥(F.level L.ground)) : ↑(((L.conjugate h).conjugateGroundLevelEquiv F g) ((L.conjugateGroundLevelEquiv F h) x)) = ↑((L.conjugateGroundLevelEquiv F (g * h)) x)

Conjugating the ground level of a layer by h and then by g is conjugating it by g * h.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : (L.conjugateGalEquiv 1).trans (MulEquiv.cast ⋯) = MulEquiv.refl L.Gal

Conjugation by 1 is the identity on the Galois group, after transporting along conjugate_one.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv_trans_conjugateGalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g h : G) : (L.conjugateGalEquiv h).trans ((L.conjugate h).conjugateGalEquiv g) = (L.conjugateGalEquiv (g * h)).trans (MulEquiv.cast ⋯)

Conjugation composes on the Galois group: conjugating by h and then by g is conjugating by g * h, up to transport along conjugate_conjugate.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) : (L.conjugateNormQuotientEquiv F 1).trans (AddEquiv.cast ⋯) = AddEquiv.refl (L.NormQuotient F)

Conjugation by 1 is the identity on the norm quotient, after transporting along conjugate_one.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateNormQuotientEquiv_trans_conjugateNormQuotientEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g h : G) : (L.conjugateNormQuotientEquiv F h).trans ((L.conjugate h).conjugateNormQuotientEquiv F g) = (L.conjugateNormQuotientEquiv F (g * h)).trans (AddEquiv.cast ⋯)

Conjugation composes on the norm quotient: conjugating by h and then by g is conjugating by g * h, up to transport along conjugate_conjugate.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (n : ℕ) : L.conjugateCohomologyIso F 1 n = CategoryTheory.eqToIso ⋯

Conjugation by 1 is the identity on ordinary cohomology, up to the transport along conjugate_one.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateCohomologyIso_trans_conjugateCohomologyIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g h : G) (n : ℕ) : L.conjugateCohomologyIso F h n ≪≫ (L.conjugate h).conjugateCohomologyIso F g n = L.conjugateCohomologyIso F (g * h) n ≪≫ CategoryTheory.eqToIso ⋯

Conjugation composes on ordinary cohomology: conjugating by h and then by g is conjugating by g * h, up to the transport along conjugate_conjugate.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (r : ℤ) : L.conjugateTateIso F 1 r = CategoryTheory.eqToIso ⋯

Conjugation by 1 is the identity on Tate cohomology, up to the transport along conjugate_one.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateTateIso_trans_conjugateTateIso {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (F : Formation G) (g h : G) (r : ℤ) : L.conjugateTateIso F h r ≪≫ (L.conjugate h).conjugateTateIso F g r = L.conjugateTateIso F (g * h) r ≪≫ CategoryTheory.eqToIso ⋯

Conjugation composes on Tate cohomology: conjugating by h and then by g is conjugating by g * h, up to the transport along conjugate_conjugate.

Conjugation of refinements

theorem TauCeti.ClassFieldTheory.LayerRefinement.conjugate {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (g : G) : LayerRefinement (old.conjugate g) (new.conjugate g)

Conjugation carries refinements to refinements: if L/F refines K/F, then gL/gF refines gK/gF.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_conjugateCohomologyIso_hom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (g : G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (new.conjugateCohomologyIso F g n).hom = CategoryTheory.CategoryStruct.comp (old.conjugateCohomologyIso F g n).hom (⋯.cohomologyInfl F n)

Conjugation commutes with inflation: inflating from K/F to L/F and then conjugating by g is conjugating by g and then inflating from gK/gF to gL/gF.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_conjugateCohomologyIso_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) (g : G) (n : ℕ) {Z : ModuleCat ℤ} (h : (new.conjugate g).H F n ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.cohomologyInfl F n) (CategoryTheory.CategoryStruct.comp (new.conjugateCohomologyIso F g n).hom h) = CategoryTheory.CategoryStruct.comp (old.conjugateCohomologyIso F g n).hom (CategoryTheory.CategoryStruct.comp (⋯.cohomologyInfl F n) h)

Conjugation commutes with inflation: inflating from K/F to L/F and then conjugating by g is conjugating by g and then inflating from gK/gF to gL/gF.

theorem TauCeti.ClassFieldTheory.LayerRefinement.cohomologyInfl_comp_conjugateCohomologyIso_hom_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (F : Formation G) (g : G) (n : ℕ) (x : ↑(old.H F n)) : (CategoryTheory.ConcreteCategory.hom (new.conjugateCohomologyIso F g n).hom) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F n)) x) = (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyInfl F n)) ((CategoryTheory.ConcreteCategory.hom (old.conjugateCohomologyIso F g n).hom) x)

Conjugation commutes with inflation: inflating from K/F to L/F and then conjugating by g is conjugating by g and then inflating from gK/gF to gL/gF.