theorem CMFieldOfDefinition.Gamma_le_Gamma1 (N : ℕ) : CongruenceSubgroup.Gamma N ≤ CongruenceSubgroup.Gamma1 N

The principal congruence subgroup $\Gamma(N)$ is contained in $\Gamma_1(N)$: a matrix congruent to the identity mod $N$ has diagonal entries $\equiv 1$ and upper-right entry $\equiv 0$ mod $N$, which are precisely the defining conditions for $\Gamma_1(N)$.

def CMFieldOfDefinition.ModularCurveOpen (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Type

The open modular curve $Y(\Gamma) = \Gamma \backslash \mathcal{H}$ as the quotient of the upper half-plane by the action of a subgroup $\Gamma \leq \mathrm{SL}_2(\mathbb{Z})$ via Mobius transformations. This is the noncompactified moduli space of elliptic curves with $\Gamma$-level structure.

opaque CMFieldOfDefinition.ExtendedUpperHalfPlane : Type

The extended upper half-plane $\mathcal{H}^* = \mathcal{H} \cup \mathbb{P}^1(\mathbb{Q})$, the upper half-plane together with the cusps. Adjoining the cusps yields the compactification used to form projective modular curves.

noncomputable def CMFieldOfDefinition.ExtendedUpperHalfPlane.mulAction_ax : MulAction (Matrix.SpecialLinearGroup (Fin 2) ℤ) ExtendedUpperHalfPlane

Existence of an action of $\mathrm{SL}_2(\mathbb{Z})$ on the extended upper half-plane $\mathcal{H}^*$ extending the Mobius action on $\mathcal{H}$ to the cusps.

@[implicit_reducible]

noncomputable instance CMFieldOfDefinition.ExtendedUpperHalfPlane.mulAction : MulAction (Matrix.SpecialLinearGroup (Fin 2) ℤ) ExtendedUpperHalfPlane

The instance registering the $\mathrm{SL}_2(\mathbb{Z})$-action on the extended upper half-plane, supplied by mulAction_ax.

def CMFieldOfDefinition.ModularCurve (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Type

The (compact) modular curve $X(\Gamma) = \Gamma \backslash \mathcal{H}^*$, the quotient of the extended upper half-plane by $\Gamma$, including cusps.

@[reducible, inline]

abbrev CMFieldOfDefinition.Y (N : ℕ) : Type

The open modular curve $Y(N) = \Gamma(N) \backslash \mathcal{H}$, parametrizing elliptic curves with full level-$N$ structure.

@[reducible, inline]

abbrev CMFieldOfDefinition.Y₁ (N : ℕ) : Type

The open modular curve $Y_1(N) = \Gamma_1(N) \backslash \mathcal{H}$, parametrizing elliptic curves equipped with a point of exact order $N$.

@[reducible, inline]

abbrev CMFieldOfDefinition.Y₀ (N : ℕ) : Type

The open modular curve $Y_0(N) = \Gamma_0(N) \backslash \mathcal{H}$, parametrizing elliptic curves equipped with a cyclic subgroup of order $N$.

@[reducible, inline]

abbrev CMFieldOfDefinition.X (N : ℕ) : Type

The (compactified) modular curve $X(N) = \Gamma(N) \backslash \mathcal{H}^*$, the compactification of $Y(N)$ obtained by adjoining the cusps.

@[reducible, inline]

abbrev CMFieldOfDefinition.X₁ (N : ℕ) : Type

The (compactified) modular curve $X_1(N) = \Gamma_1(N) \backslash \mathcal{H}^*$, the compactification of $Y_1(N)$.

@[reducible, inline]

abbrev CMFieldOfDefinition.X₀ (N : ℕ) : Type

The (compactified) modular curve $X_0(N) = \Gamma_0(N) \backslash \mathcal{H}^*$, the compactification of $Y_0(N)$.