Finite-flat split cyclic subgroup data for X₀(N)

The pinned Mathlib represents Weierstrass curves and their point groups by coordinates, but does not construct the corresponding projective scheme or its group-scheme law. The project does, however, have genuine finite-flat commutative group schemes, their base change, and explicit constant group schemes. This file connects those two layers without identifying them.

We first define an actual finite-locally-free closed subgroup of an arbitrary commutative group scheme. Over an affine base, a split cyclic subgroup is one whose finite-flat carrier is isomorphic to the constant group scheme on ZMod N. This is a restricted Γ₀(N) datum: a general cyclic subgroup need only become constant fppf-locally, and at primes dividing N the usual generalized cyclicity condition requires still more care.

The final section records the precise remaining Weierstrass scheme interface: a commutative group scheme with the expected rational point group. The extension of an injective finite constant family of rational sections to a closed subgroup-scheme immersion is constructed in the imported finite-flat group-scheme layer. Given the remaining interface, a marked point of exact order N constructs a genuine split finite-flat Γ₀(N) datum. The checked point comparison proves that its rational points recover exactly the existing point-group carrier.

No representability of X₀(N), elliptic quotient E/C, Atkin--Lehner action, or closure of split data under that action is asserted here.

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.Point {S : AlgebraicGeometry.Scheme} (G : AlgebraicGeometry.CommGroupScheme S) (X : CategoryTheory.Over S) : Type u

Points of an arbitrary commutative group scheme on a test scheme over the same base.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.Point G X = (X ⟶ G.X)

@[reducible, inline]

noncomputable abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.underlyingHom {S : AlgebraicGeometry.Scheme} {G H : AlgebraicGeometry.CommGroupScheme S} (f : G ⟶ H) : G.X.left ⟶ H.X.left

The underlying scheme morphism of a commutative group-scheme morphism.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.underlyingHom f = CategoryTheory.Over.Hom.left f.hom.hom.hom

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.mapPoint {S : AlgebraicGeometry.Scheme} {G H : AlgebraicGeometry.CommGroupScheme S} (f : G ⟶ H) (X : CategoryTheory.Over S) : Point G X →* Point H X

A commutative group-scheme morphism acts on every test-point group.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.mapPoint f X = CategoryTheory.IsMonHom.monoidHom f.hom.hom.hom X

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CommGroupScheme.mapPoint_apply {S : AlgebraicGeometry.Scheme} {G H : AlgebraicGeometry.CommGroupScheme S} (f : G ⟶ H) (X : CategoryTheory.Over S) (x : Point G X) : (mapPoint f X) x = CategoryTheory.CategoryStruct.comp x f.hom.hom.hom

structure MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.FiniteLocallyFreeSubgroup {S : AlgebraicGeometry.Scheme} (E : AlgebraicGeometry.CommGroupScheme S) : Type (u + 1)

A finite-locally-free closed subgroup of a commutative group scheme.

The carrier is a genuine finite-flat commutative group scheme and the inclusion is a group-scheme morphism whose underlying scheme map is a closed immersion.

• carrier : AlgebraicGeometry.FiniteFlatCommGroupScheme S

  The finite-flat carrier.

• inclusion : self.carrier.obj ⟶ E

  Its homomorphism into the ambient group scheme.

• inclusion_isClosedImmersion : AlgebraicGeometry.IsClosedImmersion (CommGroupScheme.underlyingHom self.inclusion)

  The homomorphism is a subgroup-scheme inclusion.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.FiniteLocallyFreeSubgroup.baseChange {S T : AlgebraicGeometry.Scheme} {E : AlgebraicGeometry.CommGroupScheme S} (C : FiniteLocallyFreeSubgroup E) (f : T ⟶ S) : FiniteLocallyFreeSubgroup ((CategoryTheory.Over.pullback f).mapCommGrp.obj E)

Base change of a finite-locally-free closed subgroup.

Equations

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

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.FiniteLocallyFreeSubgroup.baseChange_carrier {S T : AlgebraicGeometry.Scheme} {E : AlgebraicGeometry.CommGroupScheme S} (C : FiniteLocallyFreeSubgroup E) (f : T ⟶ S) : (C.baseChange f).carrier = (AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange f).obj C.carrier

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.FiniteLocallyFreeSubgroup.baseChange_inclusion {S T : AlgebraicGeometry.Scheme} {E : AlgebraicGeometry.CommGroupScheme S} (C : FiniteLocallyFreeSubgroup E) (f : T ⟶ S) : (C.baseChange f).inclusion = (CategoryTheory.Over.pullback f).mapCommGrp.map C.inclusion

@[reducible, inline]

abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CyclicIndex (N : ℕ) : Type u

Universe-compatible indexing group for the constant cyclic scheme.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CyclicIndex N = ULift.{?u.1, 0} (Multiplicative (ZMod N))

def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicIndexDown (N : ℕ) : CyclicIndex N →* Multiplicative (ZMod N)

Forget the universe lift on the cyclic indexing group.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicIndexDown N = { toFun := fun (z : MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CyclicIndex N) => z.down, map_one' := ⋯, map_mul' := ⋯ }

def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicIndexUp (N : ℕ) : Multiplicative (ZMod N) →* CyclicIndex N

Include the standard cyclic group into its universe lift.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicIndexUp N = { toFun := fun (z : Multiplicative (ZMod N)) => { down := z }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicIndexDown_up (N : ℕ) (z : Multiplicative (ZMod N)) : (cyclicIndexDown N) ((cyclicIndexUp N) z) = z

@[reducible, inline]

noncomputable abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicConstant (K : Type u) [Field K] (N : ℕ) [NeZero N] : AlgebraicGeometry.FiniteFlatCommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))

The constant finite-flat multiplicative group attached to the additive cyclic group ZMod N.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicConstant K N = AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme K (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.CyclicIndex N)

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicConstant_orderAt (K : Type u) [Field K] (N : ℕ) [NeZero N] (s : ↥(AlgebraicGeometry.Spec (CommRingCat.of K))) : (cyclicConstant K N).orderAt s = N

The constant cyclic group scheme has geometric order N.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicConstant_hasConstantOrder (K : Type u) [Field K] (N : ℕ) [NeZero N] : (cyclicConstant K N).HasConstantOrder N

The constant cyclic group scheme has constant order N.

structure MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.SplitCyclicSubgroup {K : Type u} [Field K] {N : ℕ} [NeZero N] (E : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))) extends MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.FiniteLocallyFreeSubgroup E : Type (u + 1)

A split cyclic subgroup-scheme of order N.

Only existence of a constant trivialization is retained. In particular this structure does not choose a generator, as appropriate for Γ₀(N) rather than Γ₁(N).

• carrier : AlgebraicGeometry.FiniteFlatCommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))
• inclusion : self.carrier.obj ⟶ E
• inclusion_isClosedImmersion : AlgebraicGeometry.IsClosedImmersion (CommGroupScheme.underlyingHom self.inclusion)
• isSplit : Nonempty (self.carrier ≅ cyclicConstant K N)

  The carrier is a split constant cyclic group scheme.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.SplitCyclicSubgroup.hasConstantOrder {K : Type u} [Field K] {N : ℕ} [NeZero N] {E : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))} (C : SplitCyclicSubgroup E) : C.carrier.HasConstantOrder N

A split cyclic subgroup has constant geometric order N.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.SplitCyclicSubgroup.baseChange {K : Type u} [Field K] {N : ℕ} [NeZero N] {E : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))} {L : Type u} [Field L] [Algebra K L] (C : SplitCyclicSubgroup E) : SplitCyclicSubgroup ((CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).mapCommGrp.obj E)

Scalar extension of a split cyclic subgroup remains split cyclic.

Equations

• C.baseChange = { toFiniteLocallyFreeSubgroup := C.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L))), isSplit := ⋯ }

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.constantPointHom (K : Type u) [Field K] (G : Type u) [CommGroup G] [Fintype G] : G →* CommGroupScheme.Point (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme K G).obj (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)

The distinguished rational points of a constant group scheme form a homomorphism from its indexing group.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.constantPointHom K G = { toFun := AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K G, map_one' := ⋯, map_mul' := ⋯ }

structure MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.ConstantClosedEmbedding (K : Type u) [Field K] (E : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))) (G : Type u) [CommGroup G] [Fintype G] (f : G →* CommGroupScheme.Point E (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)) : Type u

A scheme-theoretic extension of an injective finite family of rational group sections.

This is the exact construction supplied by a separated group-scheme model: the constant finite-flat group maps into the ambient group scheme, its map is a closed immersion, and it agrees with the given sections on rational points.

• hom : (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantScheme K G).obj ⟶ E

  The group-scheme morphism extending the rational sections.

• hom_isClosedImmersion : AlgebraicGeometry.IsClosedImmersion (CommGroupScheme.underlyingHom self.hom)

  Distinct constant sections form a closed finite subgroup.

• map_constantPoint (g : G) : (CommGroupScheme.mapPoint self.hom (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)) (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K G g) = f g

  The extension agrees with every distinguished constant point.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.constantClosedEmbeddingOfInjective (K : Type u) [Field K] (E : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))) (G : Type u) [CommGroup G] [Fintype G] (f : G →* CommGroupScheme.Point E (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)) (hinj : Function.Injective ⇑f) : ConstantClosedEmbedding K E G f

An injective finite group of rational sections gives a closed constant subgroup scheme. The group-scheme homomorphism and its closed-immersion proof are supplied by the checked componentwise extension theorem.

Equations

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

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.ConstantClosedEmbedding.toSplitCyclicSubgroup {K : Type u} [Field K] {E : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))} {N : ℕ} [NeZero N] {f : CyclicIndex N →* CommGroupScheme.Point E (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)} (D : ConstantClosedEmbedding K E (CyclicIndex N) f) : SplitCyclicSubgroup E

A constant closed embedding of ZMod N is a split cyclic subgroup.

Equations

• D.toSplitCyclicSubgroup = { carrier := MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.cyclicConstant K N, inclusion := D.hom, inclusion_isClosedImmersion := ⋯, isSplit := ⋯ }

structure MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface {K : Type u} [Field K] [DecidableEq K] (W : WeierstrassCurve K) : Type (u + 1)

The exact scheme-theoretic interface still missing from the pinned Weierstrass-coordinate API: a commutative group scheme whose rational points are the checked coordinate point group.

• groupScheme : AlgebraicGeometry.CommGroupScheme (AlgebraicGeometry.Spec (CommRingCat.of K))

  The projective commutative group scheme associated to W.

• rationalPointEquiv : Multiplicative W.toAffine.Point ≃* CommGroupScheme.Point self.groupScheme (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)

  Comparison between checked coordinate points and scheme-valued rational points.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.extendConstant {K : Type u} [Field K] [DecidableEq K] {W' : WeierstrassCurve K} (M : WeierstrassGroupSchemeInterface W') (G : Type u) [CommGroup G] [Fintype G] (f : G →* Multiplicative W'.toAffine.Point) (hinj : Function.Injective ⇑f) : ConstantClosedEmbedding K M.groupScheme G (M.rationalPointEquiv.toMonoidHom.comp f)

Extend an injective finite family of coordinate points to a closed constant subgroup of the associated group scheme.

Equations

• M.extendConstant G f hinj = MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.constantClosedEmbeddingOfInjective K M.groupScheme G (M.rationalPointEquiv.toMonoidHom.comp f) ⋯

def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.torsionAddHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} (W : WeierstrassCurve K) (P : W.toAffine.Point) (hP : addOrderOf P = N) : ZMod N →+ W.toAffine.Point

The additive homomorphism sending 1 : ZMod N to a point killed by N.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.torsionAddHom W P hP = MazurTorsion.IndependentCyclicGenerators.zmodHom N P ⋯

def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.torsionParameterization {K : Type u} [Field K] [DecidableEq K] {N : ℕ} (W : WeierstrassCurve K) (P : W.toAffine.Point) (hP : addOrderOf P = N) : CyclicIndex N →* Multiplicative W.toAffine.Point

The universe-lifted multiplicative parameterization used by the constant group-scheme construction.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.torsionParameterization_injective {K : Type u} [Field K] [DecidableEq K] {N : ℕ} (W : WeierstrassCurve K) (P : W.toAffine.Point) (hP : addOrderOf P = N) : Function.Injective ⇑(torsionParameterization W P hP)

Exact order makes the constant cyclic parameterization injective.

@[simp]

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.torsionParameterization_one {K : Type u} [Field K] [DecidableEq K] {N : ℕ} (W : WeierstrassCurve K) (P : W.toAffine.Point) (hP : addOrderOf P = N) : (torsionParameterization W P hP) ((cyclicIndexUp N) (Multiplicative.ofAdd 1)) = Multiplicative.ofAdd P

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.torsionParameterization_additive_range {K : Type u} [Field K] [DecidableEq K] {N : ℕ} (W : WeierstrassCurve K) (P : W.toAffine.Point) (hP : addOrderOf P = N) : (torsionAddHom W P hP).range = AddSubgroup.zmultiples P

The point-group image of the cyclic parameterization is exactly the subgroup generated by P.

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

A split finite-flat Γ₀(N) source datum relative to a supplied Weierstrass group-scheme interface. This is deliberately not named a full X₀(N) point.

• subgroup : SplitCyclicSubgroup M.groupScheme

  The finite-locally-free split cyclic subgroup.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumOfTorsion {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : SplitGammaZeroDatum W M

A marked rational point of exact order N constructs a genuine split finite-flat cyclic subgroup-scheme after the missing Weierstrass scheme interface is supplied.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumOfTorsion_hasConstantOrder {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : (splitGammaZeroDatumOfTorsion W M P hP).subgroup.carrier.HasConstantOrder N

The constructed subgroup-scheme has constant geometric order N.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumOfTorsion_map_constantPoint {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) (z : CyclicIndex N) : (CommGroupScheme.mapPoint (splitGammaZeroDatumOfTorsion W M P hP).subgroup.inclusion (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)) (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K (CyclicIndex N) z) = M.rationalPointEquiv ((torsionParameterization W P hP) z)

The constructed closed subgroup sends every constant point z to the corresponding multiple of P under the rational-point comparison.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumOfTorsion_map_one {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : (CommGroupScheme.mapPoint (splitGammaZeroDatumOfTorsion W M P hP).subgroup.inclusion (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)) (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K (CyclicIndex N) ((cyclicIndexUp N) (Multiplicative.ofAdd 1))) = M.rationalPointEquiv (Multiplicative.ofAdd P)

In particular, the distinguished constant generator maps to the marked rational torsion point.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumPointMonoidHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : CyclicIndex N →* Multiplicative W.toAffine.Point

Pull the constructed subgroup's rational constant points back through the model comparison.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumPointMonoidHom_eq {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : splitGammaZeroDatumPointMonoidHom W M P hP = torsionParameterization W P hP

The pulled-back scheme-point map is the original constant cyclic parameterization.

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumPointHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : ZMod N →+ W.toAffine.Point

Pulling back along the canonical universe lift gives an additive map on ZMod N.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumPointHom_eq {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : splitGammaZeroDatumPointHom W M P hP = torsionAddHom W P hP

The scheme-theoretically constructed additive rational-point map is the original homomorphism sending 1 to P.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumPointHom_range {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (P : W.toAffine.Point) (hP : addOrderOf P = N) : (splitGammaZeroDatumPointHom W M P hP).range = (XZeroModuli.RationalCyclicSubgroup.ofPoint P hP).carrier

The rational point image of the constructed finite-flat subgroup is exactly the carrier used by the existing split point-level Γ₀(N) datum.

Forgetting the choice of generator

@[instance_reducible]

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupFintype {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.rationalCyclicSubgroupFintype W C = Fintype.ofFinite ↥C.carrier

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

The canonical inclusion of the supplied subgroup subtype into the ambient rational point group, in multiplicative notation.

Equations

• MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupParameterization W C = AddMonoidHom.toMultiplicative C.carrier.subtype

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupParameterization_injective {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) : Function.Injective ⇑(rationalCyclicSubgroupParameterization W C)

The subgroup-subtype parameterization is injective.

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

A cyclic subgroup of order N, viewed multiplicatively, is isomorphic to the universe-compatible standard cyclic indexing group. This choice is used only to certify split cyclicity, not to define the subgroup inclusion.

Equations

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

noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalCyclicSubgroupEmbedding {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) : ConstantClosedEmbedding K M.groupScheme (Multiplicative ↥C.carrier) (M.rationalPointEquiv.toMonoidHom.comp (rationalCyclicSubgroupParameterization W C))

Extend the canonical inclusion of the supplied rational subgroup to a closed embedding of its constant finite-flat group scheme.

Equations

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

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

A split rational cyclic subgroup constructs a genuine split finite-flat Γ₀(N) datum. Its carrier is the constant scheme on the supplied subgroup subtype, so the actual closed embedding does not depend on a selected generator. A cyclic-generator choice enters only in the nonempty comparison with ZMod N that certifies split cyclicity.

Equations

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

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

The generator-free finite-flat subgroup has constant geometric order N.

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumOfRationalCyclicSubgroup_map_constantPoint {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (W : WeierstrassCurve K) (M : WeierstrassGroupSchemeInterface W) (C : XZeroModuli.RationalCyclicSubgroup W.toAffine.Point N) (z : Multiplicative ↥C.carrier) : (CommGroupScheme.mapPoint (splitGammaZeroDatumOfRationalCyclicSubgroup W M C).subgroup.inclusion (MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.baseTestObject✝ K)) (AlgebraicGeometry.FiniteFlatCommGroupScheme.constantGeometricPoint K (Multiplicative ↥C.carrier) z) = M.rationalPointEquiv ((rationalCyclicSubgroupParameterization W C) z)

The canonical subgroup inclusion agrees on every distinguished constant point with the corresponding element of the supplied rational subgroup.

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

Pull the actual constant subgroup sections back through the rational-point comparison.

Equations

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

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

The scheme-theoretic point map is the canonical subgroup-subtype inclusion.

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

The additive rational-point map induced by the actual finite-flat subgroup inclusion.

Equations

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

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

The additive scheme-point map is exactly the subtype inclusion.

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

Rational points of the constructed finite-flat subgroup recover exactly the supplied cyclic subgroup carrier, not merely a cyclic subgroup of the same cardinality.

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

A raw split rational Γ₀(N) datum, together with the checked Weierstrass group-scheme interface for its curve, constructs the corresponding split finite-flat subgroup datum. This is the generator-free source consumed by the future coarse X₀(N) classifying map.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.splitGammaZeroDatumOfRationalDatum_hasConstantOrder {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (splitGammaZeroDatumOfRationalDatum x M).subgroup.carrier.HasConstantOrder N

The finite-flat subgroup attached to a raw rational moduli datum has the required constant geometric order.

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

Pull the rational constant sections of the finite-flat subgroup attached to a raw moduli datum back to its coordinate point group.

Equations

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

theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumPointHom_range {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) : (rationalDatumPointHom x M).range = x.subgroup.carrier

The scheme-theoretic split subgroup constructed from a raw rational datum has exactly the datum's original rational-point carrier. This is the checked compatibility required before a coarse X₀(N) map may consume the new finite-flat interface.