The point-group quotient attached to a rational cyclic subgroup

A cyclic subgroup C of order N is killed by multiplication by N. Consequently multiplication by N on the ambient rational point group descends through the quotient by C. If

π : A → A ⧸ C,

the descended map π dual : A ⧸ C → A satisfies

dual ∘ π = [N] and π ∘ dual = [N].

These are the point-group identities expected from an isogeny and its dual. They are useful compatibility conditions for the future elliptic quotient in the X₀(N) moduli construction. This file does not claim that the abstract quotient group is represented by an elliptic curve or construct a quotient group scheme.

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.PointQuotient {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : Type u

The abstract quotient of the rational point group by the supplied cyclic subgroup. Representability by an elliptic quotient remains separate geometry.

Equations

• C.PointQuotient = (A ⧸ C.carrier)

def MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.quotientMap {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : A →+ C.PointQuotient

The canonical projection to the point-group quotient.

Equations

• C.quotientMap = QuotientAddGroup.mk' C.carrier

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.quotientMap_surjective {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : Function.Surjective ⇑C.quotientMap

The point-group quotient projection is surjective.

@[simp]

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.quotientMap_ker {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : C.quotientMap.ker = C.carrier

The kernel of the point-group quotient projection is exactly the supplied cyclic subgroup.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.carrier_le_nsmul_ker {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : C.carrier ≤ (nsmulAddMonoidHom N).ker

Every element of a cyclic subgroup of cardinality N is killed by multiplication by N.

def MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.dualMap {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : C.PointQuotient →+ A

Multiplication by N descended through the quotient by C.

For an elliptic quotient this is the rational-point map expected from the dual isogeny.

Equations

• C.dualMap = QuotientAddGroup.lift C.carrier (nsmulAddMonoidHom N) ⋯

@[simp]

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.dualMap_mk {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) (x : A) : C.dualMap (C.quotientMap x) = N • x

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.dualMap_comp_quotientMap {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : C.dualMap.comp C.quotientMap = nsmulAddMonoidHom N

The descended dual after the quotient projection is multiplication by N on the ambient point group.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.quotientMap_comp_dualMap {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : C.quotientMap.comp C.dualMap = nsmulAddMonoidHom N

The quotient projection after the descended dual is multiplication by N on the quotient point group.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.dualMap_ker {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) : C.dualMap.ker = AddSubgroup.map C.quotientMap (nsmulAddMonoidHom N).ker

The kernel of the descended dual is the image in A/C of the full N-torsion kernel in A.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.addOrderOf_divisorSubgroup_quotientMap_generator {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) (d : ℕ) [NeZero d] (hd : d ∣ N) : addOrderOf ((C.divisorSubgroup d hd).quotientMap ↑C.generator) = N / d

Modulo the intrinsic subgroup of order d, a generator of a cyclic subgroup of order N has exact order N / d.

The upper bound follows because (N / d) • C.generator generates the divisor subgroup. For the reverse divisibility, the descended dual map sends the quotient class to d • C.generator, which already has order N / d.

def MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.mapPointQuotient {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) {B : Type u_1} [AddCommGroup B] (e : A ≃+ B) : C.PointQuotient ≃+ (C.map e).PointQuotient

Transport the point-group quotient along an isomorphism of ambient point groups.

Equations

• C.mapPointQuotient e = QuotientAddGroup.congr C.carrier (C.map e).carrier e ⋯

@[simp]

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.mapPointQuotient_quotientMap {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) {B : Type u_1} [AddCommGroup B] (e : A ≃+ B) (x : A) : (C.mapPointQuotient e) (C.quotientMap x) = (C.map e).quotientMap (e x)

Transport of the quotient sends the class of x to the class of e x.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.mapPointQuotient_dualMap {A : Type u} [AddCommGroup A] {N : ℕ} [NeZero N] (C : RationalCyclicSubgroup A N) {B : Type u_1} [AddCommGroup B] (e : A ≃+ B) (x : C.PointQuotient) : e (C.dualMap x) = (C.map e).dualMap ((C.mapPointQuotient e) x)

The descended dual multiplication map is natural under transport of the ambient point group.

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.PointQuotient {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) : Type u

The abstract quotient of the rational point group attached to a split Γ₀(N) datum.

Equations

• x.PointQuotient = x.subgroup.PointQuotient

def MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.pointQuotientMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) : x.curve.toAffine.Point →+ x.PointQuotient

The point-group quotient projection attached to a split rational modular datum.

Equations

• x.pointQuotientMap = x.subgroup.quotientMap

def MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.pointQuotientDualMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) : x.PointQuotient →+ x.curve.toAffine.Point

The descended multiplication map attached to a split rational modular datum.

Equations

• x.pointQuotientDualMap = x.subgroup.dualMap

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.pointQuotientDualMap_comp_pointQuotientMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) : x.pointQuotientDualMap.comp x.pointQuotientMap = nsmulAddMonoidHom N

A real RationalDatum consumer of the quotient/dual API: composing the two point maps in the ambient direction is multiplication by the level.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.pointQuotientMap_comp_pointQuotientDualMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) : x.pointQuotientMap.comp x.pointQuotientDualMap = nsmulAddMonoidHom N

In the quotient direction the same two maps also compose to multiplication by the level.

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.variableChangePointEquiv {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) (C : WeierstrassCurve.VariableChange K) : x.curve.toAffine.Point ≃+ (x.variableChange C).curve.toAffine.Point

The point-group isomorphism used by an admissible change of Weierstrass variables.

Equations

• x.variableChangePointEquiv C = (WeierstrassCurve.Affine.Point.equivVariableChange x.curve C).symm

def MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.variableChangePointQuotientEquiv {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) (C : WeierstrassCurve.VariableChange K) : x.PointQuotient ≃+ (x.variableChange C).PointQuotient

An admissible change of Weierstrass variables transports the point-group quotient attached to the cyclic subgroup.

Equations

• x.variableChangePointQuotientEquiv C = x.subgroup.mapPointQuotient (x.variableChangePointEquiv C)

@[simp]

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.variableChangePointQuotientEquiv_pointQuotientMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) (C : WeierstrassCurve.VariableChange K) (P : x.curve.toAffine.Point) : (x.variableChangePointQuotientEquiv C) (x.pointQuotientMap P) = (x.variableChange C).pointQuotientMap ((x.variableChangePointEquiv C) P)

The variable-change quotient equivalence commutes with the canonical quotient projections.

theorem MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.variableChangePointQuotientEquiv_dualMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : RationalDatum K N) (C : WeierstrassCurve.VariableChange K) (Q : x.PointQuotient) : (x.variableChangePointEquiv C) (x.pointQuotientDualMap Q) = (x.variableChange C).pointQuotientDualMap ((x.variableChangePointQuotientEquiv C) Q)

The variable-change quotient equivalence also commutes with the descended dual multiplication map.