Theory Modular_Fundamental_Region
section ‹Fundamental regions of the modular group›
theory Modular_Fundamental_Region
imports Modular_Subgroups "Elliptic_Functions.Complex_Lattices" "HOL-Library.Real_Mod"
begin
unbundle modgrp_notation
subsection ‹Definition›
text ‹
A fundamental region of a subgroup of the modular group is an open subset of the upper half of
the complex plane that contains at most one representative of every equivalence class
and whose closure contains at least one representative of every equivalence class.
›
locale fundamental_region = modgrp_subgroup +
fixes R :: "complex set"
assumes "open": "open R"
assumes subset: "R ⊆ {z. Im z > 0}"
assumes unique: "⋀x y. x ∈ R ⟹ y ∈ R ⟹ rel x y ⟹ x = y"
assumes equiv_in_closure: "⋀x. Im x > 0 ⟹ ∃y∈closure R. rel x y "
begin
text ‹The uniqueness property can be extended to the closure of ‹R›:›
lemma unique':
assumes "x ∈ R" "y ∈ closure R" "rel x y" "Im y > 0"
shows "x = y"
proof (cases "y ∈ R")
case False
show ?thesis
proof (rule ccontr)
assume xy: "x ≠ y"
from assms have "rel y x"
by (simp add: rel_commutes)
then obtain f where f: "x = apply_modgrp f y" "f ∈ G"
unfolding rel_def by blast
have "continuous_on {z. Im z > 0} (apply_modgrp f)"
by (intro continuous_intros) auto
hence "isCont (apply_modgrp f) y"
using open_halfspace_Im_gt[of 0] assms continuous_on_eq_continuous_at by blast
hence lim: "apply_modgrp f ─y→ x"
using f by (simp add: isCont_def)
define ε where "ε = dist x y / 2"
have ε: "ε > 0"
using xy by (auto simp: ε_def)
have "eventually (λw. w ∈ ball x ε ∩ R) (nhds x)"
by (intro eventually_nhds_in_open) (use assms ε "open" in auto)
from this and lim have "eventually (λz. apply_modgrp f z ∈ ball x ε ∩ R) (at y)"
by (rule eventually_compose_filterlim)
moreover have "eventually (λz. z ∈ ball y ε) (nhds y)"
using assms ε by (intro eventually_nhds_in_open) auto
hence "eventually (λz. z ∈ ball y ε) (at y)"
unfolding eventually_at_filter by eventually_elim auto
ultimately have "eventually (λz. z ∈ ball y ε ∧ apply_modgrp f z ∈ R ∩ ball x ε) (at y)"
by eventually_elim auto
moreover have "y islimpt R"
using ‹y ∈ closure R› ‹y ∉ R› by (auto simp: closure_def)
hence "frequently (λz. z ∈ R) (at y)"
using islimpt_conv_frequently_at by blast
ultimately have "frequently (λz.
(z ∈ ball y ε ∧ apply_modgrp f z ∈ R ∩ ball x ε) ∧ z ∈ R) (at y)"
by (intro frequently_eventually_conj)
hence "frequently (λz. False) (at y)"
proof (rule frequently_elim1)
fix z assume z: "(z ∈ ball y ε ∧ apply_modgrp f z ∈ R ∩ ball x ε) ∧ z ∈ R"
have "ball y ε ∩ ball x ε = {}"
by (intro disjoint_ballI) (auto simp: ε_def dist_commute)
with z have "apply_modgrp f z ≠ z"
by auto
with z f subset show False
using unique[of z "apply_modgrp f z"] by auto
qed
thus False
by simp
qed
qed (use assms unique in auto)
lemma
pole_modgrp_not_in_region [simp]: "pole_modgrp f ∉ R" and
pole_image_modgrp_not_in_region [simp]: "pole_image_modgrp f ∉ R"
using subset by force+
end
subsection ‹The standard fundamental region›
text ‹
The standard fundamental region ‹ℛ⇩Γ› consists of all the points ‹z› in the upper half plane
with ‹|z| > 1› and $|\text{Re}(z)| < \frac{1}{2}$.
›
definition std_fund_region :: "complex set" ("ℛ⇩Γ") where
"ℛ⇩Γ = -cball 0 1 ∩ Re -` {-1/2<..<1/2} ∩ {z. Im z > 0}"
text ‹
The following version of ‹ℛ⇩Γ› is what Apostol refers to as the closure of ‹ℛ⇩Γ›, but it is
actually only part of the closure: since each point at the border of the fundamental region
is equivalent to its mirror image w.r.t.\ the ‹Im(z) = 0› axis, we only want one of these copies
to be in ‹ℛ⇩Γ'›, and we choose the left one.
So ‹ℛ⇩Γ'› is actually ‹ℛ⇩Γ› plus all the points on the left border plus all points on the
left half of the semicircle.
›
definition std_fund_region' :: "complex set" ("ℛ⇩Γ''") where
"ℛ⇩Γ' = ℛ⇩Γ ∪ (-ball 0 1 ∩ Re -` {-1/2..0} ∩ {z. Im z > 0})"
lemma std_fund_region_altdef:
"ℛ⇩Γ = {z. norm z > 1 ∧ norm (z + cnj z) < 1 ∧ Im z > 0}"
by (auto simp: std_fund_region_def complex_add_cnj)
lemma in_std_fund_region_iff:
"z ∈ ℛ⇩Γ ⟷ norm z > 1 ∧ Re z ∈ {-1/2<..<1/2} ∧ Im z > 0"
by (auto simp: std_fund_region_def field_simps)
lemma in_std_fund_region'_iff:
"z ∈ ℛ⇩Γ' ⟷ Im z > 0 ∧ ((norm z > 1 ∧ Re z ∈ {-1/2..<1/2}) ∨ (norm z = 1 ∧ Re z ∈ {-1/2..0}))"
by (auto simp: std_fund_region'_def std_fund_region_def field_simps)
lemma open_std_fund_region [simp, intro]: "open ℛ⇩Γ"
unfolding std_fund_region_def
by (intro open_Int open_vimage continuous_intros open_halfspace_Im_gt) auto
lemma Im_std_fund_region: "z ∈ ℛ⇩Γ ⟹ Im z > 0"
by (auto simp: std_fund_region_def)
text ‹
We now show that the closure of the standard fundamental region contains exactly those points ‹z›
with ‹|z| ≥ 1› and $|\text{Re}(z)| \leq \frac{1}{2}$.
›
context
fixes S S' :: "(real × real) set" and T :: "complex set"
fixes f :: "real × real ⇒ complex" and g :: "complex ⇒ real × real"
defines "f ≡ (λ(x,y). Complex x (y + sqrt (1 - x ^ 2)))"
defines "g ≡ (λz. (Re z, Im z - sqrt (1 - Re z ^ 2)))"
defines "S ≡ ({-1/2<..<1/2} × {0<..})"
defines "S' ≡ ({-1/2..1/2} × {0..})"
defines "T ≡ {z. norm z ≥ 1 ∧ Re z ∈ {-1/2..1/2} ∧ Im z ≥ 0}"
begin
lemma image_subset_std_fund_region: "f ` S ⊆ ℛ⇩Γ"
unfolding subset_iff in_std_fund_region_iff S_def
proof safe
fix a b :: real
assume ab: "a ∈ {-1/2<..<1/2}" "b > 0"
have "¦a¦ ^ 2 ≤ (1 / 2) ^ 2"
using ab by (intro power_mono) auto
hence "a ^ 2 ≤ 1 / 4"
by (simp add: power2_eq_square)
hence "a ^ 2 ≤ 1"
by simp
show "Im (f (a, b)) > 0"
using ab ‹a ^ 2 ≤ 1 / 4› by (auto simp: f_def intro: add_pos_nonneg)
show "Re (f (a, b)) ∈ {-1/2<..<1/2}"
using ab by (simp add: f_def)
have "1 ^ 2 = a⇧2 + (0 + sqrt (1 - a⇧2)) ^ 2"
using ‹a ^ 2 ≤ 1 / 4› by (simp add: power2_eq_square algebra_simps)
also have "a⇧2 + (0 + sqrt (1 - a⇧2)) ^ 2 < a⇧2 + (b + sqrt (1 - a⇧2)) ^ 2"
using ab ‹a ^ 2 ≤ 1› by (intro add_strict_left_mono power2_mono power2_strict_mono) auto
also have "… = norm (f (a, b)) ^ 2"
by (simp add: f_def norm_complex_def)
finally show "norm (f (a, b)) > 1"
by (rule power2_less_imp_less) auto
qed
lemma image_std_fund_region_subset: "g ` ℛ⇩Γ ⊆ S"
unfolding subset_iff g_def S_def
proof safe
fix z :: complex
assume "z ∈ ℛ⇩Γ"
hence z: "norm z > 1" "Re z ∈ {-1/2<..<1/2}" "Im z > 0"
by (auto simp: in_std_fund_region_iff)
have "¦Re z¦ ^ 2 ≤ (1 / 2) ^ 2"
using z by (intro power_mono) auto
hence "Re z ^ 2 ≤ 1 / 4"
by (simp add: power2_eq_square)
hence "Re z ^ 2 ≤ 1"
by simp
from z show "Re z ∈ {- 1 / 2<..<1 / 2}"
by auto
have "sqrt (1 - Re z ^ 2) ^ 2 = 1 - Re z ^ 2"
using ‹Re z ^ 2 ≤ 1› by simp
also have "… < Im z ^ 2"
using z by (simp add: norm_complex_def algebra_simps)
finally have "sqrt (1 - Re z ^ 2) < Im z"
by (rule power2_less_imp_less) (use z in auto)
thus "Im z - sqrt (1 - Re z ^ 2) > 0"
by simp
qed
lemma std_fund_region_map_inverses: "f (g x) = x" "g (f y) = y"
by (simp_all add: f_def g_def case_prod_unfold)
lemma bij_betw_std_fund_region1: "bij_betw f S ℛ⇩Γ"
using image_std_fund_region_subset image_subset_std_fund_region
by (intro bij_betwI[of _ _ _ g]) (auto simp: std_fund_region_map_inverses)
lemma bij_betw_std_fund_region2: "bij_betw g ℛ⇩Γ S"
using image_std_fund_region_subset image_subset_std_fund_region
by (intro bij_betwI[of _ _ _ f]) (auto simp: std_fund_region_map_inverses)
lemma image_subset_std_fund_region': "f ` S' ⊆ T"
unfolding subset_iff S'_def T_def
proof safe
fix a b :: real
assume ab: "a ∈ {-1/2..1/2}" "b ≥ 0"
have "¦a¦ ^ 2 ≤ (1 / 2) ^ 2"
using ab by (intro power_mono) auto
hence "a ^ 2 ≤ 1 / 4"
by (simp add: power2_eq_square)
hence "a ^ 2 ≤ 1"
by simp
show "Im (f (a, b)) ≥ 0"
using ab ‹a ^ 2 ≤ 1 / 4› by (auto simp: f_def intro: add_pos_nonneg)
show "Re (f (a, b)) ∈ {-1/2..1/2}"
using ab by (simp add: f_def)
have "1 ^ 2 = a⇧2 + (0 + sqrt (1 - a⇧2)) ^ 2"
using ‹a ^ 2 ≤ 1 / 4› by (simp add: power2_eq_square algebra_simps)
also have "a⇧2 + (0 + sqrt (1 - a⇧2)) ^ 2 ≤ a⇧2 + (b + sqrt (1 - a⇧2)) ^ 2"
using ab ‹a ^ 2 ≤ 1› by (intro add_left_mono power2_mono power2_strict_mono) auto
also have "… = norm (f (a, b)) ^ 2"
by (simp add: f_def norm_complex_def)
finally show "norm (f (a, b)) ≥ 1"
by (rule power2_le_imp_le) auto
qed
lemma image_std_fund_region_subset': "g ` T ⊆ S'"
unfolding subset_iff g_def S'_def
proof safe
fix z :: complex
assume "z ∈ T"
hence z: "norm z ≥ 1" "Re z ∈ {-1/2..1/2}" "Im z ≥ 0"
by (auto simp: T_def)
have "¦Re z¦ ^ 2 ≤ (1 / 2) ^ 2"
using z by (intro power_mono) auto
hence "Re z ^ 2 ≤ 1 / 4"
by (simp add: power2_eq_square)
hence "Re z ^ 2 ≤ 1"
by simp
from z show "Re z ∈ {-1/2..1/2}"
by auto
have "sqrt (1 - Re z ^ 2) ^ 2 = 1 - Re z ^ 2"
using ‹Re z ^ 2 ≤ 1› by simp
also have "… ≤ Im z ^ 2"
using z by (simp add: norm_complex_def algebra_simps)
finally have "sqrt (1 - Re z ^ 2) ≤ Im z"
by (rule power2_le_imp_le) (use z in auto)
thus "Im z - sqrt (1 - Re z ^ 2) ≥ 0"
by simp
qed
lemma bij_betw_std_fund_region1': "bij_betw f S' T"
using image_std_fund_region_subset' image_subset_std_fund_region'
by (intro bij_betwI[of _ _ _ g]) (auto simp: std_fund_region_map_inverses)
lemma bij_betw_std_fund_region2': "bij_betw g T S'"
using image_std_fund_region_subset' image_subset_std_fund_region'
by (intro bij_betwI[of _ _ _ f]) (auto simp: std_fund_region_map_inverses)
lemma closure_std_fund_region: "closure ℛ⇩Γ = T"
proof -
have homeo: "homeomorphism S ℛ⇩Γ f g"
using image_std_fund_region_subset image_subset_std_fund_region
by (intro homeomorphismI)
(auto simp: g_def f_def case_prod_unfold intro!: continuous_intros)
have "closure ℛ⇩Γ = closure (f ` S)"
using bij_betw_std_fund_region1 by (simp add: bij_betw_def)
also have "… = f ` closure S"
using bij_betw_std_fund_region1 homeo
proof (rule closure_bij_homeomorphic_image_eq)
show "continuous_on UNIV f" "continuous_on UNIV g"
by (auto simp: f_def g_def case_prod_unfold intro!: continuous_intros)
qed (auto simp: std_fund_region_map_inverses)
also have "closure S = {-1 / 2..1 / 2} × {0..}"
by (simp add: S_def closure_Times)
also have "… = S'"
by (simp add: S'_def)
also have "f ` S' = T"
using bij_betw_std_fund_region1' by (simp add: bij_betw_def)
finally show ?thesis .
qed
lemma in_closure_std_fund_region_iff:
"x ∈ closure ℛ⇩Γ ⟷ norm x ≥ 1 ∧ Re x ∈ {-1/2..1/2} ∧ Im x ≥ 0"
by (simp add: closure_std_fund_region T_def)
lemma frontier_std_fund_region:
"frontier ℛ⇩Γ =
{z. norm z ≥ 1 ∧ Im z > 0 ∧ ¦Re z¦ = 1 / 2} ∪
{z. norm z = 1 ∧ Im z > 0 ∧ ¦Re z¦ ≤ 1 / 2}" (is "_ = ?rhs")
proof -
have [simp]: "x ^ 2 ≥ 1 ⟷ x ≥ 1 ∨ x ≤ -1" for x :: real
using abs_le_square_iff[of 1 x] by auto
have "frontier ℛ⇩Γ = closure ℛ⇩Γ - ℛ⇩Γ"
unfolding frontier_def by (subst interior_open) simp_all
also have "… = ?rhs"
unfolding closure_std_fund_region unfolding std_fund_region_def
by (auto simp: cmod_def T_def)
finally show ?thesis .
qed
lemma std_fund_region'_subset_closure: "ℛ⇩Γ' ⊆ closure ℛ⇩Γ"
by (auto simp: in_std_fund_region'_iff in_closure_std_fund_region_iff)
lemma std_fund_region'_superset: "ℛ⇩Γ ⊆ ℛ⇩Γ'"
by (auto simp: in_std_fund_region'_iff in_std_fund_region_iff)
lemma in_std_fund_region'_not_on_frontier_iff:
assumes "z ∉ frontier ℛ⇩Γ"
shows "z ∈ ℛ⇩Γ' ⟷ z ∈ ℛ⇩Γ"
proof
assume "z ∈ ℛ⇩Γ'"
hence "z ∈ closure ℛ⇩Γ"
using std_fund_region'_subset_closure by blast
thus "z ∈ ℛ⇩Γ"
using assms by (auto simp: frontier_def interior_open)
qed (use std_fund_region'_superset in auto)
lemma simply_connected_std_fund_region: "simply_connected ℛ⇩Γ"
proof (rule simply_connected_retraction_gen)
show "simply_connected S"
unfolding S_def by (intro convex_imp_simply_connected convex_Times) auto
show "continuous_on S f"
unfolding f_def S_def case_prod_unfold by (intro continuous_intros)
show "continuous_on ℛ⇩Γ g"
unfolding g_def case_prod_unfold by (intro continuous_intros)
show "f ` S = ℛ⇩Γ"
using bij_betw_std_fund_region1 by (simp add: bij_betw_def)
show "g ∈ ℛ⇩Γ → S"
using bij_betw_std_fund_region2 bij_betw_imp_funcset by blast
show "f (g x) = x" for x
by (simp add: f_def g_def)
qed
lemma simply_connected_closure_std_fund_region: "simply_connected (closure ℛ⇩Γ)"
proof (rule simply_connected_retraction_gen)
show "simply_connected S'"
unfolding S'_def by (intro convex_imp_simply_connected convex_Times) auto
show "continuous_on S' f"
unfolding f_def S'_def case_prod_unfold by (intro continuous_intros)
show "continuous_on (closure ℛ⇩Γ) g"
unfolding g_def case_prod_unfold by (intro continuous_intros)
show "f ` S' = closure ℛ⇩Γ"
using bij_betw_std_fund_region1' by (simp add: bij_betw_def closure_std_fund_region)
show "g ∈ closure ℛ⇩Γ → S'"
using bij_betw_std_fund_region2' bij_betw_imp_funcset closure_std_fund_region by blast
show "f (g x) = x" for x
by (simp add: f_def g_def)
qed
lemma std_fund_region'_subset: "ℛ⇩Γ' ⊆ closure ℛ⇩Γ"
unfolding std_fund_region'_def closure_std_fund_region T_def unfolding std_fund_region_def
by auto
lemma closure_std_fund_region_Im_pos: "closure ℛ⇩Γ ⊆ {z. Im z > 0}"
unfolding closure_std_fund_region
by (auto intro!: neq_le_trans simp: norm_complex_def field_simps power2_ge_1_iff T_def)
lemma closure_std_fund_region_Im_ge: "closure ℛ⇩Γ ⊆ {z. Im z ≥ sqrt 3 / 2}"
proof
fix z assume "z ∈ closure ℛ⇩Γ"
hence *: "norm z ≥ 1" "¦Re z¦ ≤ 1 / 2" "Im z ≥ 0"
by (auto simp: closure_std_fund_region T_def)
have "1 ≤ norm z ^ 2"
using * by simp
also have "norm z ^ 2 ≤ (1 / 2) ^ 2 + Im z ^ 2"
unfolding cmod_power2 by (intro add_right_mono power2_mono) (use * in auto)
finally have "Im z ^ 2 ≥ (sqrt 3 / 2) ^ 2"
by (simp add: power2_eq_square)
hence "Im z ≥ sqrt 3 / 2"
by (subst (asm) abs_le_square_iff [symmetric]) (use * in auto)
thus "z ∈ {z. Im z ≥ sqrt 3 / 2}"
by simp
qed
lemma std_fund_region'_minus_std_fund_region:
"ℛ⇩Γ' - ℛ⇩Γ =
{z. norm z = 1 ∧ Im z > 0 ∧ Re z ∈ {-1/2..0}} ∪ {z. Re z = -1 / 2 ∧ Im z ≥ sqrt 3 / 2}"
(is "?lhs = ?rhs")
proof (intro equalityI subsetI)
fix z assume z: "z ∈ ?lhs"
from z have "Im z ≥ sqrt 3 / 2"
using closure_std_fund_region_Im_ge std_fund_region'_subset by auto
thus "z ∈ ?rhs" using z
by (auto simp: std_fund_region'_def std_fund_region_def not_less)
next
fix z assume z: "z ∈ ?rhs"
have "sqrt 3 / 2 > 0"
by simp
have "Im z > 0"
using z less_le_trans[OF ‹sqrt 3 / 2 > 0›, of "Im z"] by auto
moreover have "norm z ≥ 1"
using z
proof
assume "z ∈ {z. Re z = - 1 / 2 ∧ sqrt 3 / 2 ≤ Im z}"
hence "norm z ^ 2 ≥ (-1/2) ^ 2 + (sqrt 3 / 2) ^ 2"
unfolding cmod_power2 by (intro add_mono power2_mono) auto
also have "(-1/2) ^ 2 + (sqrt 3 / 2) ^ 2 = 1"
by (simp add: field_simps power2_eq_square)
finally show "norm z ≥ 1"
by (simp add: power2_nonneg_ge_1_iff)
qed auto
ultimately show "z ∈ ?lhs" using z
by (auto simp: std_fund_region'_def std_fund_region_def)
qed
lemma closure_std_fund_region_minus_std_fund_region':
"closure ℛ⇩Γ - ℛ⇩Γ' =
{z. norm z = 1 ∧ Im z > 0 ∧ Re z ∈ {0<..1/2}} ∪ {z. Re z = 1 / 2 ∧ Im z ≥ sqrt 3 / 2}"
(is "?lhs = ?rhs")
proof (intro equalityI subsetI)
fix z assume z: "z ∈ closure ℛ⇩Γ - ℛ⇩Γ'"
have "norm z ≥ 1"
using z by (auto simp: closure_std_fund_region in_std_fund_region'_iff not_le T_def)
from z have "Im z > 0" "Im z ≥ sqrt 3 / 2"
using closure_std_fund_region_Im_pos closure_std_fund_region_Im_ge by blast+
thus "z ∈ ?rhs" using z
by (auto simp: closure_std_fund_region in_std_fund_region'_iff not_le T_def)
next
fix z assume "z ∈ ?rhs"
thus "z ∈ ?lhs"
proof
assume "z ∈ {z. cmod z = 1 ∧ 0 < Im z ∧ Re z ∈ {0<..1 / 2}}"
thus "z ∈ ?lhs"
by (auto simp: closure_std_fund_region in_std_fund_region'_iff not_le T_def)
next
assume z: "z ∈ {z. Re z = 1 / 2 ∧ sqrt 3 / 2 ≤ Im z}"
have "0 < sqrt 3 / 2"
by simp
also have "… ≤ Im z"
using z by auto
finally have "Im z > 0" .
have "norm z ^ 2 ≥ (1 / 2) ^ 2 + (sqrt 3 / 2) ^ 2"
unfolding cmod_power2 by (intro add_mono power2_mono) (use z in auto)
also have "(1 / 2) ^ 2 + (sqrt 3 / 2) ^ 2 = 1"
by (simp add: power2_eq_square)
finally have "norm z ≥ 1"
by (simp add: power2_nonneg_ge_1_iff)
from this and ‹Im z > 0› and z show "z ∈ ?lhs"
by (auto simp: closure_std_fund_region in_std_fund_region'_iff not_le T_def)
qed
qed
lemma cis_in_std_fund_region'_iff:
assumes "φ ∈ {0..pi}"
shows "cis φ ∈ ℛ⇩Γ' ⟷ φ ∈ {pi/2..2*pi/3}"
proof
assume φ: "φ ∈ {pi/2..2*pi/3}"
have "φ > 0"
by (rule less_le_trans[of _ "pi / 2"]) (use φ in auto)
moreover have "φ < pi"
by (rule le_less_trans[of _ "2 * pi / 3"]) (use φ in auto)
ultimately have "sin φ > 0"
by (intro sin_gt_zero) auto
moreover have "cos φ ≥ cos (2 * pi / 3)"
using φ by (intro cos_monotone_0_pi_le) auto
moreover have "cos φ ≤ cos (pi / 2)"
using φ by (intro cos_monotone_0_pi_le) auto
ultimately show "cis φ ∈ ℛ⇩Γ'"
by (auto simp: in_std_fund_region'_iff cos_120)
next
assume "cis φ ∈ ℛ⇩Γ'"
hence *: "cos φ ≥ cos (2 * pi / 3)" "cos φ ≤ cos (pi / 2)"
by (auto simp: in_std_fund_region'_iff cos_120)
have "φ ≤ 2 * pi / 3"
using *(1) assms by (subst (asm) cos_mono_le_eq) auto
moreover have "φ ≥ pi / 2"
using *(2) assms by (subst (asm) cos_mono_le_eq) auto
ultimately show "φ ∈ {pi/2..2*pi/3}"
by auto
qed
lemma imag_axis_in_std_fund_region'_iff: "y *⇩R 𝗂 ∈ ℛ⇩Γ' ⟷ y ≥ 1"
by (auto simp: in_std_fund_region'_iff)
lemma vertical_left_in_std_fund_region'_iff:
"-1 / 2 + y *⇩R 𝗂 ∈ ℛ⇩Γ' ⟷ y ≥ sqrt 3 / 2"
proof
assume y: "y ≥ sqrt 3 / 2"
have "1 = (1 / 2) ^ 2 + (sqrt 3 / 2) ^ 2"
by (simp add: power2_eq_square)
also have "… ≤ (1 / 2) ^ 2 + y ^ 2"
using y by (intro add_mono power2_mono) auto
also have "… = norm (y *⇩R 𝗂 - 1 / 2) ^ 2"
unfolding cmod_power2 by simp
finally have "norm (y *⇩R 𝗂 - 1 / 2) ≥ 1"
by (simp add: power2_nonneg_ge_1_iff)
moreover have "y > 0"
by (rule less_le_trans[OF _ y]) auto
ultimately show "-1 / 2 + y *⇩R 𝗂 ∈ ℛ⇩Γ'"
using y by (auto simp: in_std_fund_region'_iff)
next
assume *: "-1 / 2 + y *⇩R 𝗂 ∈ ℛ⇩Γ'"
hence "y > 0"
by (auto simp: in_std_fund_region'_iff)
from * have "1 ≤ norm (y *⇩R 𝗂 - 1 / 2)"
by (auto simp: in_std_fund_region'_iff)
hence "1 ≤ norm (y *⇩R 𝗂 - 1 / 2) ^ 2"
by (simp add: power2_nonneg_ge_1_iff)
also have "… = (1 / 2) ^ 2 + y ^ 2"
unfolding cmod_power2 by simp
finally have "y ^ 2 ≥ (sqrt 3 / 2) ^ 2"
by (simp add: algebra_simps power2_eq_square)
hence "y ≥ sqrt 3 / 2"
by (rule power2_le_imp_le) (use ‹y > 0› in auto)
thus "y ≥ sqrt 3 / 2" using *
by (auto simp: in_std_fund_region'_iff)
qed
lemma std_fund_region'_border_aux1:
"{z. norm z = 1 ∧ 0 < Im z ∧ Re z ∈ {-1/2..0}} = cis ` {pi / 2..2 / 3 * pi}"
proof safe
fix z :: complex assume z: "norm z = 1" "Im z > 0" "Re z ∈ {-1/2..0}"
show "z ∈ cis ` {pi/2..2/3*pi}"
proof (rule rev_image_eqI)
from z have [simp]: "z ≠ 0"
by auto
have [simp]: "Arg z ≥ 0"
using z by (auto simp: Arg_less_0)
have z_eq: "cis (Arg z) = z"
using z by (auto simp: cis_Arg complex_sgn_def)
thus "z = cis (Arg z)"
by simp
have "Re (cis (Arg z)) ≥ -1/2"
using z by (subst z_eq) auto
hence "cos (Arg z) ≥ cos (2/3*pi)"
by (simp add: cos_120 cos_120')
hence "Arg z ≤ 2 / 3 * pi"
using Arg_le_pi by (subst (asm) cos_mono_le_eq) auto
moreover have "Re (cis (Arg z)) ≤ 0"
using z by (subst z_eq) auto
hence "cos (Arg z) ≤ cos (pi / 2)"
by simp
hence "Arg z ≥ pi / 2"
using Arg_le_pi by (subst (asm) cos_mono_le_eq) auto
ultimately show "Arg z ∈ {pi/2..2/3*pi}"
by simp
qed
next
fix t :: real assume t: "t ∈ {pi/2..2/3*pi}"
have "t > 0"
by (rule less_le_trans[of _ "pi/2"]) (use t in auto)
have "t < pi"
by (rule le_less_trans[of _ "2/3*pi"]) (use t in auto)
have "sin t > 0"
using ‹t > 0› ‹t < pi› by (intro sin_gt_zero) auto
moreover have "cos t ≤ cos (pi / 2)"
using t ‹t < pi› by (intro cos_monotone_0_pi_le) auto
moreover have "cos t ≥ cos (2*pi/3)"
using t by (intro cos_monotone_0_pi_le) auto
ultimately show "norm (cis t) = 1" "Im (cis t) > 0" "Re (cis t) ∈ {-1/2..0}"
by (auto simp: cos_120 cos_120')
qed
lemma std_fund_region'_border_aux2:
"{z. Re z = - 1 / 2 ∧ sqrt 3 / 2 ≤ Im z} = (λx. - 1 / 2 + x *⇩R 𝗂) ` {sqrt 3 / 2..}"
by (auto simp: complex_eq_iff)
lemma compact_std_fund_region:
assumes "B > 1"
shows "compact (closure ℛ⇩Γ ∩ {z. Im z ≤ B})"
unfolding compact_eq_bounded_closed
proof
show "closed (closure ℛ⇩Γ ∩ {z. Im z ≤ B})"
by (intro closed_Int closed_halfspace_Im_le) auto
next
show "bounded (closure ℛ⇩Γ ∩ {z. Im z ≤ B})"
proof -
have "closure ℛ⇩Γ ∩ {z. Im z ≤ B} ⊆ cbox (-1/2) (1/2 + 𝗂 * B)"
by (auto simp: in_closure_std_fund_region_iff in_cbox_complex_iff)
moreover have "bounded (cbox (-1/2) (1/2 + 𝗂 * B))"
by simp
ultimately show ?thesis
using bounded_subset by blast
qed
qed
end
subsection ‹Proving that the standard region is fundamental›
lemma norm_open_segment_less:
fixes x y z :: "'a :: euclidean_space"
assumes "norm x ≤ norm y" "z ∈ open_segment x y"
shows "norm z < norm y"
using assms
by (metis (no_types, opaque_lifting) diff_zero dist_decreases_open_segment
dist_norm norm_minus_commute order_less_le_trans)
text ‹Lemma 1›
lemma (in complex_lattice) std_fund_region_fundamental_lemma1:
obtains ω1' ω2' :: complex and a b c d :: int
where "¦a * d - b * c¦ = 1"
"ω2' = of_int a * ω2 + of_int b * ω1"
"ω1' = of_int c * ω2 + of_int d * ω1"
"Im (ω2' / ω1') ≠ 0"
"norm ω1' ≤ norm ω2'" "norm ω2' ≤ norm (ω1' + ω2')" "norm ω2' ≤ norm (ω1' - ω2')"
proof -
have "Λ⇧* ⊆ Λ" "Λ⇧* ≠ {}"
by auto
then obtain ω1' where ω1': "ω1' ∈ Λ⇧*" "⋀y. y ∈ Λ⇧* ⟹ norm ω1' ≤ norm y"
using shortest_lattice_vector_exists by blast
define X where "X = {y. y ∈ Λ⇧* ∧ y / ω1' ∉ ℝ}"
have "X ⊆ Λ"
by (auto simp: X_def lattice0_def)
moreover have "X ≠ {}"
using noncollinear_lattice_point_exists[of ω1'] ω1'(1) unfolding X_def by force
ultimately obtain ω2' where ω2': "ω2' ∈ X" "⋀z. z ∈ X ⟹ norm ω2' ≤ norm z"
using shortest_lattice_vector_exists by blast
have [simp]: "ω1' ≠ 0" "ω2' ≠ 0"
using ω1' ω2' by (auto simp: lattice0_def X_def)
have noncollinear: "ω2' / ω1' ∉ ℝ"
using ω2' by (auto simp: X_def)
hence fundpair': "fundpair (ω1', ω2')"
unfolding fundpair_def prod.case by simp
have Im_nz: "Im (ω2' / ω1') ≠ 0"
using noncollinear by (auto simp: complex_is_Real_iff)
have "norm ω1' ≤ norm ω2'"
by (intro ω1') (use ω2' in ‹auto simp: X_def›)
have triangle: "z ∉ Λ" if z: "z ∈ convex hull {0, ω1', ω2'}" "z ∉ {0, ω1', ω2'}" for z
proof
assume "z ∈ Λ"
hence "z ∈ Λ⇧*"
using z by (auto simp: lattice0_def)
from that obtain a b where ab: "a ≥ 0" "b ≥ 0" "a + b ≤ 1" "z = a *⇩R ω1' + b *⇩R ω2'"
unfolding convex_hull_3_alt by (auto simp: scaleR_conv_of_real)
have "norm z ≤ norm (a *⇩R ω1') + norm (b *⇩R ω2')"
unfolding ab using norm_triangle_ineq by blast
also have "… = a * norm ω1' + b * norm ω2'"
using ab by simp
finally have norm_z_le: "norm z ≤ a * norm ω1' + b * norm ω2'" .
also have "… ≤ a * norm ω2' + b * norm ω2'"
using ab ‹norm ω1' ≤ norm ω2'› by (intro add_mono mult_left_mono) auto
also have "… = (a + b) * norm ω2'"
by (simp add: algebra_simps)
finally have norm_z_le': "norm z ≤ (a + b) * norm ω2'" .
have "z / ω1' ∉ ℝ"
proof
assume real: "z / ω1' ∈ ℝ"
show False
proof (cases "b = 0")
case False
hence "ω2' / ω1' = (z / ω1' - of_real a) / of_real b"
by (simp add: ab field_simps scaleR_conv_of_real)
also have "… ∈ ℝ"
using real by (auto intro: Reals_divide Reals_diff)
finally show False
using noncollinear by contradiction
next
case True
hence "z = a *⇩R ω1'"
using ab by simp
from this and z have "a ≠ 1"
by auto
hence "a < 1"
using ab by simp
have "norm z = a * norm ω1'"
using ‹z = a *⇩R ω1'› ‹a ≥ 0› by simp
also have "… < 1 * norm ω1'"
using ‹a < 1› by (intro mult_strict_right_mono) auto
finally have "norm z < norm ω1'"
by simp
moreover have "norm z ≥ norm ω1'"
by (intro ω1') (use z ‹z ∈ Λ⇧*› in auto)
ultimately show False
by simp
qed
qed
hence "z ∈ X"
using ‹z ∈ Λ⇧*› by (auto simp: X_def)
hence "norm z ≥ norm ω2'"
by (intro ω2')
moreover have "norm z ≤ norm ω2'"
proof -
have "norm z ≤ (a + b) * norm ω2'"
by (rule norm_z_le')
also have "… ≤ 1 * norm ω2'"
using ab by (intro mult_right_mono) auto
finally show "norm z ≤ norm ω2'"
by simp
qed
ultimately have norm_z: "norm z = norm ω2'"
by linarith
have "¬(a + b < 1)"
proof
assume *: "a + b < 1"
have "norm z ≤ (a + b) * norm ω2'"
by (rule norm_z_le')
also have "… < 1 * norm ω2'"
by (intro mult_strict_right_mono *) auto
finally show False
using norm_z by simp
qed
with ab have b_eq: "b = 1 - a"
by linarith
have "norm z < norm ω2'"
proof (rule norm_open_segment_less)
have "a ≠ 0" "a ≠ 1"
using z ab by (auto simp: b_eq)
hence "∃u. u > 0 ∧ u < 1 ∧ z = (1 - u) *⇩R ω1' + u *⇩R ω2'"
using ab by (intro exI[of _ b]) (auto simp: b_eq)
thus "z ∈ open_segment ω1' ω2'"
using z ab noncollinear unfolding in_segment by auto
next
show "norm ω1' ≤ norm ω2'"
by fact
qed
with norm_z show False
by simp
qed
hence "convex hull {0, ω1', ω2'} ∩ Λ ⊆ {0, ω1', ω2'}"
by blast
moreover have "{0, ω1', ω2'} ⊆ convex hull {0, ω1', ω2'} ∩ Λ"
using ω1' ω2' by (auto intro: hull_inc simp: X_def)
ultimately have "convex hull {0, ω1', ω2'} ∩ Λ = {0, ω1', ω2'}"
by blast
hence "equiv_fundpair (ω1, ω2) (ω1', ω2')"
using fundpair' ω1' ω2' by (subst equiv_fundpair_iff_triangle) (auto simp: X_def)
then obtain a b c d :: int where
det: "¦a * d - b * c¦ = 1" and
abcd: "ω2' = of_int a * ω2 + of_int b * ω1" "ω1' = of_int c * ω2 + of_int d * ω1"
using fundpair fundpair' by (subst (asm) equiv_fundpair_iff) auto
have *: "norm (ω1' + of_int n * ω2') ≥ norm ω2'" if n: "n ≠ 0" for n
proof (rule ω2')
define z where "z = ω1' + of_int n * ω2'"
have "z ∈ Λ"
unfolding z_def using ω1'(1) ω2'(1) by (auto intro!: lattice_intros simp: X_def)
moreover have "z / ω1' ∉ ℝ"
proof
assume "z / ω1' ∈ ℝ"
hence "(z / ω1' - 1) / of_int n ∈ ℝ"
by auto
also have "(z / ω1' - 1) / of_int n = ω2' / ω1'"
using n by (simp add: field_simps z_def)
finally show False
using noncollinear by contradiction
qed
moreover from this have "z ≠ 0"
by auto
ultimately show "z ∈ X"
by (auto simp: X_def lattice0_def)
qed
have norms: "norm (ω1' + ω2') ≥ norm ω2'" "norm (ω1' - ω2') ≥ norm ω2'"
using *[of 1] and *[of "-1"] by simp_all
show ?thesis
using det norms abcd noncollinear ‹norm ω1' ≤ norm ω2'›
by (intro that[of a d b c ω2' ω1']) (simp_all add: complex_is_Real_iff)
qed
lemma (in complex_lattice) std_fund_region_fundamental_lemma2:
obtains ω1' ω2' :: complex and a b c d :: int
where "a * d - b * c = 1"
"ω2' = of_int a * ω2 + of_int b * ω1"
"ω1' = of_int c * ω2 + of_int d * ω1"
"Im (ω2' / ω1') ≠ 0"
"norm ω1' ≤ norm ω2'" "norm ω2' ≤ norm (ω1' + ω2')" "norm ω2' ≤ norm (ω1' - ω2')"
proof -
obtain ω1' ω2' a b c d
where abcd: "¦a * d - b * c¦ = 1"
and eq: "ω2' = of_int a * ω2 + of_int b * ω1" "ω1' = of_int c * ω2 + of_int d * ω1"
and nz: "Im (ω2' / ω1') ≠ 0"
and norms: "norm ω1' ≤ norm ω2'" "norm ω2' ≤ norm (ω1' + ω2')" "norm ω2' ≤ norm (ω1' - ω2')"
using std_fund_region_fundamental_lemma1 .
show ?thesis
proof (cases "a * d - b * c = 1")
case True
thus ?thesis
by (intro that[of a d b c ω2' ω1'] eq nz norms)
next
case False
show ?thesis
proof (intro that[of a "-d" b "-c" ω2' "-ω1'"])
from False have "a * d - b * c = -1"
using abcd by linarith
thus "a * (-d) - b * (-c) = 1"
by simp
next
show "ω2' = of_int a * ω2 + of_int b * ω1"
"-ω1' = of_int (- c) * ω2 + of_int (- d) * ω1"
using eq by (simp_all add: algebra_simps)
qed (use norms nz in ‹auto simp: norm_minus_commute add.commute›)
qed
qed
text ‹Theorem 2.2›
lemma std_fund_region_fundamental_aux1:
assumes "Im τ' > 0"
obtains τ where "Im τ > 0" "τ ∼⇩Γ τ'" "norm τ ≥ 1" "norm (τ + 1) ≥ norm τ" "norm (τ - 1) ≥ norm τ"
proof -
interpret std_complex_lattice τ'
using assms by unfold_locales (auto simp: complex_is_Real_iff)
obtain ω1 ω2 a b c d
where abcd: "a * d - b * c = 1"
and eq: "ω2 = of_int a * τ' + of_int b * 1" "ω1 = of_int c * τ' + of_int d * 1"
and nz: "Im (ω2 / ω1) ≠ 0"
and norms: "norm ω1 ≤ norm ω2" "norm ω2 ≤ norm (ω1 + ω2)" "norm ω2 ≤ norm (ω1 - ω2)"
using std_fund_region_fundamental_lemma2 .
from nz have [simp]: "ω1 ≠ 0" "ω2 ≠ 0"
by auto
interpret unimodular_moebius_transform a b c d
by unfold_locales fact
define τ where "τ = ω2 / ω1"
have τ_eq: "τ = φ τ'"
by (simp add: moebius_def τ_def eq add_ac φ_def)
show ?thesis
proof (rule that[of τ])
show "Im τ > 0"
using assms τ_eq by (simp add: Im_transform_pos)
next
show "norm τ ≥ 1" "norm (τ + 1) ≥ norm τ" "norm (τ - 1) ≥ norm τ"
using norms by (simp_all add: τ_def norm_divide field_simps norm_minus_commute)
next
have "τ = apply_modgrp as_modgrp τ'"
using τ_eq by (simp add: φ_as_modgrp)
thus "τ ∼⇩Γ τ'" using ‹Im τ' > 0›
by auto
qed
qed
lemma std_fund_region_fundamental_aux2:
assumes "norm (z + 1) ≥ norm z" "norm (z - 1) ≥ norm z"
shows "Re z ∈ {-1/2..1/2}"
proof -
have "0 ≤ norm (z + 1) ^ 2 - norm z ^ 2"
using assms by simp
also have "… = (Re z + 1)⇧2 - (Re z)⇧2"
unfolding norm_complex_def by simp
also have "… = 1 + 2 * Re z"
by (simp add: algebra_simps power2_eq_square)
finally have "Re z ≥ -1/2"
by simp
have "0 ≤ norm (z - 1) ^ 2 - norm z ^ 2"
using assms by simp
also have "… = (Re z - 1)⇧2 - (Re z)⇧2"
unfolding norm_complex_def by simp
also have "… = 1 - 2 * Re z"
by (simp add: algebra_simps power2_eq_square)
finally have "Re z ≤ 1/2"
by simp
with ‹Re z ≥ -1/2› show ?thesis
by simp
qed
lemma std_fund_region_fundamental_aux3:
fixes x y :: complex
assumes xy: "x ∈ ℛ⇩Γ" "y ∈ ℛ⇩Γ"
assumes f: "y = apply_modgrp f x"
defines "c ≡ modgrp_c f"
defines "d ≡ modgrp_d f"
assumes c: "c ≠ 0"
shows "Im y < Im x"
proof -
have ineq1: "norm (c * x + d) ^ 2 > c ^ 2 - ¦c * d¦ + d ^ 2"
proof -
have "of_int ¦c¦ * 1 < of_int ¦c¦ * norm x"
using xy c by (intro mult_strict_left_mono) (auto simp: std_fund_region_def)
hence "of_int c ^ 2 < (of_int c * norm x) ^ 2"
by (intro power2_strict_mono) auto
also have "… - ¦c * d¦ * 1 + d ^ 2 ≤
(of_int c * norm x) ^ 2 - ¦c * d¦ * (2 * ¦Re x¦) + d ^ 2"
using xy unfolding of_int_add of_int_mult of_int_power of_int_diff
by (intro add_mono diff_mono mult_left_mono) (auto simp: std_fund_region_def)
also have "… = c ^ 2 * norm x ^ 2 - ¦2 * c * d * Re x¦ + d ^ 2"
by (simp add: power_mult_distrib abs_mult)
also have "… ≤ c ^ 2 * norm x ^ 2 + 2 * c * d * Re x + d ^ 2"
by linarith
also have "… = norm (c * x + d) ^ 2"
unfolding cmod_power2 by (simp add: algebra_simps power2_eq_square)
finally show "norm (c * x + d) ^ 2 > c ^ 2 - ¦c * d¦ + d ^ 2"
by simp
qed
have "Im y = Im x / norm (c * x + d) ^ 2"
using f by (simp add: modgrp.Im_transform c_def d_def)
also have "norm (c * x + d) ^ 2 > 1"
proof (cases "d = 0")
case [simp]: True
have "0 < c ^ 2"
using c by simp
hence "1 ≤ real_of_int (c ^ 2) * 1"
by linarith
also have "… < of_int (c ^ 2) * norm x ^ 2"
using xy c by (intro mult_strict_left_mono) (auto simp: std_fund_region_def)
also have "… = norm (c * x + d) ^ 2"
by (simp add: norm_mult power_mult_distrib)
finally show ?thesis .
next
case False
have "0 < ¦c * d¦"
using c False by auto
hence "1 ≤ ¦c * d¦"
by linarith
also have "… ≤ ¦c * d¦ + (¦c¦ - ¦d¦) ^ 2"
by simp
also have "… = c ^ 2 - ¦c * d¦ + d ^ 2"
by (simp add: algebra_simps power2_eq_square abs_mult)
finally have "1 ≤ real_of_int (c ^ 2 - ¦c * d¦ + d ^ 2)"
by linarith
also have "… < norm (c * x + d) ^ 2"
using ineq1 False by simp
finally show ?thesis .
qed
hence "Im x / norm (c * x + d) ^ 2 < Im x / 1"
using xy by (intro divide_strict_left_mono) (auto simp: std_fund_region_def)
finally show ?thesis
by simp
qed
lemma std_fund_region_fundamental_aux4:
fixes x y :: complex
assumes xy: "x ∈ ℛ⇩Γ" "y ∈ ℛ⇩Γ"
assumes f: "y = apply_modgrp f x"
shows "¦f¦ = 1"
proof -
define a where "a = modgrp_a f"
define b where "b = modgrp_b f"
define c where "c = modgrp_c f"
define d where "d = modgrp_d f"
have c: "c = 0"
proof (rule ccontr)
assume c: "c ≠ 0"
have "Im y < Im x" using xy f c
by (intro std_fund_region_fundamental_aux3[where f = f]) (auto simp: c_def)
moreover have "Im y > Im x"
proof (rule std_fund_region_fundamental_aux3[where f = "inverse f"])
have "Im x > 0"
using xy by (auto simp: std_fund_region_def)
hence "x ≠ pole_modgrp f"
using pole_modgrp_in_Reals[of f, where ?'a = complex]
by (auto simp: complex_is_Real_iff)
with f have "apply_modgrp (inverse f) y = x"
by (intro apply_modgrp_inverse_eqI) auto
thus "x = apply_modgrp (inverse f) y" ..
next
have "is_singular_modgrp f"
using c by (simp add: is_singular_modgrp_altdef c_def)
hence "is_singular_modgrp (inverse f)"
by simp
thus "modgrp_c (inverse f) ≠ 0"
unfolding is_singular_modgrp_altdef by simp
qed (use xy c in ‹auto simp: c_def›)
ultimately show False
by simp
qed
define n where "n = sgn a * b"
from c have "¬is_singular_modgrp f"
by (auto simp: is_singular_modgrp_altdef c_def)
hence "¦f¦ = ¦shift_modgrp n¦"
using not_is_singular_modgrpD[of f] by (simp add: n_def a_def b_def)
hence f_eq: "f = shift_modgrp n ∨ f = -shift_modgrp n"
by (elim abs_modgrp_eqE) auto
from xy f f_eq have "n = 0"
by (auto simp: std_fund_region_def)
thus "¦f¦ = 1"
using f_eq by auto
qed
text ‹Theorem 2.3›
interpretation std_fund_region: fundamental_region UNIV std_fund_region
proof
show "std_fund_region ⊆ {z. Im z > 0}"
using Im_std_fund_region by blast
next
fix x y :: complex
assume xy: "x ∈ ℛ⇩Γ" "y ∈ ℛ⇩Γ" "x ∼⇩Γ y"
then obtain f where f: "y = apply_modgrp f x"
by (auto simp: modular_group.rel_def)
with xy have "¦f¦ = 1"
using std_fund_region_fundamental_aux4 by blast
with f xy show "x = y"
by (auto simp: abs_modgrp_eq_1_iff)
next
fix x :: complex
assume x: "Im x > 0"
obtain y where y: "Im y > 0" "y ∼⇩Γ x"
"norm y ≥ 1" "norm (y + 1) ≥ norm y" "norm (y - 1) ≥ norm y"
using std_fund_region_fundamental_aux1[OF x] by blast
from y have "Re y ∈ {-1/2..1/2}"
by (intro std_fund_region_fundamental_aux2)
with y show "∃y∈closure std_fund_region. x ∼⇩Γ y"
using x unfolding closure_std_fund_region by (auto simp: modular_group.rel_commutes)
qed auto
text ‹
Every point in the upper half plane has a canonical representative w.r.t.\ the full modular group
in the standard fundamental region.
›
lemma canonical_point_in_std_fund_region':
assumes "Im z > 0"
obtains z' where "z' ∈ ℛ⇩Γ'" "z ∼⇩Γ z'"
proof -
obtain z' where z': "z' ∈ closure ℛ⇩Γ" "z ∼⇩Γ z'"
using std_fund_region.equiv_in_closure[of z] assms by blast
show ?thesis
proof (cases "z' ∈ ℛ⇩Γ'")
case True
thus ?thesis
by (intro that[of z']) (use z' in auto)
next
case False
with z' have "z' ∈ closure ℛ⇩Γ - ℛ⇩Γ'"
by blast
hence "norm z' = 1 ∧ Im z' > 0 ∧ Re z' ∈ {0<..1/2} ∨ Re z' = 1 / 2 ∧ Im z' ≥ sqrt 3 / 2"
by (subst (asm) closure_std_fund_region_minus_std_fund_region') simp_all
thus ?thesis
proof
assume *: "norm z' = 1 ∧ Im z' > 0 ∧ Re z' ∈ {0<..1/2}"
define z'' where "z'' = apply_modgrp S_modgrp z'"
have "z ∼⇩Γ z''"
unfolding z''_def using z'(2) by blast
moreover have "z'' ∈ ℛ⇩Γ'"
using * by (auto simp: z''_def norm_divide divide_conv_cnj in_std_fund_region'_iff)
ultimately show ?thesis
by (intro that[of z''])
next
assume *: "Re z' = 1 / 2 ∧ Im z' ≥ sqrt 3 / 2"
have [simp]: "Re z' = 1 / 2"
using * by blast
define z'' where "z'' = apply_modgrp (shift_modgrp (-1)) z'"
have "z ∼⇩Γ z''"
unfolding z''_def using z'(2) by blast
moreover have "norm z'' = norm z'"
by (auto simp: z''_def cmod_def)
hence "z'' ∈ ℛ⇩Γ'" using z'
by (auto simp: z''_def in_std_fund_region'_iff in_closure_std_fund_region_iff cmod_def)
ultimately show ?thesis
by (intro that[of z''])
qed
qed
qed
theorem std_fund_region_no_fixed_point:
assumes "z ∈ ℛ⇩Γ"
assumes "apply_modgrp f z = z"
shows "¦f¦ = 1"
using std_fund_region_fundamental_aux4[of z "apply_modgrp f z" f] assms by auto
lemma std_fund_region_no_fixed_point':
assumes "z ∈ ℛ⇩Γ"
assumes "apply_modgrp f z = apply_modgrp g z"
shows "¦f¦ = ¦g¦"
proof -
have z: "Im z > 0"
using assms by (auto simp: in_std_fund_region_iff)
have "apply_modgrp (inverse f) (apply_modgrp g z) = apply_modgrp (inverse f) (apply_modgrp f z)"
by (simp only: assms(2))
also have "… = z"
using z by (intro apply_modgrp_inverse_eqI) auto
also have "apply_modgrp (inverse f) (apply_modgrp g z) = apply_modgrp (inverse f * g) z"
by (rule apply_modgrp_mult [symmetric]) (use z in auto)
finally have "¦inverse f * g¦ = 1"
using assms by (intro std_fund_region_no_fixed_point) auto
thus ?thesis
by (metis abs_uminus_modgrp minus_minus_modgrp modgrp.inverse_inverse modgrp.inverse_unique
times_modgrp_uminus_right abs_modgrp_eq_1_iff)
qed
text ‹
The image of the fundamental region under a unimodular transformation is again a
fundamental region.
›
locale std_fund_region_image =
fixes f :: modgrp and R :: "complex set"
defines "R ≡ apply_modgrp f ` ℛ⇩Γ"
begin
lemma R_altdef: "R = {z. Im z > 0} ∩ apply_modgrp (inverse f) -` ℛ⇩Γ"
unfolding R_def
proof safe
fix z assume z: "z ∈ ℛ⇩Γ"
thus "Im (apply_modgrp f z) > 0"
by (auto simp: Im_std_fund_region)
have "apply_modgrp (inverse f) (apply_modgrp f z) ∈ ℛ⇩Γ"
by (subst apply_modgrp_mult [symmetric]) (use z in auto)
thus "apply_modgrp f z ∈ apply_modgrp (inverse f) -` ℛ⇩Γ"
by (auto simp flip: apply_modgrp_mult)
next
fix z assume z: "apply_modgrp (inverse f) z ∈ ℛ⇩Γ" "Im z > 0"
have "z = apply_modgrp f (apply_modgrp (inverse f) z)"
by (subst apply_modgrp_mult [symmetric]) (use z(2) in auto)
with z show "z ∈ apply_modgrp f ` ℛ⇩Γ"
by blast
qed
lemma R_altdef': "R = apply_modgrp (inverse f) -` ℛ⇩Γ"
unfolding R_altdef by (auto simp: in_std_fund_region_iff)
sublocale fundamental_region UNIV R
proof
show "open R"
unfolding R_altdef
by (intro continuous_open_preimage continuous_intros) (auto simp: open_halfspace_Im_gt )
show "R ⊆ {z. 0 < Im z}"
unfolding R_altdef by auto
show "x = y" if "x ∈ R" "y ∈ R" "x ∼⇩Γ y" for x y
using that unfolding R_def by (auto dest: std_fund_region.unique)
show "∃y∈closure R. x ∼⇩Γ y" if "Im x > 0" for x
proof -
define x' where "x' = apply_modgrp (inverse f) x"
have x': "Im x' > 0"
using that by (simp add: x'_def)
then obtain y where y: "y ∈ closure ℛ⇩Γ" "x' ∼⇩Γ y"
using std_fund_region.equiv_in_closure[of x'] by blast
define y' where "y' = apply_modgrp f y"
have "y islimpt ℛ⇩Γ"
using y by (meson islimpt_closure_open limpt_of_closure open_std_fund_region)
then obtain h :: "nat ⇒ complex" where h: "⋀n. h n ∈ ℛ⇩Γ - {y}" "h ⇢ y"
unfolding islimpt_sequential by blast
have "(apply_modgrp f ∘ h) n ∈ R - {y'}" for n
proof -
have Ims: "Im y > 0" "Im (h n) > 0"
using y h(1)[of n] by (auto simp: in_std_fund_region_iff)
have "apply_modgrp f (h n) ∈ R" "h n ≠ y"
using h(1)[of n] by (auto simp: R_def)
moreover have "apply_modgrp f (h n) ≠ y'"
unfolding y'_def using y ‹h n ≠ y› Ims by (subst apply_modgrp_eq_iff) auto
ultimately show ?thesis
by auto
qed
moreover have "(apply_modgrp f ∘ h) ⇢ y'"
unfolding y'_def using y by (auto intro!: tendsto_compose_at[OF h(2)] tendsto_eq_intros)+
ultimately have "y' islimpt R"
unfolding islimpt_sequential by blast
hence "y' ∈ closure R"
by (simp add: closure_def)
moreover have "x ∼⇩Γ y'"
using x' that y unfolding y'_def x'_def
by (auto simp: modular_group.rel_commutes)
ultimately show ?thesis
by blast
qed
qed
end
subsection ‹The corner point of the standard fundamental region›
text ‹
The point $\rho = \exp(2/3\pi) = -\frac{1}{2} + \frac{\sqrt{3}}{2} i$ is the left corner
of the standard fundamental region, and its reflection on the imaginary axis (which is the
same as its image under $z \mapsto -1/z$) forms the right corner.
›
definition modfun_rho ("❙ρ") where
"❙ρ = cis (2 / 3 * pi)"
lemma modfun_rho_altdef: "❙ρ = -1 / 2 + sqrt 3 / 2 * 𝗂"
by (simp add: complex_eq_iff modfun_rho_def Re_exp Im_exp sin_120 cos_120)
lemma Re_modfun_rho [simp]: "Re ❙ρ = -1 / 2"
and Im_modfun_rho [simp]: "Im ❙ρ = sqrt 3 / 2"
by (simp_all add: modfun_rho_altdef)
lemma norm_modfun_rho [simp]: "norm ❙ρ = 1"
by (simp add: modfun_rho_def)
lemma modfun_rho_plus_1_eq: "❙ρ + 1 = exp (pi / 3 * 𝗂)"
by (simp add: modfun_rho_altdef complex_eq_iff Re_exp Im_exp sin_60 cos_60)
lemma norm_modfun_rho_plus_1 [simp]: "norm (❙ρ + 1) = 1"
by (simp add: modfun_rho_plus_1_eq)
lemma cnj_modfun_rho: "cnj ❙ρ = -❙ρ - 1"
and cnj_modfun_rho_plus1: "cnj (❙ρ + 1) = -❙ρ"
by (auto simp: complex_eq_iff)
lemma modfun_rho_cube: "❙ρ ^ 3 = 1"
by (simp add: modfun_rho_def Complex.DeMoivre)
lemma modfun_rho_power_mod3_reduce: "❙ρ ^ n = ❙ρ ^ (n mod 3)"
proof -
have "❙ρ ^ n = ❙ρ ^ (3 * (n div 3) + (n mod 3))"
by simp
also have "… = (❙ρ ^ 3) ^ (n div 3) * ❙ρ ^ (n mod 3)"
by (subst power_add) (simp add: power_mult)
also have "… = ❙ρ ^ (n mod 3)"
by (simp add: modfun_rho_cube)
finally show ?thesis .
qed
lemma modfun_rho_power_mod3_reduce': "n ≥ 3 ⟹ ❙ρ ^ n = ❙ρ ^ (n mod 3)"
by (rule modfun_rho_power_mod3_reduce)
lemmas [simp] = modfun_rho_power_mod3_reduce' [of "numeral num" for num]
lemma modfun_rho_square: "❙ρ ^ 2 = -❙ρ - 1"
by (simp add: modfun_rho_altdef power2_eq_square field_simps flip: of_real_mult)
lemma modfun_rho_not_real [simp]: "❙ρ ∉ ℝ"
by (simp add: modfun_rho_altdef complex_is_Real_iff)
lemma modfun_rho_nonzero [simp]: "❙ρ ≠ 0"
by (simp add: modfun_rho_def)
lemma modfun_rho_not_one [simp]: "❙ρ ≠ 1"
by (simp add: complex_eq_iff modfun_rho_altdef)
lemma i_neq_modfun_rho [simp]: "𝗂 ≠ ❙ρ"
and i_neq_modfun_rho_plus1 [simp]: "𝗂 ≠ ❙ρ + 1"
and modfun_rho_neg_i [simp]: "❙ρ ≠ 𝗂"
and modfun_rho_plus1_neg_i [simp]: "❙ρ + 1 ≠ 𝗂"
by (auto simp: complex_eq_iff)
lemma i_in_closure_std_fund_region [intro, simp]: "𝗂 ∈ closure ℛ⇩Γ"
and i_in_std_fund_region' [intro, simp]: "𝗂 ∈ ℛ⇩Γ'"
and modfun_rho_in_closure_std_fund_region [intro, simp]: "❙ρ ∈ closure ℛ⇩Γ"
and modfun_rho_in_std_fund_region' [intro, simp]: "❙ρ ∈ ℛ⇩Γ'"
and modfun_rho_plus_1_notin_closure_std_fund_region [intro, simp]: "❙ρ + 1 ∈ closure ℛ⇩Γ"
and modfun_rho_plus_1_notin_std_fund_region' [intro, simp]: "❙ρ + 1 ∉ ℛ⇩Γ'"
by (simp_all add: closure_std_fund_region std_fund_region'_def in_std_fund_region_iff)
lemma modfun_rho_power_eq_1_iff: "❙ρ ^ n = 1 ⟷ 3 dvd n"
proof -
have "❙ρ ^ n = 1 ⟷ (∃k. real n = 3 * real_of_int k)"
by (simp add: modfun_rho_def Complex.DeMoivre cis_eq_1_iff)
also have "(λk. real n = 3 * real_of_int k) = (λk. int n = 3 * k)"
by (rule ext) linarith
also have "(∃k. int n = 3 * k) ⟷ 3 dvd n"
by presburger
finally show ?thesis .
qed
subsection ‹The elliptic points of the modular group›
text ‹
We will now explicitly compute the stabilisers of $i$ and $\rho$ and, from that,
see that they are elliptic points of order 2 and 3, respectively.
We will later see that these are the only elliptic points of the modular group
(up to equivalence w.r.t.\ unimodular transformations, of course).
›
lemma abs_le_1_iff_int: "abs n ≤ 1 ⟷ n = 0 ∨ n = 1 ∨ n = (-1::int)"
by linarith
lemma abs_eq_1_iff: "abs (x :: 'a :: linordered_idom) = 1 ⟷ x = 1 ∨ x = -1"
by (auto simp: abs_if)
text ‹
The stabilisers of two equivalent points are related by conjugation.
›
lemma bij_betw_stabiliser_modgrp_apply_modgrp:
fixes h :: modgrp
assumes x: "Im x > 0"
defines "Stab ≡ (λx. {h. apply_modgrp h x = x})"
defines "y ≡ apply_modgrp h x"
shows "bij_betw (λf. h * f * inverse h) (Stab x) (Stab y)"
proof (rule bij_betwI)
show "(λf. h * f * inverse h) ∈ Stab x → Stab y"
using x unfolding Stab_def y_def Pi_def mem_Collect_eq
by (metis Im_pole_modgrp apply_modgrp_inverse_eqI
apply_modgrp_mult assms(3) linorder_not_le
modgrp.Im_transform_zero_iff order.refl)
next
show "(λf. inverse h * f * h) ∈ Stab y → Stab x"
using x unfolding Stab_def y_def Pi_def mem_Collect_eq
by (metis Im_pole_modgrp apply_modgrp_inverse_eqI
apply_modgrp_mult assms(3) linorder_not_le
modgrp.Im_transform_zero_iff order.refl)
next
show "inverse h * (h * f * inverse h) * h = f" for f
by (simp add: mult.assoc)
next
show "h * (inverse h * f * h) * inverse h = f" for f
by (simp add: mult.assoc)
qed
lemma stabiliser_ii_modgrp: "apply_modgrp h 𝗂 = 𝗂 ⟷ h ∈ {1, -1, S_modgrp, -S_modgrp}"
proof
assume h: "h ∈ {1, -1, S_modgrp, -S_modgrp}"
thus "apply_modgrp h 𝗂 = 𝗂" by auto
next
assume "apply_modgrp h 𝗂 = 𝗂"
define a b c d :: int
where abcd_def: "a = modgrp_a h" "b = modgrp_b h" "c = modgrp_c h" "d = modgrp_d h"
have det: "a * d - b * c = 1"
unfolding abcd_def by (metis modgrp.unimodular)
define n where "n = (c ^ 2 + d ^ 2)"
have "c ≠ 0 ∨ d ≠ 0"
using det by auto
hence "n > 0"
using det unfolding n_def by (elim disjE) (auto intro: add_pos_nonneg add_nonneg_pos)
have "𝗂 = apply_modgrp h 𝗂"
by (rule sym) fact
also have "apply_modgrp h 𝗂 = (a * 𝗂 + b) / (c * 𝗂 + d)"
by (simp add: apply_modgrp_altdef moebius_def field_simps abcd_def)
also have "… = (a * 𝗂 + b) * (d - c * 𝗂) / n"
by (subst complex_div_cnj) (auto simp: cmod_def n_def)
also have "… = 𝗂 ⟷ (a * 𝗂 + b) * (d - c * 𝗂) = n * 𝗂"
using ‹n > 0› by (simp add: divide_simps mult_ac)
also have "… ⟷ real_of_int (a * c + b * d) = of_int 0 ∧ real_of_int (a * d - b * c) = of_int n"
unfolding of_int_add by (simp add: complex_eq_iff algebra_simps)
also have "… ⟷ a * c + b * d = 0 ∧ a * d - b * c = n"
by (simp only: of_int_eq_iff)
also have "a * d - b * c = 1"
by (rule det)
finally have eq: "a * c + b * d = 0" and "n = 1"
by auto
from ‹n = 1› have "c = 0 ∧ abs d = 1 ∨ abs c = 1 ∧ d = 0" unfolding n_def
by (metis (no_types, lifting) abs_mult abs_zmult_eq_1
add.right_neutral add_0 add_mono_thms_linordered_field(1) div_0
nonzero_mult_div_cancel_left power2_abs power2_eq_square
zabs_less_one_iff zero_less_abs_iff)
with eq det show "h ∈ {1, -1, S_modgrp, -S_modgrp}" using det
unfolding insert_iff modgrp_eq_iff abcd_def [symmetric] abs_eq_1_iff zmult_eq_1_iff
by (elim disjE conjE) auto
qed
lemma ellorder_modgrp_UNIV_ii [simp]: "ellorder_modgrp UNIV 𝗂 = 2"
proof -
have "ellorder_modgrp UNIV 𝗂 = card {h. apply_modgrp h 𝗂 = 𝗂} div card {1::modgrp, -1}"
by (simp add: ellorder_modgrp_def)
also have "card {1::modgrp, -1} = 2"
by (auto simp: modgrp_eq_iff)
also have "{h. apply_modgrp h 𝗂 = 𝗂} = {1, -1, S_modgrp, -S_modgrp}"
by (subst stabiliser_ii_modgrp) auto
also have "card … = 4"
by (simp add: modgrp_eq_iff)
finally show ?thesis
by simp
qed
lemma ellorder_modgrp_UNIV_ii': "z ∼⇩Γ 𝗂 ⟹ ellorder_modgrp UNIV z = 2"
by (metis ellorder_modgrp_UNIV_ii modular_group.ellorder_modgrp_cong)
lemma stabiliser_rho_modgrp_aux:
assumes "a ^ 2 + a * b + b ^ 2 ≤ (1::int)"
shows "¦b¦ ≤ 1"
proof -
have "1 ≥ real_of_int (a ^ 2 + a * b + b ^ 2)"
using assms by linarith
also have "real_of_int (a ^ 2 + a * b + b ^ 2) = (a + b / 2) ^ 2 + 3 / 4 * b ^ 2"
by (simp add: algebra_simps power2_eq_square)
finally have "b ^ 2 ≤ 4 / 3 * (1 - (a + b / 2) ^ 2)"
by (simp add: algebra_simps)
also have "… ≤ 4 / 3 * (1 - 0) ^ 2"
by (intro mult_left_mono diff_left_mono) auto
finally have "real_of_int (b ^ 2) ≤ 4 / 3"
by simp
hence "b ^ 2 ≤ 1"
by linarith
thus "¦b¦ ≤ 1"
by (metis abs_square_le_1)
qed
lemma stabiliser_rho_modgrp:
defines "ST ≡ S_modgrp * T_modgrp"
shows "apply_modgrp h ❙ρ = ❙ρ ⟷ h ∈ {1, -1, ST, -ST, ST⇧2, -(ST⇧2)}"
proof
assume h: "h ∈ {1, -1, ST, -ST, ST⇧2, -(ST⇧2)}"
show "apply_modgrp h ❙ρ = ❙ρ" using h unfolding ST_def
by (elim insertE)
(simp_all add: apply_modgrp_mult power2_eq_square complex_eq_iff Re_divide Im_divide
del: apply_modgrp_abs)
next
assume "apply_modgrp h ❙ρ = ❙ρ"
define a b c d :: int
where abcd_def: "a = modgrp_a h" "b = modgrp_b h" "c = modgrp_c h" "d = modgrp_d h"
have det: "a * d - b * c = 1"
unfolding abcd_def by (metis modgrp.unimodular)
have nz: "c * ❙ρ + d ≠ 0"
using det by (auto simp: complex_eq_iff)
have "❙ρ = apply_modgrp h ❙ρ"
by (rule sym) fact
also have "apply_modgrp h❙ρ = (a * ❙ρ + b) / (c * ❙ρ + d)"
by (simp add: apply_modgrp_altdef moebius_def field_simps abcd_def)
also have "… = ❙ρ ⟷ (a * ❙ρ + b) = c * ❙ρ⇧2 + d * ❙ρ"
using nz by (simp add: field_simps power2_eq_square)
finally have "(b + c) + ❙ρ * (a + c - d) = 0"
by (simp add: modfun_rho_square algebra_simps)
hence "of_int (c + d + 2 * b) = real_of_int a ∧ of_int (a + c) * sqrt 3 = of_int d * sqrt 3"
unfolding of_int_add by (auto simp: modfun_rho_altdef algebra_simps complex_eq_iff)
also have "of_int (a + c) * sqrt 3 = of_int d * sqrt 3 ⟷ of_int (a + c) = real_of_int d"
by (subst mult_cancel_right) auto
finally have ac: "c = -b" "a = d - c"
unfolding of_int_eq_iff by (auto simp: algebra_simps)
from ac and det have *: "b ^ 2 + b * d + d ^ 2 = 1"
by (auto simp: algebra_simps power2_eq_square)
have "¦b¦ ≤ 1" "¦d¦ ≤ 1"
using stabiliser_rho_modgrp_aux[of b d] stabiliser_rho_modgrp_aux[of d b] *
by (simp_all add: add_ac mult_ac)
with * have "(b, d) ∈ {(1, 0), (-1, 0), (0, 1), (0, -1), (1, -1), (-1, 1)}"
unfolding abs_le_1_iff_int insert_iff prod.inject by (elim disjE) simp_all
thus "h ∈ {1, -1, ST, -ST, ST⇧2, -(ST⇧2)}" using ac
unfolding insert_iff modgrp_eq_iff abcd_def [symmetric] abs_eq_1_iff zmult_eq_1_iff ST_def
by (elim disjE conjE) (auto simp: power2_eq_square)
qed
lemma ellorder_modgrp_UNIV_rho [simp]: "ellorder_modgrp UNIV ❙ρ = 3"
proof -
define ST where "ST = S_modgrp * T_modgrp"
have "ellorder_modgrp UNIV ❙ρ = card {h. apply_modgrp h ❙ρ = ❙ρ} div card {1::modgrp, -1}"
by (simp add: ellorder_modgrp_def)
also have "card {1::modgrp, -1} = 2"
by (auto simp: modgrp_eq_iff)
also have "{h. apply_modgrp h ❙ρ = ❙ρ} = {1, -1, ST, -ST, ST⇧2, -(ST⇧2)}"
by (subst stabiliser_rho_modgrp) (auto simp: ST_def)
also have "card … = 6"
by (simp add: modgrp_eq_iff ST_def power2_eq_square)
finally show ?thesis
by simp
qed
lemma ellorder_modgrp_UNIV_rho': "z ∼⇩Γ ❙ρ ⟹ ellorder_modgrp UNIV z = 3"
by (metis ellorder_modgrp_UNIV_rho modular_group.ellorder_modgrp_cong)
text ‹
Other than $i$ and $\rho$, no non-trivial unimodular transformation has any fixed points
in the fundamental region.
›
lemma modgrp_fixed_point_trivial:
assumes "z ∈ ℛ⇩Γ' - {𝗂, ❙ρ}" "apply_modgrp h z = z"
shows "abs h = 1"
proof (cases "z ∈ ℛ⇩Γ")
case True
thus ?thesis
using assms std_fund_region_no_fixed_point by blast
next
case False
define a b c d :: int
where abcd_def: "a = modgrp_a h" "b = modgrp_b h" "c = modgrp_c h" "d = modgrp_d h"
have h_eq: "h = modgrp a b c d"
unfolding abcd_def by (rule modgrp.as_modgrp_altdef)
have det: "a * d - b * c = 1"
unfolding abcd_def by (metis modgrp.unimodular)
from assms have "Im z > 0"
by (auto simp: std_fund_region'_def std_fund_region_def)
from False have "norm z = 1 ∧ 0 < Im z ∧ Re z ∈ {-1/2..0} ∨ Re z = -1/2 ∧ sqrt 3 / 2 ≤ Im z"
using assms std_fund_region'_minus_std_fund_region by blast
thus ?thesis
proof
assume z: "Re z = -1/2 ∧ sqrt 3 / 2 ≤ Im z"
define y where "y = Im z"
have "y ≠ sqrt 3 / 2"
using assms z by (auto simp: complex_eq_iff y_def)
with z have y: "y > sqrt 3 / 2"
by (auto simp: y_def)
have z_eq: "z = -1/2 + 𝗂 * y"
using z by (auto simp: y_def complex_eq_iff)
have nz: "c * z + d ≠ 0"
using det y by (auto simp: complex_eq_iff z_eq)
have "y ≠ 0"
using y by auto
have "z = apply_modgrp h z"
by (rule sym) fact
also have "… = (a * z + b) / (c * z + d)"
by (simp add: apply_modgrp_altdef moebius_def flip: abcd_def)
finally have eq: "c * z ^ 2 + (d - a) * z - b = 0"
using nz by (simp add: field_simps power2_eq_square)
have "0 = Im (c * z ^ 2 + (d - a) * z - b)"
by (subst eq) auto
also have "… = y * (d - a - c)"
by (simp add: z_eq power2_eq_square field_simps)
finally have a_eq: "a = d - c"
using ‹y ≠ 0› by simp
from det have bc_eq: "b * c = d ^ 2 - c * d - 1"
by (auto simp: a_eq algebra_simps power2_eq_square)
have "0 = 4 * c * Re (c * z ^ 2 + (d - a) * z - b)"
by (subst eq) auto
also have "… = -(4 * (b * c) + c ^ 2 * (4 * y ^ 2 + 1))"
by (simp add: a_eq z_eq power2_eq_square field_simps)
also have "… = 4 - ((c - 2 * d) ^ 2 + (2*c*y)^2)"
by (subst bc_eq) (auto simp: algebra_simps power2_eq_square)
finally have eq': "(c - 2 * d) ^ 2 + (2 * c * y) ^ 2 = 4"
by simp
show "abs h = 1"
proof (cases "c = 0")
case [simp]: True
from eq' have d: "d = 1 ∨ d = -1"
by (auto simp: power2_eq_1_iff)
have "b = 0"
using d det eq by auto
with d a_eq show ?thesis
by (elim disjE) (simp_all add: h_eq modgrp_eq_iff modgrp_abcd_modgrp abs_modgrp_altdef)
next
case c: False
have "3 * c ^ 2 = (2 * c * (sqrt 3 / 2)) ^ 2"
by (simp add: power_mult_distrib)
also have "… ≤ (c - 2 * d) ^ 2 + (2 * c * (sqrt 3 / 2)) ^ 2"
by simp
also have "… < (c - 2 * d) ^ 2 + (2 * c * y) ^ 2"
unfolding power_mult_distrib using c
by (intro add_strict_left_mono power_strict_mono mult_strict_left_mono y) auto
also have "… = 4"
by (subst eq') auto
finally have "real_of_int (c ^ 2) < 4 / 3"
by simp
hence "c ^ 2 ≤ 1"
by linarith
hence "c ^ 2 = 1" "abs c = 1"
using c by (auto simp: abs_square_le_1 abs_square_eq_1)
have "real_of_int ((c - 2 * d)⇧2 + 3) = (c - 2 * d) ^ 2 + (2 * c * (sqrt 3 / 2)) ^ 2"
by (simp add: power_mult_distrib ‹c ^ 2 = 1› flip: of_int_power)
also have "… < (c - 2 * d) ^ 2 + (2 * c * y) ^ 2"
unfolding power_mult_distrib using c
by (intro add_strict_left_mono power_strict_mono mult_strict_left_mono y) auto
also have "… = 4"
by (subst eq') auto
finally have "(c - 2 * d) ^ 2 < 1"
by linarith
hence "c - 2 * d = 0"
by (simp add: abs_square_less_1)
with ‹abs c = 1› have False
by presburger
thus ?thesis ..
qed
next
assume z: "norm z = 1 ∧ Im z > 0 ∧ Re z ∈ {-1/2..0}"
define x y where "x = Re z" and "y = Im z"
have z_eq: "z = Complex x y"
by (auto simp: complex_eq_iff x_def y_def)
have xy: "x ^ 2 + y ^ 2 = 1" "y > 0" "x ∈ {-1/2..0}"
using z by (auto simp: x_def y_def cmod_def)
have "x ≠ 0"
using assms xy by (auto simp: complex_eq_iff power2_eq_1_iff x_def y_def)
moreover have "x ≠ -1/2"
proof
assume "x = -1/2"
hence "y ^ 2 = (sqrt 3 / 2) ^ 2"
using xy by (auto simp: complex_eq_iff power_divide power2_eq_1_iff x_def y_def)
hence "y = sqrt 3 / 2"
using ‹y > 0› by (subst (asm) power2_eq_iff_nonneg) auto
with ‹x = -1/2› show False
using assms by (auto simp: complex_eq_iff z_eq)
qed
ultimately have x: "x ∈ {-1/2<..<0}"
using xy by auto
have nz: "c * z + d ≠ 0"
using det xy by (auto simp: z_eq complex_eq_iff)
have "z = apply_modgrp h z"
by (rule sym) fact
also have "… = (a * z + b) / (c * z + d)"
by (simp add: apply_modgrp_altdef moebius_def flip: abcd_def)
finally have eq: "c * z ^ 2 + (d - a) * z - b = 0"
using nz by (simp add: field_simps power2_eq_square)
have "0 = Im (c * z ^ 2 + (d - a) * z - b)"
by (subst eq) auto
also have "… = y * (d - a + 2 * c * x)"
by (simp add: z_eq power2_eq_square field_simps)
finally have d_eq: "d = a - 2 * c * x"
using ‹y > 0› by simp
have "0 = Re (c * z ^ 2 + (d - a) * z - b)"
by (subst eq) auto
also have "… = -(b + c * (x ^ 2 + y ^ 2))"
by (simp add: z_eq power2_eq_square field_simps d_eq)
also have "x ^ 2 + y ^ 2 = 1"
using xy by simp
finally have b_eq: "b = -c"
by auto
show ?thesis
proof (cases "c = 0")
case True
hence "h = 1 ∨ h = -1"
using det b_eq xy eq
by (auto simp: h_eq abs_modgrp_altdef modgrp_abcd_modgrp zmult_eq_1_iff modgrp_eq_iff)
thus ?thesis
by auto
next
case False
with d_eq have x_eq: "x = (a - d) / (2 * c)"
by auto
have "¦x¦ ^ 2 * (2*c) ^ 2 ≤ (1/2) ^ 2 * (2*c) ^ 2"
using xy by (intro mult_right_mono power_mono) auto
also have "¦x¦ ^ 2 * (2*c) ^ 2 = (a - d) ^ 2"
using False by (auto simp: x_eq abs_mult power_divide power_mult_distrib)
also have "(1/2) ^ 2 * (2*c) ^ 2 = c ^ 2"
by (simp add: power_divide)
also have "c ^ 2 = 1 - a * d"
using det by (simp add: b_eq power2_eq_square)
finally have "(a - d) ^ 2 ≤ 1 - a * d"
by linarith
hence ineq: "a ^ 2 - a * d + d ^ 2 ≤ 1"
by (simp add: power2_eq_square algebra_simps)
hence "¦a¦ ≤ 1" "¦d¦ ≤ 1"
using stabiliser_rho_modgrp_aux[of "-a" d] stabiliser_rho_modgrp_aux[of "-d" a]
by (simp_all add: mult_ac add_ac)
hence False
unfolding abs_le_1_iff_int using det False ineq x
by (elim disjE) (auto simp: b_eq x_eq power_divide zmult_eq_1_iff)
thus ?thesis ..
qed
qed
qed
text ‹
Therefore, all points not equivalent to $i$ or $\rho$ have elliptic order 1, i.e.\ are not
elliptic points.
›
lemma ellorder_modgrp_UNIV_eq_1':
assumes "z ∈ ℛ⇩Γ' - {𝗂, ❙ρ}"
shows "ellorder_modgrp UNIV z = 1"
proof -
from assms have "ellorder_modgrp UNIV z = card {h. apply_modgrp h z = z} div 2"
by (simp add: ellorder_modgrp_def modgrp_eq_iff numeral_2_eq_2 in_std_fund_region'_iff)
also have "{h. apply_modgrp h z = z} = {1, -1}"
using modgrp_fixed_point_trivial[of z] assms by (auto simp: abs_modgrp_eq_1_iff)
also have "card … = 2"
by (simp add: modgrp_eq_iff numeral_2_eq_2)
finally show ?thesis
by simp
qed
lemma ellorder_modgrp_UNIV_eq_1:
assumes "Im z > 0" "¬(z ∼⇩Γ 𝗂)" "¬(z ∼⇩Γ ❙ρ)"
shows "ellorder_modgrp UNIV z = 1"
proof -
obtain z' where z': "z' ∈ ℛ⇩Γ'" "z ∼⇩Γ z'"
using canonical_point_in_std_fund_region' assms(1) by blast
have "Im z' > 0"
using z' by (auto simp: in_std_fund_region'_iff)
have "ellorder_modgrp UNIV z = ellorder_modgrp UNIV z'"
by (intro modular_group.ellorder_modgrp_cong) (use z' in auto)
also have "… = 1"
by (rule ellorder_modgrp_UNIV_eq_1') (use z' assms in auto)
finally show ?thesis .
qed
lemma ellorder_modgrp_UNIV_eq:
"ellorder_modgrp UNIV z =
(if Im z ≤ 0 then 0 else if z ∼⇩Γ 𝗂 then 2 else if z ∼⇩Γ ❙ρ then 3 else 1)"
proof (cases "Im z > 0")
case True
thus ?thesis
using ellorder_modgrp_UNIV_eq_1[of z] ellorder_modgrp_UNIV_ii ellorder_modgrp_UNIV_rho
modular_group.ellorder_modgrp_cong[of z]
by (auto dest: modular_group.ellorder_modgrp_cong)
qed (auto simp: ellorder_modgrp_def)
text ‹
A simple consequence: no unimodular transformation sends $\rho$ to $i$.
›
lemma not_rho_equiv_i [simp]: "¬(❙ρ ∼⇩Γ 𝗂)"
proof
assume "❙ρ ∼⇩Γ 𝗂"
hence "ellorder_modgrp UNIV ❙ρ = ellorder_modgrp UNIV 𝗂"
by (rule modular_group.ellorder_modgrp_cong)
thus False
by simp
qed
lemma not_i_equiv_rho [simp]: "¬(𝗂 ∼⇩Γ ❙ρ)"
by (subst modular_group.rel_commutes) simp
lemma not_modular_group_rel_rho_i [simp]: " z ∼⇩Γ ❙ρ ⟹ ¬z ∼⇩Γ 𝗂"
by (meson modular_group.rel_sym modular_group.rel_trans not_i_equiv_rho)
lemma modular_group_rel_rho_i_cases [case_names rho i neither invalid]:
obtains "z ∼⇩Γ ❙ρ" "¬z ∼⇩Γ 𝗂" | "z ∼⇩Γ 𝗂" "¬z ∼⇩Γ ❙ρ" | "Im z > 0" "¬z ∼⇩Γ ❙ρ" "¬z ∼⇩Γ 𝗂" | "Im z ≤ 0"
by (cases "Im z > 0"; cases "z ∼⇩Γ ❙ρ"; cases "z ∼⇩Γ 𝗂") auto
lemma finite_modgrp_fixpoints:
assumes "Im z > 0"
shows "finite {h∈G. apply_modgrp h z = z}"
proof -
obtain z' where z': "z' ∈ ℛ⇩Γ'" "z ∼⇩Γ z'"
using canonical_point_in_std_fund_region'[of z] assms by blast
then obtain h where h: "z' = apply_modgrp h z"
by (elim modular_group.relE)
have "finite {h. apply_modgrp h z' = z'}"
proof (rule finite_subset)
define S where "S = S_modgrp"
define ST where "ST = S_modgrp * T_modgrp"
show "{h. apply_modgrp h z' = z'} ⊆ {1, -1, S, -S, ST, -ST, ST⇧2, -(ST⇧2)}"
by (cases "z' = 𝗂"; cases "z' = ❙ρ")
(use z'(1) stabiliser_ii_modgrp stabiliser_rho_modgrp modgrp_fixed_point_trivial[of z']
in ‹auto simp: S_def ST_def abs_modgrp_eq_1_iff›)
qed auto
moreover have "bij_betw (λf. h * f * inverse h) {h. apply_modgrp h z = z} {h. apply_modgrp h z' = z'}"
unfolding h by (rule bij_betw_stabiliser_modgrp_apply_modgrp) fact
hence "finite {h. apply_modgrp h z = z} ⟷ finite {h. apply_modgrp h z' = z'}"
by (rule bij_betw_finite)
ultimately have "finite {h. apply_modgrp h z = z}"
by blast
thus ?thesis
by simp
qed
lemma (in modgrp_subgroup) ellorder_modgrp_pos:
assumes "Im z > 0"
shows "ellorder_modgrp G z > 0"
proof -
from assms have "ellorder_modgrp G z = card {h∈G. apply_modgrp h z = z} div card (G ∩ {1, -1})"
by (auto simp: ellorder_modgrp_def)
also have "… ≥ card (G ∩ {1, -1}) div card (G ∩ {1, -1})"
by (intro div_le_mono card_mono finite_modgrp_fixpoints) (use assms in auto)
also have "card (G ∩ {1, -1}) ≥ card {1::modgrp}"
by (rule card_mono) auto
hence "card (G ∩ {1, - 1}) div card (G ∩ {1, - 1}) = 1"
by simp
finally show ?thesis
by simp
qed
subsection ‹Fundamental regions for congruence subgroups›
context hecke_prime_subgroup
begin
definition std_fund_region_cong ("ℛ") where
"ℛ = ℛ⇩Γ ∪ (⋃k∈{0..<p}. (λz. -1 / (z + of_int k)) ` ℛ⇩Γ)"
lemma std_fund_region_cong_altdef:
"ℛ = ℛ⇩Γ ∪ (⋃k∈{0..<p}. apply_modgrp (S_shift_modgrp k) ` ℛ⇩Γ)"
proof -
have "apply_modgrp (S_shift_modgrp k) ` ℛ⇩Γ = (λz. -1 / (z + of_int k)) ` ℛ⇩Γ" for k
unfolding S_shift_modgrp_def
by (intro image_cong refl, subst apply_modgrp_mult) auto
thus ?thesis
by (simp add: std_fund_region_cong_def)
qed
lemma closure_UN_finite: "finite A ⟹ closure (⋃A) = (⋃X∈A. closure X)"
by (induction A rule: finite_induct) auto
sublocale std_region: fundamental_region Γ' ℛ
proof
show "open ℛ"
unfolding std_fund_region_cong_altdef
by (intro open_Un open_UN ballI open_std_fund_region apply_modgrp_open_map) auto
next
show "ℛ ⊆ {z. Im z > 0}"
by (auto simp: std_fund_region_cong_altdef in_std_fund_region_iff)
next
fix x assume "Im x > 0"
then obtain y where y: "y ∈ closure ℛ⇩Γ" "x ∼⇩Γ y"
using std_fund_region.equiv_in_closure by blast
then obtain f where f: "y = apply_modgrp f x" "Im y > 0"
by (auto simp: modular_group.rel_def)
obtain g h where gh: "g ∈ Γ'" "h = 1 ∨ (∃k∈{0..<p}. h = S_shift_modgrp k)" "inverse f = g * h"
using modgrp_decompose'[of "inverse f"] .
have inverse_g_eq: "inverse g = h * f"
using gh(3) by (metis modgrp.assoc modgrp.inverse_unique modgrp.left_inverse)
show "∃y∈closure ℛ. rel x y"
using gh(2)
proof safe
assume "h = 1"
thus ?thesis using y f gh
by (auto simp: std_fund_region_cong_altdef intro!: bexI[of _ y])
next
fix k assume k: "k ∈ {0..<p}" "h = S_shift_modgrp k"
have "apply_modgrp h y ∈ apply_modgrp h ` closure ℛ⇩Γ"
using y by blast
also have "… ⊆ closure (apply_modgrp h ` ℛ⇩Γ)"
by (intro continuous_image_closure_subset[of "{z. Im z > 0}"])
(auto intro!: continuous_intros closure_std_fund_region_Im_pos)
also have "apply_modgrp h y = apply_modgrp (inverse g) x"
unfolding inverse_g_eq using ‹Im x > 0› f by (subst apply_modgrp_mult) auto
finally have "apply_modgrp (inverse g) x ∈ closure (apply_modgrp h ` ℛ⇩Γ)" .
moreover have "rel x (apply_modgrp (inverse g) x)"
using ‹Im x > 0› gh by auto
ultimately show ?thesis
unfolding std_fund_region_cong_altdef using k by (auto simp: closure_UN_finite)
qed
next
fix x y assume xy: "x ∈ ℛ" "y ∈ ℛ" "rel x y"
define ST where "ST = (λk. apply_modgrp (S_shift_modgrp k) :: complex ⇒ complex)"
have 1: False
if xy: "x ∈ ℛ⇩Γ" "y ∈ ℛ⇩Γ" "rel x (ST k y)" and k: "k ∈ {0..<p}" for x y k
proof -
have "x ∼⇩Γ ST k y"
using xy(3) by (rule rel_imp_rel)
hence "x ∼⇩Γ y"
by (auto simp: ST_def)
hence [simp]: "x = y"
using xy(1,2) std_fund_region.unique by blast
with xy(3) have "rel (ST k x) x"
by (simp add: rel_commutes)
then obtain f where f: "f ∈ Γ'" "apply_modgrp f (ST k x) = x" "Im x > 0"
unfolding rel_def by blast
have "modgrp_c ¦f¦ = 1"
proof -
from f have "apply_modgrp (f * S_shift_modgrp k) x = x"
by (subst apply_modgrp_mult) (auto simp: ST_def)
hence "¦f * S_shift_modgrp k¦ = 1"
using xy by (intro std_fund_region_no_fixed_point) auto
hence "¦f¦ = ¦inverse (S_shift_modgrp k)¦"
by (metis abs_modgrp_congs(3) abs_modgrp_eq_1_iff abs_uminus_modgrp minus_minus_modgrp
modgrp.inverse_inverse modgrp.inverse_unique times_modgrp_uminus_right)
also have "modgrp_c (¦inverse (S_shift_modgrp k)¦) = 1"
by (simp add: S_shift_modgrp_def S_modgrp_code shift_modgrp_code inverse_modgrp_code
times_modgrp_code modgrp_c_code abs_modgrp_code)
finally show "modgrp_c ¦f¦ = 1" .
qed
hence "¦modgrp_c f¦ = 1"
by (auto simp: abs_modgrp_altdef split: if_splits)
hence "is_unit (modgrp_c f)"
by auto
moreover have "p dvd modgrp_c f"
using ‹f ∈ Γ'› unfolding subgrp_def modgrps_hecke_altdef by auto
ultimately have "is_unit p"
using dvd_trans by blast
moreover have "¬is_unit p"
using p_prime using not_prime_unit by blast
ultimately show False
by contradiction
qed
have "x ∈ ℛ⇩Γ ∪ (⋃k∈{0..<p}. ST k ` ℛ⇩Γ)" "y ∈ ℛ⇩Γ ∪ (⋃k∈{0..<p}. ST k ` ℛ⇩Γ)"
using xy unfolding ST_def std_fund_region_cong_altdef by blast+
thus "x = y"
proof safe
assume "x ∈ ℛ⇩Γ" "y ∈ ℛ⇩Γ"
thus "x = y"
using ‹rel x y› rel_imp_rel std_fund_region.unique by blast
next
fix k y'
assume "x ∈ ℛ⇩Γ" "k ∈ {0..<p}" "y' ∈ ℛ⇩Γ" "y = ST k y'"
thus "x = ST k y'"
using 1[of x y' k] ‹rel x y› by auto
next
fix k x'
assume "x' ∈ ℛ⇩Γ" "k ∈ {0..<p}" "y ∈ ℛ⇩Γ" "x = ST k x'"
thus "ST k x' = y"
using 1[of y x' k] ‹rel x y› by (auto simp: rel_commutes)
next
fix x' y' :: complex and k1 k2 :: int
assume xy': "x' ∈ ℛ⇩Γ" "y' ∈ ℛ⇩Γ" "x = ST k1 x'" "y = ST k2 y'"
assume k12: "k1 ∈ {0..<p}" "k2 ∈ {0..<p}"
have x': "Im x' > 0"
using xy' by (auto simp: in_std_fund_region_iff)
have "ST k1 x' ∼⇩Γ ST k2 y'"
using xy xy' by (intro rel_imp_rel) auto
hence "x' ∼⇩Γ y'"
by (auto simp: ST_def)
hence [simp]: "x' = y'"
using xy' by (intro std_fund_region.unique)
have "rel (ST k1 x') (ST k2 x')"
using xy xy' by simp
then obtain f where f: "f ∈ Γ'" "apply_modgrp f (ST k1 x') = ST k2 y'"
unfolding rel_def by auto
have "p dvd modgrp_c ¦f¦"
using f by (auto simp: subgrp_def modgrps_hecke_altdef abs_modgrp_altdef)
also have "modgrp_c ¦f¦ = ¦k2 - k1¦"
proof -
note ‹apply_modgrp f (ST k1 x') = ST k2 y'›
also have "apply_modgrp f (ST k1 x') = apply_modgrp (f * S_shift_modgrp k1) x'"
unfolding ST_def using x' by (subst apply_modgrp_mult) auto
finally have "¦f * S_shift_modgrp k1¦ = ¦S_shift_modgrp k2¦"
unfolding ST_def using xy' by (intro std_fund_region_no_fixed_point'[of x']) auto
hence "¦f¦ = ¦S_shift_modgrp k2 * inverse (S_shift_modgrp k1)¦"
by (smt (verit, ccfv_threshold) abs_modgrp_mult_cong modgrp.assoc modgrp.right_inverse
mult_1_right)
also have "… = ¦S_modgrp * shift_modgrp (k2 - k1) * S_modgrp¦"
using shift_modgrp_add[of k2 "-k1"]
by (simp add: S_shift_modgrp_def modgrp.inverse_distrib_swap modgrp.assoc
flip: shift_modgrp_minus)
finally have "¦f¦ = ¦S_modgrp * shift_modgrp (k2 - k1) * S_modgrp¦" .
also have "modgrp_c ¦S_modgrp * shift_modgrp (k2 - k1) * S_modgrp¦ = ¦k2 - k1¦"
by (simp add: S_modgrp_code shift_modgrp_code times_modgrp_code modgrp_c_code abs_modgrp_code)
finally show "modgrp_c ¦f¦ = ¦k2 - k1¦" .
qed
finally have "p dvd ¦k2 - k1¦" .
moreover from k12 have "¦k2 - k1¦ < p"
by auto
ultimately have "k1 = k2"
using zdvd_not_zless[of "¦k2 - k1¦" p] by (cases "k1 = k2") auto
thus "ST k1 x' = ST k2 y'"
by simp
qed
qed
end
bundle modfun_region_notation
begin
notation std_fund_region ("ℛ⇩Γ")
notation modfun_rho ("❙ρ")
end
unbundle no modfun_region_notation
unbundle no modgrp_notation
end