Definitions/Def_GroupCohomology_GlobalBridge.lean

Fix a finite set S of rational primes, a group D together with a homomorphism \pi\colon \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)\to D, two morphisms f\colon R\to P and g\colon P\to B of \mathbb Z[D]-representations, a further \mathbb Z[D]-representation X, a \mathbb Z-linear Galois representation A, an additive map \iota\colon X\to A, a prime p, a \mathbb Z/p-linear Galois representation M, and a biadditive pairing \kappa\colon B\times M\to A. For an additive map \Lambda\colon H^1\bigl(D,\operatorname{Hom}_{\mathbb Z}(R,X)\bigr)\longrightarrow \mathrm{continuousH2S}\,S\,M, the target being the quotient of the S-level-constant 2-cocycles on \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) with values in M by the coboundaries of S-level-constant 1-cochains, the predicate IsGlobalBridge₂ asserts the following for all data: whenever a is a 1-cocycle of D with values in the internal hom \operatorname{Hom}_{\mathbb Z}(R,X) (with its conjugation D-action), \psi\colon D\to \operatorname{Hom}_{\mathbb Z}(P,A) is a family of additive maps with \psi_d\circ f=\iota\circ a(d) for all d, the values \psi_d(x) are all fixed by \mathrm{Gal}(\overline{\mathbb Q}/F) for some intermediate field F that is finite over \mathbb Q and whose fixing subgroup contains the inertia group of every valuation subring of \overline{\mathbb Q} lying over a prime outside S, and m\colon \mathrm{Gal}\times\mathrm{Gal}\to M satisfies \kappa\bigl(g(x),m(\gamma_1,\gamma_2)\bigr)=\bigl(d_{12}(\psi\circ\pi)\bigr)(\gamma_1,\gamma_2)(x)\qquad(x\in P), where d_{12} is the cochain differential for the conjugation action on \operatorname{Hom}_{\mathbb Z}(P,A), and m is moreover an S-level-constant 2-cocycle, then \Lambda sends the class of a to the class of m.

Thus the predicate pins down \Lambda on the cochain level against any such pair of compatible presentations; it asserts no existence of the lifts \psi or of the cochain m, and is vacuous on classes admitting no such reading.