Definitions/Def_ModularCurve_DRResolvedModelCharts.lean

Throughout, p is a prime, \mathfrak{X} is a DRModelPackage p (a package of data and properties for the two-chart integral model DRModel p of the full modular curve of level p over \mathbb{Z}, with its two special-fibre components compInf, compZero over an algebraically closed field), O is a commutative ring, \kappa an algebraically closed field of characteristic p, \mathrm{to}\kappa : O \to \kappa a ring homomorphism, and \mathfrak{X}^{\mathrm{reg}} is a DRResolvedModelPackage p 𝔛 O κ toκ, whose carrier is a scheme Y with a proper map toDR to \mathfrak{X}_O := \mathrm{DRModel}\,p \times_{\mathbb{Z}} \operatorname{Spec} O, a finite type node of crossings with widths width, a bijection nodeEquiv onto the points of \mathrm{compInf}\,\kappa \times \mathrm{compZero}\,\kappa, and invertible ideal sheaves comp indexed by the subdivided dual graph X0MqComponents width.

First, crossingPt n is the point of \mathfrak{X}_O obtained from nodeEquiv n by the first projection of that fibre product, followed by \mathrm{compInf}\,\kappa and the base-change map \mathfrak{X}_\kappa \to \mathfrak{X}_O.

Second, for \varpi \in O and a family Fc assigning to each e and each d \in \{0,\dots,e\} an ideal sheaf datum on the project's resolution \mathrm{Res}(\varpi,e) of \operatorname{Spec} O[x,y]/(xy-\varpi^{e}), the structure DRResolvedModelCharts records, for every node n of width e: an open U_n \subseteq \mathfrak{X}_O containing crossingPt n and no other crossingPt m; an étale O-morphism f_n : U_n \to \operatorname{Spec} O[x,y]/(xy-\varpi^{e}) with f_n(y) in D(x) \cup D(y) exactly when y \neq crossingPt n; the requirement that on the fibre product U_n \times \mathrm{Res}(\varpi,e) the second projection be injective on points whose first projection is crossingPt n; a morphism g_n from \mathrm{toDR}^{-1}(U_n) to \mathrm{Res}(\varpi,e) and an isomorphism \Phi_n from U_n \times \mathrm{Res}(\varpi,e) to \mathrm{toDR}^{-1}(U_n) carrying the two projections to the restriction of toDR and to g_n; and, for each d \in \{0,\dots,e\}, equality of the restriction to \mathrm{toDR}^{-1}(U_n) of the component ideal sheaf at chain position chainPos width n d (position 0 the first strict transform, 1,\dots,e-1 the exceptional sheaves attached to n, position e the second strict transform) with the pull-back of Fc e d along g_n. The étaleness field is registered as an instance.