Definitions/Def_ModularCurve_DRModelPackageCrossingFrame.lean

Two groups of definitions are made. First, for an arbitrary scheme X and a specialisation \xi \rightsquigarrow x of points of X, the branch ideal branchIdeal is the preimage of the maximal ideal of the local ring \mathcal O_{X,\xi} under the specialisation map of stalks \mathcal O_{X,x} \to \mathcal O_{X,\xi}; it is recorded as a prime ideal of \mathcal O_{X,x}, and mem_branchIdeal_iff restates membership as the condition that the image of the germ in \mathcal O_{X,\xi} lies in the maximal ideal, i.e. that the section vanishes at \xi.

Second, in the setting of a prime p, a package \mathfrak X of data and properties for the two-chart integral model DRModel p of the modular function field with its Igusa j-coordinate, a commutative ring O, an algebraically closed field \kappa of characteristic p and a ring map O \to \kappa, the base change X_O := baseChangeO p O is the fibre product of DRModel.toBase p with \operatorname{Spec} of \mathbb Z \to O, and baseChangeO.toBase is its second projection X_O \to \operatorname{Spec} O. For o \in O, baseGerm is the germ at a point x of X_O of the global section of X_O obtained by pulling o back along this projection. For a point n of the fibre product of the two closed immersions \mathfrak X.compInf \kappa and \mathfrak X.compZero \kappa of the rational model ratModel \kappa into the geometric p-fibre, crossingPt is the image of n in X_O under the first projection followed by compInf \kappa and then the base-change map X_\kappa \to X_O. Finally ξinf and ξzero are the images in X_O of the generic point of ratModel \kappa under compInf \kappa, respectively compZero \kappa, followed by that base-change map.