Split rational cyclic subgroups and the open X₀(N) source datum #
This file isolates the part of the Γ₀(N) moduli bridge that is already
available at the project's exact Mathlib pin. A rational point of exact order
N generates a cyclic subgroup of the rational point group with exactly N
elements. Forgetting the chosen generator gives a split rational
Γ₀(N) source datum (E, C).
This is the source data needed to send rational torsion to a modular curve,
but it is not the full functor of X₀(N): a general rational X₀(N) point
has a Galois-stable finite cyclic subgroup scheme whose geometric points need
not all be rational. In particular, the type below is not closed under an
Atkin--Lehner involution. Constructing that involution requires the finite
flat subgroup-scheme moduli layer, not merely a subgroup of E(K).
Constructing the elliptic quotient E/C, and proving that the resulting datum
is classified by the coarse open modular curve, are scheme-theoretic geometry
that is not present at the core package's exact pin. The downstream theorem
XZeroFortyNine.rationalPoint_addOrderOf_ne_fortyNine_of_classifyingMap
therefore takes that genuine classifying map as its explicit remaining input
and lands in the already checked two-cusp model of X₀(49).
A finite cyclic subgroup of order N in an additive commutative group.
When the ambient group is E(K), every element of carrier is already
K-rational. The structure forgets a chosen generator, as required by a
Γ₀(N) rather than a Γ₁(N) datum.
- carrier : AddSubgroup A
The subgroup of rational points.
- isAddCyclic : IsAddCyclic ↥self.carrier
The subgroup is cyclic.
Its cardinality is the level
N.
Instances For
The subgroup generated by a point of exact order N, with its cardinality
proved from Nat.card_zmultiples.
Equations
- MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.ofPoint P hP = { carrier := AddSubgroup.zmultiples P, isAddCyclic := ⋯, card_eq := ⋯ }
Instances For
Transport a rational cyclic subgroup along an isomorphism of point groups.
Equations
- C.map e = { carrier := AddSubgroup.map e.toAddMonoidHom C.carrier, isAddCyclic := ⋯, card_eq := ⋯ }
Instances For
Generating a subgroup commutes with transport along a point-group isomorphism.
A cyclic subgroup presented without a chosen generator still has one.
Instances For
The chosen generator also has exact order N in the ambient rational
point group.
The selected generator generates the supplied subgroup, not merely some cyclic group of the same cardinality.
A cyclic subgroup of order different from one is nontrivial.
Canonical subgroups at divisor levels #
The canonical cyclic subgroup of order d inside a cyclic subgroup of
order N, for d ∣ N.
Its carrier is intrinsic: it consists of the elements of C killed by d.
The cardinality calculation uses the kernel of multiplication by d on the
finite cyclic group C. This is the functor-of-points input for the
restriction of the degeneracy map X₀(N) → X₀(d) to split source data.
Equations
- C.divisorSubgroup d hd = { carrier := C.carrier ⊓ (nsmulAddMonoidHom d).ker, isAddCyclic := ⋯, card_eq := ⋯ }
Instances For
Taking the canonical divisor-level subgroup commutes with transport along an isomorphism of ambient point groups.
Divisor-level subgroups compose as the corresponding degeneracy maps do.
For a cyclic subgroup presented by a point P of exact order N, the
intrinsic divisor-level subgroup is generated by (N / d) • P.
The intrinsic divisor-level subgroup is generated by the corresponding
multiple of any selected generator of C.
Coprime divisor-level subgroups whose orders multiply to the ambient cyclic order generate the whole subgroup. This is the group-theoretic core of the squarefree degeneracy map used at level 35.
A raw split rational Γ₀(N) source datum (E, C) over a field.
It is a restricted input to the open modular curve, not its full functor of
points: every element of C is required to lie in E(K). The raw structure
is not itself an isomorphism class; below, VariableChangeClass quotients out
the admissible Weierstrass changes already available in checked code.
Constructing the coarse moduli point and general Galois-stable subgroup
schemes remains the next geometric layer.
- curve : WeierstrassCurve K
The Weierstrass model.
- isElliptic : self.curve.IsElliptic
Smoothness of the model.
- subgroup : RationalCyclicSubgroup self.curve.toAffine.Point N
The rational cyclic subgroup of order
N.
Instances For
Package an elliptic curve and a split rational cyclic subgroup as a raw
Γ₀(N) source datum.
Equations
- MazurTorsion.ModularCurve.XZeroModuli.RationalDatum.datumOfRationalCyclicSubgroup E C = { curve := E, isElliptic := ⋯, subgroup := C }
Instances For
A rational point of exact order N supplies the open Γ₀(N) datum
by forgetting its choice of generator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conversely, a raw split rational Γ₀(N) source datum contains a rational point
of exact order N, because its subgroup is finite cyclic of order N.
Instances For
Forget part of a cyclic level structure along a divisor d ∣ N.
This is the divisor-level degeneracy map from split Γ₀(N) source data to
split Γ₀(d) source data.
Equations
Instances For
Successive forgetting along e ∣ d ∣ N agrees with forgetting directly
to level e.
Independence of the Weierstrass presentation #
Transport a raw Γ₀(N) datum along an admissible change of Weierstrass
variables. The inverse point-group equivalence transports the subgroup from
the old model to the changed model.
Equations
Instances For
The raw divisor-level degeneracy map is natural under admissible changes of Weierstrass presentation.
One-step equivalence of raw data under an admissible Weierstrass variable change. Its equivalence closure is used below, avoiding any claim that a general coarse modular quotient has already been constructed.
Equations
- x.VariableChangeRelated y = ∃ (C : WeierstrassCurve.VariableChange K), x.variableChange C = y
Instances For
The equivalence relation generated by admissible changes of a Weierstrass presentation and the induced transport of its cyclic subgroup.
Equations
Instances For
Raw split rational Γ₀(N) source data modulo the checked admissible changes of
Weierstrass presentation. This is deliberately named a variable-change
class, not a coarse-moduli point: representability and the map to X₀(N)
remain geometric work.
Equations
Instances For
Forget the chosen Weierstrass presentation of a raw rational datum.
Equations
Instances For
The variable-change class is independent of one admissible change of presentation.
Descend a function on raw rational data which is invariant under every
admissible change of Weierstrass presentation. This is the checked API through
which a future coarse X₀(N) classifying map can be built.
Equations
Instances For
The presentation-independent divisor-level degeneracy map on checked variable-change classes.
Equations
- One or more equations did not get rendered due to their size.