Theory Multiplicative_Characters
section ‹Multiplicative Characters of Finite Abelian Groups›
theory Multiplicative_Characters
imports
Complex_Main
"Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups"
begin
notation integer_mod_group ("Z")
subsection ‹Definition of characters›
text ‹
A (multiplicative) character is a completely multiplicative function from a group to the
complex numbers. For simplicity, we restrict this to finite abelian groups here, which is
the most interesting case.
Characters form a group where the identity is the \emph{principal} character that maps all
elements to $1$, multiplication is point-wise multiplication of the characters, and the inverse
is the point-wise complex conjugate.
This group is often called the \emph{Pontryagin dual} group and is isomorphic to the original
group (in a non-natural way) while the double-dual group ∗‹is› naturally isomorphic to the
original group.
To get extensionality of the characters, we also require characters to map anything that is
not in the group to $0$.
›
definition principal_char :: "('a, 'b) monoid_scheme ⇒ 'a ⇒ complex" where
"principal_char G a = (if a ∈ carrier G then 1 else 0)"
definition inv_character where
"inv_character χ = (λa. cnj (χ a))"
lemma inv_character_principal [simp]: "inv_character (principal_char G) = principal_char G"
by (simp add: inv_character_def principal_char_def fun_eq_iff)
lemma inv_character_inv_character [simp]: "inv_character (inv_character χ) = χ"
by (simp add: inv_character_def)
lemma eval_inv_character: "inv_character χ j = cnj (χ j)"
by (simp add: inv_character_def)
bundle character_syntax
begin
notation principal_char ("χ⇩0ı")
end
locale character = finite_comm_group +
fixes χ :: "'a ⇒ complex"
assumes char_one_nz: "χ 𝟭 ≠ 0"
assumes char_eq_0: "a ∉ carrier G ⟹ χ a = 0"
assumes char_mult [simp]: "a ∈ carrier G ⟹ b ∈ carrier G ⟹ χ (a ⊗ b) = χ a * χ b"
begin
subsection ‹Basic properties›
lemma char_one [simp]: "χ 𝟭 = 1"
proof-
from char_mult[of 𝟭 𝟭] have "χ 𝟭 * (χ 𝟭 - 1) = 0"
by (auto simp del: char_mult)
with char_one_nz show ?thesis by simp
qed
lemma char_power [simp]: "a ∈ carrier G ⟹ χ (a [^] k) = χ a ^ k"
by (induction k) auto
lemma char_root:
assumes "a ∈ carrier G"
shows "χ a ^ ord a = 1"
proof -
from assms have "χ a ^ ord a = χ (a [^] ord a)"
by (subst char_power) auto
also from fin and assms have "a [^] ord a = 𝟭" by (intro pow_ord_eq_1) auto
finally show ?thesis by simp
qed
lemma char_root':
assumes "a ∈ carrier G"
shows "χ a ^ order G = 1"
proof -
from assms have "χ a ^ order G = χ (a [^] order G)" by simp
also from fin and assms have "a [^] order G = 𝟭" by (intro pow_order_eq_1) auto
finally show ?thesis by simp
qed
lemma norm_char: "norm (χ a) = (if a ∈ carrier G then 1 else 0)"
proof (cases "a ∈ carrier G")
case True
have "norm (χ a) ^ order G = norm (χ a ^ order G)" by (simp add: norm_power)
also from True have "χ a ^ order G = 1" by (rule char_root')
finally have "norm (χ a) ^ order G = 1 ^ order G" by simp
hence "norm (χ a) = 1" by (subst (asm) power_eq_iff_eq_base) auto
with True show ?thesis by auto
next
case False
thus ?thesis by (auto simp: char_eq_0)
qed
lemma char_eq_0_iff: "χ a = 0 ⟷ a ∉ carrier G"
proof -
have "χ a = 0 ⟷ norm (χ a) = 0" by simp
also have "… ⟷ a ∉ carrier G" by (subst norm_char) auto
finally show ?thesis .
qed
lemma inv_character: "character G (inv_character χ)"
by standard (auto simp: inv_character_def char_eq_0)
lemma mult_inv_character: "χ k * inv_character χ k = principal_char G k"
proof -
have "χ k * inv_character χ k = of_real (norm (χ k) ^ 2)"
by (subst complex_norm_square) (simp add: inv_character_def)
also have "… = principal_char G k"
by (simp add: principal_char_def norm_char)
finally show ?thesis .
qed
lemma
assumes "a ∈ carrier G"
shows char_inv: "χ (inv a) = cnj (χ a)" and char_inv': "χ (inv a) = inverse (χ a)"
proof -
from assms have "inv a ⊗ a = 𝟭" by simp
also have "χ … = 1" by simp
also from assms have "χ (inv a ⊗ a) = χ (inv a) * χ a"
by (intro char_mult) auto
finally have *: "χ (inv a) * χ a = 1" .
thus "χ (inv a) = inverse (χ a)" by (auto simp: divide_simps)
also from mult_inv_character[of a] and assms have "inverse (χ a) = cnj (χ a)"
by (auto simp add: inv_character_def principal_char_def divide_simps mult.commute)
finally show "χ (inv a) = cnj (χ a)" .
qed
end
lemma (in finite_comm_group) character_principal [simp, intro]: "character G (principal_char G)"
by standard (auto simp: principal_char_def)
lemmas [simp,intro] = finite_comm_group.character_principal
lemma character_ext:
assumes "character G χ" "character G χ'" "⋀x. x ∈ carrier G ⟹ χ x = χ' x"
shows "χ = χ'"
proof
fix x :: 'a
show "χ x = χ' x"
using assms by (cases "x ∈ carrier G") (auto simp: character.char_eq_0)
qed
lemma character_mult [intro]:
assumes "character G χ" "character G χ'"
shows "character G (λx. χ x * χ' x)"
proof -
interpret χ: character G χ by fact
interpret χ': character G χ' by fact
show ?thesis by standard (auto simp: χ.char_eq_0)
qed
lemma character_inv_character_iff [simp]: "character G (inv_character χ) ⟷ character G χ"
proof
assume "character G (inv_character χ)"
from character.inv_character [OF this] show "character G χ" by simp
qed (auto simp: character.inv_character)
definition characters :: "('a, 'b) monoid_scheme ⇒ ('a ⇒ complex) set" where
"characters G = {χ. character G χ}"
subsection ‹The Character group›
text ‹
The characters of a finite abelian group $G$ form another group $\widehat{G}$, which is called
its Pontryagin dual group. This generalises to the more general setting of locally compact
abelian groups, but we restrict ourselves to the finite setting because it is much easier.
›
definition Characters :: "('a, 'b) monoid_scheme ⇒ ('a ⇒ complex) monoid"
where "Characters G = ⦇ carrier = characters G, monoid.mult = (λχ⇩1 χ⇩2 k. χ⇩1 k * χ⇩2 k),
one = principal_char G ⦈"
lemma carrier_Characters: "carrier (Characters G) = characters G"
by (simp add: Characters_def)
lemma one_Characters: "one (Characters G) = principal_char G"
by (simp add: Characters_def)
lemma mult_Characters: "monoid.mult (Characters G) χ⇩1 χ⇩2 = (λa. χ⇩1 a * χ⇩2 a)"
by (simp add: Characters_def)
context finite_comm_group
begin
sublocale principal: character G "principal_char G" ..
lemma finite_characters [intro]: "finite (characters G)"
proof (rule finite_subset)
show "characters G ⊆ (λf x. if x ∈ carrier G then f x else 0) `
Pi⇩E (carrier G) (λ_. {z. z ^ order G = 1})" (is "_ ⊆ ?h ` ?Chars")
proof (intro subsetI, goal_cases)
case (1 χ)
then interpret χ: character G χ by (simp add: characters_def)
have "?h (restrict χ (carrier G)) ∈ ?h ` ?Chars"
by (intro imageI) (auto simp: χ.char_root')
also have "?h (restrict χ (carrier G)) = χ" by (simp add: fun_eq_iff χ.char_eq_0)
finally show ?case .
qed
show "finite (?h ` ?Chars)"
by (intro finite_imageI finite_PiE finite_roots_unity) (auto simp: Suc_le_eq)
qed
lemma finite_comm_group_Characters [intro]: "finite_comm_group (Characters G)"
proof
fix χ χ' assume *: "χ ∈ carrier (Characters G)" "χ' ∈ carrier (Characters G)"
from * interpret χ: character G χ by (simp_all add: characters_def carrier_Characters)
from * interpret χ': character G χ' by (simp_all add: characters_def carrier_Characters)
have "character G (λk. χ k * χ' k)"
by standard (insert *, simp_all add: χ.char_eq_0 one_Characters
mult_Characters characters_def carrier_Characters)
thus "χ ⊗⇘Characters G⇙ χ' ∈ carrier (Characters G)"
by (simp add: characters_def one_Characters mult_Characters carrier_Characters)
next
have "character G (principal_char G)" ..
thus "𝟭⇘Characters G⇙ ∈ carrier (Characters G)"
by (simp add: characters_def one_Characters mult_Characters carrier_Characters)
next
fix χ assume *: "χ ∈ carrier (Characters G)"
from * interpret χ: character G χ by (simp_all add: characters_def carrier_Characters)
show "𝟭⇘Characters G⇙ ⊗⇘Characters G⇙ χ = χ" and "χ ⊗⇘Characters G⇙ 𝟭⇘Characters G⇙ = χ"
by (simp_all add: principal_char_def fun_eq_iff χ.char_eq_0 one_Characters mult_Characters)
next
have "χ ∈ Units (Characters G)" if "χ ∈ carrier (Characters G)" for χ
proof -
from that interpret χ: character G χ by (simp add: characters_def carrier_Characters)
have "χ ⊗⇘Characters G⇙ inv_character χ = 𝟭⇘Characters G⇙" and
"inv_character χ ⊗⇘Characters G⇙ χ = 𝟭⇘Characters G⇙"
by (simp_all add: χ.mult_inv_character mult_ac one_Characters mult_Characters)
moreover from that have "inv_character χ ∈ carrier (Characters G)"
by (simp add: characters_def carrier_Characters)
ultimately show ?thesis using that unfolding Units_def by blast
qed
thus "carrier (Characters G) ⊆ Units (Characters G)" ..
qed (auto simp: principal_char_def one_Characters mult_Characters carrier_Characters)
end
lemma (in character) character_in_order_1:
assumes "order G = 1"
shows "χ = principal_char G"
proof -
from assms have "card (carrier G - {𝟭}) = 0"
by (subst card_Diff_subset) (auto simp: order_def)
hence "carrier G - {𝟭} = {}"
by (subst (asm) card_0_eq) auto
hence "carrier G = {𝟭}" by auto
thus ?thesis
by (intro ext) (simp_all add: principal_char_def char_eq_0)
qed
lemma (in finite_comm_group) characters_in_order_1:
assumes "order G = 1"
shows "characters G = {principal_char G}"
using character.character_in_order_1 [OF _ assms] by (auto simp: characters_def)
lemma (in character) inv_Characters: "inv⇘Characters G⇙ χ = inv_character χ"
proof -
interpret Characters: finite_comm_group "Characters G" ..
have "character G χ" ..
thus ?thesis
by (intro Characters.inv_equality)
(auto simp: characters_def mult_inv_character mult_ac
carrier_Characters one_Characters mult_Characters)
qed
lemma (in finite_comm_group) inv_Characters':
"χ ∈ characters G ⟹ inv⇘Characters G⇙ χ = inv_character χ"
by (intro character.inv_Characters) (auto simp: characters_def)
lemmas (in finite_comm_group) Characters_simps =
carrier_Characters mult_Characters one_Characters inv_Characters'
lemma inv_Characters': "χ ∈ characters G ⟹ inv⇘Characters G⇙ χ = inv_character χ"
using character.inv_Characters[of G χ] by (simp add: characters_def)
subsection ‹The isomorphism between a group and its dual›
text ‹We start this section by inspecting the special case of a cyclic group. Here, any character
is fixed by the value it assigns to the generating element of the cyclic group. This can then be
used to construct a bijection between the nth unit roots and the elements of the character group -
implying the other results.›
lemma (in finite_cyclic_group)
defines ic: "induce_char ≡ (λc::complex. (λa. if a∈carrier G then c powi get_exp gen a else 0))"
shows order_Characters: "order (Characters G) = order G"
and gen_fixes_char: "⟦character G a; character G b; a gen = b gen⟧ ⟹ a = b"
and unity_root_induce_char: "z ^ order G = 1 ⟹ character G (induce_char z)"
proof -
interpret C: finite_comm_group "Characters G" using finite_comm_group_Characters .
define n where "n = order G"
hence n: "n > 0" using order_gt_0 by presburger
from n_def have nog: "n = ord gen" using ord_gen_is_group_order by simp
have xnz: "x ≠ 0" if "x ^ n = 1" for x::complex using n(1) that by (metis zero_neq_one zero_power)
have m: "x powi m = x powi (m mod n)" if "x ^ n = 1" for x::complex and m::int
using powi_mod[OF that n] .
show cf: "character G (induce_char x)" if x: "x ^ n = 1" for x
proof
show "induce_char x 𝟭 ≠ 0" using xnz[OF that] unfolding ic by auto
show "induce_char x a = 0" if "a ∉ carrier G" for a using that unfolding ic by simp
show "induce_char x (a ⊗ b) = induce_char x a * induce_char x b"
if "a ∈ carrier G" "b ∈ carrier G" for a b
proof -
have "x powi get_exp gen (a ⊗ b) = x powi get_exp gen a * x powi get_exp gen b"
proof -
have "x powi get_exp gen (a ⊗ b) = x powi ((get_exp gen a + get_exp gen b) mod n)"
using m[OF x] get_exp_mult_mod[OF that] n_def ord_gen_is_group_order by metis
also have "… = x powi (get_exp gen a + get_exp gen b)" using m[OF x] by presburger
finally show ?thesis by (simp add: power_int_add xnz[OF x])
qed
thus ?thesis using that unfolding ic by simp
qed
qed
define get_c where gc: "get_c = (λc::'a ⇒ complex. c gen)"
have biji: "bij_betw induce_char {z. z ^ n = 1} (characters G)"
and bijg: "bij_betw get_c (characters G) {z. z ^ n = 1}"
proof (intro bij_betwI[of _ _ _ get_c])
show iin: "induce_char ∈ {z. z ^ n = 1} → characters G" using cf unfolding characters_def
by blast
show gi: "get_c (induce_char x) = x" if "x ∈ {z. z ^ n = 1}" for x
proof (cases "n = 1")
case True
with that have "x = 1" by force
thus ?thesis unfolding ic gc by simp
next
case False
have x: "x ^ n = 1" using that by blast
have "x powi get_exp gen gen = x"
proof -
have "x powi get_exp gen gen = x powi (get_exp gen gen mod n)" using m[OF x] by blast
moreover have "(get_exp gen gen mod n) = 1"
proof -
have "1 = 1 mod int n" using False n by auto
also have "… = get_exp gen gen mod n"
by (unfold nog, intro pow_eq_int_mod[OF gen_closed],
use get_exp_fulfills[OF gen_closed] in auto)
finally show ?thesis by argo
qed
ultimately show "x powi get_exp gen gen = x" by simp
qed
thus ?thesis unfolding ic gc by simp
qed
show gin: "get_c ∈ characters G → {z. z ^ n = 1}"
proof -
have "False" if "get_c c ^ n ≠ 1" "character G c" for c
proof -
interpret character G c by fact
show False using that(1)[unfolded gc] by (simp add: char_root' n_def)
qed
thus ?thesis unfolding characters_def by blast
qed
show ig: "induce_char (get_c y) = y" if y: "y ∈ characters G" for y
proof (cases "n = 1")
case True
hence "y = principal_char G" using y n_def character.character_in_order_1 characters_def
by auto
thus ?thesis unfolding ic gc principal_char_def by force
next
case False
have yc: "y ∈ carrier (Characters G)" using y[unfolded carrier_Characters[symmetric]] .
interpret character G y using that unfolding characters_def by simp
have ygo: "y gen ^ n = 1" using char_root'[OF gen_closed] n_def by blast
have "y gen powi get_exp gen a = y a" if "a ∈ carrier G" for a using that
proof(induction rule: generator_induct1)
case gen
have "y gen powi get_exp gen gen = y gen powi (get_exp gen gen mod n)"
using m[OF ygo] by blast
also have "… = y gen powi ((1::int) mod n)"
using get_exp_self[OF gen_closed] nog by argo
also have "… = y gen powi 1" using False n by simp
finally have yg: "y gen powi get_exp gen gen = y gen" by simp
thus ?case .
case (step x)
have "y gen powi get_exp gen (x ⊗ gen) = y gen powi (get_exp gen (x ⊗ gen) mod n)"
using m[OF ygo] by blast
also have "… = y gen powi ((get_exp gen x + get_exp gen gen) mod n)"
using get_exp_mult_mod[OF step(1) gen_closed, unfolded nog[symmetric]] by argo
also have "… = y gen powi (get_exp gen x + get_exp gen gen)" using m[OF ygo] by presburger
also have "… = y gen powi get_exp gen x * y gen powi get_exp gen gen"
by (simp add: char_eq_0_iff power_int_add)
also have "… = y x * y gen" using yg step(2) by argo
also have "… = y (x ⊗ gen)" using step(1) by simp
finally show ?case .
qed
thus "induce_char (get_c y) = y" unfolding ic gc using char_eq_0 by auto
qed
show "bij_betw get_c (characters G) {z. z ^ n = 1}" using ig gi iin gin
by (auto intro: bij_betwI)
qed
with card_roots_unity_eq[OF n] n_def show "order (Characters G) = order G" unfolding order_def
by (metis bij_betw_same_card carrier_Characters)
assume assm: "character G a" "character G b" "a gen = b gen"
with bijg[unfolded gc characters_def bij_betw_def inj_on_def] show "a = b" by auto
qed
text ‹Moreover, we can show that a character that assigns a "true" root of unity to the
generating element of the group, generates the character group.›
lemma (in finite_cyclic_group) finite_cyclic_group_Characters:
obtains χ where "finite_cyclic_group (Characters G) χ"
proof -
interpret C: finite_comm_group "Characters G" by (rule finite_comm_group_Characters)
define n where n: "n = order G"
hence nnz: "n ≠ 0" by blast
from n have nog: "n = ord gen" using ord_gen_is_group_order by simp
obtain x::complex where x: "x ^ n = 1" "⋀m. ⟦0<m; m<n⟧ ⟹ x ^ m ≠ 1"
using true_nth_unity_root by blast
have xnz: "x ≠ 0" using x n by (metis order_gt_0 zero_neq_one zero_power)
have m: "x powi m = x powi (m mod n)" for m::int
using powi_mod[OF x(1)] nnz by blast
let ?f = "(λa. if a ∈ carrier G then x powi (get_exp gen a) else 0)"
have cf: "character G ?f" using unity_root_induce_char[OF x(1)[unfolded n]] .
have fpow: "(?f [^]⇘Characters G⇙ m) a = x powi ((get_exp gen a) * m)"
if "a ∈ carrier G" for a::'a and m::nat
using that
proof(unfold Characters_def principal_char_def, induction m)
case s: (Suc m)
have "x powi (get_exp gen a * int m) * x powi get_exp gen a
= x powi (get_exp gen a * (1 + int m))"
proof -
fix ma :: nat
have "x powi ((1 + int ma) * get_exp gen a)
= x powi (get_exp gen a + int ma * get_exp gen a) ∧ 0 ≠ x"
by (simp add: comm_semiring_class.distrib xnz)
then show "x powi (get_exp gen a * int ma) * x powi get_exp gen a
= x powi (get_exp gen a * (1 + int ma))"
by (simp add: mult.commute power_int_add)
qed
thus ?case using s by simp
qed simp
interpret cyclic_group "Characters G" ?f
proof (intro C.element_ord_generates_cyclic)
show fc: "?f ∈ carrier (Characters G)" using cf carrier_Characters[of G] characters_def by fast
from x nnz have fno: "?f [^]⇘Characters G⇙ m ≠ 𝟭⇘Characters G⇙" if "0 < m" "m < n" for m
proof (cases "n = 1")
case False
have "𝟭⇘Characters G⇙ gen = 1" unfolding Characters_def principal_char_def using that by simp
moreover have "(?f [^]⇘Characters G⇙ m) gen ≠ 1"
proof -
have "(?f [^]⇘Characters G⇙ m) gen = x powi ((get_exp gen gen) * m)" using fpow by blast
also have "… = (x powi (get_exp gen gen)) ^ m" by (simp add: power_int_mult)
also have "… = x ^ m"
proof -
have "x powi (get_exp gen gen) = x powi ((get_exp gen gen) mod n)" using m by blast
moreover have "((get_exp gen gen) mod n) = 1"
proof -
have "1 = 1 mod int n" using False nnz by simp
also have "… = get_exp gen gen mod n"
by (unfold nog, intro pow_eq_int_mod[OF gen_closed],
use get_exp_fulfills[OF gen_closed] in auto)
finally show ?thesis by argo
qed
ultimately have "x powi (get_exp gen gen) = x" by simp
thus ?thesis by simp
qed
finally show ?thesis using x(2)[OF that] by argo
qed
ultimately show ?thesis by fastforce
qed (use that in blast)
have "C.ord ?f = n"
proof -
from nnz have "C.ord ?f ≤ n" unfolding n
using C.ord_dvd_group_order[OF fc] order_Characters dvd_nat_bounds by auto
with C.ord_conv_Least[OF fc] C.pow_order_eq_1[OF fc] n nnz show "C.ord ?f = n"
by (metis (no_types, lifting) C.ord_pos C.pow_ord_eq_1 fc fno le_neq_implies_less)
qed
thus "C.ord ?f = order (Characters G)" using n order_Characters by argo
qed
have "finite_cyclic_group (Characters G) ?f" by unfold_locales
with that show ?thesis by blast
qed
text ‹And as two cyclic groups of the same order are isomorphic it follows the isomorphism of a
finite cyclic group and its dual.›
lemma (in finite_cyclic_group) Characters_iso:
"G ≅ Characters G"
proof -
from finite_cyclic_group_Characters obtain f where f: "finite_cyclic_group (Characters G) f" .
then interpret C: finite_cyclic_group "Characters G" f .
have "cyclic_group (Characters G) f" by unfold_locales
from iso_cyclic_groups_same_order[OF this order_Characters[symmetric]] show ?thesis .
qed
text ‹The character groups of two isomorphic groups are also isomorphic.›
lemma (in finite_comm_group) iso_imp_iso_chars:
assumes "G ≅ H" "group H"
shows "Characters G ≅ Characters H"
proof -
interpret H: finite_comm_group H by (rule iso_imp_finite_comm[OF assms])
from assms have "H ≅ G" using iso_sym by auto
then obtain g where g: "g ∈ iso H G" unfolding is_iso_def by blast
then interpret ggh: group_hom H G g by (unfold_locales, unfold iso_def, simp)
let ?f = "(λc a. if a ∈ carrier H then (c ∘ g) a else 0)"
have "?f ∈ iso (Characters G) (Characters H)"
proof (intro isoI)
interpret CG: finite_comm_group "Characters G" by (intro finite_comm_group_Characters)
interpret CH: finite_comm_group "Characters H" by (intro H.finite_comm_group_Characters)
have f_in: "?f x ∈ carrier (Characters H)" if "x ∈ carrier (Characters G)" for x
proof (unfold carrier_Characters characters_def, rule, unfold_locales)
interpret character G x using that characters_def carrier_Characters by blast
show "(if 𝟭⇘H⇙ ∈ carrier H then (x ∘ g) 𝟭⇘H⇙ else 0) ≠ 0" using g iso_iff by auto
show "⋀a. a ∉ carrier H ⟹ (if a ∈ carrier H then (x ∘ g) a else 0) = 0" by simp
show "?f x (a ⊗⇘H⇙ b) = ?f x a * ?f x b" if "a ∈ carrier H" "b ∈ carrier H" for a b
using that by auto
qed
show "?f ∈ hom (Characters G) (Characters H)"
proof (intro homI)
show "?f x ∈ carrier (Characters H)" if "x ∈ carrier (Characters G)" for x
using f_in[OF that] .
show "?f (x ⊗⇘Characters G⇙ y) = ?f x ⊗⇘Characters H⇙ ?f y"
if "x ∈ carrier (Characters G)" "y ∈ carrier (Characters G)" for x y
proof -
interpret x: character G x using that characters_def carrier_Characters by blast
interpret y: character G y using that characters_def carrier_Characters by blast
show ?thesis using that mult_Characters[of G] mult_Characters[of H] by auto
qed
qed
show "bij_betw ?f (carrier (Characters G)) (carrier (Characters H))"
proof(intro bij_betwI)
define f where "f = inv_into (carrier H) g"
hence f: "f ∈ iso G H" using H.iso_set_sym[OF g] by simp
then interpret fgh: group_hom G H f by (unfold_locales, unfold iso_def, simp)
let ?g = "(λc a. if a ∈ carrier G then (c ∘ f) a else 0)"
show "?f ∈ carrier (Characters G) → carrier (Characters H)" using f_in by fast
show "?g ∈ carrier (Characters H) → carrier (Characters G)"
proof -
have g_in: "?g x ∈ carrier (Characters G)" if "x ∈ carrier (Characters H)" for x
proof (unfold carrier_Characters characters_def, rule, unfold_locales)
interpret character H x using that characters_def carrier_Characters by blast
show "(if 𝟭⇘G⇙ ∈ carrier G then (x ∘ f) 𝟭⇘G⇙ else 0) ≠ 0" using f iso_iff by auto
show "⋀a. a ∉ carrier G ⟹ (if a ∈ carrier G then (x ∘ f) a else 0) = 0" by simp
show "?g x (a ⊗⇘G⇙ b) = ?g x a * ?g x b" if "a ∈ carrier G" "b ∈ carrier G" for a b
using that by auto
qed
thus ?thesis by simp
qed
show "?f (?g x) = x" if x: "x ∈ carrier (Characters H)" for x
proof -
interpret character H x using x characters_def carrier_Characters by blast
have "?f (?g x) a = x a" if a: "a ∉ carrier H" for a using a char_eq_0[OF a] by auto
moreover have "?f (?g x) a = x a" if a: "a ∈ carrier H" for a
proof -
from a have "inv_into (carrier H) g (g a) = a"
by (simp add: g ggh.inj_iff_trivial_ker ggh.iso_kernel)
thus ?thesis using a f_def by auto
qed
ultimately show ?thesis by fast
qed
show "?g (?f x) = x" if x: "x ∈ carrier (Characters G)" for x
proof -
interpret character G x using x characters_def carrier_Characters by blast
have "?g (?f x) a = x a" if a: "a ∉ carrier G" for a using a char_eq_0[OF a] by auto
moreover have "?g (?f x) a = x a" if a: "a ∈ carrier G" for a using a f_def
proof -
from a have "g (inv_into (carrier H) g a) = a"
by (meson f_inv_into_f g ggh.iso_iff subset_iff)
thus ?thesis using a f_def fgh.hom_closed by auto
qed
ultimately show ?thesis by fast
qed
qed
qed
thus ?thesis unfolding is_iso_def by blast
qed
text ‹The following two lemmas characterize the way a character behaves in a direct group product:
a character on the product induces characters on each of the factors. Also, any character on the
direct product can be decomposed into a pointwise product of characters on the factors.›
lemma DirProds_subchar:
assumes "finite_comm_group (DirProds Gs I)"
and x: "x ∈ carrier (Characters (DirProds Gs I))"
and i: "i ∈ I"
and I: "finite I"
defines g: "g ≡ (λc. (λi∈I. (λa. c ((λi∈I. 𝟭⇘Gs i⇙)(i:=a)))))"
shows "character (Gs i) (g x i)"
proof -
interpret DP: finite_comm_group "DirProds Gs I" by fact
interpret xc: character "DirProds Gs I" x using x unfolding Characters_def characters_def by auto
interpret Gi: finite_comm_group "Gs i"
using i DirProds_finite_comm_group_iff[OF I] DP.finite_comm_group_axioms by blast
have allg: "⋀i. i∈I ⟹ group (Gs i)" using DirProds_group_imp_groups[OF DP.is_group] .
show ?thesis
proof(unfold_locales)
have "(λi∈I. 𝟭⇘Gs i⇙) = (λi∈I. 𝟭⇘Gs i⇙)(i := 𝟭⇘Gs i⇙)" using i by force
thus "g x i 𝟭⇘Gs i⇙ ≠ 0" using i g DirProds_one''[of Gs I] xc.char_one_nz by auto
show "g x i a = 0" if a: "a ∉ carrier (Gs i)" for a
proof -
from a i have "((λi∈I. 𝟭⇘Gs i⇙)(i := a)) ∉ carrier (DirProds Gs I)"
unfolding DirProds_def by force
from xc.char_eq_0[OF this] show ?thesis using i g by auto
qed
show "g x i (a ⊗⇘Gs i⇙ b) = g x i a * g x i b"
if ab: "a ∈ carrier (Gs i)" "b ∈ carrier (Gs i)" for a b
proof -
have "g x i (a ⊗⇘Gs i⇙ b)
= x ((λi∈I. 𝟭⇘Gs i⇙)(i := a) ⊗⇘DirProds Gs I⇙ (λi∈I. 𝟭⇘Gs i⇙)(i := b))"
proof -
have "((λi∈I. 𝟭⇘Gs i⇙)(i := a) ⊗⇘DirProds Gs I⇙ (λi∈I. 𝟭⇘Gs i⇙)(i := b))
= ((λi∈I. 𝟭⇘Gs i⇙)(i := (a ⊗⇘Gs i⇙ b)))"
proof -
have "((λi∈I. 𝟭⇘Gs i⇙)(i := a) ⊗⇘DirProds Gs I⇙ (λi∈I. 𝟭⇘Gs i⇙)(i := b)) j
= ((λi∈I. 𝟭⇘Gs i⇙)(i := (a ⊗⇘Gs i⇙ b))) j"
for j
proof (cases "j ∈ I")
case True
from allg[OF True] interpret Gj: group "Gs j" .
show ?thesis using ab True i unfolding DirProds_mult by simp
next
case False
then show ?thesis unfolding DirProds_mult using i by fastforce
qed
thus ?thesis by fast
qed
thus ?thesis using i g by auto
qed
also have "… = x ((λi∈I. 𝟭⇘Gs i⇙)(i := a)) * x ((λi∈I. 𝟭⇘Gs i⇙)(i := b))"
proof -
have ac: "((λi∈I. 𝟭⇘Gs i⇙)(i := a)) ∈ carrier (DirProds Gs I)"
unfolding DirProds_def using ab i monoid.one_closed[OF group.is_monoid[OF allg]] by force
have bc: "((λi∈I. 𝟭⇘Gs i⇙)(i := b)) ∈ carrier (DirProds Gs I)"
unfolding DirProds_def using ab i monoid.one_closed[OF group.is_monoid[OF allg]] by force
from xc.char_mult[OF ac bc] show ?thesis .
qed
also have "… = g x i a * g x i b" using i g by auto
finally show ?thesis .
qed
qed
qed
lemma Characters_DirProds_single_prod:
assumes "finite_comm_group (DirProds Gs I)"
and x: "x ∈ carrier (Characters (DirProds Gs I))"
and I: "finite I"
defines g: "g ≡ (λI. (λc. (λi∈I. (λa. c ((λi∈I. 𝟭⇘Gs i⇙)(i:=a))))))"
shows "(λe. if e∈carrier(DirProds Gs I) then ∏i∈I. (g I x i) (e i) else 0) = x" (is "?g x = x")
proof
show "?g x e = x e" for e
proof (cases "e ∈ carrier (DirProds Gs I)")
case True
show ?thesis using I x assms(1) True unfolding g
proof(induction I arbitrary: x e rule: finite_induct)
case empty
interpret DP: finite_comm_group "DirProds Gs {}" by fact
from DirProds_empty[of Gs] have "order (DirProds Gs {}) = 1" unfolding order_def by simp
with DP.characters_in_order_1[OF this] empty(1) show ?case
using DirProds_empty[of Gs] unfolding Characters_def principal_char_def by auto
next
case j: (insert j I)
interpret DP: finite_comm_group "DirProds Gs (insert j I)" by fact
interpret DP2: finite_comm_group "DirProds Gs I"
proof -
from DirProds_finite_comm_group_iff[of "insert j I" Gs] DP.finite_comm_group_axioms j
have "(∀i∈(insert j I). finite_comm_group (Gs i))" by blast
with DirProds_finite_comm_group_iff[OF j(1), of Gs] show "finite_comm_group (DirProds Gs I)"
by blast
qed
interpret xc: character "DirProds Gs (insert j I)" x
using j(4) unfolding Characters_def characters_def by simp
have allg: "⋀i. i∈(insert j I) ⟹ group (Gs i)"
using DirProds_group_imp_groups[OF DP.is_group] .
have e1c: "e(j:= 𝟭⇘Gs j⇙) ∈ carrier (DirProds Gs (insert j I))"
using j(6) monoid.one_closed[OF group.is_monoid[OF allg[of j]]]
unfolding DirProds_def PiE_def Pi_def by simp
have e2c: "(λi∈(insert j I). 𝟭⇘Gs i⇙)(j := e j) ∈ carrier (DirProds Gs (insert j I))"
unfolding DirProds_def PiE_def Pi_def
using monoid.one_closed[OF group.is_monoid[OF allg]] comp_in_carr[OF j(6)] by auto
have "e = e(j:= 𝟭⇘Gs j⇙) ⊗⇘DirProds Gs (insert j I)⇙ (λi∈(insert j I). 𝟭⇘Gs i⇙)(j := e j)"
proof -
have "e k
= (e(j:= 𝟭⇘Gs j⇙) ⊗⇘DirProds Gs (insert j I)⇙ (λi∈(insert j I). 𝟭⇘Gs i⇙)(j := e j)) k"
for k
proof(cases "k∈(insert j I)")
case k: True
from allg[OF k] interpret Gk: group "Gs k" .
from allg[of j] interpret Gj: group "Gs j" by simp
from k show ?thesis unfolding comp_mult[OF k] using comp_in_carr[OF j(6) k] by auto
next
case False
then show ?thesis using j(6) unfolding DirProds_def by auto
qed
thus ?thesis by blast
qed
hence "x e = x (e(j:= 𝟭⇘Gs j⇙)) * x ((λi∈(insert j I). 𝟭⇘Gs i⇙)(j := e j))"
using xc.char_mult[OF e1c e2c] by argo
also have "… = (∏i∈I. g (insert j I) x i (e i)) * g (insert j I) x j (e j)"
proof -
have "x (e(j:= 𝟭⇘Gs j⇙)) = (∏i∈I. g (insert j I) x i (e i))"
proof -
have eu: "e(j:=undefined) ∈ carrier (DirProds Gs I)" using j(2, 6)
unfolding DirProds_def PiE_def Pi_def extensional_def by fastforce
let ?x = "λp. if p∈carrier(DirProds Gs I) then x (p(j:= 𝟭⇘Gs j⇙)) else 0"
have cx2: "character (DirProds Gs I) ?x"
proof
show "?x 𝟭⇘DirProds Gs I⇙ ≠ 0"
proof -
have "𝟭⇘DirProds Gs I⇙(j := 𝟭⇘Gs j⇙) = 𝟭⇘DirProds Gs (insert j I)⇙"
unfolding DirProds_one'' by force
thus ?thesis by simp
qed
show "?x a = 0" if a: "a ∉ carrier (DirProds Gs I)" for a using a by argo
show "?x (a ⊗⇘DirProds Gs I⇙ b) = ?x a * ?x b"
if ab: "a ∈ carrier (DirProds Gs I)" "b ∈ carrier (DirProds Gs I)" for a b
proof -
have ac: "a(j := 𝟭⇘Gs j⇙) ∈ carrier (DirProds Gs (insert j I))"
using ab monoid.one_closed[OF group.is_monoid[OF allg[of j]]]
unfolding DirProds_def PiE_def Pi_def by simp
have bc: "b(j := 𝟭⇘Gs j⇙) ∈ carrier (DirProds Gs (insert j I))"
using ab monoid.one_closed[OF group.is_monoid[OF allg[of j]]]
unfolding DirProds_def PiE_def Pi_def by simp
have m: "((a ⊗⇘DirProds Gs I⇙ b)(j := 𝟭⇘Gs j⇙))
= (a(j := 𝟭⇘Gs j⇙) ⊗⇘DirProds Gs (insert j I)⇙ b(j := 𝟭⇘Gs j⇙))"
proof -
have "((a ⊗⇘DirProds Gs I⇙ b)(j := 𝟭⇘Gs j⇙)) h
= (a(j := 𝟭⇘Gs j⇙) ⊗⇘DirProds Gs (insert j I)⇙ b(j := 𝟭⇘Gs j⇙)) h"
if h: "h∈(insert j I)" for h
proof(cases "h=j")
case True
interpret Gj: group "Gs j" using allg[of j] by blast
from True comp_mult[OF h, of Gs "a(j := 𝟭⇘Gs j⇙)" "b(j := 𝟭⇘Gs j⇙)"] show ?thesis
by auto
next
case False
interpret Gj: group "Gs h" using allg[OF h] .
from False h comp_mult[OF h, of Gs "a(j := 𝟭⇘Gs j⇙)" "b(j := 𝟭⇘Gs j⇙)"]
comp_mult[of h I Gs a b]
show ?thesis by auto
qed
moreover have "((a ⊗⇘DirProds Gs I⇙ b)(j := 𝟭⇘Gs j⇙)) h
= (a(j := 𝟭⇘Gs j⇙) ⊗⇘DirProds Gs (insert j I)⇙ b(j := 𝟭⇘Gs j⇙)) h"
if h: "h∉(insert j I)" for h using h unfolding DirProds_def PiE_def by simp
ultimately show ?thesis by blast
qed
have "x ((a ⊗⇘DirProds Gs I⇙ b)(j := 𝟭⇘Gs j⇙))
= x (a(j := 𝟭⇘Gs j⇙)) * x (b(j := 𝟭⇘Gs j⇙))"
by (unfold m, intro xc.char_mult[OF ac bc])
thus ?thesis using ab by auto
qed
qed
then interpret cx2: character "DirProds Gs I" ?x .
from cx2 have cx3:"?x ∈ carrier (Characters (DirProds Gs I))"
unfolding Characters_def characters_def by simp
from j(3)[OF cx3 DP2.finite_comm_group_axioms eu] have
"(if e(j:=undefined) ∈ carrier (DirProds Gs I)
then ∏i∈I. g I ?x i ((e(j:=undefined)) i)
else 0) = ?x (e(j:=undefined))"
using eu j(2) unfolding g by fast
with eu have "(∏i∈I. g I (λp. if p ∈ carrier (DirProds Gs I)
then x (p(j := 𝟭⇘Gs j⇙))
else 0) i ((e(j := undefined)) i)) = x (e(j := 𝟭⇘Gs j⇙))"
by simp
moreover have "g I (λa. if a ∈ carrier (DirProds Gs I)
then x (a(j := 𝟭⇘Gs j⇙))
else 0) i ((e(j := undefined)) i) = g (insert j I) x i (e i)"
if i: "i∈I" for i
proof -
have "(λi∈I. 𝟭⇘Gs i⇙)(i := e i) ∈ carrier (DirProds Gs I)"
unfolding DirProds_def PiE_def Pi_def extensional_def
using monoid.one_closed[OF group.is_monoid[OF allg]] comp_in_carr[OF j(6)] i by simp
moreover have "((λi∈I. 𝟭⇘Gs i⇙)(i := e i, j := 𝟭⇘Gs j⇙))
= ((λi∈insert j I. 𝟭⇘Gs i⇙)(i := e i))" using i j(2) by auto
ultimately show ?thesis using i j(2, 4, 6) unfolding g by auto
qed
ultimately show ?thesis by simp
qed
moreover have "x ((λi∈(insert j I). 𝟭⇘Gs i⇙)(j := e j)) = g (insert j I) x j (e j)"
unfolding g by simp
ultimately show ?thesis by argo
qed
finally show ?case using j unfolding g by auto
qed
next
case False
interpret xc: character "DirProds Gs I" x
using x unfolding Characters_def characters_def by simp
from xc.char_eq_0[OF False] False show ?thesis by argo
qed
qed
text ‹This allows for the following: the character group of a direct product is isomorphic to the
direct product of the character groups of the factors.›
lemma (in finite_comm_group) Characters_DirProds_iso:
assumes "DirProds Gs I ≅ G" "group (DirProds Gs I)" "finite I"
shows "DirProds (Characters ∘ Gs) I ≅ Characters G"
proof -
interpret DP: group "DirProds Gs I" by fact
interpret DP: finite_comm_group "DirProds Gs I"
by (intro iso_imp_finite_comm[OF DP.iso_sym[OF assms(1)]], unfold_locales)
interpret DPC: finite_comm_group "DirProds (Characters ∘ Gs) I"
using DirProds_finite_comm_group_iff[OF assms(3), of "Characters ∘ Gs"]
DirProds_finite_comm_group_iff[OF assms(3), of Gs]
DP.finite_comm_group_axioms finite_comm_group.finite_comm_group_Characters by auto
interpret CDP: finite_comm_group "Characters (DirProds Gs I)"
using DP.finite_comm_group_Characters .
interpret C: finite_comm_group "Characters G" using finite_comm_group_Characters .
have allg: "⋀i. i∈I ⟹ group (Gs i)" using DirProds_group_imp_groups[OF assms(2)] .
let ?f = "(λcp. (λe. (if e∈carrier (DirProds Gs I) then ∏i∈I. cp i (e i) else 0)))"
have f_in: "?f x ∈ carrier (Characters (DirProds Gs I))"
if x: "x ∈ carrier (DirProds (Characters ∘ Gs) I)" for x
proof(unfold carrier_Characters characters_def, safe, unfold_locales)
show "?f x 𝟭⇘DirProds Gs I⇙ ≠ 0"
proof -
have "x i (𝟭⇘DirProds Gs I⇙ i) ≠ 0" if i: "i ∈ I" for i
proof -
interpret Gi: finite_comm_group "Gs i"
using DirProds_finite_comm_group_iff[OF assms(3)] DP.finite_comm_group_axioms i by blast
interpret xi: character "Gs i" "x i"
using i x unfolding DirProds_def Characters_def characters_def by auto
show ?thesis using DirProds_one'[OF i, of Gs] by simp
qed
thus ?thesis by (simp add: assms(3))
qed
show "?f x a = 0" if "a ∉ carrier (DirProds Gs I)" for a using that by simp
show "?f x (a ⊗⇘DirProds Gs I⇙ b) = ?f x a * ?f x b"
if ab: "a ∈ carrier (DirProds Gs I)" "b ∈ carrier (DirProds Gs I)" for a b
proof -
have "a ⊗⇘DirProds Gs I⇙ b ∈ carrier (DirProds Gs I)" using that by blast
moreover have "(∏i∈I. x i ((a ⊗⇘DirProds Gs I⇙ b) i))
= (∏i∈I. x i (a i)) * (∏i∈I. x i (b i))"
proof -
have "x i ((a ⊗⇘DirProds Gs I⇙ b) i) = x i (a i) * x i (b i)" if i: "i∈I" for i
proof -
interpret xi: character "Gs i" "x i"
using i x unfolding DirProds_def Characters_def characters_def by auto
show ?thesis using ab comp_mult[OF i, of Gs a b] by(auto simp: comp_in_carr[OF _ i])
qed
thus ?thesis using prod.distrib by force
qed
ultimately show ?thesis using that by auto
qed
qed
have "?f ∈ iso (DirProds (Characters ∘ Gs) I) (Characters (DirProds Gs I))"
proof (intro isoI)
show "?f ∈ hom (DirProds (Characters ∘ Gs) I) (Characters (DirProds Gs I))"
proof (intro homI)
show "?f x ∈ carrier (Characters (DirProds Gs I))"
if x: "x ∈ carrier (DirProds (Characters ∘ Gs) I)" for x using f_in[OF that] .
show "?f (x ⊗⇘DirProds (Characters ∘ Gs) I⇙ y) = ?f x ⊗⇘Characters (DirProds Gs I)⇙ ?f y"
if "x ∈ carrier (DirProds (Characters ∘ Gs) I)" "y ∈ carrier (DirProds (Characters ∘ Gs) I)"
for x y
proof -
have "?f x ⊗⇘Characters (DirProds Gs I)⇙ ?f y
= (λe. if e ∈ carrier (DirProds Gs I) then (∏i∈I. x i (e i)) * (∏i∈I. y i (e i)) else 0)"
unfolding Characters_def by auto
also have "… = ?f (x ⊗⇘DirProds (Characters ∘ Gs) I⇙ y)"
proof -
have "(∏i∈I. x i (e i)) * (∏i∈I. y i (e i))
= (∏i∈I. (x ⊗⇘DirProds (Characters ∘ Gs) I⇙ y) i (e i))" for e
unfolding DirProds_def Characters_def by (auto simp: prod.distrib)
thus ?thesis by presburger
qed
finally show ?thesis by argo
qed
qed
then interpret fgh: group_hom "DirProds (Characters ∘ Gs) I" "Characters (DirProds Gs I)" ?f
by (unfold_locales, simp)
show "bij_betw ?f (carrier (DirProds (Characters ∘ Gs) I)) (carrier (Characters (DirProds Gs I)))"
proof (intro bij_betwI)
let ?g = "(λc. (λi∈I. (λa. c ((λi∈I. 𝟭⇘Gs i⇙)(i:=a)))))"
have allc: "character (Gs i) (?g x i)"
if x: "x ∈ carrier (Characters (DirProds Gs I))" and i: "i ∈ I" for x i
using DirProds_subchar[OF DP.finite_comm_group_axioms x i assms(3)] .
have g_in: "?g x ∈ carrier (DirProds (Characters ∘ Gs) I)"
if x: "x ∈ carrier (Characters (DirProds Gs I))" for x
using allc[OF x] unfolding DirProds_def Characters_def characters_def by simp
show fi: "?f ∈ carrier (DirProds (Characters ∘ Gs) I) → carrier (Characters (DirProds Gs I))"
using f_in by fast
show gi: "?g ∈ carrier (Characters (DirProds Gs I)) → carrier (DirProds (Characters ∘ Gs) I)"
using g_in by fast
show "?f (?g x) = x" if x: "x ∈ carrier (Characters (DirProds Gs I))" for x
proof -
from x interpret x: character "DirProds Gs I" x unfolding Characters_def characters_def
by auto
from f_in[OF g_in[OF x]] interpret character "DirProds Gs I" "?f (?g x)"
unfolding Characters_def characters_def by simp
have "(∏i∈I. (λi∈I. λa. x ((λi∈I. 𝟭⇘Gs i⇙)(i := a))) i (e i)) = x e"
if e: "e ∈ carrier (DirProds Gs I)" for e
proof -
define y where y: "y = (λe. if e ∈ carrier (DirProds Gs I)
then ∏i∈I. (λi∈I. λa. x ((λi∈I. 𝟭⇘Gs i⇙)(i := a))) i (e i)
else 0)"
from Characters_DirProds_single_prod[OF DP.finite_comm_group_axioms x assms(3)]
have "y = x" using y by force
hence "y e = x e" by blast
thus ?thesis using e unfolding y by argo
qed
with x.char_eq_0 show ?thesis by force
qed
show "?g (?f x) = x" if x: "x ∈ carrier (DirProds (Characters ∘ Gs) I)" for x
proof(intro eq_parts_imp_eq[OF g_in[OF f_in[OF x]] x])
show "?g (?f x) i = x i" if i: "i∈I" for i
proof -
interpret xi: character "Gs i" "x i"
using x i unfolding DirProds_def Characters_def characters_def by auto
have "?g (?f x) i a = x i a" if a: "a∉carrier (Gs i)" for a
proof -
have "(λi∈I. 𝟭⇘Gs i⇙)(i := a) ∉ carrier (DirProds Gs I)"
using a i unfolding DirProds_def PiE_def Pi_def by auto
with xi.char_eq_0[OF a] a i show ?thesis by auto
qed
moreover have "?g (?f x) i a = x i a" if a: "a∈carrier (Gs i)" for a
proof -
have "(λi∈I. 𝟭⇘Gs i⇙)(i := a) ∈ carrier (DirProds Gs I)"
using a i monoid.one_closed[OF group.is_monoid[OF allg]]
unfolding DirProds_def by force
moreover have "(∏j∈I. x j (((λi∈I. 𝟭⇘Gs i⇙)(i := a)) j)) = x i a"
proof -
have "(∏j∈I. x j (((λi∈I. 𝟭⇘Gs i⇙)(i := a)) j))
= x i (((λi∈I. 𝟭⇘Gs i⇙)(i := a)) i) * (∏j∈I-{i}. x j (((λi∈I. 𝟭⇘Gs i⇙)(i := a)) j))"
by (meson assms(3) i prod.remove)
moreover have "x j (((λi∈I. 𝟭⇘Gs i⇙)(i := a)) j) = 1" if j: "j∈I" "j ≠ i" for j
proof -
interpret xj: character "Gs j" "x j"
using j(1) x unfolding DirProds_def Characters_def characters_def by auto
show ?thesis using j by auto
qed
moreover have "x i (((λi∈I. 𝟭⇘Gs i⇙)(i := a)) i) = x i a" by simp
ultimately show ?thesis by auto
qed
ultimately show ?thesis using a i by simp
qed
ultimately show ?thesis by blast
qed
qed
qed
qed
hence "DirProds (Characters ∘ Gs) I ≅ Characters (DirProds Gs I)" unfolding is_iso_def by blast
moreover have "Characters (DirProds Gs I) ≅ Characters G"
using DP.iso_imp_iso_chars[OF assms(1) is_group] .
ultimately show ?thesis using iso_trans by blast
qed
text ‹As thus both the group and its character group can be decomposed into the same cyclic factors,
the isomorphism follows for any finite abelian group.›
theorem (in finite_comm_group) Characters_iso:
shows "G ≅ Characters G"
proof -
from cyclic_product obtain ns
where ns: "DirProds (λn. Z (ns ! n)) {..<length ns} ≅ G" "∀n∈set ns. n ≠ 0" .
interpret DP: group "DirProds (λn. Z (ns ! n)) {..<length ns}"
by (intro DirProds_is_group, auto)
have "G ≅ DirProds (λn. Z (ns ! n)) {..<length ns}" using DP.iso_sym[OF ns(1)] .
moreover have "DirProds (Characters ∘ (λn. Z (ns ! n))) {..<length ns} ≅ Characters G"
by (intro Characters_DirProds_iso[OF ns(1) DirProds_is_group], auto)
moreover have "DirProds (λn. Z (ns ! n)) {..<length ns}
≅ DirProds (Characters ∘ (λn. Z (ns ! n))) {..<length ns}"
proof (intro DirProds_iso1)
fix i assume i: "i ∈ {..<length ns}"
obtain a where "cyclic_group (Z (ns!i)) a" using Zn_cyclic_group .
then interpret Zi: cyclic_group "Z (ns!i)" a .
interpret Zi: finite_cyclic_group "Z (ns!i)" a
proof
have "order (Z (ns ! i)) ≠ 0" using ns(2) i Zn_order by simp
thus "finite (carrier (Z (ns ! i)))" unfolding order_def by (simp add: card_eq_0_iff)
qed
show "Group.group ((Characters ∘ (λn. Z (ns ! n))) i)"
"Group.group (Z (ns ! i))" "Z (ns ! i) ≅ (Characters ∘ (λn. Z (ns ! n))) i"
using Zi.Characters_iso Zi.finite_comm_group_Characters comm_group_def finite_comm_group_def
by auto
qed
ultimately show ?thesis by (auto elim: iso_trans)
qed
text ‹Hence, the orders are also equal.›
corollary (in finite_comm_group) order_Characters:
"order (Characters G) = order G"
using iso_same_card[OF Characters_iso] unfolding order_def by argo
corollary (in finite_comm_group) card_characters: "card (characters G) = order G"
using order_Characters unfolding order_def Characters_def by simp
subsection ‹Non-trivial facts about characters›
text ‹We characterize the character group of a quotient group as the group of characters that map
all elements of the subgroup onto $1$.›
lemma (in finite_comm_group) iso_Characters_FactGroup:
assumes H: "subgroup H G"
shows "(λχ x. if x ∈ carrier G then χ (H #> x) else 0) ∈
iso (Characters (G Mod H)) ((Characters G)⦇carrier := {χ∈characters G. ∀x∈H. χ x = 1}⦈)"
proof -
interpret H: normal H G using subgroup_imp_normal[OF H] .
interpret Chars: finite_comm_group "Characters G"
by (rule finite_comm_group_Characters)
interpret Fact: comm_group "G Mod H"
by (simp add: H.subgroup_axioms comm_group.abelian_FactGroup comm_group_axioms)
interpret Fact: finite_comm_group "G Mod H"
by unfold_locales (auto simp: carrier_FactGroup)
define C :: "('a ⇒ complex) set" where "C = {χ∈characters G. ∀x∈H. χ x = 1}"
interpret C: subgroup C "Characters G"
proof (unfold_locales, goal_cases)
case 1
thus ?case
by (auto simp: C_def one_Characters mult_Characters carrier_Characters characters_def)
next
case 2
thus ?case
by (auto simp: C_def one_Characters mult_Characters carrier_Characters characters_def)
next
case 3
thus ?case
by (auto simp: C_def one_Characters mult_Characters
carrier_Characters characters_def principal_char_def)
next
case (4 χ)
hence "inv⇘Characters G⇙ χ = inv_character χ"
by (subst inv_Characters') (auto simp: C_def carrier_Characters)
moreover have "inv_character χ ∈ characters G"
using 4 by (auto simp: C_def characters_def)
moreover have "∀x∈H. inv_character χ x = 1"
using 4 by (auto simp: C_def inv_character_def)
ultimately show ?case
by (auto simp: C_def)
qed
define f :: "('a set ⇒ complex) ⇒ ('a ⇒ complex)"
where "f = (λχ x. if x ∈ carrier G then χ (H #> x) else 0)"
have [intro]: "character G (f χ)" if "character (G Mod H) χ" for χ
proof -
interpret character "G Mod H" χ by fact
show ?thesis
proof (unfold_locales, goal_cases)
case 1
thus ?case by (auto simp: f_def char_eq_0_iff carrier_FactGroup)
next
case (2 x)
thus ?case by (auto simp: f_def)
next
case (3 x y)
have "χ (H #> x) * χ (H #> y) = χ ((H #> x) ⊗⇘G Mod H⇙ (H #> y))"
using 3 by (intro char_mult [symmetric]) (auto simp: carrier_FactGroup)
also have "(H #> x) ⊗⇘G Mod H⇙ (H #> y) = H #> (x ⊗ y)"
using 3 by (simp add: H.rcos_sum)
finally show ?case
using 3 by (simp add: f_def)
qed
qed
have [intro]: "f χ ∈ C" if "character (G Mod H) χ" for χ
proof -
interpret χ: character "G Mod H" χ
by fact
have "character G (f χ)"
using χ.character_axioms by auto
moreover have "χ (H #> x) = 1" if "x ∈ H" for x
using that H.rcos_const χ.char_one by force
ultimately show ?thesis
by (auto simp: carrier_Characters C_def characters_def f_def)
qed
show "f ∈ iso (Characters (G Mod H)) ((Characters G)⦇carrier := C⦈)"
proof (rule isoI)
show "f ∈ hom (Characters (G Mod H)) (Characters G⦇carrier := C⦈)"
proof (rule homI, goal_cases)
case (1 χ)
thus ?case
by (auto simp: carrier_Characters characters_def)
qed (auto simp: f_def carrier_Characters fun_eq_iff mult_Characters)
next
have "bij_betw f (characters (G Mod H)) C"
unfolding bij_betw_def
proof
show inj: "inj_on f (characters (G Mod H))"
proof (rule inj_onI, goal_cases)
case (1 χ1 χ2)
interpret χ1: character "G Mod H" χ1
using 1 by (auto simp: characters_def)
interpret χ2: character "G Mod H" χ2
using 1 by (auto simp: characters_def)
have "χ1 H' = χ2 H'" for H'
proof (cases "H' ∈ carrier (G Mod H)")
case False
thus ?thesis by (simp add: χ1.char_eq_0 χ2.char_eq_0)
next
case True
then obtain x where x: "x ∈ carrier G" "H' = H #> x"
by (auto simp: carrier_FactGroup)
from 1 have "f χ1 x = f χ2 x"
by simp
with x show ?thesis
by (auto simp: f_def)
qed
thus "χ1 = χ2" by force
qed
have "f ` characters (G Mod H) ⊆ C"
by (auto simp: characters_def)
moreover have "C ⊆ f ` characters (G Mod H)"
proof safe
fix χ assume χ: "χ ∈ C"
from χ interpret character G χ
by (auto simp: C_def characters_def)
have [simp]: "χ x = 1" if "x ∈ H" for x
using χ that by (auto simp: C_def)
have "∀H'∈carrier (G Mod H). ∃x∈carrier G. H' = H #> x"
by (auto simp: carrier_FactGroup)
then obtain h where h: "h H' ∈ carrier G" "H' = H #> h H'" if "H' ∈ carrier (G Mod H)" for H'
by metis
define χ' where "χ' = (λH'. if H' ∈ carrier (G Mod H) then χ (h H') else 0)"
have χ_cong: "χ x = χ y" if "H #> x = H #> y" "x ∈ carrier G" "y ∈ carrier G" for x y
proof -
have "x ∈ H #> x"
by (simp add: H.subgroup_axioms rcos_self that(2))
also have "… = H #> y"
by fact
finally obtain z where z: "z ∈ H" "x = z ⊗ y"
unfolding r_coset_def by auto
thus ?thesis
using z H.subset that by simp
qed
have "character (G Mod H) χ'"
proof (unfold_locales, goal_cases)
case 1
have H: "H ∈ carrier (G Mod H)"
using Fact.one_closed unfolding one_FactGroup .
with h[of H] have "h H ∈ carrier G"
by blast
thus ?case using H
by (auto simp: char_eq_0_iff χ'_def)
next
case (2 H')
thus ?case by (auto simp: χ'_def)
next
case (3 H1 H2)
from 3 have H12: "H1 <#> H2 ∈ carrier (G Mod H)"
using Fact.m_closed by force
have "χ (h (H1 <#> H2)) = χ (h H1 ⊗ h H2)"
proof (rule χ_cong)
show "H #> h (H1 <#> H2) = H #> (h H1 ⊗ h H2)"
by (metis "3" H.rcos_sum H12 h)
qed (use 3 h[of H1] h[of H2] h[OF H12] in auto)
thus ?case
using 3 H12 h[of H1] h[of H2] by (auto simp: χ'_def)
qed
moreover have "f χ' x = χ x" for x
proof (cases "x ∈ carrier G")
case False
thus ?thesis
by (auto simp: f_def χ'_def char_eq_0_iff)
next
case True
hence *: "H #> x ∈ carrier (G Mod H)"
by (auto simp: carrier_FactGroup)
have "χ (h (H #> x)) = χ x"
using True * h[of "H #> x"] by (intro χ_cong) auto
thus ?thesis
using True * by (auto simp: f_def fun_eq_iff χ'_def)
qed
hence "f χ' = χ" by force
ultimately show "χ ∈ f ` characters (G Mod H)"
unfolding characters_def by blast
qed
ultimately show "f ` characters (G Mod H) = C"
by blast
qed
thus "bij_betw f (carrier (Characters (G Mod H))) (carrier (Characters G⦇carrier := C⦈))"
by (simp add: carrier_Characters)
qed
qed
lemma (in finite_comm_group) is_iso_Characters_FactGroup:
assumes H: "subgroup H G"
shows "Characters (G Mod H) ≅ (Characters G)⦇carrier := {χ∈characters G. ∀x∈H. χ x = 1}⦈"
using iso_Characters_FactGroup[OF assms] unfolding is_iso_def by blast
text ‹In order to derive the number of extensions a character on a subgroup has to the entire group,
we introduce the group homomorphism ‹restrict_char› that restricts a character to a given subgroup ‹H›.›
definition restrict_char::"'a set ⇒ ('a ⇒ complex) ⇒ ('a ⇒ complex) " where
"restrict_char H χ = (λe. if e∈H then χ e else 0)"
lemma (in finite_comm_group) restrict_char_hom:
assumes "subgroup H G"
shows "group_hom (Characters G) (Characters (G⦇carrier := H⦈)) (restrict_char H)"
proof -
let ?CG = "Characters G"
let ?H = "G⦇carrier := H⦈"
let ?CH = "Characters ?H"
interpret H: subgroup H G by fact
interpret H: finite_comm_group ?H by (simp add: assms subgroup_imp_finite_comm_group)
interpret CG: finite_comm_group ?CG using finite_comm_group_Characters .
interpret CH: finite_comm_group ?CH using H.finite_comm_group_Characters .
show ?thesis
proof(unfold_locales, intro homI)
show "restrict_char H x ∈ carrier ?CH" if x: "x ∈ carrier ?CG" for x
proof -
interpret xc: character G x using x unfolding Characters_def characters_def by simp
have "character ?H (restrict_char H x)"
by (unfold restrict_char_def, unfold_locales, auto)
thus ?thesis unfolding Characters_def characters_def by simp
qed
show "restrict_char H (x ⊗⇘?CG⇙ y) = restrict_char H x ⊗⇘?CH⇙ restrict_char H y"
if x: "x ∈ carrier ?CG" and y: "y ∈ carrier ?CG" for x y
proof -
interpret xc: character G x using x unfolding Characters_def characters_def by simp
interpret yc: character G y using y unfolding Characters_def characters_def by simp
show ?thesis unfolding Characters_def restrict_char_def by auto
qed
qed
qed
text ‹The kernel is just the set of the characters that are $1$ on all of ‹H›.›
lemma (in finite_comm_group) restrict_char_kernel:
assumes "subgroup H G"
shows "kernel (Characters G) (Characters (G⦇carrier := H⦈)) (restrict_char H)
= {χ∈characters G. ∀x∈H. χ x = 1}"
by (unfold restrict_char_def kernel_def one_Characters
carrier_Characters principal_char_def characters_def, simp, metis)
text ‹Also, all of the characters on the subgroup are the image of some character on the whole group.›
lemma (in finite_comm_group) restrict_char_image:
assumes "subgroup H G"
shows "restrict_char H ` (carrier (Characters G)) = carrier (Characters (G⦇carrier := H⦈))"
proof -
interpret H: subgroup H G by fact
interpret H: finite_comm_group "G⦇carrier := H⦈" using subgroup_imp_finite_comm_group[OF assms] .
interpret r: group_hom "Characters G" "Characters (G⦇carrier := H⦈)" "restrict_char H"
using restrict_char_hom[OF assms] .
interpret Mod: finite_comm_group "G Mod H" using finite_comm_FactGroup[OF assms] .
interpret CG: finite_comm_group "Characters G" using finite_comm_group_Characters .
have c1: "order (Characters (G⦇carrier := H⦈)) = card H" using H.order_Characters
unfolding order_def by simp
have "card H * card (kernel (Characters G) (Characters (G⦇carrier := H⦈)) (restrict_char H))
= order G"
using restrict_char_kernel[OF assms] iso_same_card[OF is_iso_Characters_FactGroup[OF assms]]
Mod.order_Characters lagrange[OF assms] unfolding order_def FactGroup_def
by (force simp: algebra_simps)
moreover have "card (kernel (Characters G) (Characters (G⦇carrier := H⦈)) (restrict_char H)) ≠ 0"
using r.one_in_kernel unfolding kernel_def CG.fin by auto
ultimately have c2: "card H = card (restrict_char H ` carrier (Characters G))"
using r.image_kernel_product[unfolded order_Characters] by (metis mult_right_cancel)
have "restrict_char H ` (carrier (Characters G)) ⊆ carrier (Characters (G⦇carrier := H⦈))"
by auto
with c2 H.fin show ?thesis
by (auto, metis H.finite_imp_card_positive c1 card_subset_eq fin_gen
order_def r.H.order_gt_0_iff_finite)
qed
text ‹
It follows that any character on ‹H› can be extended
to a character on ‹G›.
›
lemma (in finite_comm_group) character_extension_exists:
assumes "subgroup H G" "character (G⦇carrier := H⦈) χ"
obtains χ' where "character G χ'" and "⋀x. x ∈ H ⟹ χ' x = χ x"
proof -
from restrict_char_image[OF assms(1)] assms(2) obtain χ'
where chi': "restrict_char H χ' = χ" "character G χ'"
by (force simp: carrier_Characters characters_def)
thus ?thesis using that restrict_char_def by metis
qed
text ‹For two characters on a group ‹G› the number of characters on subgroup ‹H› that share the
values with them is the same for both.›
lemma (in finite_comm_group) character_restrict_card:
assumes "subgroup H G" "character G a" "character G b"
shows "card {χ'∈characters G. ∀x∈H. χ' x = a x} = card {χ'∈characters G. ∀x∈H. χ' x = b x}"
proof -
interpret H: subgroup H G by fact
interpret H: finite_comm_group "G⦇carrier := H⦈" using assms(1)
by (simp add: subgroup_imp_finite_comm_group)
interpret CG: finite_comm_group "Characters G" using finite_comm_group_Characters .
interpret a: character G a by fact
interpret b: character G b by fact
have ac: "a ∈ carrier (Characters G)" unfolding Characters_def characters_def using assms by simp
have bc: "b ∈ carrier (Characters G)" unfolding Characters_def characters_def using assms by simp
define f where f: "f = (λc. b ⊗⇘Characters G⇙ inv⇘Characters G⇙ a ⊗⇘Characters G⇙ c)"
define g where g: "g = (λc. a ⊗⇘Characters G⇙ inv⇘Characters G⇙ b ⊗⇘Characters G⇙ c)"
let ?A = "{χ'∈characters G. ∀x∈H. χ' x = a x}"
let ?B = "{χ'∈characters G. ∀x∈H. χ' x = b x}"
have "bij_betw f ?A ?B"
proof(intro bij_betwI[of _ _ _ g])
show "f ∈ ?A → ?B"
proof
show "f x ∈ ?B" if x: "x ∈ ?A" for x
proof -
interpret xc: character G x using x unfolding characters_def by blast
have xc: "x ∈ carrier (Characters G)" using x unfolding Characters_def by simp
have "f x y = b y" if y: "y ∈ H" for y
proof -
have "(inv⇘Characters G⇙ a) y * a y = 1"
by (simp add: a.inv_Characters a.mult_inv_character mult.commute principal_char_def y)
thus ?thesis unfolding f mult_Characters using x y by fastforce
qed
thus "f x ∈ ?B" unfolding f carrier_Characters[symmetric] using ac bc xc by blast
qed
qed
show "g ∈ ?B → ?A"
proof
show "g x ∈ ?A" if x: "x ∈ ?B" for x
proof -
interpret xc: character G x using x unfolding characters_def by blast
have xc: "x ∈ carrier (Characters G)" using x unfolding Characters_def by simp
have "g x y = a y" if y: "y ∈ H" for y
proof -
have "(inv⇘Characters G⇙ b) y * x y = 1" using x y
by (simp add: b.inv_Characters b.mult_inv_character mult.commute principal_char_def)
thus ?thesis unfolding g mult_Characters by simp
qed
thus "g x ∈ ?A" unfolding g carrier_Characters[symmetric] using ac bc xc by blast
qed
qed
show "g (f x) = x" if x: "x ∈ ?A" for x
proof -
have xc: "x ∈ carrier (Characters G)" using x unfolding Characters_def by force
with ac bc show ?thesis unfolding f g
by (auto simp: CG.m_assoc[symmetric],
metis CG.inv_closed CG.inv_comm CG.l_inv CG.m_assoc CG.r_one)
qed
show "f (g x) = x" if x: "x ∈ ?B" for x
proof -
have xc: "x ∈ carrier (Characters G)" using x unfolding Characters_def by force
with ac bc show ?thesis unfolding f g
by (auto simp: CG.m_assoc[symmetric],
metis CG.inv_closed CG.inv_comm CG.l_inv CG.m_assoc CG.r_one)
qed
qed
thus ?thesis using bij_betw_same_card by blast
qed
text ‹These lemmas allow to show that the number of extensions of a character on ‹H› to a
character on ‹G› is just $|G|/|H|$.›
theorem (in finite_comm_group) card_character_extensions:
assumes "subgroup H G" "character (G⦇carrier := H⦈) χ"
shows "card {χ'∈characters G. ∀x∈H. χ' x = χ x} * card H = order G"
proof -
interpret H: subgroup H G by fact
interpret H: finite_comm_group "G⦇carrier := H⦈"
using subgroup_imp_finite_comm_group[OF assms(1)] .
interpret chi: character "G⦇carrier := H⦈" χ by fact
interpret C: finite_comm_group "Characters G" using finite_comm_group_Characters .
interpret Mod: finite_comm_group "G Mod H" using finite_comm_FactGroup[OF assms(1)] .
obtain a where a: "a ∈ carrier (Characters G)" "restrict_char H a = χ"
proof -
have "∃a∈carrier (Characters G). restrict_char H a = χ"
using restrict_char_image[OF assms(1)] assms(2)
unfolding carrier_Characters characters_def image_def by force
thus ?thesis using that by blast
qed
show ?thesis
proof -
have p: "{χ∈characters G. ∀x∈H. χ x = 1} = {χ∈characters G. ∀x∈H. χ x = principal_char G x}"
unfolding principal_char_def by force
have ac: "{χ'∈characters G. ∀x∈H. χ' x = χ x} = {χ'∈characters G. ∀x∈H. χ' x = a x}"
using a(2) unfolding restrict_char_def by force
have "card {χ∈characters G. ∀x∈H. χ x = 1} = card {χ'∈characters G. ∀x∈H. χ' x = χ x}"
by (unfold ac p; intro character_restrict_card[OF assms(1)],
use a[unfolded Characters_def characters_def] in auto)
moreover have "card {χ∈characters G. ∀x∈H. χ x = 1} = card (carrier (G Mod H))"
using iso_same_card[OF is_iso_Characters_FactGroup[OF assms(1)]]
Mod.order_Characters[unfolded order_def] by force
moreover have "card (carrier (G Mod H)) * card H = order G"
using lagrange[OF assms(1)] unfolding FactGroup_def by simp
ultimately show ?thesis by argo
qed
qed
text ‹
Lastly, we can also show that for each $x\in H$ of order $n > 1$ and each ‹n›-th root of
unity ‹z›, there exists a character ‹χ› on ‹G› such that $\chi(x) = z$.
›
lemma (in group) powi_get_exp_self:
fixes z::complex
assumes "z ^ n = 1" "x ∈ carrier G" "ord x = n" "n > 1"
shows "z powi get_exp x x = z"
proof -
from assms have ngt0: "n > 0" by simp
from powi_mod[OF assms(1) ngt0, of "get_exp x x"] get_exp_self[OF assms(2), unfolded assms(3)]
have "z powi get_exp x x = z powi (1 mod int n)" by argo
also have "… = z" using assms(4) by simp
finally show ?thesis .
qed
corollary (in finite_comm_group) character_with_value_exists:
assumes "x ∈ carrier G" and "x ≠ 𝟭" and "z ^ ord x = 1"
obtains χ where "character G χ" and "χ x = z"
proof -
interpret H: subgroup "generate G {x}" G using generate_is_subgroup assms(1) by simp
interpret H: finite_comm_group "G⦇carrier := generate G {x}⦈"
using subgroup_imp_finite_comm_group[OF H.subgroup_axioms] .
interpret H: finite_cyclic_group "G⦇carrier := generate G {x}⦈" x
proof(unfold finite_cyclic_group_def, safe)
show "finite_group (G⦇carrier := generate G {x}⦈)" by unfold_locales
show "cyclic_group (G⦇carrier := generate G {x}⦈) x"
proof(intro H.cyclic_groupI0)
show "x ∈ carrier (G⦇carrier := generate G {x}⦈)" using generate.incl[of x "{x}" G] by simp
show "carrier (G⦇carrier := generate G {x}⦈) = generate (G⦇carrier := generate G {x}⦈) {x}"
using generate_consistent[OF generate_sincl H.subgroup_axioms] by simp
qed
qed
have ox: "H.ord x = ord x" using H.gen_closed H.subgroup_axioms subgroup_ord_eq by auto
have ogt1: "ord x > 1" using ord_pos by (metis assms(1, 2) less_one nat_neq_iff ord_eq_1)
from assms H.unity_root_induce_char[unfolded H.ord_gen_is_group_order[symmetric] ox, OF assms(3)]
obtain c where c: "character (G⦇carrier := generate G {x}⦈) c"
"c = (λa. if a ∈ carrier (G⦇carrier := generate G {x}⦈)
then z powi H.get_exp x a else 0)" by blast
have cx: "c x = z" unfolding c(2)
using H.powi_get_exp_self[OF assms(3) _ ox ogt1] generate_sincl[of "{x}"] by simp
obtain f where f: "character G f" "⋀y. y ∈ (generate G {x}) ⟹ f y = c y"
using character_extension_exists[OF H.subgroup_axioms c(1)] by blast
show ?thesis by (intro that[OF f(1)], use cx f(2) generate_sincl in blast)
qed
text ‹
In particular, for any ‹x› that is not the identity element, there exists a character ‹χ›
such that $\chi(x)\neq 1$.
›
corollary (in finite_comm_group) character_neq_1_exists:
assumes "x ∈ carrier G" and "x ≠ 𝟭"
obtains χ where "character G χ" and "χ x ≠ 1"
proof -
define z where "z = cis (2 * pi / ord x)"
have z_pow_h: "z ^ ord x = 1"
by (auto simp: z_def DeMoivre)
from assms have "ord x ≥ 1" by (intro ord_ge_1) auto
moreover have "ord x ≠ 1"
using pow_ord_eq_1[of x] assms fin by (intro notI) simp_all
ultimately have "ord x > 1" by linarith
have [simp]: "z ≠ 1"
proof
assume "z = 1"
have "bij_betw (λk. cis (2 * pi * real k / real (ord x))) {..<ord x} {z. z ^ ord x = 1}"
using ‹ord x > 1› by (intro bij_betw_roots_unity) auto
hence inj: "inj_on (λk. cis (2 * pi * real k / real (ord x))) {..<ord x}"
by (auto simp: bij_betw_def)
have "0 = (1 :: nat)"
using ‹z = 1› and ‹ord x > 1› by (intro inj_onD[OF inj]) (auto simp: z_def)
thus False by simp
qed
obtain χ where "character G χ" and "χ x = z"
using character_with_value_exists[OF assms z_pow_h] .
thus ?thesis using that[of χ] by simp
qed
subsection ‹The first orthogonality relation›
text ‹
The entries of any non-principal character sum to 0.
›
theorem (in character) sum_character:
"(∑x∈carrier G. χ x) = (if χ = principal_char G then of_nat (order G) else 0)"
proof (cases "χ = principal_char G")
case True
hence "(∑x∈carrier G. χ x) = (∑x∈carrier G. 1)"
by (intro sum.cong) (auto simp: principal_char_def)
also have "… = order G" by (simp add: order_def)
finally show ?thesis using True by simp
next
case False
define S where "S = (∑x∈carrier G. χ x)"
from False obtain y where y: "y ∈ carrier G" "χ y ≠ 1"
by (auto simp: principal_char_def fun_eq_iff char_eq_0_iff split: if_splits)
from y have "S = (∑x∈carrier G. χ (y ⊗ x))" unfolding S_def
by (intro sum.reindex_bij_betw [symmetric] bij_betw_mult_left)
also have "… = (∑x∈carrier G. χ y * χ x)"
by (intro sum.cong refl char_mult y)
also have "… = χ y * S" by (simp add: S_def sum_distrib_left)
finally have "(χ y - 1) * S = 0" by (simp add: algebra_simps)
with y have "S = 0" by simp
with False show ?thesis by (simp add: S_def)
qed
corollary (in finite_comm_group) character_orthogonality1:
assumes "character G χ" and "character G χ'"
shows "(∑x∈carrier G. χ x * cnj (χ' x)) = (if χ = χ' then of_nat (order G) else 0)"
proof -
define C where [simp]: "C = Characters G"
interpret C: finite_comm_group C unfolding C_def
by (rule finite_comm_group_Characters)
let ?χ = "λx. χ x * inv_character χ' x"
interpret character G "λx. χ x * inv_character χ' x"
by (intro character_mult character.inv_character assms)
have "(∑x∈carrier G. χ x * cnj (χ' x)) = (∑x∈carrier G. ?χ x)"
by (intro sum.cong) (auto simp: inv_character_def)
also have "… = (if ?χ = principal_char G then of_nat (order G) else 0)"
by (rule sum_character)
also have "?χ = principal_char G ⟷ χ ⊗⇘C⇙ inv⇘C⇙ χ' = 𝟭⇘C⇙"
using assms by (simp add: Characters_simps characters_def)
also have "… ⟷ χ = χ'"
proof
assume "χ ⊗⇘C⇙ inv⇘C⇙ χ' = 𝟭⇘C⇙"
from C.inv_equality [OF this] and assms show "χ = χ'"
by (auto simp: characters_def Characters_simps)
next
assume *: "χ = χ'"
from assms show "χ ⊗⇘C⇙ inv⇘C⇙ χ' = 𝟭⇘C⇙"
by (subst *, intro C.r_inv) (auto simp: carrier_Characters characters_def)
qed
finally show ?thesis .
qed
subsection ‹The isomorphism between a group and its double dual›
text ‹
Lastly, we show that the double dual of a finite abelian group is naturally isomorphic
to the original group via the obvious isomorphism $x\mapsto (\chi\mapsto \chi(x))$.
It is easy to see that this is a homomorphism and that it is injective. The fact
$|\widehat{\widehat{G}}| = |\widehat{G}| = |G|$ then shows that it is also surjective.
›
context finite_comm_group
begin
definition double_dual_iso :: "'a ⇒ ('a ⇒ complex) ⇒ complex" where
"double_dual_iso x = (λχ. if character G χ then χ x else 0)"
lemma double_dual_iso_apply [simp]: "character G χ ⟹ double_dual_iso x χ = χ x"
by (simp add: double_dual_iso_def)
lemma character_double_dual_iso [intro]:
assumes x: "x ∈ carrier G"
shows "character (Characters G) (double_dual_iso x)"
proof -
interpret G': finite_comm_group "Characters G"
by (rule finite_comm_group_Characters)
show "character (Characters G) (double_dual_iso x)"
using x by unfold_locales (auto simp: double_dual_iso_def characters_def Characters_def
principal_char_def character.char_eq_0)
qed
lemma double_dual_iso_mult [simp]:
assumes "x ∈ carrier G" "y ∈ carrier G"
shows "double_dual_iso (x ⊗ y) =
double_dual_iso x ⊗⇘Characters (Characters G)⇙ double_dual_iso y"
using assms by (auto simp: double_dual_iso_def Characters_def fun_eq_iff character.char_mult)
lemma double_dual_iso_one [simp]:
"double_dual_iso 𝟭 = principal_char (Characters G)"
by (auto simp: fun_eq_iff double_dual_iso_def principal_char_def
carrier_Characters characters_def character.char_one)
lemma inj_double_dual_iso: "inj_on double_dual_iso (carrier G)"
proof -
interpret G': finite_comm_group "Characters G"
by (rule finite_comm_group_Characters)
interpret G'': finite_comm_group "Characters (Characters G)"
by (rule G'.finite_comm_group_Characters)
have hom: "double_dual_iso ∈ hom G (Characters (Characters G))"
by (rule homI) (auto simp: carrier_Characters characters_def)
have inj_aux: "x = 𝟭"
if x: "x ∈ carrier G" "double_dual_iso x = 𝟭⇘Characters (Characters G)⇙" for x
proof (rule ccontr)
assume "x ≠ 𝟭"
obtain χ where χ: "character G χ" "χ x ≠ 1"
using character_neq_1_exists[OF x(1) ‹x ≠ 𝟭›] .
from x have "∀χ. (if χ ∈ characters G then χ x else 0) = (if χ ∈ characters G then 1 else 0)"
by (auto simp: double_dual_iso_def Characters_def fun_eq_iff
principal_char_def characters_def)
hence eq1: "∀χ∈characters G. χ x = 1" by metis
with χ show False unfolding characters_def by auto
qed
thus ?thesis
using inj_aux hom is_group G''.is_group by (subst inj_on_one_iff') auto
qed
lemma double_dual_iso_eq_iff [simp]:
"x ∈ carrier G ⟹ y ∈ carrier G ⟹ double_dual_iso x = double_dual_iso y ⟷ x = y"
by (auto dest: inj_onD[OF inj_double_dual_iso])
theorem double_dual_iso: "double_dual_iso ∈ iso G (Characters (Characters G))"
proof (rule isoI)
interpret G': finite_comm_group "Characters G"
by (rule finite_comm_group_Characters)
interpret G'': finite_comm_group "Characters (Characters G)"
by (rule G'.finite_comm_group_Characters)
show hom: "double_dual_iso ∈ hom G (Characters (Characters G))"
by (rule homI) (auto simp: carrier_Characters characters_def)
show "bij_betw double_dual_iso (carrier G) (carrier (Characters (Characters G)))"
unfolding bij_betw_def
proof
show "inj_on double_dual_iso (carrier G)" by (fact inj_double_dual_iso)
next
show "double_dual_iso ` carrier G = carrier (Characters (Characters G))"
proof (rule card_subset_eq)
show "finite (carrier (Characters (Characters G)))"
by (fact G''.fin)
next
have "card (carrier (Characters (Characters G))) = card (carrier G)"
by (simp add: carrier_Characters G'.card_characters card_characters order_def)
also have "… = card (double_dual_iso ` carrier G)"
by (intro card_image [symmetric] inj_double_dual_iso)
finally show "card (double_dual_iso ` carrier G) =
card (carrier (Characters (Characters G)))" ..
next
show "double_dual_iso ` carrier G ⊆ carrier (Characters (Characters G))"
using hom by (auto simp: hom_def)
qed
qed
qed
lemma double_dual_is_iso: "Characters (Characters G) ≅ G"
by (rule iso_sym) (use double_dual_iso in ‹auto simp: is_iso_def›)
text ‹
The second orthogonality relation follows from the first one via Pontryagin duality:
›
theorem sum_characters:
assumes x: "x ∈ carrier G"
shows "(∑χ∈characters G. χ x) = (if x = 𝟭 then of_nat (order G) else 0)"
proof -
interpret G': finite_comm_group "Characters G"
by (rule finite_comm_group_Characters)
interpret x: character "Characters G" "double_dual_iso x"
using x by auto
from x.sum_character show ?thesis using double_dual_iso_eq_iff[of x 𝟭] x
by (auto simp: characters_def carrier_Characters order_Characters simp del: double_dual_iso_eq_iff)
qed
corollary character_orthogonality2:
assumes "x ∈ carrier G" "y ∈ carrier G"
shows "(∑χ∈characters G. χ x * cnj (χ y)) = (if x = y then of_nat (order G) else 0)"
proof -
from assms have "(∑χ∈characters G. χ x * cnj (χ y)) = (∑χ∈characters G. χ (x ⊗ inv y))"
by (intro sum.cong) (simp_all add: character.char_inv character.char_mult characters_def)
also from assms have "… = (if x ⊗ inv y = 𝟭 then of_nat (order G) else 0)"
by (intro sum_characters) auto
also from assms have "x ⊗ inv y = 𝟭 ⟷ x = y"
using inv_equality[of x "inv y"] by auto
finally show ?thesis .
qed
end
no_notation integer_mod_group ("Z")
end