Restriction and corestriction of mod-two Kummer classes

Let L/K be a finite extension of fields in which 2 is invertible, and σ : L →ₐ[K] Kˢ a K-embedding into a separable closure. Restriction TauCeti.galoisRes and corestriction TauCeti.galoisCor along σ act on H¹(-, 𝔽₂), and the Kummer class (a) ∈ H¹(G_K, 𝔽₂) of a unit is TauCeti.kummerClass. This file proves the two transfer laws of Kummer classes:

res (a) = (a)     for a ∈ Kˣ, read in Lˣ,
cor (b) = (N b)   for b ∈ Lˣ, with N = N_{L/K}.

Both are the Kummer squares at n = 2 of TauCeti.Kummer, read through the μ₂ coefficient dictionary TauCeti.mu2EquivZMod2; the one input specific to μ₂ is that the dictionaries of K and of L agree along the identification of separable closures (TauCeti.mu2EquivZMod2_kummerCoeffMap), because that identification sends -1 to -1.

Restriction is the restriction square TauCeti.kummerRes_kummerCocycleClass of the explicit Kummer cocycle classes, and corestriction is the norm square TauCeti.kummerCor_kummerMap of the Kummer isomorphism. Both are carried to 𝔽₂ coefficients by commuting squares of compatible pairs, TauCeti.ContCohomology.explicitMap1_explicitMap1_of_comp_eq, whose coefficient sides are the agreement of the two dictionaries; corestriction also uses its naturality in the coefficients, TauCeti.ContCohomology.explicitCor1_explicitMap1_id.

Finally, the map TauCeti.h2MuToUnits : H²(G_K, 𝔽₂) → H²(G_K, (Kˢ)ˣ) induced by μ₂ ⊆ (Kˢ)ˣ commutes with restriction, TauCeti.galoisRes on the source and TauCeti.galoisResUnits on the target. Both composites are compatible-pair maps along G_L → G_K (TauCeti.ContinuousCohomology.map_comp_coeffMap), and their coefficient maps agree because both send the nontrivial element of 𝔽₂ to -1.

Main results

• TauCeti.mu2EquivZMod2_kummerCoeffMap, TauCeti.mu2EquivZMod2_kummerCoeffMapSymm: the value dictionaries μ₂ ≃+ ZMod 2 of K and L agree along the identification of separable closures.
• TauCeti.galoisRes_kummerClass: restriction of the Kummer class of a ∈ Kˣ is the Kummer class of its image in Lˣ.
• TauCeti.galoisCor_kummerClass: corestriction of the Kummer class of b ∈ Lˣ is the Kummer class of N_{L/K} b.
• TauCeti.galoisRes_comp_h2MuToUnits, TauCeti.h2MuToUnits_galoisRes: TauCeti.h2MuToUnits commutes with restriction.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1) and the display following it.

theorem TauCeti.instContinuousSMulVIntTrivialF2OfIsTopologicalGroup (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousSMul G ↑(trivialF2 G)

@[simp]

theorem TauCeti.mu2EquivZMod2_kummerCoeffMap (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] (x : KummerCoeff K 2) : (mu2EquivZMod2 L) ((kummerCoeffMap K 2 L σ) x) = (mu2EquivZMod2 K) x

The μ₂ dictionaries of K and L agree along the identification of separable closures: TauCeti.kummerCoeffMap sends -1 to -1, so it does not change the value in ZMod 2.

@[simp]

theorem TauCeti.mu2EquivZMod2_kummerCoeffMapSymm (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] (y : KummerCoeff L 2) : (mu2EquivZMod2 K) ((kummerCoeffMapSymm K 2 L σ) y) = (mu2EquivZMod2 L) y

The inverse identification TauCeti.kummerCoeffMapSymm does not change the value in ZMod 2 either.

theorem TauCeti.galoisRes_kummerClass (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] [FiniteDimensional K L] (a : Kˣ) : (CategoryTheory.ConcreteCategory.hom (galoisRes K L σ 1)) (kummerClass a) = kummerClass ((Units.map ↑(algebraMap K L)) a)

Restriction of a Kummer class (NSW, the display after (6.2.1), at n = 2): for a K-embedding σ : L →ₐ[K] Kˢ of a finite extension, restriction H¹(G_K, 𝔽₂) → H¹(G_L, 𝔽₂) sends the Kummer class of a ∈ Kˣ to the Kummer class of its image in Lˣ.

theorem TauCeti.galoisCor_kummerClass (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] [FiniteDimensional K L] (b : Lˣ) : (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass b) = kummerClass ((Algebra.normUnits K) b)

Corestriction of a Kummer class is the Kummer class of the norm (NSW, the display after (6.2.1), at n = 2): for a K-embedding σ : L →ₐ[K] Kˢ of a finite extension, corestriction H¹(G_L, 𝔽₂) → H¹(G_K, 𝔽₂) sends the Kummer class of b ∈ Lˣ to the Kummer class of N_{L/K} b.

Restriction and the map to the cohomological Brauer group

theorem TauCeti.galoisRes_comp_h2MuToUnits (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] [FiniteDimensional K L] : CategoryTheory.CategoryStruct.comp (galoisRes K L σ 2) (h2MuToUnits L) = CategoryTheory.CategoryStruct.comp (h2MuToUnits K) (galoisResUnits K L σ 2)

Restriction commutes with H²(G, 𝔽₂) → H²(G, (Kˢ)ˣ), as morphisms: restricting a class of H²(G_K, 𝔽₂) to G_L and then carrying it to H²(G_L, (Lˢ)ˣ) is carrying it to H²(G_K, (Kˢ)ˣ) and then restricting with multiplicative coefficients.

theorem TauCeti.galoisRes_comp_h2MuToUnits_assoc (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] [FiniteDimensional K L] {Z : TopModuleCat ℤ} (h : continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup L) (UnitsCoeff L)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (galoisRes K L σ 2) (CategoryTheory.CategoryStruct.comp (h2MuToUnits L) h) = CategoryTheory.CategoryStruct.comp (h2MuToUnits K) (CategoryTheory.CategoryStruct.comp (galoisResUnits K L σ 2) h)

Restriction commutes with H²(G, 𝔽₂) → H²(G, (Kˢ)ˣ), as morphisms: restricting a class of H²(G_K, 𝔽₂) to G_L and then carrying it to H²(G_L, (Lˢ)ˣ) is carrying it to H²(G_K, (Kˢ)ˣ) and then restricting with multiplicative coefficients.

theorem TauCeti.h2MuToUnits_galoisRes (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [Invertible 2] [Invertible 2] [FiniteDimensional K L] (x : ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) : (TopModuleCat.Hom.hom (h2MuToUnits L)) ((TopModuleCat.Hom.hom (galoisRes K L σ 2)) x) = (TopModuleCat.Hom.hom (galoisResUnits K L σ 2)) ((TopModuleCat.Hom.hom (h2MuToUnits K)) x)

Compatibility of TauCeti.h2MuToUnits with restriction: for x ∈ H²(G_K, 𝔽₂), the image in H²(G_L, (Lˢ)ˣ) of the restriction of x is the restriction of the image of x in H²(G_K, (Kˢ)ˣ).