The arithmetic class-module extension over a finite Galois group

For a finite normal extension L/K embedded in a separable closure of K, let V be the open subgroup fixing L. The pro-p class-module extension has kernel Vᵃᵇ(p) and quotient G_K/V. This file reads its conjugation action and its projection over Gal(L/K), using the topological Galois correspondence. Its total group and kernel remain the canonical class-module carriers. The construction relabels abelianizationProPProfiniteExtension through quotientGaloisSubgroupEquiv, using ProfiniteGroupExtension.relabelQuotient.

This supplies an arithmetic extension over the same finite group as a free profinite presentation of Gal(L/K), so equivariant kernel maps can be lifted between the extensions.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).

@[reducible, inline]

noncomputable abbrev TauCeti.galoisClassModuleAction (p : ℕ) (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) : MulDistribMulAction Gal(L/K) (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))

The action of Gal(L/K) on the pro-p abelianization of the subgroup fixing L, transported from the canonical quotient conjugation action.

theorem TauCeti.galoisClassModuleAction_smul (p : ℕ) (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) (t : Gal(L/K)) (x : abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)) : t • x = (quotientGaloisSubgroupEquiv K L j).symm t • x

The transported action is conjugation by the corresponding class in G_K/V.

@[simp]

theorem TauCeti.galoisClassModuleAction_restrict_smul (p : ℕ) (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) (s : AbsoluteGaloisGroup K) (x : abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)) : have this := galoisClassModuleAction p K L j; j.restrictNormalHom s • x = ↑s • x

In the transported action, restriction to L acts by the class of the original absolute Galois automorphism.

theorem TauCeti.continuousSMul_galoisClassModuleAction (p : ℕ) (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) : have this := galoisClassModuleAction p K L j; ContinuousSMul Gal(L/K) (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))

The finite Galois group's transported conjugation action is jointly continuous.

@[reducible, inline]

noncomputable abbrev TauCeti.galoisClassModuleExtension (p : ℕ) (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) : have this := galoisClassModuleAction p K L j; ProfiniteGroupExtension Gal(L/K) (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j))

The arithmetic pro-p class-module extension with quotient Gal(L/K) and its prescribed conjugation action on Vᵃᵇ(p).

theorem TauCeti.galoisClassModuleExtension_rightHom_mk (p : ℕ) (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (j : L →ₐ[K] SeparableClosure K) (s : AbsoluteGaloisGroup K) : have this := galoisClassModuleAction p K L j; (galoisClassModuleExtension p K L j).toGroupExtension.rightHom ↑s = j.restrictNormalHom s

The arithmetic class-module extension projects a class of an absolute Galois automorphism to its restriction to the embedded finite extension.