Theory Unitary_Matrices

(* -------------------------------------------------------------------------- *)
subsection ‹Generalized Unitary Matrices›
(* -------------------------------------------------------------------------- *)

theory Unitary_Matrices
imports Matrices More_Complex
begin

text ‹In this section (generalized) $2\times 2$ unitary matrices are introduced.›

text ‹Unitary matrices›
definition unitary where
  "unitary M ⟷ mat_adj M *mm M = eye"

text ‹Generalized unitary matrices›
definition unitary_gen where
  "unitary_gen M ⟷
   (∃ k::complex. k ≠ 0 ∧ mat_adj M *mm M = k *sm eye)"

text ‹Scalar can be always be a positive real›
lemma unitary_gen_real:
  assumes "unitary_gen M"
  shows "(∃ k::real. k > 0 ∧ mat_adj M *mm M = cor k *sm eye)"
proof-
  obtain k where *: "mat_adj M *mm M = k *sm eye" "k ≠ 0"
    using assms
    by (auto simp add: unitary_gen_def)
  obtain a b c d where "M = (a, b, c, d)"
    by (cases M) auto
  hence "k = cor ((cmod a)2) + cor ((cmod c)2)"
    using *
    by (subst  complex_mult_cnj_cmod[symmetric])+ (auto simp add: mat_adj_def mat_cnj_def)
  hence "is_real k ∧ Re k > 0"
    using ‹k ≠ 0›
    by (smt (verit) add_cancel_left_left arg_0_iff arg_complex_of_real_positive not_sum_power2_lt_zero of_real_0 plus_complex.simps(1) plus_complex.simps(2))
  thus ?thesis
    using *
    by (rule_tac x="Re k" in exI) simp
qed

text ‹Generalized unitary matrices can be factored into a product of a unitary matrix and a real
positive scalar multiple of the identity matrix›
lemma unitary_gen_unitary:
  shows "unitary_gen M ⟷
         (∃ k M'. k > 0 ∧ unitary M' ∧ M = (cor k *sm eye) *mm M')" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain k where *: "k>0" "mat_adj M *mm M = cor k *sm eye"
    using unitary_gen_real[of M]
    by auto

  let ?k' = "cor (sqrt k)"
  have "?k' * cnj ?k' = cor k"
    using ‹k > 0›
    by simp
  moreover
  have "Re ?k' > 0" "is_real ?k'" "?k' ≠ 0"
    using ‹k > 0›
    by auto
  ultimately
  show ?rhs
    using * mat_eye_l
    unfolding unitary_gen_def unitary_def
    by (rule_tac x="Re ?k'" in exI) (rule_tac x="(1/?k')*smM" in exI, simp add: mult_sm_mm[symmetric])
next
  assume ?rhs
  then obtain k M' where "k > 0" "unitary M'" "M = (cor k *sm eye) *mm M'"
    by blast
  hence "M = cor k *sm M'"
    using mult_sm_mm[of "cor k" eye M'] mat_eye_l
    by simp
  thus ?lhs
    using ‹unitary M'› ‹k > 0›
    by (simp add: unitary_gen_def unitary_def)
qed

text ‹When they represent Möbius transformations, eneralized unitary matrices fix the imaginary unit circle. Therefore, they
fix a Hermitean form with (2, 0) signature (two positive and no negative diagonal elements).›
lemma unitary_gen_iff':
  shows "unitary_gen M ⟷ 
         (∃ k::complex. k ≠ 0 ∧ congruence M (1, 0, 0, 1) = k *sm (1, 0, 0, 1))"
  unfolding unitary_gen_def
  using mat_eye_r
  by (auto simp add: mult.assoc)

text ‹Unitary matrices are special cases of general unitary matrices›
lemma unitary_unitary_gen [simp]:
  assumes "unitary M" 
  shows "unitary_gen M"
  using assms
  unfolding unitary_gen_def unitary_def
  by auto

text ‹Generalized unitary matrices are regular›
lemma unitary_gen_regular:
  assumes "unitary_gen M"
  shows "mat_det M ≠ 0"
proof-
  from assms obtain k where
    "k ≠ 0" "mat_adj M *mm M = k *sm eye"
    unfolding unitary_gen_def
    by auto
  hence "mat_det (mat_adj M *mm M) ≠ 0"
    by simp
  thus ?thesis
    by (simp add: mat_det_adj)
qed

lemmas unitary_regular = unitary_gen_regular[OF unitary_unitary_gen]

(* -------------------------------------------------------------------------- *)
subsubsection ‹Group properties›
(* -------------------------------------------------------------------------- *)

text ‹Generalized $2\times 2$ unitary matrices form a group under
multiplication (usually denoted by $GU(2, \mathbb{C})$). The group is closed
under non-zero complex scalar multiplication. Since these matrices are
always regular, they form a subgroup of general linear group (usually
denoted by $GL(2, \mathbb{C})$) of all regular matrices.›

lemma unitary_gen_scale [simp]:
  assumes "unitary_gen M" and "k ≠ 0"
  shows "unitary_gen (k *sm M)"
  using assms
  unfolding unitary_gen_def
  by auto

lemma unitary_comp:
  assumes "unitary M1" and "unitary M2"
  shows "unitary (M1 *mm M2)"
  using assms
  unfolding unitary_def
  by (metis mat_adj_mult_mm mat_eye_l mult_mm_assoc)

lemma unitary_gen_comp:
  assumes "unitary_gen M1" and "unitary_gen M2"
  shows "unitary_gen (M1 *mm M2)"
proof-
  obtain k1 k2 where *: "k1 * k2 ≠ 0" "mat_adj M1 *mm M1 = k1 *sm eye" "mat_adj M2 *mm M2 = k2 *sm eye"
    using assms
    unfolding unitary_gen_def
    by auto
  have "mat_adj M2 *mm mat_adj M1 *mm (M1 *mm M2) = mat_adj M2 *mm (mat_adj M1 *mm M1) *mm M2"
    by (auto simp add: mult_mm_assoc)
  also have "... = mat_adj M2 *mm ((k1 *sm eye) *mm M2)"
    using *
    by (auto simp add: mult_mm_assoc)
  also have "... = mat_adj M2 *mm (k1 *sm M2)"
    using mult_sm_eye_mm[of k1 M2]
    by (simp del: eye_def)
  also have "... = k1 *sm (k2 *sm eye)"
    using *
    by auto
  finally
  show ?thesis
    using *
    unfolding unitary_gen_def
    by (rule_tac x="k1*k2" in exI, simp del: eye_def)
qed

lemma unitary_adj_eq_inv:
  shows "unitary M ⟷ mat_det M ≠ 0 ∧ mat_adj M = mat_inv M"
  using  unitary_regular[of M] mult_mm_inv_r[of M "mat_adj M" eye]  mat_eye_l[of "mat_inv M"] mat_inv_l[of M]
  unfolding unitary_def
  by - (rule, simp_all)

lemma unitary_inv:
  assumes "unitary M"
  shows "unitary (mat_inv M)"
  using assms
  unfolding unitary_adj_eq_inv
  using mat_adj_inv[of M] mat_det_inv[of M]
  by simp

lemma unitary_gen_inv:
  assumes "unitary_gen M"
  shows "unitary_gen (mat_inv M)"
proof-
    obtain k M' where "0 < k" "unitary M'" "M = cor k *sm eye *mm M'"
      using unitary_gen_unitary[of M] assms
      by blast
    hence "mat_inv M = cor (1/k) *sm mat_inv M'"
      by (metis mat_inv_mult_sm mult_sm_eye_mm norm_not_less_zero of_real_1 of_real_divide of_real_eq_0_iff sgn_1_neg sgn_greater sgn_if sgn_pos sgn_sgn)
    thus ?thesis
      using ‹k > 0› ‹unitary M'›
      by (subst unitary_gen_unitary[of "mat_inv M"]) (rule_tac x="1/k" in exI, rule_tac x="mat_inv M'" in exI, metis divide_pos_pos mult_sm_eye_mm unitary_inv zero_less_one)
  qed

(* -------------------------------------------------------------------------- *)
subsubsection ‹The characterization in terms of matrix elements›
(* -------------------------------------------------------------------------- *)

text ‹Special matrices are those having the determinant equal to 1. We first give their characterization.›
lemma unitary_special:
  assumes "unitary M" and "mat_det M = 1"
  shows "∃ a b. M = (a, b, -cnj b, cnj a)"
proof-
  have "mat_adj M = mat_inv M"
    using assms mult_mm_inv_r[of M "mat_adj M" "eye"] mat_eye_r mat_eye_l
    by (simp add: unitary_def)
  thus ?thesis
    using ‹mat_det M = 1›
    by (cases M) (auto simp add: mat_adj_def mat_cnj_def)
qed

lemma unitary_gen_special:
  assumes "unitary_gen M" and "mat_det M = 1"
  shows "∃ a b. M = (a, b, -cnj b, cnj a)"
proof-
  from assms
  obtain k where *: "k ≠ 0" "mat_adj M *mm M = k *sm eye"
    unfolding unitary_gen_def
    by auto
  hence "mat_det (mat_adj M *mm M) = k*k"
    by simp
  hence "k*k = 1"
    using assms(2)
    by (simp add: mat_det_adj)
  hence "k = 1 ∨ k = -1"
    using square_eq_1_iff[of k]
    by simp
  moreover
  have "mat_adj M = k *sm mat_inv M"
    using *
    using assms mult_mm_inv_r[of M "mat_adj M" "k *sm eye"] mat_eye_r mat_eye_l
    by simp (metis mult_sm_eye_mm *(2))
  moreover
  obtain a b c d where "M = (a, b, c, d)"
    by (cases M) auto
  ultimately
  have "M = (a, b, -cnj b, cnj a) ∨ M = (a, b, cnj b, -cnj a)"
    using assms(2)
    by (auto simp add: mat_adj_def mat_cnj_def)
  moreover
  have "Re (- (cor (cmod a))2 - (cor (cmod b))2) < 1"
    by (smt (verit) cmod_square complex_norm_square minus_complex.simps(1) of_real_power realpow_square_minus_le uminus_complex.simps(1))
  hence "- (cor (cmod a))2 - (cor (cmod b))2 ≠ 1"
    by force
  hence "M ≠ (a, b, cnj b, -cnj a)"
    using ‹mat_det M = 1› complex_mult_cnj_cmod[of a] complex_mult_cnj_cmod[of b]
    by auto
  ultimately
  show ?thesis
    by auto
qed

text ‹A characterization of all generalized unitary matrices›
lemma unitary_gen_iff:
  shows "unitary_gen M ⟷ 
         (∃ a b k. k ≠ 0 ∧ mat_det (a, b, -cnj b, cnj a) ≠ 0 ∧
                           M = k *sm (a, b, -cnj b, cnj a))" (is "?lhs = ?rhs")
proof
  assume ?lhs
  obtain d where *: "d*d = mat_det M"
    using ex_complex_sqrt
    by auto
  hence "d ≠ 0"
    using unitary_gen_regular[OF ‹unitary_gen M›]
    by auto
  from ‹unitary_gen M›
  obtain k where "k ≠ 0" "mat_adj M *mm M = k *sm eye"
    unfolding unitary_gen_def
    by auto
  hence "mat_adj ((1/d)*smM) *mm ((1/d)*smM) = (k / (d*cnj d)) *sm eye"
    by simp
  obtain a b where "(a, b, - cnj b, cnj a) = (1 / d) *sm M"
    using unitary_gen_special[of "(1 / d) *sm M"]  ‹unitary_gen M› *  unitary_gen_regular[of M] ‹d ≠ 0›
    by force
  moreover
  hence "mat_det (a, b, - cnj b, cnj a) ≠ 0"
    using unitary_gen_regular[OF ‹unitary_gen M›] ‹d ≠ 0›
    by auto
  ultimately
  show ?rhs
    apply (rule_tac x="a" in exI, rule_tac x="b" in exI, rule_tac x="d" in exI)
    using mult_sm_inv_l[of "1/d" M]
    by (auto simp add: field_simps)
next
  assume ?rhs
  then obtain a b k where "k ≠ 0 ∧ mat_det (a, b, - cnj b, cnj a) ≠ 0 ∧ M = k *sm (a, b, - cnj b, cnj a)"
    by auto
  thus ?lhs
    unfolding unitary_gen_def
    apply (auto simp add: mat_adj_def mat_cnj_def)
    using mult_eq_0_iff[of "cnj k * k" "cnj a * a + cnj b * b"]
    by (auto simp add: field_simps)
qed

text ‹A characterization of unitary matrices›

lemma unitary_iff:
  shows "unitary M ⟷
         (∃ a b k. (cmod a)2 + (cmod b)2 ≠ 0 ∧ 
                           (cmod k)2 = 1 / ((cmod a)2 + (cmod b)2) ∧
                           M = k *sm (a, b, -cnj b, cnj a))" (is "?lhs = ?rhs")
proof
  assume ?lhs
  obtain k a b where *: "M = k *sm (a, b, -cnj b, cnj a)" "k ≠ 0" "mat_det (a, b, -cnj b, cnj a) ≠ 0"
    using unitary_gen_iff  unitary_unitary_gen[OF ‹unitary M›]
    by auto

  have md: "mat_det (a, b, -cnj b, cnj a) = cor ((cmod a)2 + (cmod b)2)"
    by (auto simp add: complex_mult_cnj_cmod)

  have "k * cnj k * mat_det (a, b, -cnj b, cnj a) = 1"
    using ‹unitary M› *
    unfolding unitary_def
    by (auto simp add: mat_adj_def mat_cnj_def field_simps)
  hence "(cmod k)2 * ((cmod a)2 + (cmod b)2) = 1"
    by (metis (mono_tags, lifting) complex_norm_square md of_real_1 of_real_eq_iff of_real_mult)
  thus ?rhs
    using * mat_eye_l
    apply (rule_tac x="a" in exI, rule_tac x="b" in exI, rule_tac x="k" in exI)
    apply (auto simp add: complex_mult_cnj_cmod)
    by (metis ‹(cmod k)2 * ((cmod a)2 + (cmod b)2) = 1› mult_eq_0_iff nonzero_eq_divide_eq zero_neq_one)
next
  assume ?rhs
  then obtain a b k where  *: "(cmod a)2 + (cmod b)2 ≠ 0" "(cmod k)2 = 1 / ((cmod a)2 + (cmod b)2)" "M = k *sm (a, b, -cnj b, cnj a)"
    by auto
  have "(k * cnj k) * (a * cnj a) + (k * cnj k) * (b * cnj b) = 1"
    apply (subst complex_mult_cnj_cmod)+
    using *(1-2)
    by (metis (no_types, lifting) distrib_left nonzero_eq_divide_eq of_real_1 of_real_add of_real_divide of_real_eq_0_iff)
  thus ?lhs
    using *
    unfolding unitary_def
    by (simp add: mat_adj_def mat_cnj_def field_simps)
qed

end