The Evens norm of a quadratic field extension

A quadratic extension L/K and an embedding σ : L →ₐ[K] Kˢ identify G_L with the open subgroup galoisSubgroup K L σ of G_K, which has index two. This file defines the index-two Evens norm H¹(G_L, 𝔽₂) → H²(G_K, 𝔽₂) along L/K, with trivial 𝔽₂ coefficients, as the transport along galoisF2Iso K L σ followed by the norm TauCeti.ContCohomology.evensNormIndexTwo of that index-two subgroup. It is the companion of TauCeti.galoisRes and TauCeti.galoisCor, and like them it is a reading of the subgroup operation, not a second construction of it.

The norm multiplies the degree by the index, so the signature is the index-two case only: for a cubic extension the target would be H³. Like the subgroup norm, galoisEvens is a function and not an additive map.

Main definitions

• TauCeti.galoisEvens: the Evens norm from G_L to G_K on 𝔽₂-cohomology, for a quadratic extension.

Main results

• TauCeti.galoisEvens_galoisF2Iso_hom: read on the open subgroup, galoisEvens is the index-two norm evensNormIndexTwo of galoisSubgroup K L σ.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), 54–65.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5, for the open subgroup associated to a finite extension.

noncomputable def TauCeti.galoisEvens (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hL : Module.finrank K L = 2) (x : ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup L))).toModuleCat) : ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

The Evens norm H¹(G_L, 𝔽₂) → H²(G_K, 𝔽₂) of the quadratic extension L/K, relative to σ. It is the canonical identification of G_L with the index-two open subgroup galoisSubgroup K L σ, followed by the index-two Evens norm of that subgroup.

Equations

• TauCeti.galoisEvens K L σ hL x = TauCeti.ContCohomology.evensNormIndexTwo (TauCeti.galoisSubgroup K L σ) ⋯ ((CategoryTheory.ConcreteCategory.hom (TauCeti.galoisF2Iso K L σ 1).inv) x)

theorem TauCeti.galoisEvens_def (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hL : Module.finrank K L = 2) (x : ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup L))).toModuleCat) : galoisEvens K L σ hL x = ContCohomology.evensNormIndexTwo (galoisSubgroup K L σ) ⋯ ((CategoryTheory.ConcreteCategory.hom (galoisF2Iso K L σ 1).inv) x)

The definition of the field-extension Evens norm as transport to the open subgroup followed by the index-two Evens norm of that subgroup.

theorem TauCeti.galoisEvens_galoisF2Iso_hom (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (hL : Module.finrank K L = 2) (y : ↑(continuousCohomology 1 (trivialF2 ↥↑(galoisSubgroup K L σ))).toModuleCat) : galoisEvens K L σ hL ((CategoryTheory.ConcreteCategory.hom (galoisF2Iso K L σ 1).hom) y) = ContCohomology.evensNormIndexTwo (galoisSubgroup K L σ) ⋯ y

Read on the open subgroup, the field-extension Evens norm is the index-two Evens norm of galoisSubgroup K L σ: the norm of the transport of a class y ∈ H¹(galoisSubgroup K L σ, 𝔽₂) to G_L is evensNormIndexTwo y.