TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The standard fundamental domain, boundary identifications and elliptic stabilisers

Statement

Let $D = {τ \in H : ∣ ℜ τ ∣ < 1 / 2, ∣ τ ∣ > 1}$ and let $\overline{D}$ be its closure in $H$ . (a) $D$ is a fundamental domain for $P S L_{2} (Z)$ : every orbit meets $\overline{D}$ , no two points of $D$ are equivalent, and two distinct points $z, z^{'} \in \overline{D}$ are equivalent if and only if either $z^{'} = z \pm 1$ with $ℜ z = \mp 1 / 2$ , or $z^{'} = - 1 / z$ with $∣ z ∣ = 1$ . (b) The only points of $\overline{D}$ with nontrivial stabiliser are $i$ , $ω : = e^{2 π i / 3}$ and $ω + 1 = e^{i π / 3}$ : $Stab (i) = ⟨ S ⟩$ has order $2$ , $Stab (ω) = ⟨ S T ⟩$ has order $3$ , and $Stab (ω + 1) = ⟨ T S ⟩$ has order $3$ in $P S L_{2} (Z)$ . (c) $P S L_{2} (Z) = ⟨ S, T ⟩$ .

Facts & Assumptions

Given: $Γ : = P S L_{2} (Z)$ acting on $H$ , its subgroup $Γ^{'} : = ⟨ S, T ⟩$ , the set $D$ and its closure $\overline{D}$ ; $S \cdot z = - 1 / z$ , $T \cdot z = z + 1$ , and $S^{2} = (S T)^{3} = 1$ in $Γ$ (The modular group and its action on the upper half-plane, The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups, The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action, The stabilizer $G_{x}$ is a subgroup of $G$ , A free group action has no nonidentity element fixing a point).

[F1]

Every $Γ^{'}$ -orbit meets $\overline{D}$ (Reduction of orbits to the standard domain), and for $γ = (\begin{matrix} a & b \\ c & d \end{matrix}) \in S L_{2} (Z)$ one has $ℑ (γ \cdot z) = ℑ z / ∣ c z + d ∣^{2}$ , so $ℑ (γ \cdot z) \geq ℑ z$ is equivalent to $∣ c z + d ∣ \leq 1$ (The modular group and its action on the upper half-plane).

[F2]

Every $z \in \overline{D}$ satisfies $∣ ℜ z ∣ \leq 1 / 2$ and $∣ z ∣ \geq 1$ , hence $Im z \geq \sqrt{3} / 2$ (The modular group and its action on the upper half-plane, Reduction of orbits to the standard domain).

[F3]

Orbits partition the set and stabilisers are subgroups of the acting group; two points are equivalent exactly when they lie in the same orbit (The orbits of a group action are the equivalence classes of $x \sim y$ iff $y = g \cdot x$ for some $g$ , and hence partition the acted-on set, The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action, The stabilizer $G_{x}$ is a subgroup of $G$ ).

Proof

1.1F1F2givenalgebra

Every $Γ$ -orbit meets $\overline{D}$ , because $Γ^{'} \leq Γ$ and every $Γ^{'}$ -orbit does [F1]. Suppose $z, z^{'} \in \overline{D}$ satisfy $z^{'} = γ \cdot z$ with $γ = (\begin{matrix} a & b \\ c & d \end{matrix}) \in S L_{2} (Z)$ and $Im z^{'} \geq Im z$ ; replacing $γ$ by $- γ$ , which gives the same element of $Γ$ , we may assume $c \geq 0$ . Then $∣ c z + d ∣ \leq 1$ by [F1], while $Im z \geq \sqrt{3} / 2$ by [F2]; hence $∣ c ∣ \frac{\sqrt{3}}{2} \leq ∣ c ∣ Im z = ∣ Im (c z + d) ∣ \leq ∣ c z + d ∣ \leq 1$ , so $∣ c ∣ \leq 2 / \sqrt{3} < 2$ and therefore $c \in {0, 1}$ .

2.1F1F2step 1.1givencasesalgebra

Case $c = 0$ . Then $d = \pm 1$ and $γ = \pm (\begin{matrix} 1 & m \\ 0 & 1 \end{matrix})$ , so $z^{'} = z + m$ with $m \in Z$ . Since both points lie in $\overline{D}$ , $∣ m ∣ = ∣ ℜ z^{'} - ℜ z ∣ \leq 1$ . If $m = 0$ then $z^{'} = z$ . If $m = 1$ then $ℜ z^{'} = ℜ z + 1 \leq 1 / 2$ and $ℜ z \geq - 1 / 2$ force $ℜ z = - 1 / 2$ ; conversely for $z \in \overline{D}$ with $ℜ z = - 1 / 2$ the point $z^{'} = z + 1$ lies in $\overline{D}$ , since $1 / 2 \geq ℜ z^{'}$ and $∣ z^{'} ∣ = ∣ z - (- 1) ∣ = ∣ ∣ z ∣ ∣ = ∣ z ∣$ holds because $∣ z^{'} ∣^{2} = ∣ z ∣^{2} + 2 Re z + 1 = ∣ z ∣^{2}$ . The case $m = - 1$ is the mirror image with $ℜ z = 1 / 2$ .

2.2F1F2step 1.1givencasesalgebra

Case $c = 1$ . First suppose $d = 0$ . Then $b = a d - 1 = - 1$ and $∣ z ∣ = ∣ c z + d ∣ \leq 1 \leq ∣ z ∣$ shows $∣ z ∣ = 1$ ; the map is $z^{'} = a - 1 / z = a - \overset{ˉ}{z}$ with $a \in Z$ , and $∣ ℜ z^{'} ∣ \leq 1 / 2$ , $∣ ℜ z ∣ \leq 1 / 2$ give $∣ a ∣ \leq 1$ . For $a = 0$ this is $z^{'} = - 1 / z$ with $∣ z ∣ = 1$ ; for $a = - 1$ the condition $ℜ z^{'} = - 1 - ℜ z \geq - 1 / 2$ forces $ℜ z = - 1 / 2$ , so $z = ω$ and $z^{'} = - 1 - \overset{ˉ}{z} = z$ ; for $a = 1$ we get $ℜ z^{'} = 1 - ℜ z \geq 1 / 2$ , forcing $ℜ z^{'} = 1 / 2$ and $ℜ z = 1 / 2$ , after which $∣ z^{'} ∣^{2} = 1 - 2 ℜ z + ∣ z ∣^{2} = ∣ z ∣^{2} = 1$ and $z^{'} = 1 - \overset{ˉ}{z} = 1 - (\frac{1}{2} - i y) = \frac{1}{2} + i y = z$ . So for $d = 0$ the only new identification is $z^{'} = - 1 / z$ when $∣ z ∣ = 1$ . Now suppose $d \geq 1$ . Since $∣ c z + d ∣^{2} - ∣ z ∣^{2} = 2 d Re z + d^{2} \leq 1 - 1 = 0$ , we get $ℜ z \leq - d / 2 \leq - 1 / 2$ , so $d = 1$ and $ℜ z = - 1 / 2$ ; then $∣ z + 1 ∣^{2} = ∣ z ∣^{2}$ and $1 \leq ∣ z ∣$ , $∣ z + 1 ∣ \leq 1$ force $∣ z + 1 ∣ = 1 = ∣ z ∣$ , whence $z = ω$ . Here $b = a - 1$ and $z^{'} = a + ω$ (because $1 / (1 + ω) = - ω$ ), so $ℜ z^{'} = a - 1 / 2 \in [- 1 / 2, 1 / 2]$ gives $a \in {0, 1}$ : for $a = 0$ one has $z^{'} = z$ , and for $a = 1$ one has $z^{'} = ω + 1 = z + 1$ . If $d \leq - 1$ , write $d = - k$ , $k \geq 1$ ; then $∣ c z + d ∣^{2} - ∣ z ∣^{2} = - 2 k ℜ z + k^{2} \leq 0$ gives $ℜ z \geq k / 2 \geq 1 / 2$ , so $k = 1$ , $d = - 1$ , $ℜ z = 1 / 2$ , and $∣ z - 1 ∣ = ∣ z ∣ = 1$ forces $z = ω + 1$ ; with $b = - a - 1$ and $ω = ω + 1 - 1$ one computes $z^{'} = a + 1 + ω$ , so $ℜ z^{'} = a + 1 / 2 \in [- 1 / 2, 1 / 2]$ gives $a \in {- 1, 0}$ : for $a = 0$ one has $z^{'} = z$ , and for $a = - 1$ one has $z^{'} = ω = z - 1$ .

3.1F1F3step 2.1step 2.2givenalgebra

Combining 1.1, 2.1 and 2.2: for any two $Γ$ -equivalent points $z, z^{'} \in \overline{D}$ one of them, say the one with larger imaginary part, is of the listed shape; the case analysis gives either $z^{'} = z$ , or $z^{'} = z \pm 1$ with $ℜ z = \mp 1 / 2$ , or $z^{'} = - 1 / z$ with $∣ z ∣ = 1$ . Since the two identifications force $∣ z ∣ = 1$ or $∣ ℜ z ∣ = 1 / 2$ , neither can occur for two distinct points of $D$ , whose points have $∣ ℜ z ∣ < 1 / 2$ and $∣ z ∣ > 1$ ; this proves (a). For (b), a stabiliser element is a case with $z^{'} = z$ in the same analysis: besides the identity, this happens exactly for $z = i$ with $γ = \pm S$ , for $z = ω$ with $γ$ representing $S T$ or $(S T)^{2}$ , and for $z = ω + 1$ with $γ$ representing $T S$ or $(T S)^{2}$ . Since $S^{2} = (S T)^{3} = (T S)^{3} = 1$ in $Γ$ and $S \neq 1$ , $S T \neq 1$ , these give $Stab (i) = ⟨ S ⟩$ of order $2$ and $Stab (ω) = ⟨ S T ⟩$ , $Stab (ω + 1) = ⟨ T S ⟩$ of order $3$ , by [F3]; all other points of $\overline{D}$ have trivial stabiliser.

4.1F3step 3.1givenalgebra∎

For (c) let $γ \in Γ$ and fix $z_{0} : = 2 i \in D$ . By 1.1 there is $γ_{1} \in Γ^{'}$ with $γ_{1} \cdot (γ \cdot z_{0}) \in \overline{D}$ ; set $δ : = γ_{1} γ \in Γ$ . Then $z_{0} \in D \subseteq \overline{D}$ and $δ \cdot z_{0} \in \overline{D}$ are equivalent, so by (a) either $δ \cdot z_{0} = z_{0}$ or one of the two boundary identifications holds; the latter are impossible because $∣ z_{0} ∣ = 2 > 1$ and $∣ ℜ z_{0} ∣ = 0 < 1 / 2$ . Hence $δ$ stabilises $z_{0}$ , and by (b) the only points of $\overline{D}$ with nontrivial stabiliser are $i, ω, ω + 1$ , none of which equals $z_{0}$ ; so $δ = 1$ and $γ = γ_{1}^{- 1} \in Γ^{'}$ . Therefore $Γ = Γ^{'} = ⟨ S, T ⟩$ .

Depends on

Used by

Dependency tree · two levels

41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Modular Functions and Modular Forms (v1.31, 2017) (standard reference, not scraped)
D. Zagier, Elliptic Modular Forms and Their Applications, in The 1-2-3 of Modular Forms (Universitext, Springer, 2008) (standard reference, not scraped)
C. T. McMullen, Advanced Complex Analysis, Math 213a course notes (Harvard, 2010) (standard reference, not scraped)