The local Euler characteristic of an induced module

Let V be an open normal subgroup of G_K, C a subgroup of the finite quotient G_K ⧸ V, and L/K a finite extension embedded by σ : L →ₐ[K] Kˢ whose absolute Galois group is the preimage of C in G_K, so that L is the fixed field K_C of C. For a finite ℤ/n-representation B of C, read as the Galois representation shapiroGalRep of L, this file proves the Shapiro step of the dévissage of the local Euler-characteristic formula:

χ_K(Ind_C^{G_K ⧸ V} B) = χ_L(B),        φ_K(Ind_C^{G_K ⧸ V} B) = φ_L(B).

The first is Shapiro's lemma for inflated induced representations (ContinuousCohomology.indInflationShapiroIso), read on G_L through the isomorphism of G_L with the preimage of C. The second is the cardinality formula #Ind B = #B ^ [L : K] together with the tower formula [L : ℚ_p] = [L : K] [K : ℚ_p].

The hypothesis on L is met by the fixed field shapiroField K V C itself, embedded by shapiroFieldEmbedding (range_absoluteGaloisGroupExtend_shapiroFieldEmbedding); the statements are made for an abstract L because the local-field structure of a finite extension is data that L carries.

Main definitions

• TauCeti.ClassFieldTheory.shapiroGalRep: a representation of C read as a Galois representation of L.

Main results

• TauCeti.ClassFieldTheory.localEulerCharacteristic_galRepOfQuotient_ind: χ_K(Ind_C^{G_K ⧸ V} B) = χ_L(B).
• TauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind: φ_K(Ind_C^{G_K ⧸ V} B) = φ_L(B).
• localEulerCharacteristic_eq_localCardNorm_fdGalRepOfQuotient_indFDRep_iff: χ_K = φ_K holds for the inflation of Tau Ceti's finite-dimensional induction model indFDRep B exactly when χ_L = φ_L holds for B.
• localEulerCharacteristic_eq_localCardNorm_fdGalRepOfQuotient_indFDRep_of_shapiroField: the transport at the fixed field shapiroField K V C, with its finite-extension local-field structure. This is the form consumed by the modular-Artin reduction of χ_K = φ_K to representations induced from cyclic subgroups.

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.

A representation of C as a Galois representation of L

noncomputable def TauCeti.ClassFieldTheory.shapiroGalRep {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) : GalRep n L

A representation B of C ≤ G_K ⧸ V as a Galois representation of the fixed field L of C, when G_L is the preimage of C: G_L acts through G_L ≅ π⁻¹(C) → C, with the discrete topology. It is the inflation ContinuousCohomology.comapInflation of B to the preimage of C, read on G_L along absoluteGaloisGroupExtendEquiv. Its underlying module is identified with that of B by shapiroGalRepLinearEquiv.

noncomputable def TauCeti.ClassFieldTheory.shapiroGalRepLinearEquiv {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) : ↑(shapiroGalRep σ n hσ B) ≃ₗ[ZMod n] ↑B

The identification of the underlying module of shapiroGalRep with that of B.

@[simp]

theorem TauCeti.ClassFieldTheory.shapiroGalRepLinearEquiv_ρ_apply {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) (g : Field.absoluteGaloisGroup L) (b : ↑(shapiroGalRep σ n hσ B)) : (shapiroGalRepLinearEquiv σ n hσ B) (((shapiroGalRep σ n hσ B).ρ g) b) = (B.ρ (((QuotientGroup.mk' ↑V.toOpenSubgroup).subgroupComap C) ((absoluteGaloisGroupExtendEquiv K L σ hσ) g))) ((shapiroGalRepLinearEquiv σ n hσ B) b)

An element of G_L acts on shapiroGalRep through the class in C of its image in G_K (coe_absoluteGaloisGroupExtendEquiv_apply).

instance TauCeti.ClassFieldTheory.instDiscreteTopologyVZModAbsoluteGaloisGroupShapiroGalRep {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) : DiscreteTopology ↑(shapiroGalRep σ n hσ B)

shapiroGalRep carries the discrete topology.

instance TauCeti.ClassFieldTheory.instFiniteVZModAbsoluteGaloisGroupShapiroGalRepOfVSubtypeQuotientSubgroupMem {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) [Finite ↑B] : Finite ↑(shapiroGalRep σ n hσ B)

shapiroGalRep of a finite representation is finite.

instance TauCeti.ClassFieldTheory.instFactIsSmoothDiscreteZModAbsoluteGaloisGroupShapiroGalRep {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) : Fact (IsSmoothDiscrete (ZMod n) (shapiroGalRep σ n hσ B))

shapiroGalRep is smooth: it is the restriction of a smooth representation along a continuous homomorphism.

Shapiro's lemma for the two invariants

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_galRepOfQuotient_ind {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] (hn : ↑n ≠ 0) [Finite ↑B] : localEulerCharacteristic hn ((galRepOfQuotient n K V).obj (Rep.ind C.subtype B)) = localEulerCharacteristic ⋯ (shapiroGalRep σ n hσ B)

Shapiro's lemma for the local Euler characteristic. For L the fixed field of C ≤ G_K ⧸ V, the Euler characteristic over K of the inflation of Ind_C^{G_K ⧸ V} B is the Euler characteristic over L of B: χ_K(Ind B) = χ_L(B).

theorem TauCeti.ClassFieldTheory.localCardNorm_galRepOfQuotient_ind {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (n : ℕ) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : Rep.{0, 0, 0} (ZMod n) ↥C) (p : ℕ) [Fact (Nat.Prime p)] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [FinitePadicExtension K p] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [FinitePadicExtension L p] [IsScalarTower ℚ_[p] K L] [Finite ↑B] : localCardNorm p ((galRepOfQuotient n K V).obj (Rep.ind C.subtype B)) = localCardNorm p (shapiroGalRep σ n hσ B)

Shapiro's lemma for the normalized order. For L the fixed field of C ≤ G_K ⧸ V, the invariant φ_K(A) = ‖#A‖_K = |#A|_p ^ [K : ℚ_p] of the inflation of Ind_C^{G_K ⧸ V} B is that of B over L: #Ind B = #B ^ [L : K] and [L : ℚ_p] = [K : ℚ_p] [L : K].

Transport of χ = φ across Shapiro's lemma

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_fdGalRepOfQuotient_indFDRep_iff {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) {V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)} {C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)} (p : ℕ) [Fact (Nat.Prime p)] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [FinitePadicExtension K p] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [FinitePadicExtension L p] [IsScalarTower ℚ_[p] K L] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (hσ : (absoluteGaloisGroupExtend K L σ).range = Subgroup.comap (QuotientGroup.mk' ↑V.toOpenSubgroup) C) (B : FDRep (ZMod ℓ) ↥C) : localEulerCharacteristic ⋯ ((fdGalRepOfQuotient ℓ K V).obj (indFDRep B)) = localCardNorm p ((fdGalRepOfQuotient ℓ K V).obj (indFDRep B)) ↔ have x := ⋯; localEulerCharacteristic ⋯ (shapiroGalRep σ ℓ hσ ((CategoryTheory.forget₂ (FDRep (ZMod ℓ) ↥C) (Rep.{0, 0, 0} (ZMod ℓ) ↥C)).obj B)) = localCardNorm p (shapiroGalRep σ ℓ hσ ((CategoryTheory.forget₂ (FDRep (ZMod ℓ) ↥C) (Rep.{0, 0, 0} (ZMod ℓ) ↥C)).obj B))

Shapiro transport of χ = φ for finite-dimensional induction. For L the fixed field of C ≤ G_K ⧸ V and a finite-dimensional ZMod ℓ-representation B of C, the identity χ_K = φ_K holds for the inflation of indFDRep B exactly when χ_L = φ_L holds for B.

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_fdGalRepOfQuotient_indFDRep_of_shapiroField {K : Type} [Field K] (p : ℕ) [Fact (Nat.Prime p)] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [FinitePadicExtension K p] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (V : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (C : Subgroup (Field.absoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup)) (B : FDRep (ZMod ℓ) ↥C) (hB : have x := ⋯; let x_1 := finiteIntermediateFieldValuativeRel K (AlgebraicClosure K) (shapiroField K V C); let x_2 := finiteIntermediateFieldTopology K (AlgebraicClosure K) (shapiroField K V C); have x_3 := ⋯; have x_4 := ⋯; have x_5 := ⋯; have x_6 := ⋯; have x_7 := ⋯; localEulerCharacteristic ⋯ (shapiroGalRep (shapiroFieldEmbedding K V C) ℓ ⋯ ((CategoryTheory.forget₂ (FDRep (ZMod ℓ) ↥C) (Rep.{0, 0, 0} (ZMod ℓ) ↥C)).obj B)) = localCardNorm p (shapiroGalRep (shapiroFieldEmbedding K V C) ℓ ⋯ ((CategoryTheory.forget₂ (FDRep (ZMod ℓ) ↥C) (Rep.{0, 0, 0} (ZMod ℓ) ↥C)).obj B))) : localEulerCharacteristic ⋯ ((fdGalRepOfQuotient ℓ K V).obj (indFDRep B)) = localCardNorm p ((fdGalRepOfQuotient ℓ K V).obj (indFDRep B))

Shapiro transport of χ = φ at the canonical fixed field. For K/ℚ_p finite, if χ = φ holds for a finite-dimensional ZMod ℓ-representation B of C ≤ G_K ⧸ V read over the fixed field shapiroField K V C, then it holds over K for the inflation of indFDRep B.

The fixed field carries its finite-extension valuation and topology (finiteIntermediateFieldValuativeRel, finiteIntermediateFieldTopology) as local instances in the hypothesis; they are not global instances, to avoid diamonds with other realizations of the same finite extension.