Definitions/Def_AlgebraicGeometry_FormalGroupAlongSection.lean

Throughout, B is a commutative ring and f : A \to \operatorname{Spec} B a scheme over \operatorname{Spec} B carrying a relative group law L, i.e. a functorial group structure on the sets \mathrm{SchemeHomOver}\,(t, f) of A-valued points over \operatorname{Spec} B, with multiplication, unit and inverse, the group axioms and naturality along base changes \psi as fields. Two auxiliary operations handle substitution of nilpotent arguments into power series. For a finite index type \sigma, a B-algebra B', a natural number n, a series \varphi \in B[[X_\sigma]] and a tuple a : \sigma \to B', MvFormalGroup.nilEval truncates \varphi by the exponent bound n in each variable and evaluates the resulting polynomial at a through the structure map B \to B'. For F a g-dimensional formal group law over B (a g-tuple of series in 2g variables with vanishing constant term, linear part X_i^{(1)} + X_i^{(2)}, and the associativity identity as a field of the structure), MvFormalGroup.nilMul applies this truncated evaluation componentwise to the concatenated tuple \mathrm{Sum.elim}\,s\,t, giving F(s,t) for tuples s,t over B'.

Given an ideal J \subseteq B', a point P : \operatorname{Spec} B' \to A over \operatorname{Spec} B satisfies IsInfinitesimal J P when its restriction along \operatorname{Spec}(B'/J) \to \operatorname{Spec} B' equals the unit L.\mathrm{one} at \operatorname{Spec}(B'/J), i.e. P reduces modulo J to the unit section. FormalCoordinates f g is the type of families \theta assigning to each B-algebra B' and each tuple in (B')^g a point of A over \operatorname{Spec} B. The predicate IsFormalCoordinates L F θ asks: (i) naturality, \theta_{B''}(\varphi \circ s) = \operatorname{Spec}(\varphi)^* \theta_{B'}(s) for every B-algebra map \varphi : B' \to B'' and every tuple s with all entries nilpotent; and (ii) for every B-algebra B', ideal J and n with J^{n+1} = \bot: tuples with entries in J give infinitesimal points, \theta_{B'} is injective on such tuples, every J-infinitesimal point is \theta_{B'}(s) for such a tuple, and \theta_{B'}(F.\mathrm{nilMul}\,n\,s\,t) = L.\mathrm{mul}(\theta_{B'}(s), \theta_{B'}(t)). Thus \theta_{B'} is a bijection J^g \to \{P : P \equiv e \bmod J\} transporting the truncated law F to the group law of L; the values of \theta on non-nilpotent tuples are unconstrained. Finally IsFormalGroupAlong L F asserts the existence of such a \theta; it is a property of the pair (L, F), a compatibility with a chosen presentation of the formal group rather than an isomorphism of formal schemes.