Rational points of the finite-flat cyclic quotient

The split Gamma_0(N) construction attaches an actual closed finite-flat subgroup scheme to a RationalDatum. This file compares its rational-point quotient with the abstract coordinate-point quotient used by the existing cyclic-quotient API.

For a supplied WeierstrassGroupSchemeInterface, the comparison proceeds in three checked steps:

• all rational points of the constant subgroup carrier are distinguished sections indexed by the original cyclic group;
• the image of those sections under the actual closed subgroup immersion is exactly the image of the original rational cyclic subgroup;
• quotienting the represented rational point group by that image transports both the quotient projection and the descended multiplication-by-N map.

Thus the point-group quotient is compatible with the already represented source group scheme and its genuine finite-flat subgroup. No scheme representing the quotient, elliptic-curve structure on such a scheme, or base-change theorem for the quotient is asserted here.

@[instance_reducible]

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumSubgroupFintype {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) : Fintype ↥x.subgroup.carrier

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumSubgroupFintype x = Fintype.ofFinite ↥x.subgroup.carrier

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.RepresentedRationalPoint {K : Type u} [Field K] [DecidableEq K] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) : Type u

Rational points of the represented Weierstrass group scheme, written additively to match Mathlib's coordinate point group.

Equations

• M.RepresentedRationalPoint = Additive (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.Point M.groupScheme (AlgebraicGeometry.AffineCommGroupScheme.testObject K))

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalPointAddEquiv {K : Type u} [Field K] [DecidableEq K] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) : W.toAffine.Point ≃+ M.RepresentedRationalPoint

The supplied coordinate-to-scheme point comparison in additive notation.

Equations

• M.rationalPointAddEquiv = MulEquiv.toAdditive M.rationalPointEquiv

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalPointAddEquiv_apply {K : Type u} [Field K] [DecidableEq K] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) : M.rationalPointAddEquiv P = Additive.ofMul (M.rationalPointEquiv (Multiplicative.ofAdd P))

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.FiniteFlatSubgroupRationalPoint {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : Type u

Rational points of the actual finite-flat subgroup carrier attached to a raw rational datum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupPointHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : FiniteFlatSubgroupRationalPoint x M →+ M.RepresentedRationalPoint

The map on rational points induced by the genuine closed finite-flat subgroup immersion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupConstantPointEquiv {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : ↥x.subgroup.carrier ≃+ FiniteFlatSubgroupRationalPoint x M

Over the field K, the points of the constant subgroup carrier are exactly the elements of the original cyclic subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupConstantPointEquiv_apply {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (z : ↥x.subgroup.carrier) : (finiteFlatSubgroupConstantPointEquiv x M) z = Additive.ofMul (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K (Multiplicative ↥x.subgroup.carrier) (Multiplicative.ofAdd z))

The constant-point equivalence sends an element to its distinguished section of the constant finite-flat carrier.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupPointHom_constantPointEquiv_apply {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (z : ↥x.subgroup.carrier) : (finiteFlatSubgroupPointHom x M) ((finiteFlatSubgroupConstantPointEquiv x M) z) = M.rationalPointAddEquiv ↑z

The actual closed subgroup immersion agrees, on every rational point of its carrier, with the original coordinate subgroup inclusion.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupPointHom_comp_constantPointEquiv {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (finiteFlatSubgroupPointHom x M).comp (finiteFlatSubgroupConstantPointEquiv x M).toAddMonoidHom = M.rationalPointAddEquiv.toAddMonoidHom.comp x.subgroup.carrier.subtype

Homomorphism form of compatibility between the actual finite-flat subgroup points and the coordinate subgroup.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupPointRange {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : AddSubgroup M.RepresentedRationalPoint

The rational-point image of the genuine finite-flat subgroup immersion.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupPointRange_eq_map {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : finiteFlatSubgroupPointRange x M = AddSubgroup.map M.rationalPointAddEquiv.toAddMonoidHom x.subgroup.carrier

The image of the actual finite-flat subgroup immersion is precisely the coordinate cyclic subgroup transported into represented rational points.

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.RepresentedPointQuotient {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : Type u

The quotient of represented rational points by the image of the actual closed finite-flat subgroup. This is a point group, not a quotient scheme.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : M.RepresentedRationalPoint →+ RepresentedPointQuotient x M

The canonical projection to the quotient of represented rational points.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientMap_surjective {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : Function.Surjective ⇑(representedPointQuotientMap x M)

The represented rational-point quotient projection is surjective.

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientMap_ker {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (representedPointQuotientMap x M).ker = finiteFlatSubgroupPointRange x M

The kernel of the represented rational-point quotient is exactly the image of the actual finite-flat subgroup immersion.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientMap_comp_finiteFlatSubgroupPointHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (representedPointQuotientMap x M).comp (finiteFlatSubgroupPointHom x M) = 0

The quotient projection kills the rational points coming from the actual closed finite-flat subgroup.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientEquiv {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : x.PointQuotient ≃+ RepresentedPointQuotient x M

The coordinate-point quotient attached to x is canonically equivalent to the quotient by the image of its genuine finite-flat subgroup.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientEquiv_pointQuotientMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (P : x.curve.toAffine.Point) : (representedPointQuotientEquiv x M) (x.pointQuotientMap P) = (representedPointQuotientMap x M) (M.rationalPointAddEquiv P)

The quotient equivalence commutes with the two canonical quotient projections.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.finiteFlatSubgroupPointRange_le_nsmul_ker {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : finiteFlatSubgroupPointRange x M ≤ (nsmulAddMonoidHom N).ker

The rational-point image of the finite-flat cyclic subgroup is killed by multiplication by its order.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientDualMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : RepresentedPointQuotient x M →+ M.RepresentedRationalPoint

Multiplication by N descended through the quotient of represented rational points.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientDualMap_mk {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (P : M.RepresentedRationalPoint) : (representedPointQuotientDualMap x M) ((representedPointQuotientMap x M) P) = N • P

The descended map sends the class of a represented point to its N-fold multiple.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientDualMap_comp_quotientMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (representedPointQuotientDualMap x M).comp (representedPointQuotientMap x M) = nsmulAddMonoidHom N

Descended multiplication after the quotient projection is multiplication by N.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientMap_comp_dualMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (representedPointQuotientMap x M).comp (representedPointQuotientDualMap x M) = nsmulAddMonoidHom N

Quotient projection after the descended map is multiplication by N on the represented rational-point quotient.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientDualMap_ker {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (representedPointQuotientDualMap x M).ker = AddSubgroup.map (representedPointQuotientMap x M) (nsmulAddMonoidHom N).ker

The kernel of the descended map is the image of the full represented N-torsion subgroup in the point quotient.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.representedPointQuotientEquiv_dualMap {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (Q : x.PointQuotient) : (representedPointQuotientDualMap x M) ((representedPointQuotientEquiv x M) Q) = M.rationalPointAddEquiv (x.pointQuotientDualMap Q)

The quotient equivalence intertwines the abstract descended dual map with descended multiplication on represented rational points.