Definitions/Def_AlgebraicGeometry_ThetaAdaptedFrame.lean

Fix g, N, n, moduli \delta : \mathrm{Fin}\,g \to \mathbb{N} with each \delta_i \neq 0, and write H(\delta) = \prod_i \mathbb{Z}/\delta_i. The first definition, FramedPolarisedAbelianScheme.IsThetaAdapted, takes a bijection e : \mathrm{Fin}(N+1) \simeq H(\delta) and a framed polarised abelian scheme X over a commutative ring S — so X carries f : A \to \operatorname{Spec} S with relative group law, the 2g torsion points of level n, an invertible sheaf X.\mathrm{pol} of geometric fibre degree N+1, and a frame consisting of N+1 global sections of X.\mathrm{pol} forming a basis over S and defining a closed immersion into projective N-space. It asserts the existence of a Polarisation.SchrodingerFrame for f, the group law and X.\mathrm{pol}, taken with test morphism the identity of \operatorname{Spec} S and moduli \delta, whose basis sections agree with the frame after re-indexing by e: for every i, the frame section \sigma_{e(i)} of the Schrödinger frame equals the pullback of the i-th framing section along the first projection A \times_S \operatorname{Spec} S \to A. A Schrödinger frame is itself a structure: sections \sigma_h indexed by H(\delta) whose S-linear combinations exhaust the global sections bijectively, together with theta points \mathrm{lift}(h) and \mathrm{dualLift}(\chi) (each a point of A with an isomorphism between the pullback of the sheaf along translation by that point and the sheaf itself), and, as fields of the structure, the equations U_{\mathrm{lift}(h)}\sigma_{h'} = \sigma_{h+h'} and U_{\mathrm{dualLift}(\chi)}\sigma_h = \chi(h)\,\sigma_h for additive characters \chi of H(\delta) valued in S.

The second definition, PolarisedAbelianScheme.ThetaTypeLocally δ, is a predicate of the shape \forall S, \ \text{PolarisedAbelianScheme}\ g\,(N+1)\,n\,S \to \mathrm{Prop}, hence usable as the property parameter of the project's Satisfying and fine-moduli notions. It holds for u over S when: for every commutative S-algebra R and every \zeta \in R with \zeta^{N+1} = 1 and 1 - \zeta^j a unit for 0 < j < N+1, there is an R-algebra R' that is faithfully flat as an R-module and étale over R, a framed polarised abelian scheme X' over R' and a bijection e : \mathrm{Fin}(N+1) \simeq H(\delta), such that X' underlies the base change of u along S \to R \to R' in the sense of PolarisedAbelianScheme.IsPullback and X' is theta-adapted for \delta and e. The element \zeta occurs only in the hypothesis: its existence over R is the condition under which a theta-adapted framing over an étale faithfully flat cover is demanded.