Theory Modular_Fundamental_Region
section ‹Fundamental regions of the modular group›
theory Modular_Fundamental_Region
imports Modular_Group Complex_Lattices "HOL-Library.Real_Mod"
begin
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_eq: "f = shift_modgrp n"
using not_is_singular_modgrpD[of f] by (simp add: n_def a_def b_def)
from xy f have "n = 0"
by (auto simp: std_fund_region_def f_eq)
thus "f = 1"
by (simp add: f_eq)
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 simp
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
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 modgrp.left_cancel modgrp.left_inverse)
qed
lemma equiv_point_in_std_fund_region':
assumes "Im z > 0"
obtains z' where "z ∼⇩Γ z'" "z' ∈ ℛ⇩Γ'"
proof -
obtain z1 where z1: "z ∼⇩Γ z1" "z1 ∈ closure ℛ⇩Γ"
using std_fund_region.equiv_in_closure assms by blast
show ?thesis
proof (cases "z1 ∈ ℛ⇩Γ'")
case True
thus ?thesis
using z1 by (intro that[of z1]) auto
next
case False
hence "z1 ∈ closure ℛ⇩Γ - ℛ⇩Γ'"
using z1 by blast
thus ?thesis
unfolding closure_std_fund_region_minus_std_fund_region'
proof
assume z1': "z1 ∈ {z. cmod z = 1 ∧ 0 < Im z ∧ Re z ∈ {0<..1 / 2}}"
define z2 where "z2 = apply_modgrp S_modgrp z1"
show ?thesis
proof (rule that [of z2])
show "z ∼⇩Γ z2"
unfolding z2_def using z1
by (subst modular_group.rel_apply_modgrp_right_iff) auto
have "-cnj z1 ∈ ℛ⇩Γ'"
using z1' by (auto simp: z2_def in_std_fund_region'_iff)
also have "-cnj z1 = z2"
using z1' by (auto simp: z2_def divide_conv_cnj)
finally show "z2 ∈ ℛ⇩Γ'" .
qed
next
assume z1': "z1 ∈ {z. Re z = 1 / 2 ∧ sqrt 3 / 2 ≤ Im z}"
define z2 where "z2 = apply_modgrp (shift_modgrp (-1)) z1"
show ?thesis
proof (rule that [of z2])
show "z ∼⇩Γ z2"
unfolding z2_def using z1
by (subst modular_group.rel_apply_modgrp_right_iff) auto
have "-cnj z1 ∈ ℛ⇩Γ'"
using z1' z1 by (auto simp: z2_def in_std_fund_region'_iff in_closure_std_fund_region_iff)
also have "-cnj z1 = z2"
using z1' by (auto simp: z2_def complex_eq_iff)
finally show "z2 ∈ ℛ⇩Γ'" .
qed
qed
qed
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 ‹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
hence "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 modgrp.inverse_inverse modgrp.inverse_unique)
moreover 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)
moreover have "¬p dvd 1"
using p_prime using not_prime_unit by blast
ultimately show False
using ‹f ∈ Γ'› unfolding subgrp_def modgrps_cong_altdef by auto
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
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 (metis modgrp.right_inverse modgrp.right_neutral mult.assoc)
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" .
moreover 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)
moreover have "p dvd modgrp_c f"
using f by (auto simp: subgrp_def modgrps_cong_altdef)
ultimately have "p dvd ¦k2 - k1¦"
by simp
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
end