Definitions/Def_GroupCohomology_PoitouTate.lean

Fix a field k, a group \Gamma, an index type \iota with groups \Gamma_v and homomorphisms \mathrm{loc}_v \colon \Gamma_v \to \Gamma (the intended picture being a global Galois group with its decomposition groups), and k-linear representations M, M' of \Gamma. Three things are defined. First, locTotal is the k-linear map H^1(\Gamma, M) \to \prod_v H^1(\Gamma_v, M|_{\Gamma_v}) whose v-th component is the restriction map locRes, i.e. the map on H^1 induced functorially by \mathrm{loc}_v together with the identity on the restricted representation; a companion lemma records this componentwise description. Second, given a family of k-bilinear pairings \langle\cdot,\cdot\rangle_v \colon H^1(\Gamma_v, M|_{\Gamma_v}) \times H^1(\Gamma_v, M'|_{\Gamma_v}) \to k and \iota finite, totalPairing is the bilinear pairing on the products obtained by summing the local pairings on matching components, so that its value on (x,y) is \sum_v \langle x_v, y_v\rangle_v. Third, IsPoitouTateOrthogonality is a Prop-valued structure with two fields, each an equality of submodules expressed through the project's orthogonal operation (for a pairing B and a submodule L, \mathrm{orthogonal}\,B\,L is the submodule of vectors w with B x w = 0 for all x \in L): the orthogonal complement of the image of locTotal for M under the total pairing equals the image of locTotal for M', and the orthogonal complement of the image of locTotal for M' under the flipped total pairing equals the image of locTotal for M. Thus the structure carries, as hypotheses on the datum (\mathrm{loc}, M, M', \langle\cdot,\cdot\rangle), the exact mutual-annihilator statement; it is a predicate, not a theorem proved here.