def ModularFunctionField.FunctionField (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Type

The function field $\mathcal{F}(\Gamma)$ of a subgroup $\Gamma \leq \mathrm{SL}_2(\mathbb{Z})$: the type of meromorphic modular functions $f : \mathcal{H} \to \mathbb{C}$ invariant under $\Gamma$ and meromorphic at the cusps (Definition 19.2).

def ModularFunctionField.FunctionField.toFun {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : FunctionField Γ) : UpperHalfPlane → ℂ

The underlying function $\mathcal{H} \to \mathbb{C}$ of an element of FunctionField Γ.

def ModularFunctionField.FunctionField.isModular {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : FunctionField Γ) : IsModularFunction (↑f) Γ

The proof that an element of FunctionField Γ is in fact a modular function for $\Gamma$.

theorem ModularFunctionField.isModularFunction_of_top {f : UpperHalfPlane → ℂ} (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hf : IsModularFunction f ⊤) : IsModularFunction f Γ

A function modular for the full group $\mathrm{SL}_2(\mathbb{Z})$ is a fortiori modular for any subgroup $\Gamma$: meromorphicity is preserved and invariance under $\Gamma$ follows from invariance under the whole group.

def ModularFunctionField.inclusionFun (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : FunctionField ⊤ → FunctionField Γ

The inclusion of function fields induced by the inclusion $\Gamma \leq \mathrm{SL}_2(\mathbb{Z})$, sending a modular function for the full group to the same function viewed as a modular function for $\Gamma$.

theorem ModularFunctionField.instField_nonempty (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Nonempty (Field (FunctionField Γ))

The function field $\mathcal{F}(\Gamma)$ carries a (noncanonical) field structure (Theorem 19.8). The construction proceeds by exhibiting pointwise sum, product, and inverse operations on the underlying functions.

@[implicit_reducible]

noncomputable instance ModularFunctionField.instField (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Field (FunctionField Γ)

The chosen field structure on $\mathcal{F}(\Gamma)$ extracted from instField_nonempty via choice.

@[reducible, inline]

abbrev ModularFunctionField.RatFuncJ : Type

The field $\mathbb{C}(j)$ of rational functions in Klein's $j$-invariant, realized as the function field of the full modular group $\mathrm{SL}_2(\mathbb{Z})$ (Theorem 19.9).

noncomputable def ModularFunctionField.algebraMap_ratFuncJ (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : RatFuncJ →+* FunctionField Γ

The canonical ring homomorphism $\mathbb{C}(j) \hookrightarrow \mathcal{F}(\Gamma)$ making $\mathcal{F}(\Gamma)$ a $\mathbb{C}(j)$-algebra (Theorem 19.10).

@[implicit_reducible]

noncomputable instance ModularFunctionField.instAlgebra (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Algebra RatFuncJ (FunctionField Γ)

The $\mathbb{C}(j)$-algebra structure on $\mathcal{F}(\Gamma)$ obtained from the canonical ring homomorphism algebraMap_ratFuncJ.

theorem ModularFunctionField.modularFunctionField_finite_extension (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hΓ : CongruenceSubgroup.IsCongruenceSubgroup Γ) : FiniteDimensional RatFuncJ (FunctionField Γ) ∧ Module.finrank RatFuncJ (FunctionField Γ) ≤ Γ.index

For any congruence subgroup $\Gamma$, the extension $\mathcal{F}(\Gamma)/\mathbb{C}(j)$ is finite-dimensional of degree at most $[\mathrm{SL}_2(\mathbb{Z}) : \Gamma]$ (Theorem 19.11).