Definitions/Def_ModularCurve_FppfKummerInterface.lean

Two bundles of data, in a fixed universe, axiomatising the cohomological input of a Kummer-theory argument over S=\operatorname{Spec}\mathbb{Z} in purely group-theoretic terms: no site, scheme or cohomology theory occurs, only types, additive commutative group structures on them, homomorphisms, and propositions carried as fields, so that producing a term of either structure amounts to proving the asserted facts for the chosen model.

ModularCurve.FppfKummerData p, for a natural number p, consists of three types H0Gm, H1mu, H1Z, each equipped with an additive commutative group structure (the structures being instance-valued fields), a homomorphism kummerDelta : H0Gm →+ H1mu, and three propositions: kummerDelta is surjective; H1Z is a subsingleton, i.e. the trivial group; and H1mu is a subsingleton whenever p is odd. The intended reading is H^0(S,\mathbb{G}_m), H^1(S,\mu_p), H^1(S,\mathbb{Z}/p) with the Kummer boundary map; note that the vanishing of H1Z is unconditional while that of H1mu is asserted only under Odd p.

ModularCurve.JKummerRow p m M, for natural numbers p,m and an additive commutative group M, consists of three types M0, H1Jtors, H1J with additive commutative group structures, a homomorphism toM : M0 →+ M which is injective and whose range is an additive subgroup of finite index, and homomorphisms delta : M0 →+ H1Jtors, push : H1Jtors →+ H1J subject to three conditions: the kernel of delta equals the range of multiplication by p^m on M0, i.e. p^m\,M0; the pair delta, push is exact in the sense of Function.Exact (range of delta equals kernel of push); and the range of push equals the kernel of multiplication by p^m on H1J, i.e. the p^m-torsion of H1J. Thus delta induces an injection of M0/p^mM0 into H1Jtors and push maps H1Jtors onto H1J[p^m].