Theory Modular_Group
section ‹Möbius transforms and the modular group›
theory Modular_Group
imports
"HOL-Complex_Analysis.Complex_Analysis"
"HOL-Number_Theory.Number_Theory"
begin
text ‹
An integer ideal is generated by the GCD of its elements (since integers are a principal
ideal domain).
›
lemma ideal_int_conv_Gcd:
fixes A :: "int set"
assumes "0 ∈ A"
assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x + y ∈ A"
assumes "⋀x y. x ∈ A ⟹ x * y ∈ A"
shows "A = {n. Gcd A dvd n}"
proof
show "A ⊆ {n. Gcd A dvd n}"
by auto
next
have "Gcd A ∈ A"
proof (cases "A = {0}")
case False
define x :: int where "x = int (LEAST x. int x ∈ A ∧ x > 0)"
have ex: "∃x. int x ∈ A ∧ x > 0"
proof -
from False obtain x where "x ∈ A - {0}"
using assms(1) by auto
with assms(3)[of x "-1"] show ?thesis
by (intro exI[of _ "if x > 0 then nat x else nat (-x)"]) auto
qed
have x: "x ∈ A ∧ x > 0"
unfolding x_def using LeastI_ex[OF ex] by auto
have x': "x ≤ y" if y: "y ∈ A" "y > 0" for y
using y unfolding x_def
by (metis of_nat_le_iff wellorder_Least_lemma(2) zero_less_imp_eq_int)
have "x dvd Gcd A"
proof (rule Gcd_greatest)
fix y assume y: "y ∈ A"
have "y = (y div x) * x + (y mod x)"
by simp
have "y + x * (-1) * (y div x) ∈ A"
by (intro assms) (use x y in auto)
also have "y + x * (-1) * (y div x) = y mod x"
by (simp add: algebra_simps)
finally have "y mod x ∈ A" .
moreover have "y mod x ≥ 0" "y mod x < x"
using x by simp_all
ultimately have "y mod x = 0"
using x'[of "y mod x"] by (cases "y mod x = 0") auto
thus "x dvd y"
by presburger
qed
thus "Gcd A ∈ A"
using assms(3) x by (auto elim!: dvdE)
qed auto
thus "{n. Gcd A dvd n} ⊆ A"
by (auto elim!: dvdE intro!: assms)
qed
lemma Gcd_gcd_closed_set_int:
fixes A :: "int set"
assumes "0 ∈ A"
assumes "⋀x y. x ∈ A ⟹ y ∈ A ⟹ gcd x y ∈ A"
assumes "⋀x y. x ∈ A ⟹ x * y ∈ A"
shows "A = {n. Gcd A dvd n}"
proof (rule ideal_int_conv_Gcd)
fix x y assume "x ∈ A" "y ∈ A"
hence "gcd x y * ((x + y) div gcd x y) ∈ A"
by (intro assms)
also have "gcd x y * ((x + y) div gcd x y) = x + y"
by (subst dvd_mult_div_cancel) auto
finally show "x + y ∈ A" .
qed (use assms in auto)
subsection ‹Basic properties of Möbius transforms›
lemma moebius_uminus [simp]: "moebius (-a) (-b) (-c) (-d) = moebius a b c d"
by (simp add: fun_eq_iff moebius_def divide_simps) (simp add: algebra_simps add_eq_0_iff2)
lemma moebius_uminus': "moebius (-a) b c d = moebius a (-b) (-c) (-d)"
by (simp add: fun_eq_iff moebius_def divide_simps) (simp add: algebra_simps add_eq_0_iff2)
lemma moebius_diff_eq:
fixes a b c d :: "'a :: field"
defines "f ≡ moebius a b c d"
assumes *: "c = 0 ∨ z ≠ -d / c ∧ w ≠ -d / c"
shows "f w - f z = (a * d - b * c) / ((c * w + d) * (c * z + d)) * (w - z)"
using * by (auto simp: moebius_def divide_simps f_def add_eq_0_iff)
(auto simp: algebra_simps)
lemma moebius_shift:
"moebius a b c d (z + of_int n) = moebius a (a * of_int n + b) c (c * of_int n + d) z"
by (simp add: moebius_def algebra_simps)
lemma moebius_eq_shift: "moebius 1 (of_int n) 0 1 z = z + of_int n"
by (simp add: moebius_def)
lemma moebius_S:
assumes "a * d - b * c ≠ 0" "z ≠ 0"
shows "moebius a b c d (-(1 / z)) = moebius b (- a) d (- c) (z :: 'a :: field)"
using assms by (auto simp: divide_simps moebius_def)
lemma moebius_eq_S: "moebius 0 1 (-1) 0 z = -1 / z"
by (simp add: moebius_def)
lemma continuous_on_moebius [continuous_intros]:
fixes a b c d :: "'a :: real_normed_field"
assumes "c ≠ 0 ∨ d ≠ 0" "c = 0 ∨ -d / c ∉ A"
shows "continuous_on A (moebius a b c d)"
unfolding moebius_def
by (intro continuous_intros) (use assms in ‹auto simp: add_eq_0_iff›)
lemma continuous_on_moebius' [continuous_intros]:
fixes a b c d :: "'a :: real_normed_field"
assumes "continuous_on A f" "c ≠ 0 ∨ d ≠ 0" "⋀z. z ∈ A ⟹ c = 0 ∨ f z ≠ -d / c"
shows "continuous_on A (λx. moebius a b c d (f x))"
proof -
have "continuous_on A (moebius a b c d ∘ f)" using assms
by (intro continuous_on_compose assms continuous_on_moebius) force+
thus ?thesis
by (simp add: o_def)
qed
lemma holomorphic_on_moebius [holomorphic_intros]:
assumes "c ≠ 0 ∨ d ≠ 0" "c = 0 ∨ -d / c ∉ A"
shows "(moebius a b c d) holomorphic_on A"
unfolding moebius_def
by (intro holomorphic_intros) (use assms in ‹auto simp: add_eq_0_iff›)
lemma holomorphic_on_moebius' [holomorphic_intros]:
assumes "f holomorphic_on A" "c ≠ 0 ∨ d ≠ 0" "⋀z. z ∈ A ⟹ c = 0 ∨ f z ≠ -d / c"
shows "(λx. moebius a b c d (f x)) holomorphic_on A"
proof -
have "(moebius a b c d ∘ f) holomorphic_on A" using assms
by (intro holomorphic_on_compose assms holomorphic_on_moebius) force+
thus ?thesis
by (simp add: o_def)
qed
lemma analytic_on_moebius [analytic_intros]:
assumes "c ≠ 0 ∨ d ≠ 0" "c = 0 ∨ -d / c ∉ A"
shows "(moebius a b c d) analytic_on A"
unfolding moebius_def
by (intro analytic_intros) (use assms in ‹auto simp: add_eq_0_iff›)
lemma analytic_on_moebius' [analytic_intros]:
assumes "f analytic_on A" "c ≠ 0 ∨ d ≠ 0" "⋀z. z ∈ A ⟹ c = 0 ∨ f z ≠ -d / c"
shows "(λx. moebius a b c d (f x)) analytic_on A"
proof -
have "(moebius a b c d ∘ f) analytic_on A" using assms
by (intro analytic_on_compose assms analytic_on_moebius) force+
thus ?thesis
by (simp add: o_def)
qed
lemma moebius_has_field_derivative:
assumes "c = 0 ∨ x ≠ -d / c" "c ≠ 0 ∨ d ≠ 0"
shows "(moebius a b c d has_field_derivative (a * d - b * c) / (c * x + d) ^ 2) (at x within A)"
unfolding moebius_def
apply (rule derivative_eq_intros refl)+
using assms
apply (auto simp: divide_simps add_eq_0_iff power2_eq_square split: if_splits)
apply (auto simp: algebra_simps)?
done
subsection ‹Unimodular M\"obius transforms›
text ‹
A unimodular M\"obius transform has integer coefficients and determinant ‹±1›.
›
locale unimodular_moebius_transform =
fixes a b c d :: int
assumes unimodular: "a * d - b * c = 1"
begin
definition φ :: "complex ⇒ complex" where
"φ = moebius (of_int a) (of_int b) (of_int c) (of_int d)"
lemma cnj_φ: "φ (cnj z) = cnj (φ z)"
by (simp add: moebius_def φ_def)
lemma Im_transform:
"Im (φ z) = Im z / norm (of_int c * z + of_int d) ^ 2"
proof -
have "Im (φ z) = Im z * of_int (a * d - b * c) /
((real_of_int c * Re z + real_of_int d)⇧2 + (real_of_int c * Im z)⇧2)"
by (simp add: φ_def moebius_def Im_divide algebra_simps)
also have "a * d - b * c = 1"
using unimodular by simp
also have "((real_of_int c * Re z + real_of_int d)⇧2 + (real_of_int c * Im z)⇧2) =
norm (of_int c * z + of_int d) ^ 2"
unfolding cmod_power2 by (simp add: power2_eq_square algebra_simps)
finally show ?thesis
by simp
qed
lemma Im_transform_pos_aux:
assumes "Im z ≠ 0"
shows "of_int c * z + of_int d ≠ 0"
proof (cases "c = 0")
case False
hence "Im (of_int c * z + of_int d) ≠ 0"
using assms by auto
moreover have "Im 0 = 0"
by simp
ultimately show ?thesis
by metis
next
case True
thus ?thesis using unimodular
by auto
qed
lemma Im_transform_pos: "Im z > 0 ⟹ Im (φ z) > 0"
using Im_transform_pos_aux[of z] by (auto simp: Im_transform)
lemma Im_transform_neg: "Im z < 0 ⟹ Im (φ z) < 0"
using Im_transform_pos[of "cnj z"] by (simp add: cnj_φ)
lemma Im_transform_zero_iff [simp]: "Im (φ z) = 0 ⟷ Im z = 0"
using Im_transform_pos_aux[of z] by (auto simp: Im_transform)
lemma Im_transform_pos_iff [simp]: "Im (φ z) > 0 ⟷ Im z > 0"
using Im_transform_pos[of z] Im_transform_neg[of z] Im_transform_zero_iff[of z]
by (cases "Im z" "0 :: real" rule: linorder_cases) (auto simp del: Im_transform_zero_iff)
lemma Im_transform_neg_iff [simp]: "Im (φ z) < 0 ⟷ Im z < 0"
using Im_transform_pos_iff[of "cnj z"] by (simp add: cnj_φ)
lemma Im_transform_nonneg_iff [simp]: "Im (φ z) ≥ 0 ⟷ Im z ≥ 0"
using Im_transform_neg_iff[of z] by linarith
lemma Im_transform_nonpos_iff [simp]: "Im (φ z) ≤ 0 ⟷ Im z ≤ 0"
using Im_transform_pos_iff[of z] by linarith
lemma transform_in_reals_iff [simp]: "φ z ∈ ℝ ⟷ z ∈ ℝ"
using Im_transform_zero_iff[of z] by (auto simp: complex_is_Real_iff)
end
lemma Im_one_over_neg_iff [simp]: "Im (1 / z) < 0 ⟷ Im z > 0"
proof -
interpret unimodular_moebius_transform 0 1 "-1" 0
by standard auto
show ?thesis
using Im_transform_pos_iff[of z] by (simp add: φ_def moebius_def)
qed
locale inverse_unimodular_moebius_transform = unimodular_moebius_transform
begin
sublocale inv: unimodular_moebius_transform d "-b" "-c" a
by unfold_locales (use unimodular in Groebner_Basis.algebra)
lemma inv_φ:
assumes "of_int c * z + of_int d ≠ 0"
shows "inv.φ (φ z) = z"
using unimodular assms
unfolding inv.φ_def φ_def of_int_minus
by (subst moebius_inverse) (auto simp flip: of_int_mult)
lemma inv_φ':
assumes "of_int c * z - of_int a ≠ 0"
shows "φ (inv.φ z) = z"
using unimodular assms
unfolding inv.φ_def φ_def of_int_minus
by (subst moebius_inverse') (auto simp flip: of_int_mult)
end
subsection ‹The modular group›
subsubsection ‹Definition›
text ‹
We define the modular group as all integer tuples $(a,b,c,d)$ with $ad-bc = 1$.
›
typedef modgrp = "{(a,b,c,d::int). a * d - b * c = 1}"
by (rule exI[of _ "(1,0,0,1)"]) auto
setup_lifting type_definition_modgrp
instantiation modgrp :: one
begin
lift_definition one_modgrp :: modgrp is "(1, 0, 0, 1)"
by auto
instance ..
end
instantiation modgrp :: uminus
begin
lift_definition uminus_modgrp :: "modgrp ⇒ modgrp" is "λ(a,b,c,d). (-a, -b, -c, -d)"
by auto
instance ..
end
lemma minus_minus_modgrp [simp]: "-(-f :: modgrp) = f"
by transfer auto
instantiation modgrp :: sgn
begin
lift_definition sgn_modgrp :: "modgrp ⇒ modgrp"
is "λ(a,b,c,d). if c < 0 ∨ c = 0 ∧ d < 0 then (-1,0,0,-1) else (1,0,0,1)"
by (auto split: if_splits)
instance ..
end
instantiation modgrp :: abs
begin
lift_definition abs_modgrp :: "modgrp ⇒ modgrp"
is "λ(a,b,c,d). if c < 0 ∨ c = 0 ∧ d < 0 then (-a,-b,-c,-d) else (a,b,c,d)"
by (auto split: if_splits)
instance ..
end
instantiation modgrp :: times
begin
lift_definition times_modgrp :: "modgrp ⇒ modgrp ⇒ modgrp"
is "λ(a,b,c,d) (a',b',c',d'). (a * a' + b * c', a * b' + b * d', c * a' + d * c', c * b' + d * d')"
by (auto simp: algebra_simps)
instance ..
end
instantiation modgrp :: inverse
begin
lift_definition inverse_modgrp :: "modgrp ⇒ modgrp"
is "λ(a, b, c, d). (d, -b, -c, a)"
by (auto simp: algebra_simps)
definition divide_modgrp :: "modgrp ⇒ modgrp ⇒ modgrp" where
"divide_modgrp x y = x * inverse y"
instance ..
end
interpretation modgrp: Groups.group "(*) :: modgrp ⇒ _" 1 inverse
proof
show "a * b * c = a * (b * c :: modgrp)" for a b c
by transfer (auto simp: algebra_simps)
next
show "1 * a = a" for a :: modgrp
by transfer (auto simp: algebra_simps)
next
show "inverse a * a = 1" for a :: modgrp
by transfer (auto simp: algebra_simps)
qed
instance modgrp :: monoid_mult
by standard (simp_all add: modgrp.assoc)
lemma inverse_power_modgrp: "inverse (x ^ n :: modgrp) = inverse x ^ n"
by (induction n) (simp_all add: algebra_simps modgrp.inverse_distrib_swap power_commuting_commutes)
lemma inverse_mult_assoc1_modgrp [simp]: "inverse f * (f * g) = (g :: modgrp)"
by (subst mult.assoc [symmetric]) auto
lemma inverse_mult_assoc2_modgrp [simp]: "f * (inverse f * g) = (g :: modgrp)"
by (subst mult.assoc [symmetric]) auto
lemma abs_modgrp_conv_sgn: "abs f = sgn f * (f :: modgrp)"
by transfer auto
lemma modgrp_conv_sgn_abs: "f = sgn f * (abs f :: modgrp)"
by transfer auto
lemma sgn_1_modgrp [simp]: "sgn (1 :: modgrp) = 1"
by transfer auto
lemma sgn_uminus_modgrp [simp]: "sgn (-f :: modgrp) = -sgn f"
by transfer (auto simp: zmult_eq_1_iff)
lemma sgn_sgn_modgrp [simp]: "sgn (sgn f) = sgn (f :: modgrp)"
by transfer auto
lemma sgn_abs_modgrp [simp]: "sgn (abs f) = (1 :: modgrp)"
by transfer auto
lemma abs_1_modgrp [simp]: "abs (1 :: modgrp) = 1"
by transfer auto
lemma abs_uminus_modgrp [simp]: "abs (-f :: modgrp) = abs f"
by transfer (auto simp: zmult_eq_1_iff)
lemma abs_sgn_modgrp [simp]: "abs (sgn f) = (1 :: modgrp)"
by transfer auto
lemma abs_abs_modgrp [simp]: "abs (abs f) = abs (f :: modgrp)"
by transfer auto
lemma minus_modgrp_neq_self [simp]: "-f ≠ (f :: modgrp)" "f ≠ -f"
by (transfer; force)+
subsubsection ‹Basic operations›
text ‹Application to a field›
lift_definition apply_modgrp :: "modgrp ⇒ 'a :: field ⇒ 'a" is
"λ(a,b,c,d). moebius (of_int a) (of_int b) (of_int c) (of_int d)" .
text ‹The shift operation $z \mapsto z + n$›
lift_definition shift_modgrp :: "int ⇒ modgrp" is "λn. (1, n, 0, 1)"
by auto
text ‹The shift operation $z \mapsto z + 1$›
lift_definition T_modgrp :: modgrp is "(1, 1, 0, 1)"
by auto
text ‹The operation $z \mapsto -\frac{1}{z}$›
lift_definition S_modgrp :: modgrp is "(0, -1, 1, 0)"
by auto
text ‹Whether or not the transformation has a pole in the complex plane›
lift_definition is_singular_modgrp :: "modgrp ⇒ bool" is "λ(a,b,c,d). c ≠ 0" .
text ‹The position of the transformation's pole in the complex plane (if it has one)›
lift_definition pole_modgrp :: "modgrp ⇒ 'a :: field" is "λ(a,b,c,d). -of_int d / of_int c" .
lemma pole_modgrp_in_Rats: "pole_modgrp f ∈ (ℚ :: 'a :: real_field set)"
by transfer auto
lemma pole_modgrp_in_Reals: "pole_modgrp f ∈ (ℝ :: 'a :: real_field set)"
by transfer auto
lemma Im_pole_modgrp [simp]: "Im (pole_modgrp f) = 0"
by transfer auto
text ‹
The complex number to which complex infinity is mapped by the transformation.
This is undefined if the transformation maps complex infinity to itself.
›
lift_definition pole_image_modgrp :: "modgrp ⇒ 'a :: field" is "λ(a,b,c,d). of_int a / of_int c" .
lemma Im_pole_image_modgrp [simp]: "Im (pole_image_modgrp f) = 0"
by transfer auto
text ‹
The normalised coefficients of the transformation. The convention that is chosen is that
‹c› is always non-negative, and if ‹c› is zero then ‹d› is positive.
›
lift_definition modgrp_a :: "modgrp ⇒ int" is "λ(a,b,c,d). a" .
lift_definition modgrp_b :: "modgrp ⇒ int" is "λ(a,b,c,d). b" .
lift_definition modgrp_c :: "modgrp ⇒ int" is "λ(a,b,c,d). c" .
lift_definition modgrp_d :: "modgrp ⇒ int" is "λ(a,b,c,d). d" .
lemma modgrp_abcd_S [simp]:
"modgrp_a S_modgrp = 0" "modgrp_b S_modgrp = -1" "modgrp_c S_modgrp = 1" "modgrp_d S_modgrp = 0"
by (transfer; simp)+
lemma modgrp_abcd_T [simp]:
"modgrp_a T_modgrp = 1" "modgrp_b T_modgrp = 1" "modgrp_c T_modgrp = 0" "modgrp_d T_modgrp = 1"
by (transfer; simp)+
lemma modgrp_abcd_shift [simp]:
"modgrp_a (shift_modgrp n) = 1" "modgrp_b (shift_modgrp n) = n"
"modgrp_c (shift_modgrp n) = 0" "modgrp_d (shift_modgrp n) = 1"
by (transfer; simp)+
lemma modgrp_c_shift_left [simp]:
"modgrp_c (shift_modgrp n * f) = modgrp_c f"
by transfer auto
lemma modgrp_d_shift_left [simp]:
"modgrp_d (shift_modgrp n * f) = modgrp_d f"
by transfer auto
lemma modgrp_abcd_det: "modgrp_a x * modgrp_d x - modgrp_b x * modgrp_c x = 1"
by transfer auto
lemma modgrp_a_nz_or_b_nz: "modgrp_a x ≠ 0 ∨ modgrp_b x ≠ 0"
by transfer auto
lemma modgrp_c_nz_or_d_nz: "modgrp_c x ≠ 0 ∨ modgrp_d x ≠ 0"
by transfer auto
lemma apply_modgrp_altdef:
"(apply_modgrp x :: 'a :: field ⇒ _) =
moebius (of_int (modgrp_a x)) (of_int (modgrp_b x)) (of_int (modgrp_c x)) (of_int (modgrp_d x))"
proof (transfer, goal_cases)
case (1 x)
thus ?case
by (auto simp: case_prod_unfold moebius_uminus')
qed
lemma sgn_modgrp_altdef:
"sgn f = (if modgrp_c f < 0 ∨ modgrp_c f = 0 ∧ modgrp_d f < 0 then -1 else 1)"
by transfer auto
lemma abs_modgrp_altdef:
"abs f = (if modgrp_c f < 0 ∨ modgrp_c f = 0 ∧ modgrp_d f < 0 then -f else f)"
by transfer auto
lemma abs_eq_modgrpE:
assumes "abs f = (g :: modgrp)"
obtains "f = g" | "f = -g"
using assms that by (auto simp: abs_modgrp_altdef split: if_splits)
text ‹
Converting a quadruple of numbers into an element of the modular group.
›
lift_definition modgrp :: "int ⇒ int ⇒ int ⇒ int ⇒ modgrp" is
"λa b c d. if a * d - b * c = 1 then (a, b, c, d) else (1, 0, 0, 1)"
by transfer auto
lemma modgrp_eq_iff:
"f = g ⟷ modgrp_a f = modgrp_a g ∧ modgrp_b f = modgrp_b g ∧
modgrp_c f = modgrp_c g ∧ modgrp_d f = modgrp_d g"
by transfer auto
lemma modgrp_wrong: "a * d - b * c ≠ 1 ⟹ modgrp a b c d = 1"
by transfer auto
lemma modgrp_abcd [simp]: "modgrp (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x) = x"
by transfer auto
lemma
assumes "a * d - b * c = 1"
shows modgrp_a_modgrp: "modgrp_a (modgrp a b c d) = a"
and modgrp_b_modgrp: "modgrp_b (modgrp a b c d) = b"
and modgrp_c_modgrp: "modgrp_c (modgrp a b c d) = c"
and modgrp_d_modgrp: "modgrp_d (modgrp a b c d) = d"
using assms by (transfer; simp; fail)+
lemmas modgrp_abcd_modgrp = modgrp_a_modgrp modgrp_b_modgrp modgrp_c_modgrp modgrp_d_modgrp
subsubsection ‹Basic properties›
lemma continuous_on_apply_modgrp [continuous_intros]:
fixes g :: "'a :: topological_space ⇒ 'b :: real_normed_field"
assumes "continuous_on A g" "⋀z. z ∈ A ⟹ ¬is_singular_modgrp f ∨ g z ≠ pole_modgrp f"
shows "continuous_on A (λz. apply_modgrp f (g z))"
using assms
by transfer (auto intro!: continuous_intros)
lemma holomorphic_on_apply_modgrp [holomorphic_intros]:
assumes "g holomorphic_on A" "⋀z. z ∈ A ⟹ ¬is_singular_modgrp f ∨ g z ≠ pole_modgrp f"
shows "(λz. apply_modgrp f (g z)) holomorphic_on A"
using assms
by transfer (auto intro!: holomorphic_intros)
lemma analytic_on_apply_modgrp [analytic_intros]:
assumes "g analytic_on A" "⋀z. z ∈ A ⟹ ¬is_singular_modgrp f ∨ g z ≠ pole_modgrp f"
shows "(λz. apply_modgrp f (g z)) analytic_on A"
using assms
by transfer (auto intro!: analytic_intros)
lemma isCont_apply_modgrp [continuous_intros]:
fixes z :: "'a :: real_normed_field"
assumes "¬is_singular_modgrp f ∨ z ≠ pole_modgrp f"
shows "isCont (apply_modgrp f) z"
proof -
define S where "S = (if is_singular_modgrp f then -{pole_modgrp f} else (UNIV :: 'a set))"
have "continuous_on S (apply_modgrp f)"
unfolding S_def by (intro continuous_intros) auto
moreover have "open S" "z ∈ S"
using assms by (auto simp: S_def)
ultimately show ?thesis
using continuous_on_eq_continuous_at by blast
qed
lemmas tendsto_apply_modgrp [tendsto_intros] = isCont_tendsto_compose[OF isCont_apply_modgrp]
lift_definition diff_scale_factor_modgrp :: "modgrp ⇒ 'a :: field ⇒ 'a ⇒ 'a" is
"λ(a,b,c,d) w z. (of_int c * w + of_int d) * (of_int c * z + of_int d)" .
lemma diff_scale_factor_modgrp_commutes:
"diff_scale_factor_modgrp f w z = diff_scale_factor_modgrp f z w"
by transfer (simp add: case_prod_unfold)
lemma diff_scale_factor_modgrp_zero_iff:
fixes w z :: "'a :: field_char_0"
shows "diff_scale_factor_modgrp f w z = 0 ⟷ is_singular_modgrp f ∧ pole_modgrp f ∈ {w, z}"
by transfer
(auto simp: case_prod_unfold divide_simps add_eq_0_iff mult.commute
minus_equation_iff[of "of_int x" for x])
lemma apply_modgrp_diff_eq:
fixes g :: modgrp
defines "f ≡ apply_modgrp g"
assumes *: "¬is_singular_modgrp g ∨ pole_modgrp g ∉ {w, z}"
shows "f w - f z = (w - z) / diff_scale_factor_modgrp g w z"
unfolding f_def using *
by transfer
(auto simp: moebius_diff_eq zmult_eq_1_iff simp flip: of_int_diff of_int_mult split: if_splits)
lemma norm_modgrp_dividend_ge:
fixes z :: complex
shows "norm (of_int c * z + of_int d) ≥ ¦c * Im z¦"
proof -
define x y where "x = Re z" and "y = Im z"
have z_eq: "z = Complex x y"
by (simp add: x_def y_def)
have "(real_of_int c * y) ^ 2 ≤ (real_of_int c * x + real_of_int d) ^ 2 + (real_of_int c * y) ^ 2"
by simp
also have "… = norm (of_int c * z + of_int d) ^ 2"
by (simp add: cmod_power2 x_def y_def)
finally show "norm (of_int c * z + of_int d) ≥ ¦c * y¦"
by (metis abs_le_square_iff abs_norm_cancel)
qed
lemma diff_scale_factor_modgrp_altdef:
fixes g :: modgrp
defines "c ≡ modgrp_c g" and "d ≡ modgrp_d g"
shows "diff_scale_factor_modgrp g w z = (of_int c * w + of_int d) * (of_int c * z + of_int d)"
unfolding c_def d_def by transfer (auto simp: algebra_simps)
lemma norm_diff_scale_factor_modgrp_ge_complex:
fixes w z :: complex
assumes "w ≠ z"
shows "norm (diff_scale_factor_modgrp g w z) ≥ of_int (modgrp_c g) ^ 2 * ¦Im w * Im z¦"
proof -
have "norm (diff_scale_factor_modgrp g w z) ≥
¦of_int (modgrp_c g) * Im w¦ * ¦of_int (modgrp_c g) * Im z¦"
unfolding diff_scale_factor_modgrp_altdef norm_mult
by (intro mult_mono norm_modgrp_dividend_ge) auto
thus ?thesis
by (simp add: algebra_simps abs_mult power2_eq_square)
qed
lemma apply_uminus_modgrp [simp]: "apply_modgrp (-f) z = apply_modgrp f z"
by transfer auto
lemma apply_shift_modgrp [simp]: "apply_modgrp (shift_modgrp n) z = z + of_int n"
by transfer (auto simp: moebius_def)
lemma apply_modgrp_T [simp]: "apply_modgrp T_modgrp z = z + 1"
by transfer (auto simp: moebius_def)
lemma apply_modgrp_S [simp]: "apply_modgrp S_modgrp z = -1 / z"
by transfer (auto simp: moebius_def)
lemma apply_modgrp_1 [simp]: "apply_modgrp 1 z = z"
by transfer (auto simp: moebius_def)
lemma apply_modgrp_mult_aux:
fixes z :: "'a :: field_char_0"
assumes ns: "c' = 0 ∨ z ≠ -d' / c'"
assumes det: "a * d - b * c = 1" "a' * d' - b' * c' = 1"
shows "moebius a b c d (moebius a' b' c' d' z) =
moebius (a * a' + b * c') (a * b' + b * d')
(c * a' + d * c') (c * b' + d * d') z"
proof -
have det': "c ≠ 0 ∨ d ≠ 0" "c' ≠ 0 ∨ d' ≠ 0"
using det by auto
from assms have nz: "c' * z + d' ≠ 0"
by (auto simp add: divide_simps add_eq_0_iff split: if_splits)
show ?thesis using det nz
by (simp add: moebius_def divide_simps) (auto simp: algebra_simps)
qed
lemma apply_modgrp_mult:
fixes z :: "'a :: field_char_0"
assumes "¬is_singular_modgrp y ∨ z ≠ pole_modgrp y"
shows "apply_modgrp (x * y) z = apply_modgrp x (apply_modgrp y z)"
using assms
proof (transfer, goal_cases)
case (1 y z x)
obtain a b c d where [simp]: "x = (a, b, c, d)"
using prod_cases4 by blast
obtain a' b' c' d' where [simp]: "y = (a', b', c', d')"
using prod_cases4 by blast
show ?case
using apply_modgrp_mult_aux[of "of_int c'" z "of_int d'" "of_int a" "of_int d"
"of_int b" "of_int c" "of_int a'" "of_int b'"] 1
by (simp flip: of_int_mult of_int_add of_int_diff of_int_minus)
qed
lemma apply_modgrp_eq_apply_modgrp_iff:
assumes "Im w > 0" "Im z > 0"
shows "apply_modgrp f w = apply_modgrp g z ⟷ apply_modgrp (inverse g * f) w = z"
proof
assume "apply_modgrp f w = apply_modgrp g z"
hence "apply_modgrp (inverse g) (apply_modgrp f w) = apply_modgrp (inverse g) (apply_modgrp g z)"
by (rule arg_cong)
thus "apply_modgrp (inverse g * f) w = z"
using assms by (subst (asm) (1 2) apply_modgrp_mult [symmetric]) auto
next
assume "apply_modgrp (inverse g * f) w = z"
hence "apply_modgrp g (apply_modgrp (inverse g * f) w) = apply_modgrp g z"
by (rule arg_cong)
thus "apply_modgrp f w = apply_modgrp g z"
using assms by (subst (asm) apply_modgrp_mult [symmetric]) auto
qed
lemma apply_modgrp_sgn [simp]: "apply_modgrp (sgn f) = (λx. x)"
by (auto simp: sgn_modgrp_altdef)
lemma apply_modgrp_abs [simp]: "apply_modgrp (abs f) = apply_modgrp f"
by (auto simp: abs_modgrp_altdef)
lemma is_singular_modgrp_altdef: "is_singular_modgrp x ⟷ modgrp_c x ≠ 0"
by transfer (auto split: if_splits)
lemma not_is_singular_modgrpD:
assumes "¬is_singular_modgrp x"
shows "abs x = shift_modgrp (sgn (modgrp_a x) * modgrp_b x)"
using assms
proof (transfer, goal_cases)
case (1 x)
obtain a b c d where [simp]: "x = (a, b, c, d)"
using prod_cases4 by blast
from 1 have [simp]: "c = 0"
by auto
from 1 have "a = 1 ∧ d = 1 ∨ a = -1 ∧ d = -1"
by (auto simp: zmult_eq_1_iff)
thus ?case
by auto
qed
lemma is_singular_modgrp_inverse [simp]: "is_singular_modgrp (inverse x) ⟷ is_singular_modgrp x"
by transfer auto
lemma is_singular_modgrp_S_left_iff [simp]: "is_singular_modgrp (S_modgrp * f) ⟷ modgrp_a f ≠ 0"
by transfer (auto split: if_splits)
lemma is_singular_modgrp_S_right_iff [simp]: "is_singular_modgrp (f * S_modgrp) ⟷ modgrp_d f ≠ 0"
by transfer (auto split: if_splits)
lemma is_singular_modgrp_T_left_iff [simp]:
"is_singular_modgrp (T_modgrp * f) ⟷ is_singular_modgrp f"
by transfer (auto split: if_splits)
lemma is_singular_modgrp_T_right_iff [simp]:
"is_singular_modgrp (f * T_modgrp) ⟷ is_singular_modgrp f"
by transfer (auto split: if_splits)
lemma is_singular_modgrp_shift_left_iff [simp]:
"is_singular_modgrp (shift_modgrp n * f) ⟷ is_singular_modgrp f"
by transfer (auto split: if_splits)
lemma is_singular_modgrp_shift_right_iff [simp]:
"is_singular_modgrp (f * shift_modgrp n) ⟷ is_singular_modgrp f"
by transfer (auto split: if_splits)
lemma pole_modgrp_inverse [simp]: "pole_modgrp (inverse x) = pole_image_modgrp x"
by transfer auto
lemma pole_image_modgrp_inverse [simp]: "pole_image_modgrp (inverse x) = pole_modgrp x"
by transfer auto
lemma pole_image_modgrp_in_Reals: "pole_image_modgrp x ∈ (ℝ :: 'a :: {real_field, field} set)"
by transfer (auto intro!: Reals_divide)
lemma apply_modgrp_inverse_eqI:
fixes x y :: "'a :: field_char_0"
assumes "¬is_singular_modgrp f ∨ y ≠ pole_modgrp f" "apply_modgrp f y = x"
shows "apply_modgrp (inverse f) x = y"
proof -
have "apply_modgrp (inverse f) x = apply_modgrp (inverse f * f) y"
using assms by (subst apply_modgrp_mult) auto
also have "… = y"
by simp
finally show ?thesis .
qed
lemma apply_modgrp_eq_iff [simp]:
fixes x y :: "'a :: field_char_0"
assumes "¬is_singular_modgrp f ∨ x ≠ pole_modgrp f ∧ y ≠ pole_modgrp f"
shows "apply_modgrp f x = apply_modgrp f y ⟷ x = y"
using assms by (metis apply_modgrp_inverse_eqI)
lemma is_singular_modgrp_times_aux:
assumes det: "a * d - b * c = 1" "a' * d' - b' * (c' :: int) = 1"
shows "(c * a' + d * c' ≠ 0) ⟷ ((c = 0 ⟶ c' ≠ 0) ∧ (c = 0 ∨ c' = 0 ∨ -d * c' ≠ a' * c))"
using assms by Groebner_Basis.algebra
lemma is_singular_modgrp_times_iff:
"is_singular_modgrp (x * y) ⟷
(is_singular_modgrp x ∨ is_singular_modgrp y) ∧
(¬is_singular_modgrp x ∨ ¬is_singular_modgrp y ∨ pole_modgrp x ≠ (pole_image_modgrp y :: real))"
proof (transfer, goal_cases)
case (1 x y)
obtain a b c d where [simp]: "x = (a, b, c, d)"
using prod_cases4 by blast
obtain a' b' c' d' where [simp]: "y = (a', b', c', d')"
using prod_cases4 by blast
show ?case
using is_singular_modgrp_times_aux[of a d b c a' d' b' c'] 1
by (auto simp: field_simps simp flip: of_int_mult of_int_add of_int_minus of_int_diff)
qed
lemma is_singular_modgrp_uminus_iff [simp]: "is_singular_modgrp (-f) ⟷ is_singular_modgrp f"
by transfer auto
lemma times_modgrp_uminus_left [simp]: "(-f :: modgrp) * g = -(f * g)"
by transfer auto
lemma times_modgrp_uminus_right [simp]: "(f :: modgrp) * (-g) = -(f * g)"
by transfer auto
lemma inverse_modgrp_uminus [simp]: "inverse (-f :: modgrp) = -inverse f"
by transfer auto
lemma shift_modgrp_1: "shift_modgrp 1 = T_modgrp"
by transfer auto
lemma shift_modgrp_eq_iff: "shift_modgrp n = shift_modgrp m ⟷ n = m"
by transfer auto
lemma shift_modgrp_neq_S [simp]: "shift_modgrp n ≠ S_modgrp"
by transfer auto
lemma S_neq_shift_modgrp [simp]: "S_modgrp ≠ shift_modgrp n"
by transfer auto
lemma shift_modgrp_eq_T_iff [simp]: "shift_modgrp n = T_modgrp ⟷ n = 1"
by transfer auto
lemma T_eq_shift_modgrp_iff [simp]: "T_modgrp = shift_modgrp n ⟷ n = 1"
by transfer auto
lemma shift_modgrp_0 [simp]: "shift_modgrp 0 = 1"
by transfer auto
lemma shift_modgrp_add: "shift_modgrp (m + n) = shift_modgrp m * shift_modgrp n"
by transfer auto
lemma shift_modgrp_minus: "shift_modgrp (-m) = inverse (shift_modgrp m)"
proof -
have "1 = shift_modgrp (m + (-m))"
by simp
also have "shift_modgrp (m + (-m)) = shift_modgrp m * shift_modgrp (-m)"
by (subst shift_modgrp_add) auto
finally show ?thesis
by (simp add: modgrp.inverse_unique)
qed
lemma shift_modgrp_power: "shift_modgrp n ^ m = shift_modgrp (n * m)"
by (induction m) (auto simp: algebra_simps shift_modgrp_add)
lemma shift_modgrp_power_int: "shift_modgrp n powi m = shift_modgrp (n * m)"
by (cases "m ≥ 0")
(auto simp: power_int_def shift_modgrp_power simp flip: shift_modgrp_minus)
lemma shift_shift_modgrp: "shift_modgrp n * (shift_modgrp m * x) = shift_modgrp (n + m) * x"
by (simp add: mult.assoc shift_modgrp_add)
lemma shift_modgrp_conv_T_power: "shift_modgrp n = T_modgrp powi n"
by (simp flip: shift_modgrp_1 add: shift_modgrp_power_int)
lemma modgrp_S_S [simp]: "S_modgrp * S_modgrp = -1"
by transfer auto
lemma inverse_S_modgrp [simp]: "inverse S_modgrp = -S_modgrp"
by (rule modgrp.inverse_unique) simp
lemma modgrp_S_S_' [simp]: "S_modgrp * (S_modgrp * x) = -x"
by (subst mult.assoc [symmetric], subst modgrp_S_S) simp
lemma not_is_singular_1_modgrp [simp]: "¬is_singular_modgrp 1"
by transfer auto
lemma not_is_singular_T_modgrp [simp]: "¬is_singular_modgrp T_modgrp"
by transfer auto
lemma not_is_singular_shift_modgrp [simp]: "¬is_singular_modgrp (shift_modgrp n)"
by transfer auto
lemma is_singular_S_modgrp [simp]: "is_singular_modgrp S_modgrp"
by transfer auto
lemma pole_modgrp_S [simp]: "pole_modgrp S_modgrp = 0"
by transfer auto
lemma pole_modgrp_1 [simp]: "pole_modgrp 1 = 0"
by transfer auto
lemma pole_modgrp_T [simp]: "pole_modgrp T_modgrp = 0"
by transfer auto
lemma pole_modgrp_shift [simp]: "pole_modgrp (shift_modgrp n) = 0"
by transfer auto
lemma pole_image_modgrp_1 [simp]: "pole_image_modgrp 1 = 0"
by transfer auto
lemma pole_image_modgrp_T [simp]: "pole_image_modgrp T_modgrp = 0"
by transfer auto
lemma pole_image_modgrp_shift [simp]: "pole_image_modgrp (shift_modgrp n) = 0"
by transfer auto
lemma pole_image_modgrp_S [simp]: "pole_image_modgrp S_modgrp = 0"
by transfer auto
lemma minus_minus_power2_eq: "(-x - y :: 'a :: ring_1) ^ 2 = (x + y) ^ 2"
by (simp add: algebra_simps power2_eq_square)
lemma modgrp_a_1 [simp]: "modgrp_a 1 = 1"
and modgrp_b_1 [simp]: "modgrp_b 1 = 0"
and modgrp_c_1 [simp]: "modgrp_c 1 = 0"
and modgrp_d_1 [simp]: "modgrp_d 1 = 1"
by (transfer; simp; fail)+
lemma not_singular_modgrpD:
assumes "¬is_singular_modgrp f"
shows "abs f = shift_modgrp (modgrp_b (abs f))"
using assms by transfer (auto simp: zmult_eq_1_iff)
lemma S_conv_modgrp: "S_modgrp = modgrp 0 (-1) 1 0"
and T_conv_modgrp: "T_modgrp = modgrp 1 1 0 1"
and shift_conv_modgrp: "shift_modgrp n = modgrp 1 n 0 1"
and one_conv_modgrp: "1 = modgrp 1 0 0 1"
by (transfer; simp; fail)+
lemma modgrp_times:
assumes "a * d - b * c = 1"
assumes "a' * d' - b' * c' = 1"
shows "modgrp a b c d * modgrp a' b' c' d' =
modgrp (a * a' + b * c') (a * b' + b * d') (c * a' + d * c') (c * b' + d * d')"
using assms by transfer (auto simp: algebra_simps)
lemma modgrp_uminus: "a * d - b * c = 1 ⟹ -modgrp a b c d = modgrp (-a) (-b) (-c) (-d)"
by transfer auto
lemma modgrp_inverse:
assumes "a * d - b * c = 1"
shows "inverse (modgrp a b c d) = modgrp d (-b) (-c) a"
by (intro modgrp.inverse_unique, subst modgrp_times)
(use assms in ‹auto simp: algebra_simps one_conv_modgrp›)
lemma modgrp_a_mult_shift [simp]: "modgrp_a (f * shift_modgrp m) = modgrp_a f"
by transfer auto
lemma modgrp_b_mult_shift [simp]: "modgrp_b (f * shift_modgrp m) = modgrp_a f * m + modgrp_b f"
by transfer auto
lemma modgrp_c_mult_shift [simp]: "modgrp_c (f * shift_modgrp m) = modgrp_c f"
by transfer auto
lemma modgrp_d_mult_shift [simp]: "modgrp_d (f * shift_modgrp m) = modgrp_c f * m + modgrp_d f"
by transfer auto
lemma coprime_modgrp_c_d: "coprime (modgrp_c f) (modgrp_d f)"
proof -
define a b c d where "a = modgrp_a f" "b = modgrp_b f" "c = modgrp_c f" "d = modgrp_d f"
have "[a * 0 - b * c = a * d - b * c] (mod d)"
by (intro cong_diff cong_refl cong_mult) (auto simp: Cong.cong_def)
also have "a * d - b * c = 1"
unfolding a_b_c_d_def modgrp_abcd_det[of f] by simp
finally have "[c * (-b) = 1] (mod d)"
by (simp add: mult_ac)
thus "coprime c d"
by (subst coprime_iff_invertible_int) (auto intro!: exI[of _ "-b"])
qed
context unimodular_moebius_transform
begin
lift_definition as_modgrp :: modgrp is "(a, b, c, d)"
using unimodular by auto
lemma as_modgrp_altdef: "as_modgrp = modgrp a b c d"
using unimodular by transfer auto
lemma φ_as_modgrp: "φ = apply_modgrp as_modgrp"
unfolding φ_def by transfer simp
end
interpretation modgrp: unimodular_moebius_transform "modgrp_a x" "modgrp_b x" "modgrp_c x" "modgrp_d x"
rewrites "modgrp.as_modgrp = x" and "modgrp.φ = apply_modgrp x"
proof -
show *: "unimodular_moebius_transform (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x)"
by unfold_locales (rule modgrp_abcd_det)
show "unimodular_moebius_transform.as_modgrp (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x) = x"
by (subst unimodular_moebius_transform.as_modgrp_altdef[OF *]) auto
show "unimodular_moebius_transform.φ (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x) = apply_modgrp x"
by (subst unimodular_moebius_transform.φ_def[OF *], subst apply_modgrp_altdef) auto
qed
subsection ‹Code generation›
code_datatype modgrp
lemma one_modgrp_code [code]: "1 = modgrp 1 0 0 1"
and S_modgrp_code [code]: "S_modgrp = modgrp 0 (-1) 1 0"
and T_modgrp_code [code]: "T_modgrp = modgrp 1 1 0 1"
and shift_modgrp_code [code]: "shift_modgrp n = modgrp 1 n 0 1"
by (simp_all add: one_conv_modgrp S_conv_modgrp T_conv_modgrp shift_conv_modgrp)
lemma inverse_modgrp_code [code]: "inverse (modgrp a b c d) = modgrp d (-b) (-c) a"
by (cases "a * d - b * c = 1")
(auto simp: modgrp_inverse modgrp_wrong algebra_simps)
lemma modgrp_a_uminus [simp]: "modgrp_a (-f) = -modgrp_a f"
and modgrp_b_uminus [simp]: "modgrp_b (-f) = -modgrp_b f"
and modgrp_c_uminus [simp]: "modgrp_c (-f) = -modgrp_c f"
and modgrp_d_uminus [simp]: "modgrp_d (-f) = -modgrp_d f"
by (transfer; force)+
lemma modgrp_a_inverse [simp]: "modgrp_a (inverse f) = modgrp_d f"
and modgrp_b_inverse [simp]: "modgrp_b (inverse f) = -modgrp_b f"
and modgrp_c_inverse [simp]: "modgrp_c (inverse f) = -modgrp_c f"
and modgrp_d_inverse [simp]: "modgrp_d (inverse f) = modgrp_a f"
by (transfer; force)+
lemma times_modgrp_code [code]:
"modgrp a b c d * modgrp a' b' c' d' = (
if a * d - b * c ≠ 1 then modgrp a' b' c' d'
else if a' * d' - b' * c' ≠ 1 then modgrp a b c d
else modgrp (a * a' + b * c') (a * b' + b * d') (c * a' + d * c') (c * b' + d * d'))"
by (simp add: modgrp_times modgrp_wrong)
lemma modgrp_a_times [simp]: "modgrp_a (f * g) = modgrp_a f * modgrp_a g + modgrp_b f * modgrp_c g"
and modgrp_b_times [simp]: "modgrp_b (f * g) = modgrp_a f * modgrp_b g + modgrp_b f * modgrp_d g"
and modgrp_c_times [simp]: "modgrp_c (f * g) = modgrp_c f * modgrp_a g + modgrp_d f * modgrp_c g"
and modgrp_d_times [simp]: "modgrp_d (f * g) = modgrp_c f * modgrp_b g + modgrp_d f * modgrp_d g"
by (transfer; force)+
lemma modgrp_a_code [code]:
"modgrp_a (modgrp a b c d) = (if a * d - b * c = 1 then a else 1)"
by transfer auto
lemma modgrp_b_code [code]:
"modgrp_b (modgrp a b c d) = (if a * d - b * c = 1 then b else 0)"
by transfer auto
lemma modgrp_c_code [code]:
"modgrp_c (modgrp a b c d) = (if a * d - b * c = 1 then c else 0)"
by transfer auto
lemma modgrp_d_code [code]:
"modgrp_d (modgrp a b c d) = (if a * d - b * c = 1 then d else 1)"
by transfer auto
lemma sgn_modgrp_code [code]:
"sgn (modgrp a b c d) = (if a * d - b * c = 1 ∧ (c < 0 ∨ c = 0 ∧ d < 0) then -1 else 1)"
by (auto simp: sgn_modgrp_altdef modgrp_a_code modgrp_b_code modgrp_c_code modgrp_d_code)
lemma abs_modgrp_code [code]:
"abs (modgrp a b c d) =
(if a * d - b * c = 1 ∧ (c < 0 ∨ c = 0 ∧ d < 0) then -modgrp a b c d else modgrp a b c d)"
by (auto simp: abs_modgrp_altdef modgrp_a_code modgrp_b_code modgrp_c_code modgrp_d_code)
lemma apply_modgrp_code [code]:
"apply_modgrp (modgrp a b c d) z =
(if a * d - b * c ≠ 1 then z else (of_int a * z + of_int b) / (of_int c * z + of_int d))"
by transfer (auto simp: moebius_def)
lemma is_singular_modgrp_code [code]:
"is_singular_modgrp (modgrp a b c d) ⟷ a * d - b * c = 1 ∧ c ≠ 0"
by transfer auto
lemma pole_modgrp_code [code]:
"pole_modgrp (modgrp a b c d) = (if a * d - b * c = 1 then -of_int d / of_int c else 0)"
by transfer auto
lemma pole_image_modgrp_code [code]:
"pole_image_modgrp (modgrp a b c d) =
(if a * d - b * c = 1 ∧ c ≠ 0 then of_int a / of_int c else 0)"
by transfer auto
subsection ‹The factor of automorphy and the slash operator›
text ‹
The following will be needed to define the slash operator and it appears in a few other
places as well. Diamond and Shurman call it the ∗‹factor of automorphy› of a modular
transformation.
›
lift_definition automorphy_factor :: "modgrp ⇒ complex ⇒ complex" is
"λ(a,b,c,d) z. of_int c * z + of_int d" .
lemma automorphy_factor_altdef:
"automorphy_factor g z = of_int (modgrp_c g) * z + of_int (modgrp_d g)"
by transfer auto
lemma automorphy_factor_uminus [simp]: "automorphy_factor (-h) z = -automorphy_factor h z"
by (auto simp: automorphy_factor_altdef)
lemma automorphy_factor_1 [simp]: "automorphy_factor 1 z = 1"
by (auto simp: automorphy_factor_altdef)
lemma automorphy_factor_shift [simp]: "automorphy_factor (shift_modgrp n) z = 1"
by (simp add: automorphy_factor_altdef)
lemma automorphy_factor_T [simp]: "automorphy_factor T_modgrp z = 1"
by (simp add: automorphy_factor_altdef)
lemma automorphy_factor_S [simp]: "automorphy_factor S_modgrp z = z"
by (simp add: automorphy_factor_altdef)
lemma automorphy_factor_shift_right [simp]:
"automorphy_factor (f * shift_modgrp n) z = automorphy_factor f (z + of_int n)"
unfolding automorphy_factor_def
by transfer (auto simp: algebra_simps)
lemma automorphy_factor_shift_left [simp]:
"automorphy_factor (shift_modgrp n * f) z = automorphy_factor f z"
by (simp add: automorphy_factor_altdef)
lemma automorphy_factor_T_right [simp]:
"automorphy_factor (f * T_modgrp) z = automorphy_factor f (z + 1)"
unfolding shift_modgrp_1 [symmetric] by (subst automorphy_factor_shift_right) auto
lemma automorphy_factor_T_left [simp]:
"automorphy_factor (T_modgrp * f) z = automorphy_factor f z"
unfolding shift_modgrp_1 [symmetric] by (subst automorphy_factor_shift_left) auto
lemma automorphy_factor_nonzero [simp]:
assumes "Im z ≠ 0"
shows "automorphy_factor g z ≠ 0"
proof -
define c d where "c = modgrp_c g" and "d = modgrp_d g"
have "c ≠ 0 ∨ d ≠ 0"
unfolding c_def d_def using modgrp_c_nz_or_d_nz by blast
have "of_int c * z + of_int d ≠ 0"
using assms ‹c ≠ 0 ∨ d ≠ 0› by (auto simp: complex_eq_iff)
thus ?thesis
by (simp add: automorphy_factor_altdef c_def d_def)
qed
lemma automorphy_factor_mult:
assumes "Im z ≠ 0"
shows "automorphy_factor (f * g) z =
automorphy_factor f (apply_modgrp g z) * automorphy_factor g z"
proof -
define x where "x = (of_int (modgrp_a g) * z + of_int (modgrp_b g))"
define y where "y = automorphy_factor g z"
have "y ≠ 0"
using assms by (auto simp: y_def)
have "automorphy_factor f (apply_modgrp g z) * automorphy_factor g z =
(of_int (modgrp_c f) * x / y + of_int (modgrp_d f)) * y"
by (auto simp: x_def y_def automorphy_factor_altdef apply_modgrp_altdef moebius_def)
also have "… = of_int (modgrp_c f) * x + of_int (modgrp_d f) * y"
using ‹y ≠ 0› by (auto simp: field_simps)
also have "… = automorphy_factor (f * g) z"
by (auto simp: automorphy_factor_altdef x_def y_def algebra_simps)
finally show ?thesis ..
qed
lemma has_field_derivative_automorphy_factor [derivative_intros]:
assumes "(f has_field_derivative f') (at x within A)"
shows "((λx. automorphy_factor g (f x)) has_field_derivative (of_int (modgrp_c g) * f')) (at x within A)"
unfolding automorphy_factor_altdef by (auto intro!: derivative_eq_intros assms)
lemma automorphy_factor_analytic [analytic_intros]: "automorphy_factor g analytic_on A"
unfolding automorphy_factor_altdef by (auto simp: automorphy_factor_def intro!: analytic_intros)
lemma automorphy_factor_meromorphic [meromorphic_intros]: "automorphy_factor h meromorphic_on A"
unfolding automorphy_factor_altdef by (auto intro!: meromorphic_intros)
lemma tendsto_automorphy_factor [tendsto_intros]:
"(f ⤏ c) F ⟹ ((λx. automorphy_factor g (f x)) ⤏ automorphy_factor g c) F"
unfolding automorphy_factor_altdef by (auto intro!: tendsto_intros)
lemma apply_modgrp_has_field_derivative [derivative_intros]:
assumes "¬is_singular_modgrp f ∨ x ≠ pole_modgrp f"
shows "(apply_modgrp f has_field_derivative (1 / automorphy_factor f x ^ 2)) (at x within A)"
using assms
proof (transfer, goal_cases)
case (1 f x A)
obtain a b c d where [simp]: "f = (a, b, c, d)"
using prod_cases4 .
have "(moebius (of_int a) (of_int b) (of_int c) (of_int d) has_field_derivative
(of_int (a * d - b * c) / ((of_int c * x + of_int d)⇧2)))
(at x within A)"
unfolding of_int_mult of_int_diff
by (rule moebius_has_field_derivative) (use 1 in auto)
also have "a * d - b * c = 1"
using 1 by simp
finally show ?case
by (simp add: field_simps)
qed
lemma apply_modgrp_has_field_derivative' [derivative_intros]:
assumes "(g has_field_derivative g') (at x within A)"
assumes "¬is_singular_modgrp f ∨ g x ≠ pole_modgrp f"
shows "((λx. apply_modgrp f (g x)) has_field_derivative g' / automorphy_factor f (g x) ^ 2)
(at x within A)"
proof -
have "((apply_modgrp f ∘ g) has_field_derivative
(1 / automorphy_factor f (g x) ^ 2) * g') (at x within A)"
by (intro DERIV_chain assms derivative_intros)
thus ?thesis
by (simp add: o_def)
qed
lemma Im_apply_modgrp: "Im (apply_modgrp f t) = Im t / norm (automorphy_factor f t) ^ 2"
by (auto simp: modgrp.Im_transform automorphy_factor_altdef)
subsection ‹Sending rational numbers to infinity›
text ‹
The following gives a unimodular transformation that sends a specific rational number
to infinity. This is not unique.
›
lift_definition modgrp_of_rat :: "rat ⇒ modgrp" is
"λx. let (u, v) = quotient_of x; (a, b) = bezout_coefficients u v in (a, b, -v, u)"
proof goal_cases
case (1 x)
obtain u v where x_eq: "quotient_of x = (u, v)"
by (cases "quotient_of x")
obtain a b where ab: "bezout_coefficients u v = (a, b)"
by (cases "bezout_coefficients u v")
have "coprime u v"
using x_eq by (metis quotient_of_coprime)
hence "a * u + b * v = 1"
using bezout_coefficients_fst_snd[of u v] unfolding ab by auto
thus ?case
by (auto simp: x_eq ab)
qed
lemma modgrp_of_rat_of_int: "modgrp_of_rat (of_int n) = -S_modgrp * shift_modgrp (-n)"
by transfer (auto simp: bezout_coefficients_def euclid_ext_aux.simps)
lemma modgrp_of_rat_of_nat: "modgrp_of_rat (of_nat n) = -S_modgrp * shift_modgrp (-int n)"
using modgrp_of_rat_of_int[of "int n"] by simp
lemma modgrp_of_rat_0 [simp]: "modgrp_of_rat 0 = -S_modgrp"
using modgrp_of_rat_of_int[of 0] by simp
lemma pole_modgrp_of_rat [simp]: "pole_modgrp (modgrp_of_rat x) = x"
proof (transfer, goal_cases)
case (1 x)
have "rat_of_int (fst (quotient_of x)) / rat_of_int (snd (quotient_of x)) = x"
by (metis snd_conv quotient_of_div fst_conv prod_eqI)
thus ?case
by (auto simp: case_prod_unfold Let_def)
qed
subsection ‹Representation as product of powers of generators›
definition modgrp_from_gens :: "int option list ⇒ modgrp" where
"modgrp_from_gens xs = prod_list (map (λx. case x of None ⇒ S_modgrp | Some n ⇒ shift_modgrp n) xs)"
lemma modgrp_from_gens_Nil [simp]:
"modgrp_from_gens [] = 1"
and modgrp_from_gens_append [simp]:
"modgrp_from_gens (xs @ ys) = modgrp_from_gens xs * modgrp_from_gens ys"
and modgrp_from_gens_Cons1 [simp]:
"modgrp_from_gens (None # xs) = S_modgrp * modgrp_from_gens xs"
and modgrp_from_gens_Cons2 [simp]:
"modgrp_from_gens (Some n # xs) = shift_modgrp n * modgrp_from_gens xs"
and modgrp_from_gens_Cons:
"modgrp_from_gens (x # xs) =
(case x of None ⇒ S_modgrp | Some n ⇒ shift_modgrp n) * modgrp_from_gens xs"
by (simp_all add: modgrp_from_gens_def)
definition invert_modgrp_gens :: "int option list ⇒ int option list"
where "invert_modgrp_gens = rev ∘ map (map_option uminus)"
lemma invert_modgrp_gens_Nil [simp]:
"invert_modgrp_gens [] = []"
and invert_modgrp_gens_append [simp]:
"invert_modgrp_gens (xs @ ys) = invert_modgrp_gens ys @ invert_modgrp_gens xs"
and invert_modgrp_gens_Cons1 [simp]:
"invert_modgrp_gens (None # xs) = invert_modgrp_gens xs @ [None]"
and invert_modgrp_gens_Cons2 [simp]:
"invert_modgrp_gens (Some n # xs) = invert_modgrp_gens xs @ [Some (-n)]"
and invert_modgrp_gens_Cons:
"invert_modgrp_gens (x # xs) = invert_modgrp_gens xs @ [map_option uminus x]"
by (simp_all add: invert_modgrp_gens_def)
lemma sgn_S_modgrp [simp]: "sgn S_modgrp = 1"
by transfer auto
lemma sgn_T_modgrp [simp]: "sgn T_modgrp = 1"
by transfer auto
lemma sgn_shift_modgrp [simp]: "sgn (shift_modgrp n) = 1"
by transfer auto
lemma abs_S_modgrp [simp]: "abs S_modgrp = S_modgrp"
by transfer auto
lemma abs_T_modgrp [simp]: "abs T_modgrp = T_modgrp"
by transfer auto
lemma abs_shift_modgrp [simp]: "abs (shift_modgrp n) = shift_modgrp n"
by transfer auto
lemma abs_modgrp_eqE:
assumes "abs f = abs g"
obtains "f = g" | "f = (-g :: modgrp)"
using assms by transfer (auto split: if_splits)
lemma abs_modgrp_eq_1_iff: "abs (f :: modgrp) = 1 ⟷ f = 1 ∨ f = -1"
using abs_modgrp_eqE[of f 1] by auto
lemma abs_modgrp_uminus_cong:
"abs f = abs f' ⟹ abs (-f) = abs (-f' :: modgrp)"
by auto
lemma abs_modgrp_mult_cong:
"abs f = abs f' ⟹ abs g = abs g' ⟹ abs (f * g) = abs (f' * g' :: modgrp)"
by (auto elim!: abs_modgrp_eqE)
lemma abs_modgrp_inverse_cong:
"abs f = abs f' ⟹ abs (inverse f) = abs (inverse f' :: modgrp)"
by (auto elim!: abs_modgrp_eqE)
lemmas abs_modgrp_congs = abs_modgrp_uminus_cong abs_modgrp_mult_cong abs_modgrp_inverse_cong
lemma modgrp_from_gens_invert [simp]:
"abs (modgrp_from_gens (invert_modgrp_gens xs)) = abs (inverse (modgrp_from_gens xs))"
by (induction xs)
(auto simp: invert_modgrp_gens_Cons map_option_case algebra_simps
modgrp.inverse_distrib_swap shift_modgrp_minus
intro: abs_modgrp_congs split: option.splits)
function modgrp_genseq :: "int ⇒ int ⇒ int ⇒ int ⇒ int option list" where
"modgrp_genseq a b c d =
(if c = 0 then let b' = (if a > 0 then b else -b) in [Some b']
else modgrp_genseq (-a * (d div c) + b) (-a) (d mod c) (-c) @ [None, Some (d div c)])"
by auto
termination
by (relation "Wellfounded.measure (nat ∘ abs ∘ (λ(_,_,c,_) ⇒ c))") (auto simp: abs_mod_less)
lemmas [simp del] = modgrp_genseq.simps
lemma modgrp_genseq_c_0: "modgrp_genseq a b 0 d = (let b' = (if a > 0 then b else -b) in [Some b'])"
and modgrp_genseq_c_nz:
"c ≠ 0 ⟹ modgrp_genseq a b c d =
(let q = d div c in modgrp_genseq (-a * q + b) (-a) (d mod c) (-c) @ [None, Some q])"
by (subst modgrp_genseq.simps; simp add: Let_def)+
lemma modgrp_genseq_code [code]:
"modgrp_genseq a b c d =
(if c = 0 then [Some (if a > 0 then b else -b)]
else (let q = d div c in modgrp_genseq (-a * q + b) (-a) (d mod c) (-c) @ [None, Some q]))"
by (subst modgrp_genseq.simps) (auto simp: Let_def)
lemma modgrp_genseq_correct:
assumes "a * d - b * c = 1"
shows "abs (modgrp_from_gens (modgrp_genseq a b c d)) = abs (modgrp a b c d)"
using assms
proof (induction a b c d rule: modgrp_genseq.induct)
case (1 a b c d)
write S_modgrp ("S")
write shift_modgrp ("T")
show ?case
proof (cases "c = 0")
case [simp]: True
thus ?thesis using 1
by (auto simp: modgrp_genseq_c_0 zmult_eq_1_iff shift_conv_modgrp abs_modgrp_code modgrp_uminus)
next
case False
define q r where "q = d div c" and "r = d mod c"
have "q * c + r = d"
by (simp add: q_def r_def)
with ‹a * d - b * c = 1› have det': "a * r - (b - a * q) * c = 1"
by Groebner_Basis.algebra
have "¦modgrp_from_gens (modgrp_genseq a b c d)¦ = ¦modgrp (-a * q + b) (-a) r (-c) * (S * T q)¦"
using False "1.IH" det'
by (auto simp: modgrp_genseq_c_nz Let_def q_def r_def intro: abs_modgrp_congs)
also have "S * T q = modgrp 0 (- 1) 1 q"
unfolding S_conv_modgrp shift_conv_modgrp by (subst modgrp_times) simp_all
also have "modgrp (-a * q + b) (-a) r (-c) * … = modgrp (- a) (- b) (- c) (-r - c * q)"
using det' by (subst modgrp_times) simp_all
also have "¦…¦ = ¦modgrp a b c (q * c + r)¦"
using det' by (auto simp: abs_modgrp_code algebra_simps modgrp_uminus)
also have "q * c + r = d"
by (simp add: q_def r_def)
finally show ?thesis .
qed
qed
lemma filterlim_apply_modgrp_at:
assumes "¬is_singular_modgrp g ∨ z ≠ pole_modgrp g"
shows "filterlim (apply_modgrp g) (at (apply_modgrp g z)) (at (z :: 'a :: real_normed_field))"
proof -
have "∀⇩F x in at z. x ∈ (if is_singular_modgrp g then -{pole_modgrp g} else UNIV) - {z}"
by (intro eventually_at_in_open) (use assms in auto)
hence "∀⇩F x in at z. apply_modgrp g x ≠ apply_modgrp g z"
by eventually_elim (use assms in ‹auto split: if_splits›)
thus ?thesis
using assms by (auto simp: filterlim_at intro!: tendsto_eq_intros)
qed
lemma apply_modgrp_neq_pole_image [simp]:
"is_singular_modgrp g ⟹ z ≠ pole_modgrp g ⟹
apply_modgrp g (z :: 'a :: field_char_0) ≠ pole_image_modgrp g"
by transfer (auto simp: field_simps add_eq_0_iff moebius_def
simp flip: of_int_add of_int_mult of_int_diff)
lemma image_apply_modgrp_conv_vimage:
fixes A :: "'a :: field_char_0 set"
assumes "¬is_singular_modgrp f ∨ pole_modgrp f ∉ A"
defines "S ≡ (if is_singular_modgrp f then -{pole_image_modgrp f :: 'a} else UNIV)"
shows "apply_modgrp f ` A = apply_modgrp (inverse f) -` A ∩ S"
proof (intro equalityI subsetI)
fix z assume z: "z ∈ (apply_modgrp (inverse f) -` A) ∩ S"
thus "z ∈ apply_modgrp f ` A" using assms
by (auto elim!: rev_image_eqI simp flip: apply_modgrp_mult simp: S_def split: if_splits)
next
fix z assume z: "z ∈ apply_modgrp f ` A"
then obtain x where x: "x ∈ A" "z = apply_modgrp f x"
by auto
have "apply_modgrp (inverse f) (apply_modgrp f x) ∈ A"
using x assms by (subst apply_modgrp_mult [symmetric]) auto
moreover have "apply_modgrp f x ≠ pole_image_modgrp f" if "is_singular_modgrp f"
using x assms that by (intro apply_modgrp_neq_pole_image) auto
ultimately show "z ∈ (apply_modgrp (inverse f) -` A) ∩ S"
using x by (auto simp: S_def)
qed
lemma apply_modgrp_open_map:
fixes A :: "'a :: real_normed_field set"
assumes "open A" "¬is_singular_modgrp f ∨ pole_modgrp f ∉ A"
shows "open (apply_modgrp f ` A)"
proof -
define S :: "'a set" where "S = (if is_singular_modgrp f then -{pole_image_modgrp f} else UNIV)"
have "open S"
by (auto simp: S_def)
have "apply_modgrp f ` A = apply_modgrp (inverse f) -` A ∩ S"
using image_apply_modgrp_conv_vimage[of f A] assms by (auto simp: S_def)
also have "apply_modgrp (inverse f) -` A ∩ S = S ∩ apply_modgrp (inverse f) -` A"
by (simp only: Int_commute)
also have "open …"
using assms by (intro continuous_open_preimage continuous_intros assms ‹open S›)
(auto simp: S_def)
finally show ?thesis .
qed
lemma filtermap_at_apply_modgrp:
fixes z :: "'a :: real_normed_field"
assumes "¬is_singular_modgrp g ∨ z ≠ pole_modgrp g"
shows "filtermap (apply_modgrp g) (at z) = at (apply_modgrp g z)"
proof (rule filtermap_fun_inverse)
show "filterlim (apply_modgrp g) (at (apply_modgrp g z)) (at z)"
using assms by (intro filterlim_apply_modgrp_at) auto
next
have "filterlim (apply_modgrp (inverse g)) (at (apply_modgrp (inverse g) (apply_modgrp g z)))
(at (apply_modgrp g z))"
using assms by (intro filterlim_apply_modgrp_at) auto
also have "apply_modgrp (inverse g) (apply_modgrp g z) = z"
using assms by (simp flip: apply_modgrp_mult)
finally show "filterlim (apply_modgrp (inverse g)) (at z) (at (apply_modgrp g z))" .
next
have "eventually (λx. x ∈ (if is_singular_modgrp g then -{pole_image_modgrp g} else UNIV))
(at (apply_modgrp g z))"
by (intro eventually_at_in_open') (use assms in auto)
thus "∀⇩F x in at (apply_modgrp g z). apply_modgrp g (apply_modgrp (inverse g) x) = x"
by eventually_elim (auto simp flip: apply_modgrp_mult split: if_splits)
qed
lemma zorder_moebius_zero:
assumes "a ≠ 0" "a * d - b * c ≠ 0"
shows "zorder (moebius a b c d) (-b / a) = 1"
proof (rule zorder_eqI)
note [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
define A where "A = (if c = 0 then UNIV else -{-d/c})"
show "open A"
by (auto simp: A_def)
show "-b/a ∈ A"
using assms by (auto simp: A_def field_simps)
show "(λx. a / (c * x + d)) holomorphic_on A"
proof (intro holomorphic_intros)
fix x assume "x ∈ A"
thus "c * x + d ≠ 0"
unfolding A_def using assms
by (auto simp: A_def field_simps add_eq_0_iff split: if_splits)
qed
show "a / (c * (-b / a) + d) ≠ 0"
using assms by (auto simp: field_simps)
show "moebius a b c d w = a / (c * w + d) * (w - - b / a) powi 1"
if "w ∈ (if c = 0 then UNIV else - {- d / c})" "w ≠ - b / a" for w
using that assms by (auto simp: divide_simps moebius_def split: if_splits)
qed
lemma zorder_moebius_pole:
assumes "c ≠ 0" "a * d - b * c ≠ 0"
shows "zorder (moebius a b c d) (-d / c) = -1"
proof -
note [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
have "zorder (moebius a b c d) (-d / c) =
zorder (λx. (a * x + b) / c / (x - (-d / c)) ^ 1) (-d / c)"
proof (rule zorder_cong)
have "eventually (λz. z ≠ -d/c) (at (-d/c))"
by (simp add: eventually_neq_at_within)
thus "∀⇩F z in at (- d / c). moebius a b c d z = (a * z + b) / c / (z - - d / c) ^ 1"
by eventually_elim (use assms in ‹auto simp: moebius_def divide_simps mult_ac›)
qed auto
also have "zorder (λx. (a * x + b) / c / (x - (-d / c)) ^ 1) (-d / c) = -int 1"
proof (rule zorder_nonzero_div_power)
show "(λw. (a * w + b) / c) holomorphic_on UNIV"
using assms by (intro holomorphic_intros)
show "(a * (-d / c) + b) / c ≠ 0"
using assms by (auto simp: field_simps)
qed auto
finally show ?thesis by simp
qed
lemma zorder_moebius:
assumes "c = 0 ∨ z ≠ -d / c" "a * d - b * c ≠ 0"
shows "zorder (λx. moebius a b c d x - moebius a b c d z) z = 1"
proof (rule zorder_eqI)
define S where "S = (if c = 0 then UNIV else -{-d/c})"
define g where "g = (λw. (a * d - b * c) / ((c * w + d) * (c * z + d)))"
show "open S" "z ∈ S"
using assms by (auto simp: S_def)
show "g holomorphic_on S"
unfolding g_def using assms
by (intro holomorphic_intros no_zero_divisors)
(auto simp: S_def field_simps add_eq_0_iff split: if_splits)
show "(a * d - b * c) / ((c * z + d) * (c * z + d)) ≠ 0"
using assms by (auto simp: add_eq_0_iff split: if_splits)
show "moebius a b c d w - moebius a b c d z =
(a * d - b * c) / ((c * w + d) * (c * z + d)) * (w - z) powi 1" if "w ∈ S" for w
by (subst moebius_diff_eq) (use that assms in ‹auto simp: S_def split: if_splits›)
qed
lemma zorder_apply_modgrp:
assumes "¬is_singular_modgrp g ∨ z ≠ pole_modgrp g"
shows "zorder (λx. apply_modgrp g x - apply_modgrp g z) z = 1"
using assms
proof (transfer, goal_cases)
case (1 f z)
obtain a b c d where [simp]: "f = (a, b, c, d)"
using prod_cases4 .
show ?case using 1 zorder_moebius[of c z d a b]
by (auto simp: simp flip: of_int_mult)
qed
lemma zorder_fls_modgrp_pole:
assumes "is_singular_modgrp f"
shows "zorder (apply_modgrp f) (pole_modgrp f) = -1"
using assms
proof (transfer, goal_cases)
case (1 f)
obtain a b c d where [simp]: "f = (a, b, c, d)"
using prod_cases4 .
show ?case using 1 zorder_moebius_pole[of c a d b]
by (auto simp: simp flip: of_int_mult)
qed
subsection ‹Induction rules in terms of generators›
text ‹Theorem 2.1›
lemma modgrp_induct_S_shift [case_names id uminus S shift]:
assumes "P 1"
"⋀x. P x ⟹ P (-x)"
"⋀x. P x ⟹ P (S_modgrp * x)"
"⋀x n. P x ⟹ P (shift_modgrp n * x)"
shows "P x"
proof -
define xs where "xs = modgrp_genseq (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x)"
have "P (modgrp_from_gens xs)"
by (induction xs) (auto intro: assms simp: modgrp_from_gens_Cons split: option.splits)
moreover have "¦x¦ = ¦modgrp_from_gens xs¦" unfolding xs_def
using modgrp_genseq_correct[of "modgrp_a x" "modgrp_d x" "modgrp_b x" "modgrp_c x"]
modgrp_abcd_det[of x] by auto
hence "x = modgrp_from_gens xs ∨ x = -modgrp_from_gens xs"
by (elim abs_modgrp_eqE) auto
ultimately show ?thesis
using assms(2)[of "modgrp_from_gens xs"] by auto
qed
lemma modgrp_induct [case_names id uminus S T inv_T]:
assumes "P 1"
"⋀x. P x ⟹ P (-x)"
"⋀x. P x ⟹ P (S_modgrp * x)"
"⋀x. P x ⟹ P (T_modgrp * x)"
"⋀x. P x ⟹ P (inverse T_modgrp * x)"
shows "P x"
proof -
define xs where "xs = modgrp_genseq (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x)"
have *: "P (T_modgrp ^ n * x)" if "P x" for n x
by (induction n) (auto simp: mult.assoc shift_modgrp_1 intro: assms that)
have **: "P (inverse T_modgrp ^ n * x)" if "P x" for n x
by (induction n) (auto simp: shift_modgrp_add mult.assoc shift_modgrp_1 intro: assms that)
have ***: "P (shift_modgrp n * x)" if "P x" for n x
using *[of x "nat n"] **[of x "nat (-n)"] that
by (auto simp: shift_modgrp_conv_T_power power_int_def)
have "P (modgrp_from_gens xs)"
by (induction xs) (auto intro: assms *** simp: modgrp_from_gens_Cons split: option.splits)
moreover have "¦x¦ = ¦modgrp_from_gens xs¦" unfolding xs_def
using modgrp_genseq_correct[of "modgrp_a x" "modgrp_d x" "modgrp_b x" "modgrp_c x"]
modgrp_abcd_det[of x] by auto
hence "x = modgrp_from_gens xs ∨ x = -modgrp_from_gens xs"
by (elim abs_modgrp_eqE) auto
ultimately show ?thesis
using assms(2)[of "modgrp_from_gens xs"] by auto
qed
lemma modgrp_induct_S_shift' [case_names id uminus S shift]:
assumes "P 1"
"⋀x. P x ⟹ P (-x)"
"⋀x. abs x = x ⟹ P x ⟹ P (x * S_modgrp)"
"⋀x n. abs x = x ⟹ P x ⟹ P (x * shift_modgrp n)"
shows "P x"
proof -
define xs where "xs = modgrp_genseq (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x)"
have 1: "P (x * S_modgrp)" if "P x" for x using assms that
by (metis abs_eq_modgrpE abs_modgrp_altdef abs_uminus_modgrp times_modgrp_uminus_left)
have 2: "P (x * shift_modgrp n)" if "P x" for x n using assms that
by (metis abs_eq_modgrpE abs_modgrp_altdef abs_uminus_modgrp times_modgrp_uminus_left)
have "P (modgrp_from_gens xs)"
by (induction xs rule: rev_induct)
(auto intro: assms(1,2) 1 2 simp: modgrp_from_gens_Cons split: option.splits)
moreover have "¦x¦ = ¦modgrp_from_gens xs¦" unfolding xs_def
using modgrp_genseq_correct[of "modgrp_a x" "modgrp_d x" "modgrp_b x" "modgrp_c x"]
modgrp_abcd_det[of x] by auto
hence "x = modgrp_from_gens xs ∨ x = -modgrp_from_gens xs"
by (elim abs_modgrp_eqE) auto
ultimately show ?thesis
using assms(2)[of "modgrp_from_gens xs"] by auto
qed
lemma modgrp_induct' [case_names id uminus S T inv_T]:
assumes "P 1"
"⋀x. P x ⟹ P (-x)"
"⋀x. P x ⟹ P (x * S_modgrp)"
"⋀x. P x ⟹ P (x * T_modgrp)"
"⋀x. P x ⟹ P (x * inverse T_modgrp)"
shows "P x"
proof -
define xs where "xs = modgrp_genseq (modgrp_a x) (modgrp_b x) (modgrp_c x) (modgrp_d x)"
have *: "P (x * T_modgrp ^ n)" if "P x" for n x
using assms(4)[of "x * T_modgrp ^ n" for n]
by (induction n) (auto intro: that simp: algebra_simps power_commuting_commutes)
have **: "P (x * inverse T_modgrp ^ n)" if "P x" for n x
using assms(5)[of "x * inverse T_modgrp ^ n" for n]
by (induction n) (auto intro: that simp: algebra_simps power_commuting_commutes)
have ***: "P (x * shift_modgrp n)" if "P x" for n x
using *[of x "nat n"] **[of x "nat (-n)"] that
by (auto simp: shift_modgrp_conv_T_power power_int_def)
have "P (modgrp_from_gens xs)"
by (induction xs rule: rev_induct)
(auto intro: assms *** simp: modgrp_from_gens_Cons split: option.splits)
moreover have "¦x¦ = ¦modgrp_from_gens xs¦" unfolding xs_def
using modgrp_genseq_correct[of "modgrp_a x" "modgrp_d x" "modgrp_b x" "modgrp_c x"]
modgrp_abcd_det[of x] by auto
hence "x = modgrp_from_gens xs ∨ x = -modgrp_from_gens xs"
by (elim abs_modgrp_eqE) auto
ultimately show ?thesis
using assms(2)[of "modgrp_from_gens xs"] by auto
qed
definition apply_modgrp' :: "modgrp ⇒ 'a × 'a ⇒ 'a × 'a :: ring_1"
where "apply_modgrp' f =
(λ(x,y). (of_int (modgrp_a f) * x + of_int (modgrp_b f) * y,
of_int (modgrp_c f) * x + of_int (modgrp_d f) * y))"
lemma apply_modgrp'_z_one:
assumes "z ∉ ℝ"
shows "apply_modgrp' f (z, 1) = (automorphy_factor f z * apply_modgrp f z, automorphy_factor f z)"
proof -
from assms have "complex_of_int (modgrp_c f) * z + complex_of_int (modgrp_d f) ≠ 0"
by (simp add: complex_is_Real_iff modgrp.Im_transform_pos_aux)
thus ?thesis
by (simp add: apply_modgrp'_def automorphy_factor_altdef apply_modgrp_altdef moebius_def)
qed
subsection ‹Reduction map›
text ‹
Two elements of the modular group are considered congruent modulo $n$ if their entries are.
›
definition cong_modgrp :: "modgrp ⇒ modgrp ⇒ int ⇒ bool"
(‹(‹indent=1 notation=‹mixfix cong››[_ = _] '(' mod⇩Γ _'))›) where
"[f = g] (mod⇩Γ n) ⟷ list_all (λh. [h f = h g] (mod n)) [modgrp_a, modgrp_b, modgrp_c, modgrp_d]"
lemma cong_modgrp_abs [simp]: "[f = g] (mod⇩Γ (abs n)) ⟷ [f = g] (mod⇩Γ n)"
by (auto simp: cong_modgrp_def)
lemma cong_modgrp_refl [intro]: "[f = f] (mod⇩Γ n)"
by (auto simp: cong_modgrp_def)
lemma cong_modgrp_mult:
"[f1 = g1] (mod⇩Γ n) ⟹ [f2 = g2] (mod⇩Γ n) ⟹ [f1 * f2 = g1 * g2] (mod⇩Γ n)"
unfolding cong_modgrp_def list_all_Cons_iff list_all_Nil_iff
modgrp_a_times modgrp_b_times modgrp_c_times modgrp_d_times
by (elim conjE TrueE; intro conjI TrueI cong_add cong_mult)
lemma cong_modgrp_inverse:
"[f = g] (mod⇩Γ n) ⟹ [inverse f = inverse g] (mod⇩Γ n)"
unfolding cong_modgrp_def list_all_Cons_iff list_all_Nil_iff
modgrp_a_inverse modgrp_b_inverse modgrp_c_inverse modgrp_d_inverse
by (elim conjE TrueE; intro conjI TrueI cong_add cong_mult cong_uminus)
text ‹
The following version of the Chinese Remainder Theorem also works when the two moduli
are not coprime.
›
lemma chinese_remainder_theorem_gen:
fixes m n :: "'a :: {unique_euclidean_ring, euclidean_ring_gcd}"
assumes "[x = y] (mod gcd m n)"
obtains z where "[z = x] (mod m)" "[z = y] (mod n)"
proof -
obtain u v where "bezout_coefficients m n = (u, v)"
by (cases "bezout_coefficients m n")
hence uv: "gcd m n = u * m + v * n"
using bezout_coefficients_fst_snd[of m n] by simp
define k where "k = (x - y) div gcd m n"
have "x = y + k * gcd m n"
using assms by (auto simp: cong_iff_dvd_diff k_def)
hence x_eq: "x = y + k * u * m + k * v * n"
by (simp add: uv algebra_simps)
show ?thesis
proof (rule that)
have "[y + k * u * 0 + k * v * n = y + k * u * m + k * v * n] (mod m)"
by (intro cong_add cong_mult cong_refl) (auto simp: cong_def)
thus "[y + k * v * n = x] (mod m)"
by (simp add: x_eq)
next
have "[y + k * v * n = y + k * v * 0] (mod n)"
by (intro cong_add cong_mult cong_refl) (auto simp: cong_def)
thus "[y + k * v * n = y] (mod n)"
by (simp add: x_eq)
qed
qed
lemma cong_solve:
fixes a :: "'a :: {unique_euclidean_semiring, euclidean_ring_gcd}"
shows "∃x. [a * x = gcd a n] (mod n)"
proof -
obtain u v where uv: "bezout_coefficients a n = (u, v)"
by (cases "bezout_coefficients a n")
have "gcd a n = u * a + v * n"
using bezout_coefficients[of a n u v] uv by auto
also have "[u * a + v * n = u * a + v * 0] (mod n)"
by (intro cong_add cong_mult) (auto simp: cong_0_iff)
finally show ?thesis
by (intro exI[of _ u]) (simp add: cong_sym_eq mult_ac)
qed
lemma cong_solve_coprime:
fixes a :: "'a :: {unique_euclidean_ring, euclidean_ring_gcd}"
shows "coprime a n ⟹ ∃x. [a * x = 1] (mod n)"
using cong_solve[of a n] by simp
lemma chinese_remainder:
fixes A :: "'a set"
and m :: "'a ⇒ 'b :: {unique_euclidean_ring, euclidean_ring_gcd}"
and u :: "'a ⇒ 'b"
assumes fin: "finite A"
and cop: "∀i ∈ A. ∀j ∈ A. i ≠ j ⟶ coprime (m i) (m j)"
shows "∃x. ∀i ∈ A. [x = u i] (mod m i)"
proof -
have "∃b. (∀i ∈ A. [b i = 1] (mod m i) ∧ [b i = 0] (mod (∏j ∈ A - {i}. m j)))"
proof (rule finite_set_choice, rule fin, rule ballI)
fix i
assume "i ∈ A"
with cop have "coprime (∏j ∈ A - {i}. m j) (m i)"
by (intro prod_coprime_left) auto
then have "∃x. [(∏j ∈ A - {i}. m j) * x = 1] (mod m i)"
by (elim cong_solve_coprime)
then obtain x where "[(∏j ∈ A - {i}. m j) * x = 1] (mod m i)"
by auto
moreover have "[(∏j ∈ A - {i}. m j) * x = 0] (mod (∏j ∈ A - {i}. m j))"
by (simp add: cong_0_iff)
ultimately show "∃a. [a = 1] (mod m i) ∧ [a = 0] (mod prod m (A - {i}))"
by blast
qed
then obtain b where b: "⋀i. i ∈ A ⟹ [b i = 1] (mod m i) ∧ [b i = 0] (mod (∏j ∈ A - {i}. m j))"
by blast
let ?x = "∑i∈A. (u i) * (b i)"
show ?thesis
proof (rule exI, clarify)
fix i
assume a: "i ∈ A"
show "[?x = u i] (mod m i)"
proof -
from fin a have "?x = (∑j ∈ {i}. u j * b j) + (∑j ∈ A - {i}. u j * b j)"
by (subst sum.union_disjoint [symmetric]) (auto intro: sum.cong)
then have "[?x = u i * b i + (∑j ∈ A - {i}. u j * b j)] (mod m i)"
by auto
also have "[u i * b i + (∑j ∈ A - {i}. u j * b j) =
u i * 1 + (∑j ∈ A - {i}. u j * 0)] (mod m i)"
proof (intro cong_add cong_scalar_left cong_sum)
show "[b i = 1] (mod m i)"
using a b by blast
show "[b x = 0] (mod m i)" if "x ∈ A - {i}" for x
proof -
have "x ∈ A" "x ≠ i"
using that by auto
then show ?thesis
using a b [OF ‹x ∈ A›] cong_dvd_modulus fin by blast
qed
qed
finally show ?thesis
by simp
qed
qed
qed
lemma coprime_via_prime_factors:
fixes x y :: "'a :: factorial_semiring_gcd"
assumes "x ≠ 0" "⋀p. prime p ⟹ p dvd x ⟹ ¬p dvd y"
shows "coprime x y"
proof (rule ccontr)
assume "¬coprime x y"
with ‹x ≠ 0› have "¬is_unit (gcd x y)" "gcd x y ≠ 0"
by auto
then obtain p where "prime p" "p dvd gcd x y"
by (metis prime_divisor_exists)
with assms(2)[of p] show False
by auto
qed
text ‹
The following shows that the reduction map
$\text{SL}(2,\mathbb{Z}) \to \text{SL}(2,\mathbb{Z}/n\mathbb{Z})$ is surjective.
This means that if we have a matrix $A = \begin{pmatrix}a & b\\c & d\end{pmatrix}$ with
$ad-bc = 1\ (\text{mod}\ n)$, there exists a matrix
$A' = \begin{pmatrix}a' & b'\\c' & d'\end{pmatrix}$ with $a'd'-b'c'=1$ and
$A = A'\ (\text{mod}\ n)$.
So, basically, we can take a matrix whose determinant is only congruent to 1 modulo $n$ and
turn it into one with determinant exactly 1 while only adding and subtracting multiples of $n$
to the entries.
›
lemma exists_coprime_shifted_int_aux:
fixes c d :: int
assumes c: "c ≠ 0"
assumes coprime: "coprime (gcd c d) n"
obtains d' where "[d' = d] (mod n)" "coprime c d'"
proof -
define g where "g = gcd c d"
have "g ≠ 0"
using c by (auto simp: g_def)
have g: "coprime g n"
using coprime unfolding g_def by (metis coprime_iff_gcd_eq_1 gcd.assoc gcd_1_int)
define P1 where "P1 = prime_factors g"
define P2 where "P2 = prime_factors c - P1"
define a where "a = (λp. if p dvd d then modular_inverse p n * (1 - d) else 0)"
have "∃x. ∀p∈prime_factors c. [x = a p] (mod p)"
proof (rule chinese_remainder)
show "finite (prime_factors c)"
by (auto simp: P1_def P2_def)
next
show "∀p∈prime_factors c. ∀j∈prime_factors c. p ≠ j ⟶ coprime p j"
by (auto simp: P1_def P2_def in_prime_factors_iff intro: primes_coprime)
qed
then obtain x where x: "⋀p. prime p ⟹ p dvd c ⟹ [x = a p] (mod p)"
using c by (auto simp: prime_factors_dvd)
define d' where "d' = d + x * n"
have "coprime c d'"
proof (rule coprime_via_prime_factors)
fix p assume p: "prime p" "p dvd c"
show "¬p dvd d'"
proof (cases "p dvd d")
case False
have "[d' = d + a p * n] (mod p)"
unfolding d'_def by (intro cong_add cong_mult x cong_refl p)
hence "[d' = d] (mod p)"
using False by (simp add: a_def)
thus "¬p dvd d'"
using False cong_dvd_iff by blast
next
case True
with coprime have "coprime p n"
using coprime_divisors[OF _ dvd_refl, of p "gcd c d" n] p by auto
have "[d' = d + a p * n] (mod p)"
unfolding d'_def by (intro cong_add cong_mult x cong_refl p)
also have "a p * n = (1 - d) * (modular_inverse p n * n)"
using True by (simp add: algebra_simps a_def)
also have "[d + … = d + (1 - d) * 1] (mod p)"
unfolding a_def using ‹coprime p n›
by (intro cong_add cong_mult cong_modular_inverse2 cong_refl) (auto simp: coprime_commute)
finally have "[d' = 1] (mod p)"
by simp
hence "coprime d' p"
by (simp add: coprime_cong_cong_left)
thus "¬p dvd d'"
using coprime_absorb_right not_prime_unit p(1) by blast
qed
qed fact+
thus ?thesis
by (intro that[of d']) (auto simp: d'_def cong_iff_dvd_diff)
qed
lemma exists_coprime_shifted_int:
fixes c d :: int
assumes coprime: "coprime (gcd c d) n"
obtains c' d' where "[c' = c] (mod n)" "[d' = d] (mod n)" "coprime c' d'"
proof (cases "abs n = 1")
case True
hence "n = 1 ∨ n = -1"
by linarith
thus ?thesis
by (intro that[of 0 1]) auto
next
case False
hence "c ≠ 0 ∨ d ≠ 0"
using coprime by auto
thus ?thesis
proof
assume "c ≠ 0"
then obtain d' where "[d' = d] (mod n)" "coprime c d'"
using exists_coprime_shifted_int_aux[of c d n] coprime by auto
thus ?thesis
by (intro that[of c d']) auto
next
assume "d ≠ 0"
then obtain c' where "[c' = c] (mod n)" "coprime c' d"
using exists_coprime_shifted_int_aux[of d c n] coprime
by (auto simp: gcd.commute coprime_commute)
thus ?thesis
by (intro that[of c' d]) auto
qed
qed
theorem modgrp_reduction_surj:
fixes a b c d n :: int
assumes "[a * d - b * c = 1] (mod n)"
obtains f :: modgrp where
"[modgrp_a f = a] (mod n)" "[modgrp_b f = b] (mod n)"
"[modgrp_c f = c] (mod n)" "[modgrp_d f = d] (mod n)"
proof -
obtain c' d' where cd': "[c' = c] (mod n)" "[d' = d] (mod n)" "coprime c' d'"
proof (rule exists_coprime_shifted_int)
have "coprime (a * d - b * c) n"
using assms by (simp add: coprime_cong_cong_left)
thus "coprime (gcd c d) n"
using coprime_divisors[OF _ dvd_refl, of "gcd c d" "a * d - b * c" n] by auto
qed metis
define z where "z = (a * d' - b * c' - 1) div n"
have "[a * d' - b * c' = a * d - b * c] (mod n)"
by (intro cong_diff cong_mult cd' cong_refl)
also have "[a * d - b * c = 1] (mod n)"
by fact
finally have z: "a * d' - b * c' = 1 + z * n"
by (auto simp: cong_iff_dvd_diff z_def)
obtain x y where xy: "y * c' - x * d' = z"
proof -
obtain u v where "u * c' + v * d' = 1"
using bezout_int[of c' d'] cd'(3) by auto
hence "z * (u * c' + v * d') = z * 1"
by (rule arg_cong)
thus ?thesis
by (intro that[of "z * u" "-z * v"]) (auto simp: algebra_simps)
qed
define a' b' where "a' = a + x * n" and "b' = b + y * n"
have ab_cong: "[a' = a] (mod n)" "[b' = b] (mod n)"
by (auto simp: a'_def b'_def cong_iff_dvd_diff)
have "a' * d' - b' * c' = a * d' - b * c' - (y * c' - x * d') * n"
by (simp add: a'_def b'_def algebra_simps)
also have "a * d' - b * c' = 1 + z * n"
by (rule z)
also have "y * c' - x * d' = z"
by (rule xy)
finally have det: "a' * d' - b' * c' = 1"
by simp
show ?thesis using det ab_cong cd'
by (intro that[of "modgrp a' b' c' d'"]) (auto simp: modgrp_abcd_modgrp)
qed
end