Definitions/Def_GaloisRep_DeligneOrdinaryShape.lean

Fixed throughout are a commutative ring A and a group H. The single declaration GaloisRep.DeligneOrdinaryShape is a predicate in the data of a homomorphism \rho_{\mathrm{loc}} : H \to \mathrm{GL}_2(A), a subgroup I \le H (the inertia subgroup in the intended application), a distinguished element \mathrm{frob} \in H, a homomorphism \chi : H \to A^{\times} in the form of a monoid homomorphism H \to A, a natural number k, and two ring elements a_p, \varepsilon_p \in A. It asserts the existence of one matrix g \in \mathrm{GL}_2(A) such that the conjugated representation \sigma \mapsto g\,\rho_{\mathrm{loc}}(\sigma)\,g^{-1} satisfies five entrywise equations, the indices being those of Fin 2, namely 0 and 1: the (1,0) entry vanishes for every \sigma \in H, so the conjugate is upper triangular; the (1,1) entry equals 1 for every \sigma \in I, and equals a_p at \sigma = \mathrm{frob}; the (0,0) entry equals \chi(\sigma)^{k-1} for every \sigma \in I; and the product of a_p with the (0,0) entry at \mathrm{frob} equals \chi(\mathrm{frob})^{k-1}\varepsilon_p, a determinant-type normalisation at \mathrm{frob}.

Thus the predicate records, in the language of matrix entries after a single change of basis, that \rho_{\mathrm{loc}} is reducible with unramified quotient character taking the value a_p on \mathrm{frob} and with sub-character agreeing with \chi^{k-1} on I. The exponent k-1 is natural-number subtraction, so the case k = 0 reads as k = 1; consumers bind k subject to their own weight conditions. No structure or instance is introduced: the content is a plain existential statement about a chosen basis, not an isomorphism of representations.