Definitions/Def_GoodReductionJacobian_RelativeGroupLawAction.lean

Throughout, R is a commutative ring, J a scheme and f\colon J\to\operatorname{Spec}R a morphism; L is a RelativeGroupLaw R f, i.e. the project's functor-of-points datum assigning to every t\colon T\to\operatorname{Spec}R a group structure (mul, one, inv with associativity, two-sided unit and left inverse) on the set \mathrm{SchemeHomOver}\,t\,f of morphisms T\to J over \operatorname{Spec}R, together with the naturality field mul_natural expressing compatibility of mul with precomposition along any \psi\colon T'\to T with \psi\circ t=t'. Fix in addition a morphism \iota\colon E\to J.

The pullback P of \iota followed by f against f — that is, E\times_{\operatorname{Spec}R}J — is given the structure morphism actionSource f ι, defined as the second projection followed by f. Two points of J over this base are then singled out: actionFstPoint is the first projection followed by \iota, lying over actionSource f ι by the pullback square, and actionSndPoint is the second projection, which lies over actionSource f ι by construction of the latter. The morphism action L ι : P ⟶ J is the underlying scheme morphism of the product of these two points in the group \mathrm{SchemeHomOver}\,(\mathrm{actionSource}\,f\,\iota)\,f supplied by L; on points it is (e,x)\mapsto \iota(e)\cdot x. The remaining declarations form the elementary interface: action_def restates the definition, actionFstPoint_coe and actionSndPoint_coe identify the underlying morphisms of the two points with \mathrm{pr}_1 followed by \iota and with \mathrm{pr}_2, and action_over records that action L ι followed by f equals actionSource f ι, i.e. the action morphism is a morphism over \operatorname{Spec}R, this being exactly the defining property of the product point.