Base change of Brauer classes along an arbitrary field extension

For an arbitrary field extension L/K, not necessarily algebraic, this file defines the base change of cohomological Brauer classes

brBaseChange K L : Br K →+ Br L.

Choose a K-embedding τ : Kˢ →ₐ[K] Lˢ of separable closures. It induces the compatible pair made of the continuous homomorphism TauCeti.absoluteGaloisGroupMap τ : G_L → G_K and the map (Kˢ)ˣ → (Lˢ)ˣ of units, unitsCoeffBaseChange τ, and brBaseChange K L is the pullback along this pair on the explicit model H²(Gal(Kˢ/K), (Kˢ)ˣ) of Br K (unitsRepH2Equiv). For the completion K_v of a number field it is the localization map Br K → Br K_v, restriction to the decomposition group, which is how the local invariants of a global Brauer class are defined.

The map does not depend on τ (brBaseChange_apply holds for every τ): two embeddings differ by an automorphism h of Kˢ, which changes the compatible pair by the inner automorphism of h, and inner automorphisms act trivially on cohomology (TauCeti.ContCohomology.explicitMap2_eq_self_of_inner). Consequently base change is functorial (brBaseChange_self, brBaseChange_brBaseChange), and for an extension embedded in Kˢ it is the restriction brRes of TauCeti.NumberTheory.ClassFieldTheory.Brauer.Restriction, whichever embedding is used there (brBaseChange_eq_brRes).

On central simple algebras, base change is A ↦ A ⊗_K L; that comparison is not made here.

Main definitions

• TauCeti.ClassFieldTheory.unitsCoeffBaseChange τ: the map (Kˢ)ˣ → (Lˢ)ˣ along τ.
• TauCeti.ClassFieldTheory.brBaseChange K L: base change Br K →+ Br L.

Main results

• TauCeti.ClassFieldTheory.explicitMap2_absoluteGaloisGroupMap_eq: a pullback on H² along the decomposition map of an embedding τ of separable closures and a coefficient map that depends on τ compatibly with the Galois action does not depend on τ.
• TauCeti.ClassFieldTheory.brBaseChange_apply: base change is the pullback along the compatible pair of any embedding τ of separable closures.
• TauCeti.ClassFieldTheory.brBaseChange_self, TauCeti.ClassFieldTheory.brBaseChange_brBaseChange: functoriality in the extension.
• TauCeti.ClassFieldTheory.brBaseChange_eq_brRes: for an extension embedded in Kˢ, base change is restriction.
• TauCeti.ClassFieldTheory.brBaseChange_eq_zero_of_algHom: a class split by L is split by every extension of L.
• TauCeti.ClassFieldTheory.brBaseChange_relBrInfl: base change of a class inflated from a finite normal layer L/K is inflated from any finite normal layer M/F receiving L, along restriction Gal(M/F) → Gal(L/K) and the inclusion Lˣ → Mˣ.
• TauCeti.ClassFieldTheory.brBaseChange_characterCarryCocycle: base change of the carry class a ∪ δχ of a character χ of G_K and a ∈ Kˣ is the carry class of χ read on G_L and the image of a in Lˣ.
• TauCeti.ClassFieldTheory.mem_range_relBrInfl_iff_brBaseChange_eq_zero: the classes inflated from a finite normal layer L/K are exactly those whose base change to L vanishes.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5, and Chapter VIII, §1, for the localization maps of Galois cohomology.
• J.-P. Serre, Local Fields, Chapter X, §4.

The coefficient map

noncomputable def TauCeti.ClassFieldTheory.unitsCoeffBaseChange {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) : UnitsCoeff K →+ UnitsCoeff L

The units of Kˢ as units of Lˢ along an embedding τ : Kˢ →ₐ[K] Lˢ: the coefficient leg of base change of Brauer classes.

@[simp]

theorem TauCeti.ClassFieldTheory.toMul_unitsCoeffBaseChange {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (x : UnitsCoeff K) : Additive.toMul ((unitsCoeffBaseChange τ) x) = (Units.map ↑τ) (Additive.toMul x)

unitsCoeffBaseChange τ applies τ to a unit.

theorem TauCeti.ClassFieldTheory.unitsCoeffBaseChange_smul {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (g : AbsoluteGaloisGroup L) (x : UnitsCoeff K) : (unitsCoeffBaseChange τ) ((absoluteGaloisGroupMap τ) g • x) = g • (unitsCoeffBaseChange τ) x

unitsCoeffBaseChange τ is equivariant along absoluteGaloisGroupMap τ : G_L → G_K.

theorem TauCeti.ClassFieldTheory.unitsCoeffBaseChange_comp {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (h : AbsoluteGaloisGroup K) (x : UnitsCoeff K) : (unitsCoeffBaseChange (τ.comp ↑h)) x = (unitsCoeffBaseChange τ) (h • x)

Changing the embedding τ by an automorphism h of Kˢ precomposes the coefficient map with the action of h.

Base change of Brauer classes

theorem TauCeti.ClassFieldTheory.explicitMap2_absoluteGaloisGroupMap_eq (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] {M : Type u} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction (AbsoluteGaloisGroup K) M] [ContinuousSMul (AbsoluteGaloisGroup K) M] {N : Type v} [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction (AbsoluteGaloisGroup L) N] [ContinuousSMul (AbsoluteGaloisGroup L) N] (F : (SeparableClosure K →ₐ[K] SeparableClosure L) → M →+ N) (hF : ∀ (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (g : AbsoluteGaloisGroup L) (m : M), (F τ) ((absoluteGaloisGroupMap τ) g • m) = g • (F τ) m) (hFcomp : ∀ (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (h : AbsoluteGaloisGroup K) (m : M), (F (τ.comp ↑h)) m = (F τ) (h • m)) (τ τ' : SeparableClosure K →ₐ[K] SeparableClosure L) : ContCohomology.explicitMap2 (AbsoluteGaloisGroup K) M (AbsoluteGaloisGroup L) N (absoluteGaloisGroupMap τ) (F τ) ⋯ ⋯ = ContCohomology.explicitMap2 (AbsoluteGaloisGroup K) M (AbsoluteGaloisGroup L) N (absoluteGaloisGroupMap τ') (F τ') ⋯ ⋯

Pullbacks along embeddings of separable closures do not depend on the embedding. Let M be a discrete G_K-module, N a discrete G_L-module, and F τ : M → N a coefficient map for every K-embedding τ : Kˢ →ₐ[K] Lˢ, equivariant along absoluteGaloisGroupMap τ, such that changing τ by an automorphism h of Kˢ precomposes F τ with the action of h. Then the pullback on the explicit H² along (absoluteGaloisGroupMap τ, F τ) is the same for every τ: a second embedding is τ ∘ h, and the pair of τ ∘ h is that of τ after the inner pair of h, which acts trivially on cohomology.

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

Base change of Brauer classes Br K → Br L along an arbitrary field extension L/K: the pullback along the absolute Galois groups G_L → G_K and the units (Kˢ)ˣ → (Lˢ)ˣ induced by an embedding of separable closures Kˢ → Lˢ. It does not depend on the embedding (brBaseChange_apply). For a completion K_v of a number field K it is the localization map Br K → Br K_v.

theorem TauCeti.ClassFieldTheory.brBaseChange_apply (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (x : Br K) : (brBaseChange K L) x = (unitsRepH2Equiv L) ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup K) (UnitsCoeff K) (AbsoluteGaloisGroup L) (UnitsCoeff L) (absoluteGaloisGroupMap τ) (unitsCoeffBaseChange τ) ⋯ ⋯) ((unitsRepH2Equiv K).symm x))

Base change is the pullback along any embedding of separable closures: for every K-embedding τ : Kˢ →ₐ[K] Lˢ, brBaseChange K L is the pullback along G_L → G_K and (Kˢ)ˣ → (Lˢ)ˣ induced by τ, read on the explicit models of Br K and Br L.

@[simp]

theorem TauCeti.ClassFieldTheory.brBaseChange_self (K : Type u) [Field K] (x : Br K) : (brBaseChange K K) x = x

Base change along the trivial extension K/K is the identity.

@[simp]

theorem TauCeti.ClassFieldTheory.brBaseChange_brBaseChange (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (M : Type w) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (x : Br K) : (brBaseChange L M) ((brBaseChange K L) x) = (brBaseChange K M) x

Base change is transitive: for a tower K ⊆ L ⊆ M, base change from K to L followed by base change from L to M is base change from K to M.

theorem TauCeti.ClassFieldTheory.brBaseChange_eq_zero_of_algHom {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] {M : Type w} [Field M] [Algebra K M] (f : L →ₐ[K] M) {x : Br K} (hx : (brBaseChange K L) x = 0) : (brBaseChange K M) x = 0

A class split by L is split by every extension of L. If the base change of x to L vanishes, so does its base change to any field M receiving a K-embedding of L.

theorem TauCeti.ClassFieldTheory.brBaseChange_eq_brRes (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : brBaseChange K L = brRes K L σ

Base change along an embedded extension is restriction: if L/K is embedded in Kˢ by σ, then brBaseChange K L is the restriction brRes K L σ. In particular brRes K L σ does not depend on σ.

Base change of carry classes

theorem TauCeti.ClassFieldTheory.brBaseChange_characterCarryCocycle (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (χ : Additive (AbsoluteGaloisGroup K) →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : Kˣ) : (brBaseChange K L) ((unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle χ hχ) ((baseUnitsEquivInvariants K) (Additive.ofMul a)))) = (unitsRepH2Equiv L) ↑((ContCohomology.characterCarryCocycle (χ.comp (MonoidHom.toAdditive ↑(absoluteGaloisGroupMap τ))) ⋯) ((baseUnitsEquivInvariants L) (Additive.ofMul ((Units.map ↑(algebraMap K L)) a))))

Base change of a carry class. For a character χ : G_K → ℚ/ℤ with open kernel and a ∈ Kˣ, base change to L of the Brauer class a ∪ δχ of the carry cocycle of χ and a is the carry class of the character χ read on G_L through the decomposition map of any K-embedding τ : Kˢ → Lˢ and of the image of a in Lˣ.

Base change of inflated classes

theorem TauCeti.ClassFieldTheory.brBaseChange_relBrInfl (K : Type) [Field K] (F : Type) [Field F] [Algebra K F] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (M : Type) [Field M] [Algebra F M] [FiniteDimensional F M] [Normal F M] [Algebra K M] [IsScalarTower K F M] [Algebra L M] [IsScalarTower K L M] (σ : L →ₐ[K] SeparableClosure K) (σ' : M →ₐ[F] SeparableClosure F) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)) : (brBaseChange K F) ((relBrInfl K L σ) y) = (relBrInfl F M σ') ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map ((AlgEquiv.restrictNormalHom L).comp (AlgEquiv.restrictScalarsHom K)) (unitsBaseChangeHom K L F M) 2)) y)

Base change of an inflated Brauer class. Let L/K be finite normal, embedded in Kˢ by σ, let F/K be any extension and M/F finite normal, embedded in Fˢ by σ', with a compatible K-embedding L → M. Then base change to F of the class inflated from y ∈ H²(Gal(L/K), Lˣ) is the class inflated from the image of y in H²(Gal(M/F), Mˣ), along restriction Gal(M/F) → Gal(L/K) and the inclusion Lˣ → Mˣ.

The relative Brauer group as a kernel

theorem TauCeti.ClassFieldTheory.mem_range_relBrInfl_iff_brBaseChange_eq_zero (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] (σ : L →ₐ[K] SeparableClosure K) (x : Br K) : x ∈ (relBrInfl K L σ).range ↔ (brBaseChange K L) x = 0

The relative Brauer group is the kernel of base change. For a finite normal extension L/K, embedded in Kˢ by σ, a class of Br K is inflated from H²(Gal(L/K), Lˣ) exactly when its base change to L vanishes: Br(L/K) = ker(Br K → Br L).