Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.Geom.Hom

Homomorphisms and endomorphisms of elliptic curves over a scheme #

Let E and E' be elliptic curves over a scheme S, with their group laws. This file regards E as a commutative group scheme over S, that is, a commutative group object E.toCommGrp of Over S. A homomorphism E ⟶ E' of elliptic curves over S is then a morphism E.toCommGrp ⟶ E'.toCommGrp of CommGrp (Over S): a morphism of schemes over S together with the property of being a homomorphism of group schemes. A bare morphism of schemes over S carrying zero to zero is not a homomorphism by definition: that every such morphism is one is a theorem (Katz–Mazur 2.5.1) which this type does not presuppose.

Since CommGrp (Over S) is preadditive (CategoryTheory.CommGrp.instPreadditive), the homomorphisms E.toCommGrp ⟶ E'.toCommGrp form an abelian group Hom_S(E, E'), and the endomorphisms End E.toCommGrp form a ring End_S(E) whose multiplication is composition, f * g = g ≫ f. On underlying schemes, the sum of two homomorphisms is their sum under the addition morphism of E', the zero homomorphism is the composite of the structure morphism of E and the zero section of E', and the negative is the composite with the negation morphism.

In End_S(E), the integer n is multiplication by n (EllipticCurveGeom.mulBy), so the ring homomorphism ℤ → End_S(E) is multiplication by integers. Its image in the category of group schemes over S is the homomorphism whose kernel is the n-torsion E[n].

Main definitions #

Main results #

References #

source
@[reducible, inline]
noncomputable abbrev TauCeti.AlgebraicGeometry.EllipticCurveGeom.toCommGrp {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) :
CategoryTheory.CommGrp (CategoryTheory.Over S)

An elliptic curve as a commutative group scheme. The elliptic curve E over S, as the object Over.mk E.structureMap of Over S with its commutative group law, is a commutative group object of Over S. The morphisms E.toCommGrp ⟶ E'.toCommGrp are the homomorphisms of elliptic curves over S, and they form an abelian group.

Instances For
    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_ext_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {E' : EllipticCurveGeom S} {f g : E.toCommGrp ⟶ E'.toCommGrp} (h : CategoryTheory.Over.Hom.left f.hom.hom.hom = CategoryTheory.Over.Hom.left g.hom.hom.hom) :
    f = g

    Homomorphisms of elliptic curves are determined by their morphisms of schemes.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_hom_hom_left_comp_structureMap {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom.hom.hom) E'.structureMap = E.structureMap

    The morphism of schemes underlying a homomorphism of elliptic curves over S commutes with the structure morphisms to S.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_hom_hom_left_comp_structureMap_assoc {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom.hom.hom) (CategoryTheory.CategoryStruct.comp E'.structureMap h) = CategoryTheory.CategoryStruct.comp E.structureMap h

    The morphism of schemes underlying a homomorphism of elliptic curves over S commutes with the structure morphisms to S.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIso_iff_isIso_hom_hom_hom_left {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} {f : E.toCommGrp ⟶ E'.toCommGrp} :
    CategoryTheory.IsIso f ↔ CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom.hom.hom)

    A homomorphism of elliptic curves is an isomorphism exactly when its morphism of schemes is one.

    source
    instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.locallyOfFinitePresentation_hom_hom_hom_left {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) :
    AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Over.Hom.left f.hom.hom.hom)

    Homomorphisms of elliptic curves are locally of finite presentation: the underlying morphism of schemes is a morphism over S between schemes smooth over S.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.add_hom_hom_hom_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {E' : EllipticCurveGeom S} (f g : E.toCommGrp ⟶ E'.toCommGrp) :
    CategoryTheory.Over.Hom.left (f + g).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.Over.Hom.left f.hom.hom.hom) (CategoryTheory.Over.Hom.left g.hom.hom.hom) ⋯) E'.addition

    The sum of two homomorphisms of elliptic curves over S is, on underlying schemes, their sum under the addition morphism of the target.

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

    The zero homomorphism of elliptic curves over S is, on underlying schemes, the structure morphism of the source followed by the zero section of the target.

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_hom_hom_hom_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) :
    CategoryTheory.Over.Hom.left (-f).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom.hom.hom) E'.neg

    The negative of a homomorphism of elliptic curves over S is, on underlying schemes, the homomorphism followed by the negation morphism of the target.

    Multiplication by an integer in the endomorphism ring #

    source
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.homMk_mulBy {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    CategoryTheory.CommGrp.homMk (E.mulBy n) = (↑n).asHom

    Multiplication by n is the integer n of the endomorphism ring. The homomorphism of elliptic curves given by [n] : E ⟶ E is the image of n under ℤ → End_S(E).

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.intCast_hom_hom_hom {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    (↑n).asHom.hom.hom.hom = E.mulBy n

    The integer n of the endomorphism ring of E is multiplication by n. This takes priority over the general CategoryTheory.CommGrp.intCast_hom_hom_hom, so that E.mulBy n is the simp normal form.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.natCast_hom_hom_hom {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℕ) :
    (↑n).asHom.hom.hom.hom = E.mulBy ↑n

    The natural number n of the endomorphism ring of E is multiplication by n.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.forget₂Grp_map_intCast {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (n : ℤ) :
    (CategoryTheory.CommGrp.forget₂Grp (CategoryTheory.Over S)).map (↑n).asHom = CategoryTheory.Grp.ofHom (E.mulBy n)

    The image of the integer n of the endomorphism ring of E in the category of group schemes over S is multiplication by n.