Definitions/Def_GaloisRep_DeformationRingData.lean

This module introduces a single structure, GaloisRep.DeformationRingData, which is a hypothesis interface recording that a given deformation problem is represented by a ring. Its parameters are: a complete discrete valuation ring \mathcal{O} (a domain, discrete valuation ring, and adically complete for its maximal ideal); a residual representation ρbar over the residue field k=\mathcal{O}/\lambda, i.e. a two-dimensional k-vector space with a monoid homomorphism from \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) (realised as the \mathbb{Q}-algebra automorphisms of AlgebraicClosure ℚ) into its endomorphisms, trivial on the subgroup fixing some finite subextension L/\mathbb{Q}; and a predicate \mathcal{D} on rank-two Galois representations over arbitrary local \mathcal{O}-algebras, the deformation condition, left entirely arbitrary here. A term of the structure consists of a ring R which is commutative, local, Noetherian, \mathfrak{m}_R-adically complete, an \mathcal{O}-algebra via a local homomorphism, together with: surjectivity of \mathcal{O}\to R\to R/\mathfrak{m}_R (the residue field condition, stated map-free); absolute irreducibility of ρbar, meaning that after base change to an algebraic closure of k the only Galois-stable submodules are \bot and \top; a representation \rho on a free R-module of rank two whose Galois action is \mathfrak{m}_R-adically continuous (for each n some finite L/\mathbb{Q} with (\rho(\sigma)-1)V\subseteq\mathfrak{m}_R^nV for \sigma fixing L); the assertion \mathcal{D}(\rho); an intertwining R/\mathfrak{m}_R-linear isomorphism between R/\mathfrak{m}_R\otimes_R V and the base change of ρbar along the canonical map of residue fields; and the universal property, carried as a field: for every Noetherian complete local \mathcal{O}-algebra A (local structure map, residue field generated by \mathcal{O}) and every \rho_A of type \mathcal{D} whose reduction is equivalent to the base change of ρbar along the induced map of residue fields k \to A/\mathfrak{m}_A, there is a unique \mathcal{O}-algebra map \varphi\colon R\to A which is local and for which A\otimes_R V\cong \rho_A as Galois representations. Equivalence of representations is throughout the existence of an intertwining linear isomorphism, not a basis-preserving (strict) one; under the assumed absolute irreducibility the two agree. All carriers live in Type, so the structure itself is in Type 1. Nothing here asserts that such data exist: inhabiting the structure for a given (\rho bar,\mathcal{D}) is the representability theorem, and for a \mathcal{D} that does not restrict ramification to a finite set of primes no Noetherian R need exist.