Recovering rational Gamma_0 data from a split finite-flat subgroup

This file records the inverse, point-level direction of the existing finite-flat Gamma_0(N) construction. A split finite-flat cyclic subgroup of a represented Weierstrass group scheme has a finite cyclic group of rational points. Its closed immersion and the supplied comparison with Weierstrass coordinates therefore cut out a genuine RationalCyclicSubgroup of exact order N.

For the canonical finite-flat subgroup constructed from a rational cyclic subgroup, the recovered carrier is definitionally independent of the cyclic trivialization and is proved to be the original carrier. This is the strongest classifying-data bridge below the remaining representability boundary: neither an elliptic quotient E/C nor a coarse X_0(N) point is asserted.

@[instance_reducible]

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.classifyingDataRationalCyclicSubgroupFintype {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) : Fintype ↥C.carrier

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.classifyingDataRationalCyclicSubgroupFintype C = Fintype.ofFinite ↥C.carrier

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.SplitSubgroupRationalPoint {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : Type u

Rational points of the carrier of an arbitrary split finite-flat subgroup.

Equations

• M.SplitSubgroupRationalPoint D = Additive (D.subgroup.carrier.Point (AlgebraicGeometry.AffineCommGroupScheme.testObject K))

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitTrivialization {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : D.subgroup.carrier ≅ cyclicConstant K N

A chosen split trivialization. Its choice affects the auxiliary equivalence below, but not the subgroup image used to recover rational moduli data.

Equations

• M.splitTrivialization D = ⋯.some

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitSubgroupPointAddEquiv {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : M.SplitSubgroupRationalPoint D ≃+ Additive (CyclicIndex N)

The rational points of a split carrier form the standard cyclic group of order N.

Equations

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

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitSubgroupCoordinatePointHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : M.SplitSubgroupRationalPoint D →+ W.toAffine.Point

The point homomorphism induced by the actual finite-flat closed immersion, transported back to Weierstrass coordinates.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitSubgroupCoordinatePointHom_injective {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : Function.Injective ⇑(M.splitSubgroupCoordinatePointHom D)

Closedness of the subgroup immersion makes its map on rational points injective.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupOfSplitGammaZeroDatum {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N

The coordinate-point image of an arbitrary split finite-flat subgroup is a rational cyclic subgroup of exact order N.

Equations

• M.rationalCyclicSubgroupOfSplitGammaZeroDatum D = { carrier := (M.splitSubgroupCoordinatePointHom D).range, isAddCyclic := ⋯, card_eq := ⋯ }

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumOfSplitGammaZeroDatum {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} [W.IsElliptic] (M : WeierstrassGroupSchemeInterface W) (D : SplitGammaZeroDatum W M) : XZeroModuli.RationalDatum K N

Forget a represented split finite-flat Gamma_0(N) datum to the checked raw rational moduli datum.

Equations

• M.rationalDatumOfSplitGammaZeroDatum D = MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.datumOfRationalCyclicSubgroup W (M.rationalCyclicSubgroupOfSplitGammaZeroDatum D)

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitSubgroupCoordinatePointHom_ofRationalCyclicSubgroup_apply {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) (z : ↥C.carrier) : (M.splitSubgroupCoordinatePointHom (splitGammaZeroDatumOfRationalCyclicSubgroup W M C)) (Additive.ofMul (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K (Multiplicative ↥C.carrier) (Multiplicative.ofAdd z))) = ↑z

On the canonical finite-flat datum attached to a coordinate subgroup, the recovered coordinate map sends the distinguished constant point indexed by z to z itself.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupOfSplitGammaZeroDatum_carrier_ofRationalCyclicSubgroup {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) : (M.rationalCyclicSubgroupOfSplitGammaZeroDatum (splitGammaZeroDatumOfRationalCyclicSubgroup W M C)).carrier = C.carrier

The rational-point carrier recovered from the canonical finite-flat construction is exactly the original coordinate subgroup. In particular it does not depend on the cyclic trivialization chosen to prove splitness.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupOfSplitGammaZeroDatum_ofRationalCyclicSubgroup {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] {W : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W) (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) : M.rationalCyclicSubgroupOfSplitGammaZeroDatum (splitGammaZeroDatumOfRationalCyclicSubgroup W M C) = C

Constructing finite-flat Gamma_0(N) data from a rational subgroup and then recovering coordinate data returns the original rational subgroup.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumOfSplitGammaZeroDatum_ofRationalDatum {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : M.rationalDatumOfSplitGammaZeroDatum (splitGammaZeroDatumOfRationalDatum x M) = x

The finite-flat construction followed by coordinate recovery is a section of the forgetful map on every checked raw rational Gamma_0(N) datum.