Definitions/Def_GaloisRep_ConditionLifts.lean

Fix a local ring \mathcal{O} and a family of predicates \mathcal{D} which, for every local ring A carrying an \mathcal{O}-algebra structure, singles out certain elements of GaloisRepAdic A — the structures consisting of a free finite A-module V of rank 2, a monoid homomorphism \rho from \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) = \overline{\mathbb{Q}} \simeq_{\mathbb{Q}} \overline{\mathbb{Q}} to \operatorname{End}_A(V), and the adic continuity condition that for each n there is a finite extension L/\mathbb{Q} inside \overline{\mathbb{Q}} such that every \sigma fixing L pointwise acts trivially on V/\mathfrak{m}_A^n V. Given in addition a point \rho_0 of the representation functor at the residue field, i.e. a continuous homomorphism \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) \to \mathrm{GL}_2(k), and an object A of the category of local pro-Artinian \mathcal{O}-algebras, GaloisRep.conditionLifts is the set of continuous homomorphisms \rho' : \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) \to \mathrm{GL}_2(A) such that: \rho' belongs to liftFunctor at A, that is, the push-forward of \rho' along the unique (terminal) morphism A \to k is exactly \rho_0; and, for every morphism f : A \to B in the category with B Artinian, every \rho_B \in GaloisRepAdic B and every basis b of the underlying module of \rho_B indexed by \mathrm{Fin}\,2 whose associated matrices \mathrm{toMatrix}\,b\,b\,(\rho_B(\sigma)) agree for all \sigma with the matrices of the push-forward of \rho' along f, one has \mathcal{D}(\rho_B). Thus the condition is imposed not on \rho' directly but on every module-theoretic realisation, in a basis, of each Artinian push-forward of \rho'.

GaloisRep.conditionSubfunctor assembles these sets into a subfunctor of the representation functor: stability under a morphism g : A \to A' holds because the lift subfunctor is one, and because a test morphism f out of A' pulls back to g followed by f out of A. A simp lemma records that the object part of this subfunctor is the set just described.