Theory Localization_Interface
theory Localization_Interface
imports
"HOL-Algebra.Ring_Divisibility"
"HOL-Algebra.QuotRing"
Localization_Ring.Localization
begin
section ‹Localization helper lemmas›
text ‹
The AFP entry \<^theory>‹Localization_Ring.Localization› develops localizations as
quotient rings in the HOL-Algebra hierarchy. For the present development we
package a small wrapper layer at the level of equality of representatives,
denominator rescaling, units coming from the multiplicative set, and
injectivity of the canonical map.
›
context eq_obj_rng_of_frac
begin
lemma fraction_eq_iff_rel:
assumes "(r, s) ∈ carrier rel"
and "(r', s') ∈ carrier rel"
shows "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s') ⟷ (r, s) .=⇘rel⇙ (r', s')"
proof
from assms have rs: "(r, s) ∈ carrier R × S" and rs': "(r', s') ∈ carrier R × S"
by (simp_all add: rel_def)
assume "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s')"
then show "(r, s) .=⇘rel⇙ (r', s')"
using eq_class_to_rel[of r s r' s'] rs rs' by blast
next
assume hrel: "(r, s) .=⇘rel⇙ (r', s')"
have "class_of⇘rel⇙ (r, s) = class_of⇘rel⇙ (r', s')"
using equiv_obj_rng_of_frac assms hrel by (rule elem_eq_class)
then show "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s')"
by (simp add: class_of_to_rel)
qed
lemma fraction_zero_rep [simp]:
assumes "s ∈ S"
shows "(𝟬 |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
using assms by (rule class_of_zero_rng_of_frac)
lemma fraction_surj:
assumes "x ∈ carrier rec_rng_of_frac"
shows "∃r ∈ carrier R. ∃s ∈ S. x = (r |⇘rel⇙ s)"
using assms
unfolding rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def rel_def
by auto
lemma fraction_rescale:
assumes "(r, s) ∈ carrier rel"
and "s' ∈ S"
shows "(r |⇘rel⇙ s) = (s' ⊗ r |⇘rel⇙ s' ⊗ s)"
using assms by (rule simp_in_frac)
lemma fraction_mult_rep:
assumes rs: "(r, s) ∈ carrier rel"
and r's': "(r', s') ∈ carrier rel"
shows "(r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') =
(r ⊗⇘R⇙ r' |⇘rel⇙ s ⊗⇘R⇙ s')"
proof -
have hfund:
"(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') =
(r ⊗⇘R⇙ r' |⇘rel⇙ s ⊗⇘R⇙ s')"
using mult_rng_of_frac_fundamental_lemma[OF rs r's']
by simp
have hmonoid_mult:
"(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') =
mult_rng_of_frac (r |⇘rel⇙ s) (r' |⇘rel⇙ s')"
by (simp add: rec_monoid_rng_of_frac_def)
have "(r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') =
mult_rng_of_frac (r |⇘rel⇙ s) (r' |⇘rel⇙ s')"
by (simp only: rec_rng_of_frac_def ring_record_simps)
also have "… = (r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s')"
using hmonoid_mult by simp
also have "… = (r ⊗⇘R⇙ r' |⇘rel⇙ s ⊗⇘R⇙ s')"
by (rule hfund)
finally show ?thesis .
qed
lemma map_mul_fraction:
assumes a_in: "a ∈ carrier R"
and rs: "(r, s) ∈ carrier rel"
shows "rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (a ⊗⇘R⇙ r |⇘rel⇙ s)"
proof -
have one_in: "𝟭 ∈ S"
by (rule one_closed)
have a_rel: "(a, 𝟭) ∈ carrier rel"
using a_in one_in by (simp add: rel_def)
have s_in: "s ∈ S"
using rs by (simp add: rel_def)
have s_carrier: "s ∈ carrier R"
using subset s_in by blast
have one_s: "𝟭 ⊗⇘R⇙ s = s"
using s_carrier by simp
have "rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (a |⇘rel⇙ 𝟭) ⊗⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s)"
by (simp add: rng_to_rng_of_frac_def)
also have "… = (a ⊗⇘R⇙ r |⇘rel⇙ 𝟭 ⊗⇘R⇙ s)"
by (rule fraction_mult_rep[OF a_rel rs])
also have "… = (a ⊗⇘R⇙ r |⇘rel⇙ s)"
using one_s by simp
finally show ?thesis .
qed
lemma fraction_mul_map:
assumes rs: "(r, s) ∈ carrier rel"
and a_in: "a ∈ carrier R"
shows "(r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac a = (r ⊗⇘R⇙ a |⇘rel⇙ s)"
proof -
have one_in: "𝟭 ∈ S"
by (rule one_closed)
have a_rel: "(a, 𝟭) ∈ carrier rel"
using a_in one_in by (simp add: rel_def)
have s_in: "s ∈ S"
using rs by (simp add: rel_def)
have s_carrier: "s ∈ carrier R"
using subset s_in by blast
have s_one: "s ⊗⇘R⇙ 𝟭 = s"
using s_carrier by simp
have "(r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac a = (r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (a |⇘rel⇙ 𝟭)"
by (simp add: rng_to_rng_of_frac_def)
also have "… = (r ⊗⇘R⇙ a |⇘rel⇙ s ⊗⇘R⇙ 𝟭)"
by (rule fraction_mult_rep[OF rs a_rel])
also have "… = (r ⊗⇘R⇙ a |⇘rel⇙ s)"
using s_one by simp
finally show ?thesis .
qed
lemma fraction_eq_iff_cross_multiply:
assumes rs: "(r, s) ∈ carrier rel"
and rs': "(r', s') ∈ carrier rel"
and zero_notin: "𝟬 ∉ S"
and no_zero_div: "∀a ∈ carrier R. ∀b ∈ carrier R. a ⊗ b = 𝟬 ⟶ a = 𝟬 ∨ b = 𝟬"
shows "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s') ⟷ s' ⊗⇘R⇙ r = s ⊗⇘R⇙ r'"
proof (intro iffI)
from rs rs' have r_in: "r ∈ carrier R" and s_in: "s ∈ S"
and r'_in: "r' ∈ carrier R" and s'_in: "s' ∈ S"
by (simp_all add: rel_def)
have s_carrier: "s ∈ carrier R" and s'_carrier: "s' ∈ carrier R"
using s_in s'_in subset rev_subsetD by auto
have lhs_in: "s' ⊗⇘R⇙ r ∈ carrier R"
using s'_carrier r_in by auto
have rhs_in: "s ⊗⇘R⇙ r' ∈ carrier R"
using s_carrier r'_in by auto
assume eq_frac: "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s')"
have hrel: "(r, s) .=⇘rel⇙ (r', s')"
using fraction_eq_iff_rel[OF rs rs'] eq_frac by blast
then obtain t where t_in: "t ∈ S" and t_zero: "t ⊗ ((s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r')) = 𝟬"
unfolding rel_def by auto
have t_carrier: "t ∈ carrier R"
using t_in subset rev_subsetD by auto
have diff_in: "(s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r') ∈ carrier R"
using lhs_in rhs_in by auto
have "t = 𝟬 ∨ (s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r') = 𝟬"
using no_zero_div t_carrier diff_in t_zero by blast
moreover have "t ≠ 𝟬"
using t_in zero_notin by auto
ultimately have "(s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r') = 𝟬"
by auto
then have "((s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r')) ⊕⇘R⇙ (s ⊗⇘R⇙ r') =
𝟬 ⊕⇘R⇙ (s ⊗⇘R⇙ r')"
by simp
then have "(s' ⊗⇘R⇙ r) ⊕⇘R⇙ ((⊖⇘R⇙ (s ⊗⇘R⇙ r')) ⊕⇘R⇙ (s ⊗⇘R⇙ r')) =
s ⊗⇘R⇙ r'"
using lhs_in rhs_in by (simp add: a_minus_def a_assoc)
have inv_cancel: "(⊖⇘R⇙ (s ⊗⇘R⇙ r')) ⊕⇘R⇙ (s ⊗⇘R⇙ r') = 𝟬"
using rhs_in by (rule l_neg)
then have "(s' ⊗⇘R⇙ r) ⊕⇘R⇙ ((⊖⇘R⇙ (s ⊗⇘R⇙ r')) ⊕⇘R⇙ (s ⊗⇘R⇙ r')) =
(s' ⊗⇘R⇙ r) ⊕⇘R⇙ 𝟬"
by simp
then have "(s' ⊗⇘R⇙ r) ⊕⇘R⇙ 𝟬 = s ⊗⇘R⇙ r'"
using ‹(s' ⊗⇘R⇙ r) ⊕⇘R⇙ ((⊖⇘R⇙ (s ⊗⇘R⇙ r')) ⊕⇘R⇙ (s ⊗⇘R⇙ r')) =
s ⊗⇘R⇙ r'›
by simp
then show "s' ⊗⇘R⇙ r = s ⊗⇘R⇙ r'"
using lhs_in by (simp add: r_zero)
next
assume cross_mul: "s' ⊗⇘R⇙ r = s ⊗⇘R⇙ r'"
from rs rs' have r_in': "r ∈ carrier R" and s'_in': "s' ∈ S"
by (simp_all add: rel_def)
have lhs_in': "s' ⊗⇘R⇙ r ∈ carrier R"
proof -
have "s' ∈ carrier R"
using s'_in' subset rev_subsetD by auto
then show ?thesis
using r_in' by auto
qed
have diff_zero: "(s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r') = 𝟬"
proof -
have "(s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r') = (s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s' ⊗⇘R⇙ r)"
using cross_mul by simp
also have "… = (s' ⊗⇘R⇙ r) ⊕⇘R⇙ (⊖⇘R⇙ (s' ⊗⇘R⇙ r))"
by (simp add: a_minus_def)
also have "… = 𝟬"
using lhs_in' by (rule r_neg)
finally show ?thesis .
qed
have "(r, s) .=⇘rel⇙ (r', s')"
proof -
have "𝟭 ∈ S"
by (rule one_closed)
moreover have "𝟭 ⊗ ((s' ⊗⇘R⇙ r) ⊖⇘R⇙ (s ⊗⇘R⇙ r')) = 𝟬"
using diff_zero by simp
ultimately show ?thesis
unfolding rel_def using rs rs' by auto
qed
then show "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s')"
using fraction_eq_iff_rel[OF rs rs'] by blast
qed
lemma fraction_eq_zero_iff:
assumes rs: "(r, s) ∈ carrier rel"
and zero_notin: "𝟬 ∉ S"
and no_zero_div: "∀a ∈ carrier R. ∀b ∈ carrier R. a ⊗ b = 𝟬 ⟶ a = 𝟬 ∨ b = 𝟬"
shows "(r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙ ⟷ r = 𝟬"
proof
from rs have s_in: "s ∈ S"
by (simp add: rel_def)
have s_carrier: "s ∈ carrier R"
using subset s_in by blast
from rs have r_in: "r ∈ carrier R"
by (simp add: rel_def)
have zero_rel: "(𝟬, 𝟭) ∈ carrier rel"
by (simp add: rel_def one_closed)
assume hzero: "(r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
have "(r |⇘rel⇙ s) = (𝟬 |⇘rel⇙ 𝟭)"
using hzero by (simp add: class_of_zero_rng_of_frac[OF one_closed])
then have "𝟭 ⊗⇘R⇙ r = s ⊗⇘R⇙ 𝟬"
using fraction_eq_iff_cross_multiply[OF rs zero_rel zero_notin no_zero_div]
by simp
then have "r = s ⊗⇘R⇙ 𝟬"
using r_in by simp
also have "… = 𝟬"
using s_carrier by simp
finally show "r = 𝟬" .
next
assume "r = 𝟬"
then have r_zero: "r = 𝟬" .
have s_in: "s ∈ S"
using rs by (simp add: rel_def)
from r_zero s_in show "(r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
by simp
qed
lemma map_eq_zero_iff:
assumes a_in: "a ∈ carrier R"
and zero_notin: "𝟬 ∉ S"
and no_zero_div: "∀a' ∈ carrier R. ∀b' ∈ carrier R. a' ⊗ b' = 𝟬 ⟶ a' = 𝟬 ∨ b' = 𝟬"
shows "rng_to_rng_of_frac a = 𝟬⇘rec_rng_of_frac⇙ ⟷ a = 𝟬"
proof -
have a_rel: "(a, 𝟭) ∈ carrier rel"
using a_in one_closed by (simp add: rel_def)
show ?thesis
using fraction_eq_zero_iff[OF a_rel zero_notin no_zero_div]
by (simp add: rng_to_rng_of_frac_def)
qed
lemma dvd_map_iff:
assumes a_in: "a ∈ carrier R"
and b_in: "b ∈ carrier R"
and zero_notin: "𝟬 ∉ S"
and no_zero_div: "∀a' ∈ carrier R. ∀b' ∈ carrier R. a' ⊗ b' = 𝟬 ⟶ a' = 𝟬 ∨ b' = 𝟬"
shows "rng_to_rng_of_frac a divides⇘rec_rng_of_frac⇙ rng_to_rng_of_frac b ⟷ (∃s ∈ S. a divides⇘R⇙ (s ⊗⇘R⇙ b))"
proof
assume hdiv: "rng_to_rng_of_frac a divides⇘rec_rng_of_frac⇙ rng_to_rng_of_frac b"
then obtain x where x_mem: "x ∈ carrier rec_rng_of_frac"
and hx: "rng_to_rng_of_frac b = rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ x"
unfolding factor_def by blast
from fraction_surj[OF x_mem] obtain c where c_in: "c ∈ carrier R"
and hs: "∃s ∈ S. x = (c |⇘rel⇙ s)"
by blast
from hs obtain s where s_in: "s ∈ S" and x_def: "x = (c |⇘rel⇙ s)"
by blast
have b_rel: "(b, 𝟭) ∈ carrier rel"
using b_in one_closed by (simp add: rel_def)
have cs_rel: "(c, s) ∈ carrier rel"
using c_in s_in by (simp add: rel_def)
have ac_rel: "(a ⊗⇘R⇙ c, s) ∈ carrier rel"
using a_in c_in s_in by (simp add: rel_def)
have "(b |⇘rel⇙ 𝟭) = (a ⊗⇘R⇙ c |⇘rel⇙ s)"
proof -
have h1: "rng_to_rng_of_frac b = rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ (c |⇘rel⇙ s)"
using hx x_def by simp
have h2: "rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ (c |⇘rel⇙ s) = (a ⊗⇘R⇙ c |⇘rel⇙ s)"
using map_mul_fraction[OF a_in cs_rel] by simp
from h1 h2 show ?thesis
by (simp add: rng_to_rng_of_frac_def)
qed
then have "s ⊗⇘R⇙ b = 𝟭 ⊗⇘R⇙ (a ⊗⇘R⇙ c)"
using fraction_eq_iff_cross_multiply[OF b_rel ac_rel zero_notin no_zero_div]
by simp
then have "s ⊗⇘R⇙ b = a ⊗⇘R⇙ c"
using a_in c_in by simp
then have "a divides⇘R⇙ (s ⊗⇘R⇙ b)"
unfolding factor_def using c_in by blast
then show "∃s ∈ S. a divides⇘R⇙ (s ⊗⇘R⇙ b)"
using s_in by blast
next
assume hdiv: "∃s ∈ S. a divides⇘R⇙ (s ⊗⇘R⇙ b)"
then obtain s where s_in: "s ∈ S" and hsab: "a divides⇘R⇙ (s ⊗⇘R⇙ b)"
by blast
then obtain c where c_in: "c ∈ carrier R" and hc: "s ⊗⇘R⇙ b = a ⊗⇘R⇙ c"
unfolding factor_def by blast
have cs_rel: "(c, s) ∈ carrier rel"
using c_in s_in by (simp add: rel_def)
have ac_rel: "(a ⊗⇘R⇙ c, s) ∈ carrier rel"
using a_in c_in s_in by (simp add: rel_def)
have b_rel: "(b, 𝟭) ∈ carrier rel"
using b_in one_closed by (simp add: rel_def)
have eq_frac: "(b |⇘rel⇙ 𝟭) = (a ⊗⇘R⇙ c |⇘rel⇙ s)"
proof -
have "s ⊗⇘R⇙ b = 𝟭 ⊗⇘R⇙ (a ⊗⇘R⇙ c)"
using hc a_in c_in by simp
then show ?thesis
using fraction_eq_iff_cross_multiply[OF b_rel ac_rel zero_notin no_zero_div]
by blast
qed
have frac_mem: "(c |⇘rel⇙ s) ∈ carrier rec_rng_of_frac"
using cs_rel unfolding rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def
by auto
have "rng_to_rng_of_frac b = rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ (c |⇘rel⇙ s)"
proof -
have h1: "rng_to_rng_of_frac b = (b |⇘rel⇙ 𝟭)"
by (simp add: rng_to_rng_of_frac_def)
have h2: "(b |⇘rel⇙ 𝟭) = (a ⊗⇘R⇙ c |⇘rel⇙ s)"
using eq_frac by simp
have h3: "rng_to_rng_of_frac a ⊗⇘rec_rng_of_frac⇙ (c |⇘rel⇙ s) = (a ⊗⇘R⇙ c |⇘rel⇙ s)"
using map_mul_fraction[OF a_in cs_rel] by simp
from h1 h2 h3 show ?thesis
by simp
qed
then show "rng_to_rng_of_frac a divides⇘rec_rng_of_frac⇙ rng_to_rng_of_frac b"
unfolding factor_def using frac_mem by blast
qed
lemma image_submonoid_is_unit:
assumes "x ∈ rng_to_rng_of_frac ` S"
shows "x ∈ Units rec_rng_of_frac"
using assms by (rule Im_rng_to_rng_of_frac_unit)
lemma map_submonoid_elem_is_unit:
assumes "s ∈ S"
shows "rng_to_rng_of_frac s ∈ Units rec_rng_of_frac"
using assms image_submonoid_is_unit by blast
lemma map_unit_is_unit:
assumes u_unit: "u ∈ Units R"
shows "rng_to_rng_of_frac u ∈ Units rec_rng_of_frac"
proof -
have u_in: "u ∈ carrier R"
using u_unit by blast
have inv_u_in: "inv u ∈ carrier R"
using u_unit by blast
have map_u_in: "rng_to_rng_of_frac u ∈ carrier rec_rng_of_frac"
using ring_hom_closed[OF rng_to_rng_of_frac_is_ring_hom u_in] .
have map_inv_u_in: "rng_to_rng_of_frac (inv u) ∈ carrier rec_rng_of_frac"
using ring_hom_closed[OF rng_to_rng_of_frac_is_ring_hom inv_u_in] .
have left_inv:
"rng_to_rng_of_frac u ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac (inv u) =
𝟭⇘rec_rng_of_frac⇙"
proof -
have "rng_to_rng_of_frac u ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac (inv u) =
rng_to_rng_of_frac (u ⊗⇘R⇙ inv u)"
using ring_hom_mult[OF rng_to_rng_of_frac_is_ring_hom u_in inv_u_in]
by simp
also have "… = rng_to_rng_of_frac 𝟭"
using u_unit by simp
also have "… = 𝟭⇘rec_rng_of_frac⇙"
using ring_hom_one[OF rng_to_rng_of_frac_is_ring_hom] .
finally show ?thesis .
qed
have right_inv:
"rng_to_rng_of_frac (inv u) ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac u =
𝟭⇘rec_rng_of_frac⇙"
proof -
have "rng_to_rng_of_frac (inv u) ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac u =
rng_to_rng_of_frac (inv u ⊗⇘R⇙ u)"
using ring_hom_mult[OF rng_to_rng_of_frac_is_ring_hom inv_u_in u_in]
by simp
also have "… = rng_to_rng_of_frac 𝟭"
using u_unit by simp
also have "… = 𝟭⇘rec_rng_of_frac⇙"
using ring_hom_one[OF rng_to_rng_of_frac_is_ring_hom] .
finally show ?thesis .
qed
show ?thesis
unfolding Units_def
using map_u_in map_inv_u_in left_inv right_inv by blast
qed
lemma fraction_unit_numerator_is_unit:
assumes u_unit: "u ∈ Units R"
and s_in: "s ∈ S"
shows "(u |⇘rel⇙ s) ∈ Units rec_rng_of_frac"
proof -
have u_in: "u ∈ carrier R"
using Units_closed[OF u_unit] .
have s_carrier: "s ∈ carrier R"
using subset s_in by blast
have u_rel: "(u, 𝟭) ∈ carrier rel"
using u_in one_closed by (simp add: rel_def)
have one_rel: "(𝟭, s) ∈ carrier rel"
using s_in by (simp add: rel_def)
have frac_eq':
"rng_to_rng_of_frac u ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) =
(u |⇘rel⇙ s)"
proof -
have "rng_to_rng_of_frac u ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) =
(u |⇘rel⇙ 𝟭) ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s)"
by (simp add: rng_to_rng_of_frac_def)
also have "… = (u ⊗⇘R⇙ 𝟭 |⇘rel⇙ 𝟭 ⊗⇘R⇙ s)"
by (rule fraction_mult_rep[OF u_rel one_rel])
also have "… = (u |⇘rel⇙ s)"
using u_in s_carrier by simp
finally show ?thesis .
qed
have frac_eq:
"(u |⇘rel⇙ s) =
rng_to_rng_of_frac u ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s)"
using frac_eq' by simp
have map_unit: "rng_to_rng_of_frac u ∈ Units rec_rng_of_frac"
using u_unit by (rule map_unit_is_unit)
have denom_unit: "(𝟭 |⇘rel⇙ s) ∈ Units rec_rng_of_frac"
proof -
have s_carrier: "s ∈ carrier R"
using subset s_in by blast
have s_rel: "(s, 𝟭) ∈ carrier rel"
using s_carrier one_closed by (simp add: rel_def)
have left_inv:
"(𝟭 |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac s =
𝟭⇘rec_rng_of_frac⇙"
proof -
have "(𝟭 |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac s =
(𝟭 |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (s |⇘rel⇙ 𝟭)"
by (simp add: rng_to_rng_of_frac_def)
also have "… = (𝟭 ⊗⇘R⇙ s |⇘rel⇙ s ⊗⇘R⇙ 𝟭)"
by (rule fraction_mult_rep[OF one_rel s_rel])
also have "… = (𝟭 |⇘rel⇙ 𝟭)"
proof -
have one_rel': "(𝟭, 𝟭) ∈ carrier rel"
using one_closed by (simp add: rel_def)
have "(𝟭 |⇘rel⇙ 𝟭) = (s ⊗⇘R⇙ 𝟭 |⇘rel⇙ s ⊗⇘R⇙ 𝟭)"
by (rule fraction_rescale[OF one_rel' s_in])
then show ?thesis
using s_carrier by simp
qed
also have "… = 𝟭⇘rec_rng_of_frac⇙"
by (simp only: rec_rng_of_frac_def ring_record_simps)
finally show ?thesis .
qed
have right_inv:
"rng_to_rng_of_frac s ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) =
𝟭⇘rec_rng_of_frac⇙"
proof -
have "rng_to_rng_of_frac s ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) =
(s |⇘rel⇙ 𝟭) ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s)"
by (simp add: rng_to_rng_of_frac_def)
also have "… = (s ⊗⇘R⇙ 𝟭 |⇘rel⇙ 𝟭 ⊗⇘R⇙ s)"
by (rule fraction_mult_rep[OF s_rel one_rel])
also have "… = (𝟭 |⇘rel⇙ 𝟭)"
proof -
have one_rel': "(𝟭, 𝟭) ∈ carrier rel"
using one_closed by (simp add: rel_def)
have "(𝟭 |⇘rel⇙ 𝟭) = (s ⊗⇘R⇙ 𝟭 |⇘rel⇙ s ⊗⇘R⇙ 𝟭)"
by (rule fraction_rescale[OF one_rel' s_in])
then show ?thesis
using s_carrier by simp
qed
also have "… = 𝟭⇘rec_rng_of_frac⇙"
by (simp only: rec_rng_of_frac_def ring_record_simps)
finally show ?thesis .
qed
have frac_in: "(𝟭 |⇘rel⇙ s) ∈ carrier rec_rng_of_frac"
proof -
have one_s_rel: "(𝟭, s) ∈ carrier rel"
using s_in by (simp add: rel_def)
show ?thesis
using one_s_rel
unfolding rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def
by auto
qed
have s_carrier: "s ∈ carrier R"
using s_in subset rev_subsetD by blast
have map_s_in: "rng_to_rng_of_frac s ∈ carrier rec_rng_of_frac"
using ring_hom_closed[OF rng_to_rng_of_frac_is_ring_hom s_carrier] .
show ?thesis
unfolding Units_def using frac_in map_s_in left_inv right_inv by blast
qed
show ?thesis
proof -
have "rng_to_rng_of_frac u ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) ∈ Units rec_rng_of_frac"
by (rule monoid.Units_m_closed[OF ring.is_monoid[OF rng_rng_of_frac] map_unit denom_unit])
then show ?thesis
using frac_eq by simp
qed
qed
lemma map_inj_on:
assumes "𝟬 ∉ S"
and "∀a ∈ carrier R. ∀b ∈ carrier R. a ⊗ b = 𝟬 ⟶ a = 𝟬 ∨ b = 𝟬"
shows "inj_on rng_to_rng_of_frac (carrier R)"
proof -
have "a_kernel R rec_rng_of_frac rng_to_rng_of_frac = {𝟬}"
using assms by (rule rng_to_rng_of_frac_without_zero_div_is_inj)
then show ?thesis
using ring_hom_ring.trivial_ker_imp_inj[
OF ring_hom_ringI2[OF ring_axioms rng_rng_of_frac rng_to_rng_of_frac_is_ring_hom]
]
by blast
qed
end
end