Restriction–corestriction exactness for quadratic extensions

For a quadratic extension L/K, an embedding of L into the separable closure of K determines an open subgroup of index two in G_K, whose cohomology is identified with that of G_L by TauCeti.galoisF2Iso. The subgroup index-two exact sequence therefore says, in every degree, that a class over L has zero corestriction precisely when it is the restriction of a class over K:

Hⁿ(G_K, 𝔽₂) --res--> Hⁿ(G_L, 𝔽₂) --cor--> Hⁿ(G_K, 𝔽₂).

This file transports the existing subgroup theorem through TauCeti.galoisF2Iso, so the statement uses the field-extension operations TauCeti.galoisRes and TauCeti.galoisCor rather than rebuilding either operation.

The degree-two part of the other index-two exact sequence identifies the kernel of restriction with cup products by the quadratic character.

Main result

• TauCeti.exact_galoisRes_galoisCor_of_finrank_eq_two: restriction followed by corestriction is exact for a quadratic extension, in every degree.
• TauCeti.galoisRes_eq_zero_iff: a degree-two class restricts to zero exactly when it is the cup product of the quadratic character with a degree-one class.

References

• J. Kr. Arason, Cohomologische Invarianten quadratischer Formen, J. Algebra 36 (1975), 448–491.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.2).

theorem TauCeti.exact_galoisRes_galoisCor_of_finrank_eq_two (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) (n : ℕ) : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom (galoisRes K L σ n)) ⇑(CategoryTheory.ConcreteCategory.hom (galoisCor K L σ n))

Exactness of restriction followed by corestriction for a quadratic extension. In every degree, a class in Hⁿ(G_L, 𝔽₂) has zero corestriction if and only if it is the restriction of a class in Hⁿ(G_K, 𝔽₂).

theorem TauCeti.galoisRes_eq_zero_iff (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 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (galoisRes K L σ 2)) x = 0 ↔ ∃ (y : ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat), x = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (galoisCharacter K L σ hL)) y

The kernel of restriction to a quadratic extension is generated by its character. A class x ∈ H²(G_K, 𝔽₂) restricts to zero in H²(G_L, 𝔽₂) if and only if x = χ_{L/K} ⌣ y for some y ∈ H¹(G_K, 𝔽₂).