Isogenies of elliptic curves over a scheme

Let E and E' be elliptic curves over a scheme S. A homomorphism f : E ⟶ E' of elliptic curves over S (a morphism E.toCommGrp ⟶ E'.toCommGrp of commutative group schemes) is an isogeny when it is an isogeny of group schemes (TauCeti.GroupScheme.IsIsogeny): its underlying morphism of schemes is finite, flat and surjective (EllipticCurveGeom.IsIsogeny). Every homomorphism of elliptic curves is locally of finite presentation (EllipticCurveGeom.locallyOfFinitePresentation_hom_hom_hom_left), so an isogeny is finite locally free.

The degree of an isogeny is the degree TauCeti.GroupScheme.degree f.hom of the underlying homomorphism of group schemes, the rank of its kernel, and an isogeny of constant degree n is TauCeti.GroupScheme.IsogenyOfDegree f.hom n. The instances of this file supply the finiteness, flatness, surjectivity and local finite presentation hypotheses of that API, so its results (local constancy and positivity of the degree, multiplicativity under composition, the isogenies of degree one being the isomorphisms, and the kernel of an isogeny of degree n being killed by n) apply to every isogeny of elliptic curves directly. Multiplication by a nonzero integer n is an isogeny of degree n² over any base.

Consequently the factorisation dual TauCeti.GroupScheme.factorisationDual of an isogeny of elliptic curves of degree n ≠ 0, which factors multiplication by n through the isogeny, is again an isogeny of degree n, and multiplication by m ≠ 0 is its own factorisation dual.

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsIsogeny f: the homomorphism f is an isogeny.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIsogeny_iff: f is an isogeny exactly when its underlying morphism of schemes is finite, flat and surjective.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.degree_intCast and TauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_intCast: multiplication by a nonzero integer n is an isogeny of degree n².
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_factorisationDual: the factorisation dual of an isogeny of degree n ≠ 0 is an isogeny of degree n.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.factorisationDual_intCast: multiplication by a nonzero integer is its own factorisation dual.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §2.4 and 2.3.1.

Isogenies

class TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsIsogeny {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) : Prop

Isogenies of elliptic curves. A homomorphism f : E ⟶ E' of elliptic curves over S is an isogeny when it is an isogeny of group schemes, that is, its underlying morphism of schemes is finite, flat and surjective (Katz–Mazur §2.4). It is then finite locally free, since it is locally of finite presentation like every homomorphism of elliptic curves (locallyOfFinitePresentation_hom_hom_hom_left).

• isIsogeny : GroupScheme.IsIsogeny f.hom

  The underlying homomorphism of group schemes is an isogeny.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIsogeny_iff {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) : IsIsogeny f ↔ AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom.hom) ∧ AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom.hom) ∧ AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom.hom)

A homomorphism of elliptic curves is an isogeny exactly when its underlying morphism of schemes is finite, flat and surjective.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsIsogeny.isFinite {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) [IsIsogeny f] : AlgebraicGeometry.IsFinite (CategoryTheory.Over.Hom.left f.hom.hom.hom)

The morphism of schemes underlying an isogeny is finite.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsIsogeny.flat {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) [IsIsogeny f] : AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom.hom)

The morphism of schemes underlying an isogeny is flat.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsIsogeny.surjective {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) [IsIsogeny f] : AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom.hom)

The morphism of schemes underlying an isogeny is surjective.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIsogeny_of_isIso {S : AlgebraicGeometry.Scheme} {E E' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) [CategoryTheory.IsIso f] : IsIsogeny f

An isomorphism of elliptic curves is an isogeny.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIsogeny_comp {S : AlgebraicGeometry.Scheme} {E E' E'' : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) (g : E'.toCommGrp ⟶ E''.toCommGrp) [IsIsogeny f] [IsIsogeny g] : IsIsogeny (CategoryTheory.CategoryStruct.comp f g)

The composite of two isogenies is an isogeny.

Multiplication by an integer

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIsogeny_intCast {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) : IsIsogeny (↑n).asHom

Multiplication by a nonzero integer is an isogeny (Katz–Mazur 2.3.1), over any base.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.degree_intCast {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) (s : ↥S) : GroupScheme.degree (↑n).asHom.hom s = n.natAbs ^ 2

Multiplication by a nonzero integer n has degree n² (Katz–Mazur 2.3.1): the rank of its kernel E[n] is n² at every point of S.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_intCast {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {n : ℤ} (hn : n ≠ 0) : GroupScheme.IsogenyOfDegree (↑n).asHom.hom (n.natAbs ^ 2)

Multiplication by a nonzero integer n is an isogeny of degree n².

The factorisation dual

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.factorisationDual_intCast {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {m : ℤ} (hm : m ≠ 0) : GroupScheme.factorisationDual (↑m).asHom ⋯ = (↑m).asHom

Multiplication by a nonzero integer is its own factorisation dual. Multiplication by m ≠ 0 is an isogeny of degree m², and its factorisation dual is multiplication by m.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_factorisationDual {S : AlgebraicGeometry.Scheme} {E' E : EllipticCurveGeom S} (f : E.toCommGrp ⟶ E'.toCommGrp) {n : ℕ} [NeZero n] (hf : GroupScheme.IsogenyOfDegree f.hom n) : GroupScheme.IsogenyOfDegree (GroupScheme.factorisationDual f hf).hom n

The factorisation dual of an isogeny of degree n is an isogeny of degree n. For an isogeny f : E ⟶ E' of degree n ≠ 0, the factorisation dual E' ⟶ E is again an isogeny of degree n; by TauCeti.GroupScheme.factorisationDual_factorisationDual, its own factorisation dual is f.