Corestriction and cup products across a finite field extension

For a finite extension L/K embedded in a separable closure of K, restriction and corestriction on continuous cohomology with trivial 𝔽₂ coefficients satisfy the projection formula

cor (res x ⌣ y) = x ⌣ cor y.

The formula computes the corestriction of a degree-two cup product in which one factor is the restriction of a degree-one class on G_K: that ambient class can be pulled outside the corestriction, so only the degree-one corestriction of the other factor remains to be computed.

Main result

• TauCeti.galoisCor_cup: the degree-(1,1) projection formula.

Reference

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.5.3)(iv).

theorem TauCeti.galoisCor_cup (K : Type u) [Field K] (L : Type u) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) [FiniteDimensional K L] (x : ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat) (y : ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup L))).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 2)) ((((trivialF2TopPairing (AbsoluteGaloisGroup L)).cup 1 1) ((CategoryTheory.ConcreteCategory.hom (galoisRes K L σ 1)) x)) y) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) x) ((CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) y)

The degree-(1,1) projection formula for a finite field extension: cor (res x ⌣ y) = x ⌣ cor y on continuous cohomology with trivial 𝔽₂ coefficients (NSW (1.5.3)(iv)).