Equivariant Kummer theory on a finite Galois quotient of G_F

Let F be a field, n a natural number invertible in F, G_F = Field.absoluteGaloisGroup F, and V an open normal subgroup of G_F. Let L/F be a finite normal extension embedded in the separable closure by σ : L →ₐ[F] Fˢ so that the image of G_L in G_F along σ is V ((absoluteGaloisGroupExtend F L σ).range = V), and suppose that V acts trivially on μₙ, which is then the inflation of a representation M of G = G_F ⧸ V (exists_fdGalRepOfQuotient_iso_muNRep). This file proves equivariant Kummer theory in the form in which the local Euler characteristic computes with it:

kummerH1ConjRepresentationEquiv σ hn hV e : H¹(V, ℤ/n) ≅ M^∨ ⊗ Lˣ ⧸ (Lˣ)ⁿ

as ZMod n-representations of G. Here G acts on H¹(V, ℤ/n) by conjugation, which is the representation h1ConjRepresentation of the H¹-tensor comparison, on M^∨ = Hom(M, ℤ/n) dually, and on the power classes of L through G ≃* Gal(L/F) (TauCeti.absoluteGaloisGroupExtendQuotientEquiv). The representation M is the same datum as in the computation of H² by duality (finrank_continuousCohomology_two_fdGalRepOfQuotient), so H¹(V, ℤ/n) ≅ μₙ^{-1} ⊗ Lˣ ⧸ (Lˣ)ⁿ as representations of G, natural in the F-automorphisms of L.

The equivariant Kummer isomorphism kummerH1FiniteRepresentationEquiv is stated on Tau Ceti's separable-closure model AbsoluteGaloisGroup F of the absolute Galois group, for the subgroup fixing σ(L). The restriction isomorphism absoluteGaloisGroupRestrictEquiv carries V onto that subgroup (TauCeti.absoluteGaloisGroupRestrictSubgroupEquiv) and identifies the two first cohomology groups compatibly with conjugation (restrictSubgroupH1Equiv, restrictSubgroupH1Equiv_smul). Along this identification the cyclotomic twist of the Kummer isomorphism with trivial coefficients (nsmul_smul_fixingSubgroupKummerEquivOfTrivial) is the character of G on M, and the rank-one twist removal Representation.rankOneTwistEquiv gives the equivalence.

Main definitions

• TauCeti.ClassFieldTheory.restrictSubgroupH1Equiv: the induced identification of H¹ with ℤ/n coefficients.
• TauCeti.ClassFieldTheory.kummerH1ConjRepresentationEquiv: equivariant Kummer theory, H¹(V, ℤ/n) ≅ M^∨ ⊗ Lˣ ⧸ (Lˣ)ⁿ as representations of G_F ⧸ V.

Main results

• TauCeti.ClassFieldTheory.restrictSubgroupH1Equiv_smul: the identification of H¹ intertwines the two conjugation actions.
• TauCeti.ClassFieldTheory.smul_kummerCoeff_eq_self_of_mem_fixingSubgroup: if M inflates to μₙ, the subgroup fixing σ(L) acts trivially on μₙ.
• TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv: the Kummer class of x corresponds to m ↦ log(m) • x.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, proof of Theorem 2.8.

theorem TauCeti.ClassFieldTheory.instContinuousSMulZMod_tauCeti {n : ℕ} {H : Type u_1} [Monoid H] [TopologicalSpace H] : ContinuousSMul H (ZMod n)

ZMod n, with the discrete topology and the trivial action, is a continuous module.

H¹(G_L, ℤ/n) in the two models of G_F

noncomputable def TauCeti.ClassFieldTheory.restrictSubgroupH1Equiv {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} (n : ℕ) (hV : (absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup) : ContCohomology.H1 (↥σ.fieldRange.fixingSubgroup) (ZMod n) ≃+ ContCohomology.H1 (↥↑V.toOpenSubgroup) (ZMod n)

H¹(G_L, ℤ/n) in the two models of G_F: pullback along absoluteGaloisGroupRestrictSubgroupEquiv identifies the first cohomology, with trivial coefficients ℤ/n, of the subgroup of Gal(Fˢ/F) fixing σ(L) with that of V.

theorem TauCeti.ClassFieldTheory.restrictSubgroupH1Equiv_apply {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} (n : ℕ) (hV : (absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup) (x : ContCohomology.H1 (↥σ.fieldRange.fixingSubgroup) (ZMod n)) : (restrictSubgroupH1Equiv σ n hV) x = (ContCohomology.explicitMap1 (↥σ.fieldRange.fixingSubgroup) (ZMod n) (↥↑V.toOpenSubgroup) (ZMod n) (↑(absoluteGaloisGroupRestrictSubgroupEquiv F L σ hV)) (AddMonoidHom.id (ZMod n)) ⋯ ⋯) x

restrictSubgroupH1Equiv is the pullback along absoluteGaloisGroupRestrictSubgroupEquiv.

theorem TauCeti.ClassFieldTheory.restrictSubgroupH1Equiv_smul {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} (n : ℕ) [Normal F L] (hV : (absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup) (g : Field.absoluteGaloisGroup F) (x : ContCohomology.H1 (↥σ.fieldRange.fixingSubgroup) (ZMod n)) : (restrictSubgroupH1Equiv σ n hV) ((absoluteGaloisGroupRestrictEquiv F) g • x) = g • (restrictSubgroupH1Equiv σ n hV) x

The identification of H¹ is Galois equivariant: it intertwines conjugation by the image of g ∈ G_F in Gal(Fˢ/F) on the cohomology of the subgroup fixing σ(L) with conjugation by g on the cohomology of V.

The roots of unity as a representation of the quotient

theorem TauCeti.ClassFieldTheory.smul_kummerCoeff_eq_self_of_mem_fixingSubgroup {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {n : ℕ} (hn : IsUnit ↑n) (hV : (absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup) {M : FDRep (ZMod n) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)} (e : (fdGalRepOfQuotient n F V).obj M ≅ muNRep n F) (h : AbsoluteGaloisGroup F) (hh : h ∈ σ.fieldRange.fixingSubgroup) (ξ : KummerCoeff F n) : h • ξ = ξ

If M inflates to μₙ, the subgroup of Gal(Fˢ/F) fixing σ(L) acts trivially on μₙ.

Equivariant Kummer theory

noncomputable def TauCeti.ClassFieldTheory.kummerH1ConjRepresentationEquiv {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {n : ℕ} [Normal F L] (hn : IsUnit ↑n) (hV : (absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup) {M : FDRep (ZMod n) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)} (e : (fdGalRepOfQuotient n F V).obj M ≅ muNRep n F) : h1ConjRepresentation.Equiv ((Representation.dual M.ρ).tprod (MonoidHom.comp (powerClassRepresentation n) (absoluteGaloisGroupExtendQuotientEquiv F L σ hV).toMonoidHom))

Equivariant Kummer theory on a finite Galois quotient of G_F. Let n be invertible in F, let the image of G_L in G_F along σ be the open normal subgroup V, and let M be a representation of G = G_F ⧸ V inflating to μₙ (e). Then H¹(V, ℤ/n) is isomorphic to M^∨ ⊗ Lˣ ⧸ (Lˣ)ⁿ as a ZMod n-representation of G, where G acts on H¹(V, ℤ/n) by conjugation (h1ConjRepresentation) and on the power classes of L through absoluteGaloisGroupExtendQuotientEquiv F L σ hV : G ≃* Gal(L/F). That is, H¹(L, ℤ/n) ≅ μₙ^{-1} ⊗ Lˣ ⧸ (Lˣ)ⁿ, naturally in the F-automorphisms of L.

It sends the Kummer class of x to m ↦ log(m) • x (dualTensorHom_kummerH1ConjRepresentationEquiv).

@[simp]

theorem TauCeti.ClassFieldTheory.dualTensorHom_kummerH1ConjRepresentationEquiv {F : Type} [Field F] {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] (σ : L →ₐ[F] SeparableClosure F) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {n : ℕ} [Normal F L] (hn : IsUnit ↑n) (hV : (absoluteGaloisGroupExtend F L σ).range = ↑V.toOpenSubgroup) {M : FDRep (ZMod n) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)} (e : (fdGalRepOfQuotient n F V).obj M ≅ muNRep n F) (x : Additive (powerClassQuotient Lˣ n)) (m : ↑M.V) : ((dualTensorHom (ZMod n) (↑M.V) (Additive (powerClassQuotient Lˣ n))) ((kummerH1ConjRepresentationEquiv σ hn hV e) ((restrictSubgroupH1Equiv σ n hV) ((fixingSubgroupKummerEquivOfTrivial σ hn (kummerCoeffAddEquivZMod hn) ⋯ ⋯) x)))) m = (kummerCoeffAddEquivZMod hn) ((kummerCoeffEquivMuNRep n F).symm ((TopRep.Hom.hom (CategoryTheory.eqToIso ⋯ ≪≫ e).hom) m)) • x

The equivariant Kummer isomorphism on Kummer classes. Under kummerH1ConjRepresentationEquiv, the Kummer class of a power class x, read on V through restrictSubgroupH1Equiv, corresponds to the homomorphism M → Lˣ ⧸ (Lˣ)ⁿ sending m to log(m) • x, where log : M ≃ μₙ ≃ ℤ/n is e followed by kummerCoeffAddEquivZMod.