Definitions/Def_GaloisRep_OrdinaryUnitClasses.lean

Throughout, k is a field, p a prime and \bar\rho a residual representation over k with underlying space \bar V; the local group is G_p = \mathrm{Gal}(\overline{\mathbb Q}_p/\mathbb Q_p), mapped to \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) by primeLocalToGlobal, and the coefficient module is the full adjoint \mathrm{End}_k(\bar V) with \sigma acting by f \mapsto \bar\rho(\sigma) f \bar\rho(\sigma^{-1}) (no trace condition is imposed), restricted to G_p. Four items are defined. First, unitRootInertia is the subset of \sigma \in G_p lying in the inertia subgroup attached to the valuation subring of \overline{\mathbb Q}_p over \mathbb Q_p, fixing every \zeta with \zeta^p = 1, and fixing every \beta with \|\beta\|_+ = 1 whose p-th power is fixed by the whole inertia subgroup; that is, the subgroup of inertia acting trivially on \mu_p and on the p-th roots of the units fixed by inertia. Second, for a k-submodule V_1 \subseteq \bar V, a 1-cocycle c is ordinary when c(\sigma)V_1 \subseteq V_1 for all \sigma \in G_p, and, for \sigma in inertia, c(\sigma)\bar V \subseteq V_1 and c(\sigma)|_{V_1} = 0. Third, c is an ordinary unit cocycle if it is ordinary, is of finite level — there is an intermediate field F of \overline{\mathbb Q}/\mathbb Q, finite over \mathbb Q, with c(gs) = c(g) whenever the global image of s fixes F pointwise — and satisfies c(\sigma) = 0 for all \sigma in unitRootInertia. Fourth, ordinaryUnitClassesAd is the k-submodule of H^1(G_p, \mathrm{ad}\,\bar\rho) spanned by the classes of ordinary unit cocycles, the classes being taken through the canonical map from cocycles to H^1. The predicates are conditions on cocycles, not on cohomology classes, and the subspace is defined as a span rather than as a set of classes, so that closure under addition is not asserted by the definition.