Definitions/Def_CuspForm_HeckeModuleCornerRealization.lean

Fix a complete discrete valuation ring \mathcal O with residue field k= IsLocalRing.ResidueField 𝒪, a natural number p, a residual two-dimensional Galois representation \bar\rho over k (an object of ResidualGaloisRep), levels N,L\ge 1, a set S of naturals, a ring homomorphism \theta\colon \mathbb{T}= CuspForm.heckeAlgebra N 2 S \to k, a module M over the localised Hecke algebra CuspForm.heckeLocal N S 𝒪 θ which is also an \mathcal O-module, and an \mathcal O-bilinear form B\colon M\times M\to\mathcal O. The predicate IsCornerRealization asserts the existence of the following data. First, a proof hcomm that the operators opFamily L ⊤ S 𝒪 — the endomorphisms heckeTL attached to generators T_\ell (\ell prime, \ell\notin S, \ell\nmid L) and U_q (q prime, q\mid L), and the diamond operators diamondL — commute pairwise on the level-L carrier H1 L ⊤ 𝒪; a system of scalars \bar\theta on the generators with values in k; an IdempotentSplitting Sp of the \mathcal O-subalgebra generated by these operators, i.e. complete orthogonal idempotents e_1,\dots,e_n together with maximal ideals \mathfrak m_1,\dots,\mathfrak m_n exhausting the maximal spectrum and satisfying e_i\in\mathfrak m_j \iff i\neq j; an index i_0; an \mathcal O-algebra map \pi_k from the corner ring e_{i_0}\cdot(-)\cdot e_{i_0} to k; a proof hpar that every element of the corner submodule e_{i_0}\cdotH1 L ⊤ 𝒪 lies in ModularCurve.Period.parabolicHoms 𝒪 (GammaH L ⊤) 𝒪; and an \mathcal O-linear isomorphism e from M onto that corner submodule.

These data are required to satisfy: \bar\theta(T_\ell)=\theta(T_\ell) for all primes \ell\notin S with \ell\nmid L and \ell\nmid N; \bar\theta(U_q)=0 for primes q with q\mid L and q^2\mid L; \bar\theta(U_p)\neq 0 whenever p is prime, p\mid L, and \bar\rho, viewed through GaloisRepAdic.ofResidualGaloisRep, satisfies IsOrdinaryAt p; \pi_k sends the image in the corner ring of each generator's operator to \bar\theta of that generator; e intertwines the action of \pi(T_\ell) on M with heckeT L ⊤ ℓ 𝒪 on the carrier, for all primes \ell\notin S with \ell\nmid N; and B is the restriction along e of the level-L member Bfam₀ 𝒪 L of the chosen family of pairings on parabolic homomorphisms. Thus IsCornerRealization is a predicate on the pair (M,B) recording that it is isomorphic, with its Hecke action and its pairing, to an idempotent corner of the level-L carrier cut out by a residual eigensystem with prescribed behaviour at the primes dividing L.