# Theory Ring_Hom

theory Ring_Hom
imports Complex Factorial_Ring
```(*
Author:      René Thiemann
*)
section ‹Several Locales for Homomorphisms Between Types.›

theory Ring_Hom
imports
HOL.Complex
Main
"HOL-Library.Multiset"
"HOL-Computational_Algebra.Factorial_Ring"
begin

hide_const (open) mult

text ‹
Many standard operations can be interpreted as homomorphisms in some sense.
Since declaring some lemmas as [simp] will interfere with existing simplification rules,
we introduce named theorems that would be added to the simp set when necessary.

The following collects distribution lemmas for homomorphisms.
Its symmetric version can often be useful.›
named_theorems hom_distribs

subsection ‹Basic Homomorphism Locales›

locale zero_hom =
fixes hom :: "'a :: zero ⇒ 'b :: zero"
assumes hom_zero[simp]: "hom 0 = 0"

locale one_hom =
fixes hom :: "'a :: one ⇒ 'b :: one"
assumes hom_one[simp]: "hom 1 = 1"

locale times_hom =
fixes hom :: "'a :: times ⇒ 'b :: times"
assumes hom_mult[hom_distribs]: "hom (x * y) = hom x * hom y"

locale plus_hom =
fixes hom :: "'a :: plus ⇒ 'b :: plus"
assumes hom_add[hom_distribs]: "hom (x + y) = hom x + hom y"

locale semigroup_mult_hom =
times_hom hom for hom :: "'a :: semigroup_mult ⇒ 'b :: semigroup_mult"

plus_hom hom for hom :: "'a :: semigroup_add ⇒ 'b :: semigroup_add"

locale monoid_mult_hom = one_hom hom + semigroup_mult_hom hom
for hom :: "'a :: monoid_mult ⇒ 'b :: monoid_mult"
begin
text ‹Homomorphism distributes over product:›
lemma hom_prod_list: "hom (prod_list xs) = prod_list (map hom xs)"
by (induct xs, auto simp: hom_distribs)
text ‹but since it introduces unapplied @{term hom}, the reverse direction would be simp.›
lemmas prod_list_map_hom[simp] = hom_prod_list[symmetric]
lemma hom_power[hom_distribs]: "hom (x ^ n) = hom x ^ n"
by (induct n, auto simp: hom_distribs)
end

begin
lemma hom_sum_list: "hom (sum_list xs) = sum_list (map hom xs)"
by (induct xs, auto simp: hom_distribs)
lemmas sum_list_map_hom[simp] = hom_sum_list[symmetric]
lemma hom_add_eq_zero: assumes "x + y = 0" shows "hom x + hom y = 0"
proof -
have "0 = x + y" using assms..
hence "hom 0 = hom (x + y)" by simp
thus ?thesis by (auto simp: hom_distribs)
qed
end

begin
lemma hom_uminus[hom_distribs]: "hom (-x) = - hom x"
lemma hom_minus [hom_distribs]: "hom (x - y) = hom x - hom y"
end

subsection ‹Commutativity›

locale ab_semigroup_mult_hom = semigroup_mult_hom hom
for hom :: "'a :: ab_semigroup_mult ⇒ 'b :: ab_semigroup_mult"

locale comm_monoid_mult_hom = monoid_mult_hom hom
for hom :: "'a :: comm_monoid_mult ⇒ 'b :: comm_monoid_mult"
begin
sublocale ab_semigroup_mult_hom..
lemma hom_prod[hom_distribs]: "hom (prod f X) = (∏x ∈ X. hom (f x))"
by (cases "finite X", induct rule:finite_induct; simp add: hom_distribs)
lemma hom_prod_mset: "hom (prod_mset X) = prod_mset (image_mset hom X)"
by (induct X, auto simp: hom_distribs)
lemmas prod_mset_image[simp] = hom_prod_mset[symmetric]
lemma hom_dvd[intro,simp]: assumes "p dvd q" shows "hom p dvd hom q"
proof -
from assms obtain r where "q = p * r" unfolding dvd_def by auto
from arg_cong[OF this, of hom] show ?thesis unfolding dvd_def by (auto simp: hom_distribs)
qed
lemma hom_dvd_1[simp]: "x dvd 1 ⟹ hom x dvd 1" using hom_dvd[of x 1] by simp
end

begin
lemma hom_sum[hom_distribs]: "hom (sum f X) = (∑x ∈ X. hom (f x))"
by (cases "finite X", induct rule:finite_induct; simp add: hom_distribs)
lemma hom_sum_mset[hom_distribs,simp]: "hom (sum_mset X) = sum_mset (image_mset hom X)"
by (induct X, auto simp: hom_distribs)
end

begin
end

locale semiring_hom = comm_monoid_add_hom hom + monoid_mult_hom hom
for hom :: "'a :: semiring_1 ⇒ 'b :: semiring_1"
begin
lemma hom_mult_eq_zero: assumes "x * y = 0" shows "hom x * hom y = 0"
proof -
have "0 = x * y" using assms..
hence "hom 0 = hom (x * y)" by simp
thus ?thesis by (auto simp:hom_distribs)
qed
end

locale ring_hom = semiring_hom hom
for hom :: "'a :: ring_1 ⇒ 'b :: ring_1"
begin
end

locale comm_semiring_hom = semiring_hom hom
for hom :: "'a :: comm_semiring_1 ⇒ 'b :: comm_semiring_1"
begin
sublocale comm_monoid_mult_hom..
end

locale comm_ring_hom = ring_hom hom
for hom :: "'a :: comm_ring_1 ⇒ 'b :: comm_ring_1"
begin
sublocale comm_semiring_hom..
end

locale idom_hom = comm_ring_hom hom
for hom :: "'a :: idom ⇒ 'b :: idom"

subsection ‹Division›

locale idom_divide_hom = idom_hom hom
for hom :: "'a :: idom_divide ⇒ 'b :: idom_divide" +
assumes hom_div[hom_distribs]: "hom (x div y) = hom x div hom y"
begin

end

locale field_hom = idom_hom hom
for hom :: "'a :: field ⇒ 'b :: field"
begin

lemma hom_inverse[hom_distribs]: "hom (inverse x) = inverse (hom x)"
by (metis hom_mult hom_one hom_zero inverse_unique inverse_zero right_inverse)

sublocale idom_divide_hom hom
proof
fix x y
have "hom (x / y) = hom (x * inverse y)" by (simp add: field_simps)
thus "hom (x / y) = hom x / hom y" unfolding hom_distribs by (simp add: field_simps)
qed

end

locale field_char_0_hom = field_hom hom
for hom :: "'a :: field_char_0 ⇒ 'b :: field_char_0"

subsection ‹(Partial) Injectivitiy›

locale zero_hom_0 = zero_hom +
assumes hom_0: "⋀x. hom x = 0 ⟹ x = 0"
begin
lemma hom_0_iff[iff]: "hom x = 0 ⟷ x = 0" using hom_0 by auto
end

locale one_hom_1 = one_hom +
assumes hom_1: "⋀x. hom x = 1 ⟹ x = 1"
begin
lemma hom_1_iff[iff]: "hom x = 1 ⟷ x = 1" using hom_1 by auto
end

text ‹Next locales are at this point not interesting.
They will retain some results when we think of polynomials.
›
locale monoid_mult_hom_1 = monoid_mult_hom + one_hom_1

locale comm_monoid_mult_hom_1 = monoid_mult_hom_1 hom
for hom :: "'a :: comm_monoid_mult ⇒ 'b :: comm_monoid_mult"

locale injective =
fixes f :: "'a ⇒ 'b" assumes injectivity: "⋀x y. f x = f y ⟹ x = y"
begin
lemma eq_iff[simp]: "f x = f y ⟷ x = y" using injectivity by auto
lemma inj_f: "inj f" by (auto intro: injI)
lemma inv_f_f[simp]: "inv f (f x) = x" by (fact inv_f_f[OF inj_f])
end

locale inj_zero_hom = zero_hom + injective hom
begin
sublocale zero_hom_0 by (unfold_locales, auto intro: injectivity)
end

locale inj_one_hom = one_hom + injective hom
begin
sublocale one_hom_1 by (unfold_locales, auto intro: injectivity)
end

locale inj_semigroup_mult_hom = semigroup_mult_hom + injective hom

locale inj_monoid_mult_hom = monoid_mult_hom + inj_semigroup_mult_hom
begin
sublocale inj_one_hom..
sublocale monoid_mult_hom_1..
end

begin
sublocale inj_zero_hom..
end

locale inj_comm_monoid_mult_hom = comm_monoid_mult_hom + inj_monoid_mult_hom
begin
sublocale comm_monoid_mult_hom_1..
end

begin
end

locale inj_semiring_hom = semiring_hom + injective hom
begin
end

locale inj_comm_semiring_hom = comm_semiring_hom + inj_semiring_hom
begin
sublocale inj_comm_monoid_mult_hom..
end

text ‹For groups, injectivity is easily ensured.›
begin
sublocale injective hom
proof
fix x y assume "hom x = hom y"
then have "hom (x-y) = 0" by (auto simp: hom_distribs)
then show "x = y" by simp
qed
end

begin
end

locale inj_ring_hom = ring_hom + zero_hom_0
begin
sublocale inj_semiring_hom..
end

locale inj_comm_ring_hom = comm_ring_hom + zero_hom_0
begin
sublocale inj_ring_hom..
sublocale inj_comm_semiring_hom..
end

locale inj_idom_hom = idom_hom + zero_hom_0
begin
sublocale inj_comm_ring_hom..
end

text ‹Field homomorphism is always injective.›
context field_hom begin
sublocale zero_hom_0
proof (unfold_locales, rule ccontr)
fix x
assume "hom x = 0" and x0: "x ≠ 0"
then have "inverse (hom x) = 0" by simp
then have "hom (inverse x) = 0" by (simp add: hom_distribs)
then have "hom (inverse x * x) = 0" by (simp add: hom_distribs)
with x0 have "hom 1 = hom 0" by simp
then have "(1 :: 'b) = 0" by simp
then show False by auto
qed
sublocale inj_idom_hom..
end

subsection ‹Surjectivity and Isomorphisms›

locale surjective =
fixes f :: "'a ⇒ 'b"
assumes surj: "surj f"
begin
lemma f_inv_f[simp]: "f (inv f x) = x"
by (rule cong, auto simp: surj[unfolded surj_iff o_def id_def])
end

locale bijective = injective + surjective

lemma bijective_eq_bij: "bijective f = bij f"
proof(intro iffI)
assume "bijective f"
then interpret bijective f.
show "bij f" using injectivity surj by (auto intro!: bijI injI)
next
assume "bij f"
from this[unfolded bij_def]
show "bijective f" by (unfold_locales, auto dest: injD)
qed

context bijective
begin
lemmas bij = bijective_axioms[unfolded bijective_eq_bij]
interpretation inv: bijective "inv f"
using bijective_axioms bij_imp_bij_inv by (unfold bijective_eq_bij)
sublocale inv: surjective "inv f"..
sublocale inv: injective "inv f"..
lemma inv_inv_f_eq[simp]: "inv (inv f) = f" using inv_inv_eq[OF bij].
lemma f_eq_iff[simp]: "f x = y ⟷ x = inv f y" by auto
lemma inv_f_eq_iff[simp]: "inv f x = y ⟷ x = f y" by auto
end

locale monoid_mult_isom = inj_monoid_mult_hom + bijective hom
begin
sublocale inv: bijective "inv hom"..
sublocale inv: inj_monoid_mult_hom "inv hom"
proof (unfold_locales)
fix hx hy :: 'b
from bij obtain x y where hx: "hx = hom x" and hy: "hy = hom y" by (meson bij_pointE)
show "inv hom (hx*hy) = inv hom hx * inv hom hy" by (unfold hx hy, fold hom_mult, simp)
have "inv hom (hom 1) = 1" by (unfold inv_f_f, simp)
then show "inv hom 1 = 1" by simp
qed
end

begin
sublocale inv: bijective "inv hom"..
proof (unfold_locales)
fix hx hy :: 'b
from bij obtain x y where hx: "hx = hom x" and hy: "hy = hom y" by (meson bij_pointE)
show "inv hom (hx+hy) = inv hom hx + inv hom hy" by (unfold hx hy, fold hom_add, simp)
have "inv hom (hom 0) = 0" by (unfold inv_f_f, simp)
then show "inv hom 0 = 0" by simp
qed
end

locale comm_monoid_mult_isom = monoid_mult_isom hom
for hom :: "'a :: comm_monoid_mult ⇒ 'b :: comm_monoid_mult"
begin
sublocale inv: monoid_mult_isom "inv hom"..
sublocale inj_comm_monoid_mult_hom..

lemma hom_dvd_hom[simp]: "hom x dvd hom y ⟷ x dvd y"
proof
assume "hom x dvd hom y"
then obtain hz where "hom y = hom x * hz" by (elim dvdE)
moreover obtain z where "hz = hom z" using bij by (elim bij_pointE)
ultimately have "hom y = hom (x * z)" by (auto simp: hom_distribs)
from this[unfolded eq_iff] have "y = x * z".
then show "x dvd y" by (intro dvdI)
qed (rule hom_dvd)

lemma hom_dvd_simp[simp]:
shows "hom x dvd y' ⟷ x dvd inv hom y'"
using hom_dvd_hom[of x "inv hom y'"] by simp

end

begin
end

locale semiring_isom = inj_semiring_hom hom + bijective hom for hom
begin
sublocale inv: inj_semiring_hom "inv hom" by (unfold_locales; simp add: hom_distribs)
sublocale inv: bijective "inv hom"..
sublocale monoid_mult_isom..
end

locale comm_semiring_isom = semiring_isom hom
for hom :: "'a :: comm_semiring_1 ⇒ 'b :: comm_semiring_1"
begin
sublocale inv: semiring_isom "inv hom" by (unfold_locales; simp add: hom_distribs)
sublocale comm_monoid_mult_isom..
sublocale inj_comm_semiring_hom..
end

locale ring_isom = inj_ring_hom + surjective hom
begin
sublocale semiring_isom..
sublocale inv: inj_ring_hom "inv hom" by (unfold_locales; simp add: hom_distribs)
end

locale comm_ring_isom = ring_isom hom
for hom :: "'a :: comm_ring_1 ⇒ 'b :: comm_ring_1"
begin
sublocale comm_semiring_isom..
sublocale inj_comm_ring_hom..
sublocale inv: ring_isom "inv hom" by (unfold_locales; simp add: hom_distribs)
end

locale idom_isom = comm_ring_isom + inj_idom_hom
begin
sublocale inv: comm_ring_isom "inv hom" by (unfold_locales; simp add: hom_distribs)
sublocale inv: inj_idom_hom "inv hom"..
end

locale field_isom = field_hom + surjective hom
begin
sublocale idom_isom..
sublocale inv: field_hom "inv hom" by (unfold_locales; simp add: hom_distribs)
end

locale inj_idom_divide_hom = idom_divide_hom hom + inj_idom_hom hom
for hom :: "'a :: idom_divide ⇒ 'b :: idom_divide"
begin
lemma hom_dvd_iff[simp]: "(hom p dvd hom q) = (p dvd q)"
proof (cases "p = 0")
case False
show ?thesis
proof
assume "hom p dvd hom q" from this[unfolded dvd_def] obtain k where
id: "hom q = hom p * k" by auto
hence "(hom q div hom p) = (hom p * k) div hom p" by simp
also have "… = k" by (rule nonzero_mult_div_cancel_left, insert False, simp)
also have "hom q div hom p = hom (q div p)" by (simp add: hom_div)
finally have "k = hom (q div p)" by auto
from id[unfolded this] have "hom q = hom (p * (q div p))" by (simp add: hom_mult)
hence "q = p * (q div p)" by simp
thus "p dvd q" unfolding dvd_def ..
qed simp
qed simp
end

context field_hom
begin
sublocale inj_idom_divide_hom ..
end

subsection ‹Example Interpretations›

interpretation of_int_hom: ring_hom of_int by (unfold_locales, auto)
interpretation of_int_hom: comm_ring_hom of_int by (unfold_locales, auto)
interpretation of_int_hom: idom_hom of_int by (unfold_locales, auto)
interpretation of_int_hom: inj_ring_hom "of_int :: int ⇒ 'a :: {ring_1,ring_char_0}"
by (unfold_locales, auto)
interpretation of_int_hom: inj_comm_ring_hom "of_int :: int ⇒ 'a :: {comm_ring_1,ring_char_0}"
by (unfold_locales, auto)
interpretation of_int_hom: inj_idom_hom "of_int :: int ⇒ 'a :: {idom,ring_char_0}"
by (unfold_locales, auto)

text ‹Somehow @{const of_rat} is defined only on ‹char_0›.›
interpretation of_rat_hom: field_char_0_hom "of_rat"
by (unfold_locales, auto simp: of_rat_add of_rat_mult of_rat_inverse of_rat_minus)

interpretation of_real_hom: inj_ring_hom of_real by (unfold_locales, auto)
interpretation of_real_hom: inj_comm_ring_hom of_real by (unfold_locales, auto)
interpretation of_real_hom: inj_idom_hom of_real by (unfold_locales, auto)
interpretation of_real_hom: field_hom of_real by (unfold_locales, auto)
interpretation of_real_hom: field_char_0_hom "of_real" by (unfold_locales, auto)

text ‹Constant multiplication in a semiring is only a monoid homomorphism.›

interpretation mult_hom: comm_monoid_add_hom "λx. c * x" for c :: "'a :: semiring_1"
by (unfold_locales, auto simp: field_simps)

end
```