The fixed field in the finite-quotient Shapiro argument

Let V be an open normal subgroup of the absolute Galois group G_F and let C be a subgroup of the finite quotient G_F / V. The subgroup of G_F relevant to Shapiro's lemma is the preimage of C. This file constructs its fixed field shapiroField F V C and proves

[shapiroField F V C : F] = [G_F / V : C].

Consequently, induction from C multiplies both dimension and the exponent in the cardinality of a finite-vector-space coefficient module by this field degree. The degree formula in a scalar tower gives the arithmetic factor used in the local Euler-characteristic argument.

The cohomological comparison itself is ContinuousCohomology.indInflationShapiroIso; this file supplies its fixed-field and coefficient- size interpretation.

Main definitions

• shapiroOpenSubgroup: the preimage of C in G_F.
• shapiroField: the fixed field of that preimage in an algebraic closure of F.
• shapiroFieldEmbedding: its inclusion into the separable closure Fˢ.

Main results

• fixingSubgroup_shapiroField: the Shapiro fixed field is fixed exactly by the preimage of C.
• finrank_shapiroField: the fixed-field degree is the index of C.
• index_eq_finrank_of_range_absoluteGaloisGroupExtend_eq_comap: more generally, the index of C is the degree of any finite extension whose absolute Galois group is the preimage of C.
• range_absoluteGaloisGroupExtend_shapiroFieldEmbedding: the absolute Galois group of the Shapiro fixed field, embedded in G_F along shapiroFieldEmbedding, is the preimage of C.
• finrank_ind_eq_finrank_shapiroField_mul: induction scales coefficient dimension by that degree.
• natCard_ind_eq_pow_finrank_shapiroField_mul: the corresponding coefficient-cardinality formula over a prime field.
• finrank_base_shapiroField: the degree formula in a finite scalar tower.
• finrank_base_mul_finrank_ind_eq_shapiroField: the equality of arithmetic exponents on the two sides of Shapiro's lemma.

References

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

noncomputable def TauCeti.ClassFieldTheory.shapiroOpenSubgroup (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : OpenSubgroup (Field.absoluteGaloisGroup F)

The open subgroup of G_F obtained as the preimage of C ≤ G_F / V.

@[simp]

theorem TauCeti.ClassFieldTheory.shapiroOpenSubgroup_toSubgroup (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : ↑(shapiroOpenSubgroup F V C) = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C

noncomputable def TauCeti.ClassFieldTheory.shapiroField (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : IntermediateField F (AlgebraicClosure F)

The fixed field in an algebraic closure of the subgroup used by finite-quotient Shapiro.

theorem TauCeti.ClassFieldTheory.shapiroField_def (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : shapiroField F V C = IntermediateField.fixedField ↑(shapiroOpenSubgroup F V C)

shapiroField F V C is the fixed field of shapiroOpenSubgroup F V C.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_shapiroField (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) {x : AlgebraicClosure F} : x ∈ shapiroField F V C ↔ ∀ (σ : Gal(AlgebraicClosure F/F)), ↑σ ∈ C → σ x = x

An element lies in the Shapiro fixed field iff it is fixed by every element of G_F whose image in G_F / V lies in C.

theorem TauCeti.ClassFieldTheory.shapiroOpenSubgroup_index (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : (↑(shapiroOpenSubgroup F V C)).index = C.index

The index of the preimage of C in G_F is the index of C in the finite quotient.

theorem TauCeti.ClassFieldTheory.index_eq_finrank_of_range_absoluteGaloisGroupExtend_eq_comap {F : Type u} [Field F] {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)} {L : Type u_1} [Field L] [Algebra F L] [FiniteDimensional F L] {σ : L →ₐ[F] SeparableClosure F} (hσ : (absoluteGaloisGroupExtend F L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) : C.index = Module.finrank F L

The index of C is the degree of a field whose absolute Galois group is the preimage of C. If L/F is a finite extension embedded by σ and the image of G_L in G_F is the preimage of C, then [G_F / V : C] = [L : F].

theorem TauCeti.ClassFieldTheory.fixingSubgroup_shapiroField (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) [IsGalois F (AlgebraicClosure F)] : (shapiroField F V C).fixingSubgroup = ↑(shapiroOpenSubgroup F V C)

The Shapiro fixed field is fixed exactly by the preimage of C: the preimage is open, hence closed, and infinite Galois theory recovers a closed subgroup from its fixed field.

theorem TauCeti.ClassFieldTheory.finrank_shapiroField (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) [IsGalois F (AlgebraicClosure F)] : Module.finrank F ↥(shapiroField F V C) = C.index

The degree of the Shapiro fixed field over F is the index of C in G_F / V.

instance TauCeti.ClassFieldTheory.instFiniteDimensionalSubtypeAlgebraicClosureMemIntermediateFieldShapiroFieldOfIsGalois (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) [IsGalois F (AlgebraicClosure F)] : FiniteDimensional F ↥(shapiroField F V C)

The Shapiro fixed field is a finite extension of F, of degree the index of C.

noncomputable def TauCeti.ClassFieldTheory.shapiroFieldEmbedding (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) [IsGalois F (AlgebraicClosure F)] : ↥(shapiroField F V C) →ₐ[F] SeparableClosure F

The inclusion of the Shapiro fixed field into the separable closure of F: when AlgebraicClosure F is Galois over F, every element of it is separable over F.

@[simp]

theorem TauCeti.ClassFieldTheory.coe_shapiroFieldEmbedding_apply (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) [IsGalois F (AlgebraicClosure F)] (x : ↥(shapiroField F V C)) : ↑((shapiroFieldEmbedding F V C) x) = ↑x

shapiroFieldEmbedding is the inclusion of subfields of AlgebraicClosure F.

theorem TauCeti.ClassFieldTheory.range_absoluteGaloisGroupExtend_shapiroFieldEmbedding (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) [IsGalois F (AlgebraicClosure F)] : (absoluteGaloisGroupExtend F (↥(shapiroField F V C)) (shapiroFieldEmbedding F V C)).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C

The absolute Galois group of the Shapiro fixed field is the preimage of C. Along the inclusion shapiroFieldEmbedding, the image of G_{K_C} in G_F is the preimage of C in G_F.

theorem TauCeti.ClassFieldTheory.finrank_ind_eq_finrank_shapiroField_mul (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) {R : Type v} [Field R] [IsGalois F (AlgebraicClosure F)] (B : Rep.{max u v, v, u} R ↥C) : Module.finrank R ↑(Rep.ind C.subtype B) = Module.finrank F ↥(shapiroField F V C) * Module.finrank R ↑B

Induction from C scales dimension by the degree of the associated fixed field.

theorem TauCeti.ClassFieldTheory.natCard_ind_eq_pow_finrank_shapiroField_mul (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) (p : ℕ) [Fact (Nat.Prime p)] [IsGalois F (AlgebraicClosure F)] (B : Rep.{u, 0, u} (ZMod p) ↥C) [FiniteDimensional (ZMod p) ↑B] : Nat.card ↑(Rep.ind C.subtype B) = p ^ (Module.finrank F ↥(shapiroField F V C) * Module.finrank (ZMod p) ↑B)

Over a prime field, the cardinality of an induced coefficient module is the prime raised to the fixed-field degree times the dimension of the original module.

theorem TauCeti.ClassFieldTheory.finrank_base_shapiroField (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) {k : Type w} [Field k] [Algebra k F] : Module.finrank k ↥(shapiroField F V C) = Module.finrank F ↥(shapiroField F V C) * Module.finrank k F

The Shapiro fixed-field degree satisfies the tower formula over any scalar subfield.

theorem TauCeti.ClassFieldTheory.finrank_base_mul_finrank_ind_eq_shapiroField (F : Type u) [Field F] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (C : Subgroup (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) {R : Type v} [Field R] {k : Type w} [Field k] [IsGalois F (AlgebraicClosure F)] [Algebra k F] (B : Rep.{max u v, v, u} R ↥C) : Module.finrank k F * Module.finrank R ↑(Rep.ind C.subtype B) = Module.finrank k ↥(shapiroField F V C) * Module.finrank R ↑B

The arithmetic exponents on the two sides of finite-quotient Shapiro agree: induction scales coefficient dimension by the same index by which passage to the fixed field scales base degree.