Definitions/Def_AlgebraicGeometry_TangentCoordsOfPairAt.lean

Throughout, T' is a commutative local ring with residue field k, I \subseteq T' an ideal, V a k-module (with compatible right module and central-scalar structures) which is also a T'-module over the tower T' \to k, \iota \colon V \to T' a T'-linear map, and C a commutative T'-algebra; thickening T' V C denotes (k \otimes_{T'} C) \otimes_k \mathrm{TrivSqZeroExt}\,k\,V, whose spectrum is the fibre product of \operatorname{Spec}(k \otimes_{T'} C) with the square-zero disc \operatorname{Spec}(k \oplus V) over \operatorname{Spec} k.

chartRingHom is pullback of functions along a morphism w_1 \colon \operatorname{Spec}(\mathrm{thickening}\,T'\,V\,C) \to U_e into an open subscheme U_e of a scheme A_k: the ring map \Gamma(A_k, U_e) \to \mathrm{thickening}\,T'\,V\,C obtained from the identification of \Gamma(A_k,U_e) with the global sections of U_e, the map on global sections induced by w_1, and the identification of the global sections of an affine spectrum with its ring.

IsTangentCoordsOfPairAt is a predicate on the data: a scheme Y with two morphisms u, v \colon \operatorname{Spec} C \to Y; a scheme A_k with a structure morphism x_k \colon A_k \to \operatorname{Spec} k, a relative group law L_k on x_k (a functorial group structure on the k-points of x_k over arbitrary bases, with naturality in the base), a morphism a_k \colon A_k \to Y, an open U_e \subseteq A_k, and a function c from \Gamma(A_k, U_e) to \operatorname{Hom}_k(V^\vee, k \otimes_{T'} C). It asserts the existence of w_0 \colon \operatorname{Spec}(\mathrm{thickening}\,T'\,V\,C) \to A_k lying over the structure map of the thickening, and of w_1 \colon \operatorname{Spec}(\mathrm{thickening}\,T'\,V\,C) \to U_e, such that three conditions hold. First, w_0 followed by a_k is a tangent morphism of the pair (u,v) in the sense of IsTangentOfPair: there are a ring map \vartheta from the subring of pairs in C \times C congruent modulo I\cdot C to the thickening, satisfying the two Schlessinger normalisations (diagonal pairs (a,a) go to a \otimes 1, and pairs (0, \iota(v)c) go to c \otimes \mathrm{inr}\,v), and a morphism \varphi from the spectrum of that subring to Y restricting along the two projections to u and v, with w_0 \circ a_k = \varphi \circ \operatorname{Spec}\vartheta. Second, w_1 followed by the open immersion U_e \to A_k is the left translate of w_0 by the inverse of its restriction along the zero section, formed in L_k, which is a relative tangent point based at the unit section. Third, c is the tangent-coordinate function of the ring map chartRingHom of w_1: the V-component of the image of a section, taken in (k \otimes_{T'} C) \otimes_k V, read as a k-linear map V^\vee \to k \otimes_{T'} C via m \otimes w \mapsto (\xi \mapsto \xi(w)\,m). Thus the predicate fixes a chart at the unit and records the coordinates in that chart, rather than quantifying over an abstract dictionary of tangent identifications.