Restriction and corestriction of Brauer classes along a field extension

Let L/K be an extension and σ : L →ₐ[K] Kˢ a K-embedding into a separable closure of K. Through σ, the absolute Galois group G_L is the subgroup Gal(Kˢ/σ(L)) of G_K fixing σ(L) (TauCeti.absoluteGaloisGroupEquivFixingSubgroup), and the identification of separable closures carries the units of Kˢ, with the action of this subgroup, to the units of Lˢ, with the action of G_L (TauCeti.unitsCoeffMap, TauCeti.unitsCoeffMapSymm). This file defines the two maps between the Brauer groups Br K = H²(G_K, (Kˢ)ˣ) and Br L that they induce:

• restriction brRes K L σ : Br K →+ Br L, restriction to Gal(Kˢ/σ(L)) followed by the transport to G_L;
• corestriction brCor K L σ : Br L →+ Br K, for a finite L/K: the transport to Gal(Kˢ/σ(L)), an open subgroup of index [L : K], followed by corestriction to G_K.

Both are computed on the explicit model H²(Gal(Kˢ/K), (Kˢ)ˣ) of Br K (unitsRepH2Equiv), exactly as TauCeti.kummerRes and TauCeti.kummerCor are on H¹(·, μₙ). Restriction is the pullback along the single compatible pair G_L → G_K, (Kˢ)ˣ → (Lˢ)ˣ (brRes_eq_explicitMap2), and corestriction after restriction is multiplication by the degree (brCor_brRes). Together with the restriction square inv_L (brRes x) = [L : K] • inv_K x of a local invariant, the latter gives the corestriction square inv_K (brCor y) = inv_L y, since restriction is then surjective.

Main definitions

• TauCeti.ClassFieldTheory.brRes: restriction Br K → Br L.
• TauCeti.ClassFieldTheory.brCor: corestriction Br L → Br K, for a finite L/K.

Main results

• TauCeti.ClassFieldTheory.brRes_eq_explicitMap2: restriction is the pullback along G_L → G_K and (Kˢ)ˣ → (Lˢ)ˣ.
• TauCeti.ClassFieldTheory.brCor_brRes: brCor (brRes x) = [L : K] • x.

References

• J.-P. Serre, Local Fields, Chapter VII, §7 and Chapter XIII, §3.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5, and (1.5.7).

noncomputable def TauCeti.ClassFieldTheory.brRes (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : Br K →+ Br L

Restriction of Brauer classes Br K → Br L along the extension L/K embedded in Kˢ by σ: restriction from G_K to the subgroup Gal(Kˢ/σ(L)) fixing σ(L), followed by the pullback along G_L ≃ₜ* Gal(Kˢ/σ(L)) with the coefficient identification TauCeti.unitsCoeffMap K L σ : (Kˢ)ˣ → (Lˢ)ˣ.

theorem TauCeti.ClassFieldTheory.brRes_apply (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : Br K) : (brRes K L σ) x = (unitsRepH2Equiv L) ((ContCohomology.explicitMap2 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K) (AbsoluteGaloisGroup L) (UnitsCoeff L) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ)) (unitsCoeffMap K L σ) ⋯ ⋯) ((ContCohomology.explicitRes2 (AbsoluteGaloisGroup K) (UnitsCoeff K) σ.fieldRange.fixingSubgroup) ((unitsRepH2Equiv K).symm x)))

brRes K L σ is restriction to the subgroup fixing σ(L) followed by the transport to G_L, read on the explicit models of Br K and Br L.

theorem TauCeti.ClassFieldTheory.brRes_eq_explicitMap2 (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : Br K) : (brRes K L σ) x = (unitsRepH2Equiv L) ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup K) (UnitsCoeff K) (AbsoluteGaloisGroup L) (UnitsCoeff L) ((ContinuousMonoidHom.subgroupSubtype σ.fieldRange.fixingSubgroup).comp ↑(absoluteGaloisGroupEquivFixingSubgroup K L σ)) (unitsCoeffMap K L σ) ⋯ ⋯) ((unitsRepH2Equiv K).symm x))

Restriction is a pullback along a compatible pair: on the explicit models, brRes K L σ pulls a class back along the composite G_L ≃ Gal(Kˢ/σ(L)) ↪ G_K, with coefficients carried by TauCeti.unitsCoeffMap K L σ : (Kˢ)ˣ → (Lˢ)ˣ.

theorem TauCeti.ClassFieldTheory.explicitMap2_unitsCoeffMapSymm_explicitMap2_unitsCoeffMap (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (x : ContCohomology.H2 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K)) : (ContCohomology.explicitMap2 (AbsoluteGaloisGroup L) (UnitsCoeff L) (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ).symm) (unitsCoeffMapSymm K L σ) ⋯ ⋯) ((ContCohomology.explicitMap2 (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K) (AbsoluteGaloisGroup L) (UnitsCoeff L) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ)) (unitsCoeffMap K L σ) ⋯ ⋯) x) = x

The transport of H² from Gal(Kˢ/σ(L)) to G_L and back is the identity: the transport used by brCor is a left inverse of the transport used by brRes. Both are the two directions of explicitMap2Equiv for the coefficient identification (Kˢ)ˣ ≃ (Lˢ)ˣ.

noncomputable def TauCeti.ClassFieldTheory.brCor (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] : Br L →+ Br K

Corestriction of Brauer classes Br L → Br K along the finite extension L/K embedded in Kˢ by σ: the pullback along Gal(Kˢ/σ(L)) ≃ₜ* G_L with the coefficient identification TauCeti.unitsCoeffMapSymm K L σ : (Lˢ)ˣ → (Kˢ)ˣ, followed by corestriction from the open subgroup Gal(Kˢ/σ(L)) to G_K.

theorem TauCeti.ClassFieldTheory.brCor_apply (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (y : Br L) : (brCor K L σ) y = (unitsRepH2Equiv K) ((ContCohomology.explicitCor2 (AbsoluteGaloisGroup K) (UnitsCoeff K) σ.fieldRange.fixingSubgroup ⋯) ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup L) (UnitsCoeff L) (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ).symm) (unitsCoeffMapSymm K L σ) ⋯ ⋯) ((unitsRepH2Equiv L).symm y)))

brCor K L σ is the transport to the subgroup fixing σ(L) followed by corestriction to G_K, read on the explicit models of Br L and Br K.

@[simp]

theorem TauCeti.ClassFieldTheory.brCor_brRes (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (x : Br K) : (brCor K L σ) ((brRes K L σ) x) = Module.finrank K L • x

Corestriction after restriction is multiplication by the degree: brCor (brRes x) = [L : K] • x for every Brauer class x of K.