Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.Geom.MulBy

Multiplication by an integer on an elliptic curve over a scheme #

Let E be an elliptic curve over a scheme S, with its group law: the object Over.mk π of Over S, for the structure morphism π : E ⟶ S, is a commutative group object (EllipticCurveGeom.grpObj). For an integer n, multiplication by n is the endomorphism [n] : E ⟶ E over S that sends a point x of E, with values in any T over S, to n • x, written x ^ n for the multiplicative group law on points. It is defined as the n-th power of the identity of E in the commutative group of points of E with values in E itself, and it is a homomorphism of group schemes over S, so that Grp.ofHom (E.mulBy n) is the corresponding morphism of Grp (Over S), to which the kernel constructions for group schemes apply.

On underlying schemes, [0] is the composite of the structure morphism and the zero section, [-1] is the negation morphism and [m + n] is the sum of [m] and [n] under the addition morphism. Multiplication by an integer commutes with every homomorphism of group schemes, and with arbitrary base change: a pointed morphism of elliptic curves forming a pullback square over a morphism of bases carries [n] to [n].

Main definitions #

Main results #

References #

Multiplication by an integer #

source
noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
CategoryTheory.Over.mk E.structureMap ⟶ CategoryTheory.Over.mk E.structureMap

Multiplication by an integer [n] : E ⟶ E on an elliptic curve E over a scheme S, as an endomorphism of E in Over S. It is the n-th power of the identity of E for the group law on points of E, and it sends every point x of E to x ^ n (comp_mulBy).

Instances For
    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_eq_zpow {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    E.mulBy n = CategoryTheory.CategoryStruct.id (CategoryTheory.Over.mk E.structureMap) ^ n

    Multiplication by n is the n-th power of the identity for the group law on points.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.comp_mulBy {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) (n : ℤ) :
    CategoryTheory.CategoryStruct.comp x (E.mulBy n) = x ^ n

    Multiplication by n sends a point x of E, with values in any Z over S, to x ^ n.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.comp_mulBy_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) (n : ℤ) {Z✝ : CategoryTheory.Over S} (h : CategoryTheory.Over.mk E.structureMap ⟶ Z✝) :
    CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp (E.mulBy n) h) = CategoryTheory.CategoryStruct.comp (x ^ n) h

    Multiplication by n sends a point x of E, with values in any Z over S, to x ^ n.

    source
    instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isMonHom_mulBy {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    CategoryTheory.IsMonHom (E.mulBy n)

    Multiplication by n is a homomorphism of group schemes.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_zero {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :
    E.mulBy 0 = 1

    [0] is the zero point of the group of points of E with values in E.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_one {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :
    E.mulBy 1 = CategoryTheory.CategoryStruct.id (CategoryTheory.Over.mk E.structureMap)

    [1] is the identity.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_add {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (m n : ℤ) :
    E.mulBy (m + n) = E.mulBy m * E.mulBy n

    [m + n] is the product of [m] and [n] for the group law on points.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    E.mulBy (-n) = (E.mulBy n)⁻¹

    [-n] is the inverse of [n] for the group law on points.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_sub {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (m n : ℤ) :
    E.mulBy (m - n) = E.mulBy m / E.mulBy n

    [m - n] is the quotient of [m] by [n] for the group law on points.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_mul {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (m n : ℤ) :
    E.mulBy (m * n) = CategoryTheory.CategoryStruct.comp (E.mulBy n) (E.mulBy m)

    [m * n] is [n] followed by [m].

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_comp {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {E' : EllipticCurveGeom S} (n : ℤ) (f : CategoryTheory.Over.mk E.structureMap ⟶ CategoryTheory.Over.mk E'.structureMap) [CategoryTheory.IsMonHom f] :
    CategoryTheory.CategoryStruct.comp (E.mulBy n) f = CategoryTheory.CategoryStruct.comp f (E'.mulBy n)

    Homomorphisms commute with multiplication by n. A homomorphism of group schemes f : E ⟶ E' between elliptic curves over S satisfies [n] ≫ f = f ≫ [n].

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_comp_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {E' : EllipticCurveGeom S} (n : ℤ) (f : CategoryTheory.Over.mk E.structureMap ⟶ CategoryTheory.Over.mk E'.structureMap) [CategoryTheory.IsMonHom f] {Z : CategoryTheory.Over S} (h : CategoryTheory.Over.mk E'.structureMap ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (E.mulBy n) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (E'.mulBy n) h)

    Homomorphisms commute with multiplication by n. A homomorphism of group schemes f : E ⟶ E' between elliptic curves over S satisfies [n] ≫ f = f ≫ [n].

    Multiplication by an integer on the underlying scheme #

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_left_structureMap {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) E.structureMap = E.structureMap

    Multiplication by n lies over S.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_left_structureMap_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) (CategoryTheory.CategoryStruct.comp E.structureMap h) = CategoryTheory.CategoryStruct.comp E.structureMap h

    Multiplication by n lies over S.

    source
    instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isProper_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    AlgebraicGeometry.IsProper (CategoryTheory.Over.Hom.left (E.mulBy n))

    Multiplication by n is proper, as a morphism over S between schemes proper over S.

    source
    instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.locallyOfFinitePresentation_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left (E.mulBy n))

    Multiplication by n is locally of finite presentation: it is a morphism over S between schemes smooth over S.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    CategoryTheory.CategoryStruct.comp E.zero (CategoryTheory.Over.Hom.left (E.mulBy n)) = E.zero

    Multiplication by n fixes the zero section.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_mulBy_left_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : (CategoryTheory.Over.mk E.structureMap).left ⟶ Z) :
    CategoryTheory.CategoryStruct.comp E.zero (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) h) = CategoryTheory.CategoryStruct.comp E.zero h

    Multiplication by n fixes the zero section.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zpow_eq_one_iff_left_comp_mulBy_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (n : ℤ) :
    P ^ n = 1 ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left P) (CategoryTheory.Over.Hom.left (E.mulBy n)) = E.zero

    A point is killed by n exactly when [n] carries it to the zero section. An S-point P of E satisfies P ^ n = 1 in the group of points if and only if its composite with multiplication by n is the zero section.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_zero_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :
    CategoryTheory.Over.Hom.left (E.mulBy 0) = CategoryTheory.CategoryStruct.comp E.structureMap E.zero

    On the underlying scheme, [0] is the composite of the structure morphism and the zero section.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_neg_one_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :
    CategoryTheory.Over.Hom.left (E.mulBy (-1)) = E.neg

    On the underlying scheme, [-1] is the negation morphism.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_add_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (m n : ℤ) :
    CategoryTheory.Over.Hom.left (E.mulBy (m + n)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.Over.Hom.left (E.mulBy m)) (CategoryTheory.Over.Hom.left (E.mulBy n)) ⋯) E.addition

    On the underlying scheme, [m + n] is the sum of [m] and [n] under the addition morphism.

    Multiplication by an integer and base change #

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_left_comp_of_isPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {g : E'.carrier ⟶ E.carrier} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) (n : ℤ) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E'.mulBy n)) g = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Over.Hom.left (E.mulBy n))

    Multiplication by n commutes with base change. Let g : E' ⟶ E be a morphism of elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure morphisms is a pullback square, and carrying the zero section of E' to that of E. Then g carries multiplication by n on E' to multiplication by n on E.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_left_comp_of_isPullback_assoc {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {g : E'.carrier ⟶ E.carrier} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E'.mulBy n)) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) h)

    Multiplication by n commutes with base change. Let g : E' ⟶ E be a morphism of elliptic curves lying over f : S' ⟶ S, such that the square formed by g, f and the structure morphisms is a pullback square, and carrying the zero section of E' to that of E. Then g carries multiplication by n on E' to multiplication by n on E.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isPullback_mulBy_left_of_isPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {g : E'.carrier ⟶ E.carrier} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) (n : ℤ) :
    CategoryTheory.IsPullback g (CategoryTheory.Over.Hom.left (E'.mulBy n)) (CategoryTheory.Over.Hom.left (E.mulBy n)) g

    Multiplication by n on a base change is a base change of multiplication by n. For a morphism g : E' ⟶ E of elliptic curves forming a pullback square over f : S' ⟶ S and carrying the zero section of E' to that of E, the square formed by g on both sides and the two multiplications by n is a pullback square.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_left_baseChangeIso_hom_fst {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {S' : AlgebraicGeometry.Scheme} (f : S' ⟶ S) (n : ℤ) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((E.baseChange f).mulBy n)) (CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.Limits.pullback.fst E.structureMap f)) = CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst E.structureMap f) (CategoryTheory.Over.Hom.left (E.mulBy n)))

    Multiplication by n on a base change. The projection from the base change E.baseChange f to E carries multiplication by n on E.baseChange f to multiplication by n on E.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mulBy_left_baseChangeIso_hom_fst_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {S' : AlgebraicGeometry.Scheme} (f : S' ⟶ S) (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((E.baseChange f).mulBy n)) (CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst E.structureMap f) h)) = CategoryTheory.CategoryStruct.comp (E.baseChangeIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst E.structureMap f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) h))

    Multiplication by n on a base change. The projection from the base change E.baseChange f to E carries multiplication by n on E.baseChange f to multiplication by n on E.