Definitions/Def_AlgebraicGeometry_TorsionCharacter.lean

The setting is a commutative ring S, a scheme morphism f\colon A \to \operatorname{Spec} S carrying a relative group law L : RelativeGroupLaw S f, a natural number n, and a morphism \iota\colon \operatorname{Spec} R \to \operatorname{Spec} S with R a commutative ring, thought of as an affine base change of S. Recall that a RelativeGroupLaw equips, for every scheme T and every morphism t\colon T \to \operatorname{Spec} S, the set SchemeHomOver t f of morphisms T \to A over \operatorname{Spec} S with a group structure, natural in (T,t); L.IsTorsionPoint t n x is the condition L.nsmul t n x = L.one t, where nsmul is the n-fold iterate of L.mul starting from the unit section, so it says that x is killed by n in that group.

The structure TorsionCharacter L n ι packages a character of the n-torsion over R in functor-of-points form. Its field val assigns, to each commutative ring T, each morphism \kappa\colon \operatorname{Spec} T \to \operatorname{Spec} R, each point x of A over \kappa followed by \iota, and each proof that x is n-torsion for L, a unit \chi(x) \in T^{\times}. The field val_mul asserts multiplicativity: whenever x, y and their product L.mul are n-torsion, the value at the product is the product of the values. The field val_natural expresses naturality in the test ring relationally rather than by transport of structure: given ring homomorphisms \varphi\colon T \to T' and morphisms \kappa, \kappa' with \operatorname{Spec}\varphi followed by \kappa equal to \kappa', and n-torsion points x over \kappa and x' over \kappa' whose underlying scheme morphisms satisfy x' = \operatorname{Spec}\varphi followed by x, the value at x' is the image of the value at x under the induced map T^{\times} \to T'^{\times}. The accompanying extensionality lemma ext states that two such characters with equal val fields coincide. Values are taken in the full unit group, not in n-th roots of unity, and no finiteness, flatness or representability hypothesis on the n-torsion is imposed.