Definitions/Def_CerednikDrinfeld_QMFormalCompletionAlong.lean

Fix a commutative ring B and two B-schemes f : A \to \operatorname{Spec} B and f' : A' \to \operatorname{Spec} B. Recall that a family of formal coordinates RelativeGroupLaw.FormalCoordinates f g is simply an assignment, to every B-algebra B' and every g-tuple s \in (B')^g, of a B'-point of A over \operatorname{Spec} B, i.e. an element of \mathrm{Hom}_{\operatorname{Spec} B}(\operatorname{Spec} B', A); no axiom is part of that type. Given such data \theta in g variables for f and \theta' in g' variables for f', a morphism h : A \to A' with h followed by f' equal to f, and a g'-tuple \varphi = (\varphi_i)_{i < g'} of formal power series in g variables over B, the predicate IsFormalCompletionAlong asserts: for every B-algebra B', every ideal J \subseteq B', every n with J^{n+1} = 0, and every s : \mathrm{Fin}\,g \to B' with all s_i \in J, \theta'\bigl(B'; (\,\mathrm{nilEval}\,n\,\varphi_i\,s\,)_i\bigr) = \mathrm{mapPt}\,h\,(\theta(B'; s)). Here MvFormalGroup.nilEval n (φ i) s is the value at s of the truncation of \varphi_i to multidegrees with every exponent at most n (a well-defined substitute for \varphi_i(s), since monomials of total degree > n vanish on J), and mapPt h hh is the operation of composing a point of A with h to obtain a point of A' over the same base.

Thus the predicate says that, on all points with coordinates in a nilpotent ideal, h is given in the coordinates \theta, \theta' by the tuple of power series \varphi; it is a relation between a chosen presentation \theta, \theta' and \varphi, constraining \theta and \theta' only on such tuples, and imposing no condition of its own on \varphi (such as vanishing constant term) nor requiring \theta, \theta' to be formal coordinates for group laws.