Definitions/Def_GroupCohomology_SelmerLe.lean

The standing context is a field k, a group \Gamma, a finite index type \iota with groups \Gamma_v and homomorphisms \mathrm{loc}_v:\Gamma_v\to\Gamma, two objects M,M' of Rep k Γ, and for each v a k-bilinear pairing pairing v between H^1 of the restriction of M along \mathrm{loc}_v and H^1 of the restriction of M'. Throughout, for a family L of local conditions L_v\subseteq H^1(\Gamma_v,M), selmer loc M L is the intersection over v of the preimages of L_v under the restriction maps H^1(\Gamma,M)\to H^1(\Gamma_v,M), and dualConditions loc M M' pairing L is the family whose v-th member consists of those w with pairing v x w = 0 for all x\in L_v; \rho-invariants play the role of H^0.

greenbergWilesLe is the predicate asserting the single inequality of natural numbers \dim_k \mathrm{Sel}_L(M)+\dim_k (M')^{\Gamma}+\sum_v \dim_k M^{\Gamma_v}\ \le\ \dim_k \mathrm{Sel}_{L^{\perp}}(M')+\dim_k M^{\Gamma}+\sum_v \dim_k L_v, with all dimensions taken as Module.finrank (hence 0 in the infinite-dimensional case). greenbergWilesLe_of_greenbergWilesEq deduces it from the corresponding equality predicate greenbergWilesEq of the imported module. IsGreenbergWilesLeDatum is a Prop-valued structure bundling, for a given family L: finite-dimensionality of the Selmer group, of the dual Selmer group attached to L^{\perp}, and of each L_v, together with the above inequality as a field; IsGreenbergWilesDatum.toLe converts the equality-bearing datum of the imported module into this weaker one.

selmerComparisonStep L L' is the predicate stating that if L_v\subseteq L'_v for all v then \dim_k \mathrm{Sel}_{L'}(M)+\dim_k \mathrm{Sel}_{L^{\perp}}(M')+\sum_v \dim_k L_v\ \le\ \dim_k \mathrm{Sel}_{L}(M)+\dim_k \mathrm{Sel}_{L'^{\perp}}(M')+\sum_v \dim_k L'_v, a subtraction-free form of the statement that enlarging the local conditions increases the Selmer defect by at most the change in local dimensions. selmerComparisonStep_refl records the case L'=L, where both sides agree.