Definitions/Def_GaloisRep_LocalFlatClasses.lean

Fix a field k, a prime p and a residual representation \bar\rho over k, with underlying space \bar\rho.V and global Galois action \bar\rho.\rho on \Gamma_{\mathbb Q}=\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q). Write G_p for primeLocalGaloisGroup (pPrime p), the group of \mathbb Q_p-algebra automorphisms of PadicAlgCl p, mapped to \Gamma_{\mathbb Q} by primeLocalToGlobal; localAut is the coercion of an element of this type synonym to an automorphism of PadicAlgCl p. Given a 1-cocycle c of G_p with values in the restriction of \mathrm{ad}^0\bar\rho (trace-zero endomorphisms of \bar\rho.V under conjugation), dualLiftModuleAct defines the action of \sigma\in G_p on \bar\rho.V\times\bar\rho.V by (v,w)\mapsto(\bar\rho(\sigma)v,\;c(\sigma)\bar\rho(\sigma)v+\bar\rho(\sigma)w), i.e. the first-order deformation \sigma\mapsto(1+\varepsilon c(\sigma))\bar\rho(\sigma) of \bar\rho|_{G_p} written out on \bar V\oplus\varepsilon\bar V, in the same normalisation as the dual-number dictionary of groupCohomology.cocycleToDualLift.

IsLocallyFlatCocycle asserts the existence of a commutative ring H with a Hopf algebra structure over \mathbb Z_p that is finite and flat as a \mathbb Z_p-module and cocommutative as a coalgebra, together with a bijection e from WithConv (H →ₐ[ℤ_p] PadicAlgCl p) — the \overline{\mathbb Q}_p-points of \mathrm{Spec}\,H with their convolution product — onto \bar\rho.V\times\bar\rho.V, subject to two conditions: e carries convolution to addition, e(f\ast g)=e(f)+e(g); and for all \sigma and all points f,g with g(h)=\sigma(f(h)) for every h\in H, one has e(g)= dualLiftModuleAct c\,\sigma\,(e(f)). Thus e is an isomorphism of G_p-modules from the points of a finite flat cocommutative Hopf algebra onto the dual-lift module of c; no k-linearity of e is required. localFlatClasses is the k-span inside H^1(G_p,\mathrm{ad}^0\bar\rho) of the classes [c], images under H1π of cocycles satisfying this predicate; the span is taken rather than proving that the set of such classes is already a subspace. dualLiftModuleActAd, IsLocallyFlatCocycleAd and localFlatClassesAd repeat the three definitions verbatim with \mathrm{ad}^0 replaced by the full adjoint representation \mathrm{ad}\,\bar\rho on \mathrm{End}_k(\bar\rho.V).