Definitions/Def_AlgebraicGeometry_PicDualNumberDeformationClassSpec.lean

Throughout: a commutative ring R, a scheme C with a morphism c\colon C\to\operatorname{Spec}R, a rigidifying datum \varepsilon (a morphism over the identity of \operatorname{Spec}R relative to c), a commutative R-algebra A, and a two-affine open cover \mathcal V=(U_0,U_1) of C; A[\epsilon] denotes the dual numbers DualNumber A. Three auxiliary notions are named. dualNumberThickening is the cover morphism HomOver.stage attached to the structure map A\to A[\epsilon]: a morphism of two-affine covers lying over that ring homomorphism, whose underlying scheme map is the projection C\times_{\operatorname{Spec}R}\operatorname{Spec}A[\epsilon]\to C\times_{\operatorname{Spec}R}\operatorname{Spec}A and which induces semilinear pullback maps map0, map1, map01 on sections of the structure sheaf over the charts and their intersection. For f a function on the intersection of the two charts of the A-pullback, oneAddEpsMul is the section 1+\epsilon\cdot\iota(f) on the intersection of the charts of the A[\epsilon]-pullback, \iota being map01 of that thickening. H1StructureSheaf is the two-chart Čech H^1 of the structure sheaf of C\times_{\operatorname{Spec}R}\operatorname{Spec}A with the pulled-back cover, i.e. functions on the intersection modulo the image of (s_0,s_1)\mapsto s_1|-s_0|.

The main declaration IsDeformationClassMap is a predicate on a map \delta from RigKerDualNumber c ε A — classes of rigidified line bundles on the A[\epsilon]-stage whose pullback along the reduction \operatorname{Spec}A\to\operatorname{Spec}A[\epsilon] has underlying module isomorphic to the unit, taken modulo the equivalence of rigidified line bundles — to H1StructureSheaf. It asserts: for every representative M, every sections e_0,e_1 of M over the two charts of the A[\epsilon]-pullback which are frames there in the sense of Scheme.Modules.IsFrameOn (on each smaller open set, multiplication by the restricted section is a bijection from functions to sections), and every f on the intersection of the A-charts such that the restriction of e_1 equals (1+\epsilon\,\iota f) times the restriction of e_0, one has \delta of the class of M equal to the class of f. This is thus a specification of \delta by its behaviour on normalised frames, not a construction of it: existence, uniqueness, additivity and naturality in A are the subject of separate statements.