Theory Fraction_Field
theory Fraction_Field
imports "HOL-Algebra.UnivPoly"
Localization_Ring.Localization
"HOL-Algebra.Subrings"
Padic_Ints.Supplementary_Ring_Facts
begin
section‹The Field of Fractions of a Ring›
text‹
This theory defines the fraction field of a domain and establishes its basic properties.
The fraction field is defined in the standard way as the localization of a domain at its nonzero
elements. This is done by importing the AFP session \texttt{Localization\_Ring}. Choice functions
for numerator and denominators of fractions are introduced, and the inclusion of a domain into
its ring of fractions is defined.
›
subsection‹The Monoid of Nonzero Elements in a Domain›
locale domain_frac = domain
lemma zero_not_in_nonzero: "𝟬⇘R⇙ ∉ nonzero R"
unfolding nonzero_def by blast
lemma(in domain) nonzero_is_submonoid: "submonoid R (nonzero R)"
proof
show " nonzero R ⊆ carrier R"
using nonzero_def by fastforce
show "⋀x y. x ∈ nonzero R ⟹ y ∈ nonzero R ⟹ x ⊗ y ∈ nonzero R"
by (metis (mono_tags, lifting) local.integral m_closed mem_Collect_eq nonzero_def)
show "𝟭 ∈ nonzero R"
by (simp add: nonzero_def)
qed
lemma(in domain) nonzero_closed:
assumes "a ∈ nonzero R"
shows "a ∈ carrier R"
using assms
by (simp add: nonzero_def)
lemma(in domain) nonzero_mult_closed:
assumes "a ∈ nonzero R"
assumes "b ∈ nonzero R"
shows "a ⊗ b ∈ carrier R"
using assms
by (simp add: nonzero_def)
lemma(in domain) nonzero_one_closed:
"𝟭 ∈ nonzero R"
by (simp add: nonzero_def)
lemma(in domain) nonzero_memI:
assumes "a ∈ carrier R"
assumes "a ≠ 𝟬"
shows "a ∈ nonzero R"
using assms by(simp add: nonzero_def)
lemma(in domain) nonzero_memE:
assumes "a ∈ nonzero R"
shows "a ∈ carrier R" "a ≠𝟬"
using assms by(auto simp: nonzero_def)
lemma(in domain) not_nonzero_memE:
assumes "a ∉ nonzero R"
assumes "a ∈ carrier R"
shows "a = 𝟬"
using assms
by (simp add: nonzero_def)
lemma(in domain) not_nonzero_memI:
assumes "a = 𝟬"
shows "a ∉ nonzero R"
using assms nonzero_memE(2) by auto
lemma(in domain) one_nonzero:
"𝟭 ∈ nonzero R"
by (simp add: nonzero_one_closed)
lemma(in domain_frac) eq_obj_rng_of_frac_nonzero:
"eq_obj_rng_of_frac R (nonzero R)"
using nonzero_is_submonoid
by (simp add: eq_obj_rng_of_frac.intro
is_cring local.ring_axioms mult_submonoid_of_crng_def mult_submonoid_of_rng_def)
subsection‹Numerator and Denominator Choice Functions›
definition(in eq_obj_rng_of_frac) denom where
"denom a = (if (a = 𝟬⇘rec_rng_of_frac⇙) then 𝟭 else ( snd (SOME x. x ∈ a)))"
text‹The choice function for numerators must be compatible with denom:›
definition(in eq_obj_rng_of_frac) numer where
"numer a = (if (a = 𝟬⇘rec_rng_of_frac⇙) then 𝟬 else (fst (SOME x. x ∈ a ∧ (snd x = denom a))))"
text‹Basic properties of numer and denom:›
lemma(in eq_obj_rng_of_frac) numer_denom_facts0:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier rec_rng_of_frac"
assumes "a ≠ 𝟬⇘rec_rng_of_frac⇙"
shows "a = ((numer a) |⇘rel⇙ (denom a))"
"(numer a) ∈ carrier R"
"(denom a) ∈ S"
"numer a = 𝟬 ⟹ a = 𝟬⇘rec_rng_of_frac⇙"
"a ⊗⇘rec_rng_of_frac⇙ (rng_to_rng_of_frac(denom a)) = rng_to_rng_of_frac (numer a)"
"(rng_to_rng_of_frac(denom a)) ⊗⇘rec_rng_of_frac⇙ a = rng_to_rng_of_frac (numer a)"
proof-
have 0: "carrier rel ≠ {}"
by (metis (no_types, lifting) SigmaI empty_iff one_closed partial_object.select_convs(1) rel_def zero_closed)
have 1: "(numer a, denom a) ∈ a"
proof-
have "∃ r s. (r ∈ carrier R ∧ s ∈ S ∧ (a = (r |⇘rel⇙ s)))"
using rel_def assms(3) assms(1) set_eq_class_of_rng_of_frac_def rec_rng_of_frac_def
by (smt mem_Collect_eq mem_Sigma_iff partial_object.select_convs(1))
then obtain r s where "r ∈ carrier R ∧ s ∈ S ∧ (a = (r |⇘rel⇙ s))"
by blast
hence "a = class_of⇘rel⇙ (r, s)"
by (simp add: class_of_to_rel)
hence "(r,s) ∈ a" using eq_class_of_def rel_def
using ‹r ∈ carrier R ∧ s ∈ S ∧ a = (r |⇘rel⇙ s)› equiv_obj_rng_of_frac equivalence.refl by fastforce
hence "(∃ x. x ∈ a)"
by blast
hence "(SOME x. x ∈ a) ∈ a"
by (meson some_eq_ex)
hence "(∃ x. x ∈ a ∧ (snd x = denom a))"
using denom_def assms by metis
hence "∃x. x ∈ a ∧ (snd x = denom a) ∧ (fst x = numer a)"
using numer_def assms by (metis (mono_tags, lifting) exE_some)
thus ?thesis
by simp
qed
have "a ∈ {r |⇘rel⇙ s |r s. (r, s) ∈ carrier rel}"
using assms(3) rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def by auto
hence "∃ x y. a = (x |⇘rel⇙ y) ∧ (x,y) ∈ carrier rel"
using rec_rng_of_frac_def eq_class_of_rng_of_frac_def set_eq_class_of_rng_of_frac_def
by blast
then obtain x y where "a = (x |⇘rel⇙ y)" and P0:"(x,y) ∈ carrier rel"
by blast
hence P1: "(numer a, denom a) ∈(x |⇘rel⇙ y)"
using "1" by blast
thus 2:"a = ((numer a) |⇘rel⇙ (denom a))"
proof-
have P2:"(numer a, denom a) ∈ carrier rel ∧ (x, y).=⇘rel⇙ (numer a, denom a) "
using eq_class_of_rng_of_frac_def P1 by fastforce
hence "(x, y).=⇘rel⇙ (numer a, denom a)"
by blast
hence "(numer a, denom a).=⇘rel⇙(x, y)"
using equiv_obj_rng_of_frac by (simp add: equivalence.sym P0 P2)
thus ?thesis
by (metis P0 P2 ‹a = (x |⇘rel⇙ y)› class_of_to_rel elem_eq_class equiv_obj_rng_of_frac)
qed
have 3:"(numer a, denom a) ∈ carrier rel"
using P1 by (simp add: eq_class_of_rng_of_frac_def)
thus 4: "numer a ∈ carrier R"
by (simp add: rel_def)
show 5: "denom a ∈ S"
using "3" rel_def by auto
show "numer a = 𝟬 ⟹ a = 𝟬⇘rec_rng_of_frac⇙"
proof-
assume "numer a = 𝟬"
hence "a = (𝟬 |⇘rel⇙ (denom a))"
using "2" by auto
thus ?thesis
using "5" class_of_zero_rng_of_frac by auto
qed
show "a ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac (denom a) = rng_to_rng_of_frac (numer a)"
proof-
have S: "(denom a, 𝟭) ∈carrier rel"
using "5" rel_def subset by auto
hence "a ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac (denom a) = (((numer a) ⊗ (denom a)) |⇘rel⇙ ((denom a) ⊗ 𝟭)) "
using 2 3 mult_rng_of_frac_fundamental_lemma rng_to_rng_of_frac_def
rec_monoid_rng_of_frac_def rec_rng_of_frac_def by fastforce
hence "a ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac (denom a) = (((denom a)⊗ (numer a)) |⇘rel⇙ ((denom a) ⊗ 𝟭))"
using "4" "5" m_comm subset by auto
hence "a ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac (denom a) = ((denom a) |⇘rel⇙ (denom a)) ⊗⇘rec_rng_of_frac⇙( (numer a) |⇘rel⇙ 𝟭)"
using mult_rng_of_frac_fundamental_lemma "4" "5" S
rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def by auto
thus ?thesis
using "4" "5" ‹a ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac
(denom a) = (denom a ⊗ numer a |⇘rel⇙ denom a ⊗ 𝟭)› rel_def
rng_to_rng_of_frac_def simp_in_frac by auto
qed
thus "(rng_to_rng_of_frac(denom a)) ⊗⇘rec_rng_of_frac⇙ a = rng_to_rng_of_frac (numer a)"
by (smt "5" assms(3) cring.cring_simprules(14) crng_rng_of_frac ring_hom_closed rng_to_rng_of_frac_is_ring_hom subset subsetD)
qed
lemma(in eq_obj_rng_of_frac) frac_zero:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier R"
assumes "b ∈ S"
assumes "(a |⇘rel⇙ b) = 𝟬⇘rec_rng_of_frac⇙"
shows "a = 𝟬"
proof-
have 0: "(a |⇘rel⇙ b) = (𝟬 |⇘rel⇙ 𝟭)"
by (simp add: assms(5) class_of_zero_rng_of_frac)
have 1: "(a,b) ∈ carrier rel"
by (simp add: assms(3) assms(4) rel_def)
have 2: "(𝟬, 𝟭) ∈ carrier rel"
by (simp add: rel_def)
have 3: "(b, 𝟭) ∈ carrier rel"
using assms(4) rel_def subset by auto
have "(a,b) .=⇘rel⇙ (𝟬, 𝟭)"
by (metis (no_types, lifting) "0" "1" "2" eq_class_to_rel partial_object.select_convs(1) rel_def)
have "(a |⇘rel⇙ b) ⊗⇘rec_rng_of_frac⇙ (b |⇘rel⇙𝟭) = (𝟬 |⇘rel⇙ b)"
by (metis (no_types, opaque_lifting) assms(4) assms(5)
basic_trans_rules(31) class_of_zero_rng_of_frac cring.axioms(1)
crng_rng_of_frac ring.ring_simprules(24) ring_hom_closed
rng_to_rng_of_frac_def rng_to_rng_of_frac_is_ring_hom subset)
hence 4: "((a ⊗ b) |⇘rel⇙ b) = (𝟬 |⇘rel⇙ b)"
using "1" "3" assms(4) mult_rng_of_frac_fundamental_lemma
rec_monoid_rng_of_frac_def rec_rng_of_frac_def subset by auto
have S: "((a ⊗ b) , b) ∈ carrier rel"
using assms(3) assms(4) rel_def subset by auto
have T: "(𝟬, b) ∈carrier rel"
by (simp add: assms(4) rel_def)
hence " ((a ⊗ b) , b).=⇘rel⇙ (𝟬 , b)"
using 4 S eq_class_to_rel rel_def by auto
hence "eq rel ((a ⊗ b) , b) (𝟬 , b)"
by blast
hence "∃t∈S. t ⊗ (b ⊗ (a ⊗ b) ⊖ b ⊗ 𝟬) = 𝟬"
using rel_def by auto
then obtain t where "t ∈ S" and "t ⊗ (b ⊗ (a ⊗ b) ⊖ b ⊗ 𝟬) = 𝟬"
by blast
have "t ≠𝟬"
using ‹t ∈ S› assms(2) by blast
hence "(b ⊗ (a ⊗ b) ⊖ b ⊗ 𝟬) = 𝟬"
by (meson ‹t ∈ S› ‹t ⊗ (b ⊗ (a ⊗ b) ⊖ b ⊗ 𝟬) = 𝟬› assms(1) assms(3)
assms(4) domain.integral_iff minus_closed semiring_simprules(3)
set_mp subset zero_closed)
hence "b ⊗ (a ⊗ b) = 𝟬"
using "3" S rel_def abelian_group.minus_to_eq is_abelian_group by fastforce
thus "a = 𝟬"
by (metis (no_types, lifting) assms(1) assms(2)
assms(3) assms(4) domain.integral_iff
semiring_simprules(3) subset subsetCE)
qed
text‹When S does not contain 0, and R is a domain, the localization is a domain.›
lemma(in eq_obj_rng_of_frac) rec_rng_of_frac_is_domain:
assumes "domain R"
assumes "𝟬 ∉ S"
shows "domain rec_rng_of_frac"
proof(rule domainI)
show "cring rec_rng_of_frac"
by (simp add: crng_rng_of_frac)
show "𝟭⇘rec_rng_of_frac⇙ ≠ 𝟬⇘rec_rng_of_frac⇙"
proof-
have " 𝟭⇘R⇙ ≠ 𝟬⇘R⇙"
by (simp add: assms domain.one_not_zero)
hence 0: " 𝟭⇘R⇙ ∉ (a_kernel R rec_rng_of_frac rng_to_rng_of_frac)"
using assms(1) rng_to_rng_of_frac_without_zero_div_is_inj
by (simp add: assms(2) domain_axioms_def domain_def)
hence "rng_to_rng_of_frac 𝟭 ≠ 𝟬⇘rec_rng_of_frac⇙"
by (simp add: a_kernel_def')
thus ?thesis
using ring_hom_one rng_to_rng_of_frac_is_ring_hom by blast
qed
show "⋀a b. a ⊗⇘rec_rng_of_frac⇙ b = 𝟬⇘rec_rng_of_frac⇙ ⟹
a ∈ carrier rec_rng_of_frac ⟹
b ∈ carrier rec_rng_of_frac ⟹
a = 𝟬⇘rec_rng_of_frac⇙ ∨ b = 𝟬⇘rec_rng_of_frac⇙"
proof-
fix a b
assume A1: "a ⊗⇘rec_rng_of_frac⇙ b = 𝟬⇘rec_rng_of_frac⇙"
assume A2: " a ∈ carrier rec_rng_of_frac"
assume A3: "b ∈ carrier rec_rng_of_frac"
show "a = 𝟬⇘rec_rng_of_frac⇙ ∨ b = 𝟬⇘rec_rng_of_frac⇙"
proof(rule disjCI)
assume "b ≠ 𝟬⇘rec_rng_of_frac⇙"
have "¬ a ≠ 𝟬⇘rec_rng_of_frac⇙ "
proof
assume "a ≠ 𝟬⇘rec_rng_of_frac⇙"
have B1: "numer a ≠ 𝟬"
using A2 ‹a ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2) numer_denom_facts0(4) by blast
have B2: "numer b ≠ 𝟬"
using A3 ‹b ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2) numer_denom_facts0(4) by blast
have B3: "denom a ≠𝟬"
using A2 ‹a ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2)
eq_obj_rng_of_frac.numer_denom_facts0(1) eq_obj_rng_of_frac_axioms
using numer_denom_facts0(3) by force
have B4: "denom b ≠𝟬"
using A3 ‹b ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2)
eq_obj_rng_of_frac_axioms by (metis (no_types, lifting) numer_denom_facts0(3))
have "a ⊗⇘rec_rng_of_frac⇙ b = (((numer a) ⊗ (numer b)) |⇘rel⇙ ((denom a) ⊗ (denom b)))"
proof-
have S0: "a = (numer a |⇘rel⇙ denom a)"
by (simp add: A2 ‹a ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2) numer_denom_facts0(1))
have S1: "b= (numer b |⇘rel⇙ denom b)"
by (simp add: A3 ‹b ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2) numer_denom_facts0(1))
have S2: "(numer a, denom a) ∈ carrier rel"
using A2 ‹a ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2)
eq_obj_rng_of_frac.numer_denom_facts0(2) eq_obj_rng_of_frac.numer_denom_facts0(3)
eq_obj_rng_of_frac_axioms rel_def by fastforce
have S3: "(numer b, denom b) ∈ carrier rel"
using A3 ‹b ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2)
eq_obj_rng_of_frac.numer_denom_facts0(2) eq_obj_rng_of_frac_axioms
numer_denom_facts0(3) rel_def by auto
show ?thesis using S0 S1 S2 S3 mult_rng_of_frac_fundamental_lemma
using rec_monoid_rng_of_frac_def rec_rng_of_frac_def by force
qed
hence "(((numer a) ⊗ (numer b)) |⇘rel⇙ ((denom a) ⊗ (denom b))) = 𝟬⇘rec_rng_of_frac⇙"
using A1 by blast
hence "(numer a) ⊗ (numer b) = 𝟬"
by (meson A2 A3 ‹a ≠ 𝟬⇘rec_rng_of_frac⇙› ‹b ≠ 𝟬⇘rec_rng_of_frac⇙›
assms(1) assms(2) eq_obj_rng_of_frac.numer_denom_facts0(2)
eq_obj_rng_of_frac.numer_denom_facts0(3) eq_obj_rng_of_frac_axioms
frac_zero m_closed semiring_simprules(3))
thus False
by (meson A2 A3 B1 B2 ‹a ≠ 𝟬⇘rec_rng_of_frac⇙›
‹b ≠ 𝟬⇘rec_rng_of_frac⇙› assms(1) assms(2)
domain.integral_iff eq_obj_rng_of_frac.numer_denom_facts0(2)
eq_obj_rng_of_frac_axioms)
qed
thus "a = 𝟬⇘rec_rng_of_frac⇙"
by auto
qed
qed
qed
lemma(in eq_obj_rng_of_frac) numer_denom_facts:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier rec_rng_of_frac"
shows "a = (numer a |⇘rel⇙ denom a)"
"(numer a) ∈ carrier R"
"(denom a) ∈ S"
"a ≠ 𝟬⇘rec_rng_of_frac⇙ ⟹ (numer a) ≠𝟬"
"a ⊗⇘rec_rng_of_frac⇙ (rng_to_rng_of_frac(denom a)) = rng_to_rng_of_frac (numer a)"
"(rng_to_rng_of_frac(denom a)) ⊗⇘rec_rng_of_frac⇙ a = rng_to_rng_of_frac (numer a)"
using assms(1) assms(2) assms(3) class_of_zero_rng_of_frac denom_def numer_def numer_denom_facts0(1) apply force
using assms(1) assms(2) assms(3) numer_def numer_denom_facts0(2) apply force
using assms(1) assms(2) assms(3) denom_def numer_denom_facts0(3) apply force
using assms(1) assms(2) assms(3) numer_denom_facts0(4) apply blast
apply (metis (no_types, lifting) assms(1) assms(2) assms(3) class_of_zero_rng_of_frac
denom_def monoid.r_one monoid.simps(2) numer_def numer_denom_facts0(5) one_closed
rec_rng_of_frac_def ringE(2) rng_rng_of_frac rng_to_rng_of_frac_def)
by (metis (no_types, lifting) assms(1) assms(2) assms(3) class_of_zero_rng_of_frac
cring.cring_simprules(12) crng_rng_of_frac denom_def monoid.simps(2) numer_def
numer_denom_facts0(6) one_closed rec_rng_of_frac_def rng_to_rng_of_frac_def)
lemma(in eq_obj_rng_of_frac) numer_denom_closed:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier rec_rng_of_frac"
shows "(numer a, denom a) ∈ carrier rel"
by (simp add: assms(1) assms(2) assms(3) numer_denom_facts(2) numer_denom_facts(3) rel_def)
text‹Fraction function which suppresses the "rel" argument.›
definition(in eq_obj_rng_of_frac) fraction where
"fraction x y = (x |⇘rel⇙ y)"
lemma(in eq_obj_rng_of_frac) a_is_fraction:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier rec_rng_of_frac"
shows "a = fraction (numer a) (denom a)"
by (simp add: assms(1) assms(2) assms(3) fraction_def numer_denom_facts(1))
lemma(in eq_obj_rng_of_frac) add_fraction:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier R"
assumes "b ∈ S"
assumes "c ∈ carrier R"
assumes "d ∈ S"
shows "(fraction a b) ⊕⇘rec_rng_of_frac⇙ (fraction c d) = (fraction ((a ⊗ d) ⊕ (b ⊗ c)) (b ⊗ d))"
proof-
have 0:"(a,b) ∈ carrier rel"
by (simp add: assms(3) assms(4) rel_def)
have 1:"(c,d) ∈ carrier rel"
by (simp add: assms(5) assms(6) rel_def)
show ?thesis
using 0 1 add_rng_of_frac_fundamental_lemma assms numer_denom_facts fraction_def
domain_def m_comm subset
by auto
qed
lemma(in eq_obj_rng_of_frac) mult_fraction:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier R"
assumes "b ∈ S"
assumes "c ∈ carrier R"
assumes "d ∈ S"
shows "(fraction a b) ⊗⇘rec_rng_of_frac⇙ (fraction c d) = (fraction (a ⊗ c) (b ⊗ d))"
proof-
have 0:"(a,b) ∈ carrier rel"
by (simp add: assms(3) assms(4) rel_def)
have 1:"(c,d) ∈ carrier rel"
by (simp add: assms(5) assms(6) rel_def)
show ?thesis using 0 1 mult_rng_of_frac_fundamental_lemma
by (simp add: fraction_def rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
qed
lemma(in eq_obj_rng_of_frac) fraction_zero:
"𝟬⇘rec_rng_of_frac⇙ = fraction 𝟬 𝟭 "
by (simp add: class_of_zero_rng_of_frac fraction_def)
lemma(in eq_obj_rng_of_frac) fraction_zero':
assumes "a ∈ S"
assumes "𝟬 ∉ S"
shows "𝟬⇘rec_rng_of_frac⇙ = fraction 𝟬 a"
by (simp add: assms(1) class_of_zero_rng_of_frac fraction_def)
lemma(in eq_obj_rng_of_frac) fraction_one:
"𝟭⇘rec_rng_of_frac⇙ = fraction 𝟭 𝟭"
by (simp add: fraction_def rec_rng_of_frac_def)
lemma(in eq_obj_rng_of_frac) fraction_one':
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ S"
shows "fraction a a = 𝟭⇘rec_rng_of_frac⇙"
using assms fraction_def fraction_one one_closed simp_in_frac subset
by (smt mem_Sigma_iff partial_object.select_convs(1) r_one rel_def subsetD)
lemma(in eq_obj_rng_of_frac) fraction_closed:
assumes "domain R"
assumes "𝟬 ∉ S"
assumes "a ∈ carrier R"
assumes "b ∈ S"
shows "fraction a b ∈ carrier rec_rng_of_frac"
proof-
have "(a,b) ∈ carrier rel"
by (simp add: assms(3) assms(4) rel_def)
hence "(a |⇘rel⇙ b) ∈ set_class_of⇘rel⇙"
using set_eq_class_of_rng_of_frac_def
by blast
thus ?thesis using fraction_def
by (simp add: rec_rng_of_frac_def)
qed
subsection‹Defining the Field of Fractions›
definition Frac where
"Frac R = eq_obj_rng_of_frac.rec_rng_of_frac R (nonzero R)"
lemma(in domain_frac) fraction_field_is_domain:
"domain (Frac R)"
using domain_axioms eq_obj_rng_of_frac.rec_rng_of_frac_is_domain
eq_obj_rng_of_frac_nonzero Frac_def
by (metis nonzero_memE(2))
subsubsection‹Numerator and Denominator Choice Functions for \texttt{domain\_frac}›
definition numerator where
"numerator R = eq_obj_rng_of_frac.numer R (nonzero R)"
abbreviation(in domain_frac)(input) numer where
"numer ≡ numerator R"
definition denominator where
"denominator R = eq_obj_rng_of_frac.denom R (nonzero R)"
abbreviation(in domain_frac)(input) denom where
"denom ≡ denominator R"
definition fraction where
"fraction R = eq_obj_rng_of_frac.fraction R (nonzero R)"
abbreviation(in domain_frac)(input) frac where
"frac ≡ fraction R"
subsubsection‹The inclusion of R into its fraction field›
definition Frac_inc where
"Frac_inc R = eq_obj_rng_of_frac.rng_to_rng_of_frac R (nonzero R)"
abbreviation(in domain_frac)(input) inc ("ι") where
"inc ≡ Frac_inc R"
lemma(in domain_frac) inc_equation:
assumes "a ∈ carrier R"
shows "ι a = frac a 𝟭"
unfolding Frac_inc_def fraction_def
using assms
by (simp add: eq_obj_rng_of_frac.fraction_def eq_obj_rng_of_frac.rng_to_rng_of_frac_def eq_obj_rng_of_frac_nonzero)
lemma(in domain_frac) inc_is_hom:
"inc ∈ ring_hom R (Frac R)"
by (simp add: eq_obj_rng_of_frac.rng_to_rng_of_frac_is_ring_hom Frac_def
eq_obj_rng_of_frac_nonzero Frac_inc_def)
lemma(in domain_frac) inc_is_hom1:
"ring_hom_ring R (Frac R) inc"
apply(rule ring_hom_ringI2)
using cring_def domain.axioms(1) fraction_field_is_domain
by(auto simp:inc_is_hom local.ring_axioms)
text‹Inclusion map is injective:›
lemma(in domain_frac) inc_inj0:
"a_kernel R (Frac R) inc = {𝟬}"
proof-
have 0: "𝟬 ∉ nonzero R"
by (simp add: nonzero_def)
have 1: "eq_obj_rng_of_frac R (nonzero R)"
by (simp add: eq_obj_rng_of_frac_nonzero)
have 2: "∀ a∈ carrier R. ∀ b∈carrier R. a ⊗ b = 𝟬 ⟶ a = 𝟬 ∨ b = 𝟬"
using local.integral by blast
show ?thesis using 0 1 2
by (simp add: eq_obj_rng_of_frac.rng_to_rng_of_frac_without_zero_div_is_inj
Frac_def Frac_inc_def)
qed
lemma(in domain_frac) inc_inj1:
assumes "a ∈ carrier R"
assumes "inc a = 𝟬⇘Frac R⇙"
shows "a = 𝟬"
proof-
have "a ∈ a_kernel R (Frac R) inc" using a_kernel_def' assms(2)
by (simp add: a_kernel_def' assms(1))
thus ?thesis
using inc_inj0 by blast
qed
lemma(in domain_frac) inc_inj2:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
assumes "inc a = inc b"
shows "a = b"
proof-
have "inc (a ⊖ b) = (inc a) ⊕⇘Frac R⇙ (inc (⊖ b))"
using inc_is_hom by (simp add: ring_hom_add assms(1) assms(2) minus_eq)
hence "inc (a ⊖ b) = 𝟬⇘Frac R⇙" using assms inc_is_hom
by (smt Frac_def add.inv_closed eq_obj_rng_of_frac.rng_rng_of_frac
eq_obj_rng_of_frac_nonzero local.ring_axioms r_neg ring_hom_add ring_hom_zero)
thus ?thesis
by (meson abelian_group.minus_to_eq assms(1) assms(2) domain_frac.inc_inj1 domain_frac_axioms is_abelian_group minus_closed)
qed
text‹Image of inclusion map is a subring:›
lemma(in domain_frac) inc_im_is_subring:
"subring (ι ` (carrier R)) (Frac R)"
using carrier_is_subring inc_is_hom1 ring_hom_ring.img_is_subring by blast
subsubsection‹Basic Properties of numer, denom, and frac›
lemma(in domain_frac) numer_denom_facts:
assumes "a ∈ carrier (Frac R)"
shows "a = frac (numer a) (denom a)"
"(numer a) ∈ carrier R"
"(denom a) ∈ nonzero R"
"a ≠ 𝟬⇘Frac R⇙ ⟹ numer a ≠ 𝟬 "
"a ⊗⇘Frac R⇙ (inc (denom a)) = inc (numer a)"
unfolding fraction_def numerator_def denominator_def Frac_inc_def
apply (metis Frac_def assms domain_axioms eq_obj_rng_of_frac.a_is_fraction eq_obj_rng_of_frac_nonzero not_nonzero_memI)
apply (metis Frac_def assms domain_axioms eq_obj_rng_of_frac.numer_denom_facts(2) eq_obj_rng_of_frac_nonzero nonzero_memE(2))
apply (metis Frac_def assms domain_axioms eq_obj_rng_of_frac.numer_denom_facts(3) eq_obj_rng_of_frac_nonzero not_nonzero_memI)
apply (metis Frac_def assms domain_axioms eq_obj_rng_of_frac.numer_denom_facts0(4) eq_obj_rng_of_frac_nonzero not_nonzero_memI)
by (metis Frac_def assms domain_axioms eq_obj_rng_of_frac.numer_denom_facts(5) eq_obj_rng_of_frac_nonzero nonzero_memE(2))
lemma(in domain_frac) frac_add:
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
assumes "c ∈ carrier R"
assumes "d ∈ nonzero R"
shows "(frac a b) ⊕⇘Frac R⇙ (frac c d) = (frac ((a ⊗ d) ⊕ (b ⊗ c)) (b ⊗ d))"
using eq_obj_rng_of_frac.add_fraction[of R "nonzero R" a b c d]
eq_obj_rng_of_frac_nonzero assms zero_not_in_nonzero[of R]
by (simp add: Frac_def domain_axioms fraction_def)
lemma(in domain_frac) frac_mult:
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
assumes "c ∈ carrier R"
assumes "d ∈ nonzero R"
shows "(frac a b) ⊗⇘Frac R⇙ (frac c d) = (frac (a ⊗ c) (b ⊗ d))"
by (simp add: Frac_def assms(1) assms(2) assms(3) assms(4) domain_axioms
eq_obj_rng_of_frac.mult_fraction eq_obj_rng_of_frac_nonzero fraction_def not_nonzero_memI)
lemma(in domain_frac) frac_one:
assumes "a ∈ nonzero R"
shows "frac a a = 𝟭⇘Frac R⇙"
by (metis Frac_def assms domain_axioms eq_obj_rng_of_frac.fraction_one' eq_obj_rng_of_frac_nonzero fraction_def nonzero_memE(2))
lemma(in domain_frac) frac_closed:
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
shows "frac a b ∈ carrier (Frac R)"
by (metis Frac_def assms(1) assms(2) domain_axioms eq_obj_rng_of_frac.fraction_closed eq_obj_rng_of_frac_nonzero fraction_def nonzero_memE(2))
lemma(in domain_frac) nonzero_fraction:
assumes "a ∈ nonzero R"
assumes "b ∈ nonzero R"
shows "frac a b ≠ 𝟬⇘Frac R⇙"
proof
assume "frac a b = 𝟬⇘Frac R⇙"
hence "(frac a b) ⊗⇘Frac R⇙ (frac b a) = 𝟬⇘Frac R⇙ ⊗⇘Frac R⇙ (frac b a)"
by simp
hence "(frac a b) ⊗⇘Frac R⇙ (frac b a) = 𝟬⇘Frac R⇙"
by (metis Localization.submonoid.subset assms(1) assms(2) cring.cring_simprules(26)
domain.axioms(1) frac_closed fraction_field_is_domain nonzero_is_submonoid subsetCE)
hence "frac (a ⊗b) (b ⊗ a) = 𝟬⇘Frac R⇙"
by (metis (no_types, lifting) Localization.submonoid.subset
assms(1) assms(2) frac_mult nonzero_is_submonoid subsetCE)
hence "frac (a ⊗b) (a ⊗ b) = 𝟬⇘Frac R⇙"
by (metis (no_types, lifting) Localization.submonoid.subset assms(1) assms(2) m_comm nonzero_is_submonoid subsetCE)
hence "𝟭⇘Frac R⇙ = 𝟬⇘Frac R⇙"
using Localization.submonoid.m_closed assms(1) assms(2) frac_one nonzero_is_submonoid by force
thus False
using domain.one_not_zero fraction_field_is_domain by blast
qed
lemma(in comm_monoid) UnitsI:
assumes "a ∈ carrier G"
assumes "b ∈ carrier G"
assumes "a ⊗ b = 𝟭"
shows "a ∈ Units G" "b ∈ Units G"
unfolding Units_def using comm_monoid_axioms_def assms m_comm[of a b]
by auto
lemma(in comm_monoid) is_invI:
assumes "a ∈ carrier G"
assumes "b ∈ carrier G"
assumes "a ⊗ b = 𝟭"
shows "inv⇘G⇙ b = a" "inv⇘G⇙ a = b"
using assms inv_char m_comm
by auto
lemma(in ring) ring_in_Units_imp_not_zero:
assumes "𝟭 ≠ 𝟬"
assumes "a ∈ Units R"
shows "a ≠ 𝟬"
using assms monoid.Units_l_cancel
by (metis l_null monoid_axioms one_closed zero_closed)
lemma(in domain_frac) in_Units_imp_not_zero:
assumes "a ∈ Units R"
shows "a ≠ 𝟬"
using assms ring_in_Units_imp_not_zero domain_axioms
by simp
lemma(in domain_frac) units_of_fraction_field0:
assumes "a ∈ carrier (Frac R)"
assumes "a ≠ 𝟬⇘Frac R⇙"
shows "inv⇘Frac R⇙ a = frac (denom a) (numer a)"
"a⊗⇘Frac R⇙ (inv⇘Frac R⇙ a) = 𝟭⇘Frac R⇙"
"(inv⇘Frac R⇙ a)⊗⇘Frac R⇙a = 𝟭⇘Frac R⇙"
proof-
have 0: "a ⊗⇘Frac R⇙ (frac (denom a) (numer a)) =
frac ((numer a) ⊗ (denom a)) ((numer a) ⊗ (denom a))"
proof -
have "denom a ∈ nonzero R"
by (simp add: assms(1) numer_denom_facts(3))
hence "frac (numer a) (denom a) ⊗⇘Frac R⇙ frac (denom a) (numer a)
= frac (numer a ⊗ denom a) (denom a ⊗ numer a)"
by (simp add: assms(1) assms(2) domain_frac.numer_denom_facts(2) domain_frac_axioms frac_mult nonzero_closed nonzero_memI numer_denom_facts(4))
thus ?thesis
using assms(1) numer_denom_facts(5) domain_frac.numer_denom_facts(2)
domain_axioms m_comm nonzero_closed numer_denom_facts(1)
by (simp add: domain_frac.numer_denom_facts(2) ‹denominator R a ∈ nonzero R› domain_frac_axioms)
qed
have 1:"((numer a) ⊗ (denom a)) ∈ nonzero R"
by (metis assms(1) assms(2) domain_frac.numer_denom_facts(2) domain_frac_axioms
local.integral m_closed nonzero_closed nonzero_memI numer_denom_facts(3) numer_denom_facts(4))
have 2: "a ⊗⇘Frac R⇙ (frac (denom a) (numer a)) = 𝟭⇘Frac R⇙"
using 0 1 frac_one by blast
have 3: "(frac (denom a) (numer a)) ∈ carrier (Frac R)"
by (simp add: assms(1) assms(2) frac_closed nonzero_closed nonzero_memI numer_denom_facts(2) numer_denom_facts(3) numer_denom_facts(4))
hence 4: "(frac (denom a) (numer a)) ∈ carrier (Frac R) ∧
a ⊗⇘Frac R⇙ (frac (denom a) (numer a)) = 𝟭⇘Frac R⇙ ∧
(frac (denom a) (numer a)) ⊗⇘Frac R⇙ a = 𝟭⇘Frac R⇙"
by (simp add: "2" assms(1) cring.cring_simprules(14) domain.axioms(1) fraction_field_is_domain)
thus 5: "inv⇘Frac R⇙ a = frac (denom a) (numer a)"
using m_inv_def 2 assms(1) comm_monoid.comm_inv_char cring_def
domain_def fraction_field_is_domain by fastforce
thus 6: "a⊗⇘Frac R⇙ (inv⇘Frac R⇙ a) = 𝟭⇘Frac R⇙"
by (simp add: "2")
thus "(inv⇘Frac R⇙ a)⊗⇘Frac R⇙a = 𝟭⇘Frac R⇙"
using assms
by (simp add: "4" "5")
qed
lemma(in domain_frac) units_of_fraction_field:
"Units (Frac R) = carrier (Frac R) - {𝟬⇘Frac R⇙}"
proof
show "Units (Frac R) ⊆ carrier (Frac R) - {𝟬⇘Frac R⇙}"
proof fix x assume A: "x ∈ Units (Frac R)"
have "x ∈ carrier (Frac R)"
using Units_def ‹x ∈ Units (Frac R)› by force
hence "x ≠ 𝟬⇘Frac R⇙"
using fraction_field_is_domain
by (simp add: A domain_frac.in_Units_imp_not_zero domain_frac.intro)
thus "x ∈ carrier (Frac R) - {𝟬⇘Frac R⇙}"
by (simp add: ‹x ∈ carrier (Frac R)›)
qed
show "carrier (Frac R) - {𝟬⇘Frac R⇙} ⊆ Units (Frac R)"
proof fix x assume A: "x ∈ carrier (Frac R) - {𝟬⇘Frac R⇙}"
show "x ∈ Units (Frac R)"
using comm_monoid.UnitsI(1)[of "Frac R" x "inv⇘Frac R⇙ x"]
by (metis A Diff_iff cring.axioms(2) domain.axioms(1) domain_frac.numer_denom_facts(2)
domain_frac.numer_denom_facts(3) domain_frac.units_of_fraction_field0(1)
domain_frac.units_of_fraction_field0(2) domain_frac_axioms frac_closed
fraction_field_is_domain insert_iff nonzero_closed nonzero_memI numer_denom_facts(4))
qed
qed
subsection‹The Fraction Field as a Field›
lemma(in domain_frac) fraction_field_is_field:
"field (Frac R)"
proof(rule Ring.field.intro)
show "domain (Frac R)" by(auto simp: fraction_field_is_domain)
show "field_axioms (Frac R)"
proof
show "Units (Frac R) = carrier (Frac R) - {𝟬⇘Frac R⇙}"
using units_of_fraction_field by blast
qed
qed
lemma(in domain_frac) frac_inv:
assumes "a ∈ nonzero R"
assumes "b ∈ nonzero R"
shows "inv⇘Frac R⇙ (frac a b) = (frac b a)"
using cring_def[of "Frac R"] domain_def[of "Frac R"] fraction_field_is_domain
frac_closed[of a b] frac_closed[of b a] nonzero_closed[of a]
nonzero_closed[of b] assms comm_monoid.is_invI(2)[of "Frac R" "frac a b" "frac b a"]
by (metis frac_mult frac_one integral_iff m_comm nonzero_memE(2) nonzero_memI nonzero_mult_closed)
lemma(in domain_frac) frac_inv_id:
assumes "a ∈ nonzero R"
assumes "b ∈ nonzero R"
assumes "c ∈ nonzero R"
assumes "d ∈ nonzero R"
assumes "frac a b = frac c d"
shows "frac b a = frac d c"
using frac_inv assms by metis
lemma(in domain_frac) frac_uminus:
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
shows "⊖⇘Frac R⇙ (frac a b) = frac (⊖ a) b"
proof-
have "frac (⊖ a) b ⊕⇘Frac R⇙ (frac a b) = frac (((⊖ a)⊗b) ⊕ (a ⊗b)) (b⊗b)"
using frac_add by (smt Localization.submonoid.subset add.inv_closed
assms(1) assms(2) m_comm nonzero_is_submonoid subsetCE)
hence "frac (⊖ a) b ⊕⇘Frac R⇙ (frac a b) = frac (b ⊗((⊖ a) ⊕ a)) (b⊗b)"
by (metis (no_types, lifting) add.inv_closed assms(1) assms(2)
local.ring_axioms m_comm mem_Collect_eq nonzero_def ringE(4) )
hence "frac (⊖ a) b ⊕⇘Frac R⇙ (frac a b) = (frac 𝟬 (b ⊗b))"
using Localization.submonoid.subset assms(1) assms(2) l_neg nonzero_is_submonoid by fastforce
hence "frac (⊖ a) b ⊕⇘Frac R⇙ (frac a b) = (frac 𝟬 𝟭) ⊗⇘Frac R⇙ (frac 𝟬 (b ⊗b))"
using frac_mult by (smt Localization.submonoid.m_closed Localization.submonoid.one_closed
Localization.submonoid.subset assms(2) l_one nonzero_is_submonoid r_null subsetCE zero_closed)
hence "frac (⊖ a) b ⊕⇘Frac R⇙ (frac a b) = 𝟬⇘Frac R⇙ ⊗⇘Frac R⇙ (frac 𝟬 (b ⊗b))"
using Frac_def eq_obj_rng_of_frac.fraction_zero' eq_obj_rng_of_frac_nonzero
by (simp add: Frac_def eq_obj_rng_of_frac.fraction_zero fraction_def)
hence "frac (⊖ a) b ⊕⇘Frac R⇙ (frac a b) = 𝟬⇘Frac R⇙"
using fraction_field_is_field
by (simp add: Localization.submonoid.m_closed assms(2) cring.cring_simprules(26)
domain.axioms(1) frac_closed fraction_field_is_domain nonzero_is_submonoid)
thus 0: "⊖⇘Frac R⇙ (frac a b) = frac (⊖ a) b"
by (metis add.inv_closed assms(1) assms(2) cring.sum_zero_eq_neg
domain.axioms(1) frac_closed fraction_field_is_domain)
qed
lemma(in domain_frac) frac_eqI:
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
assumes "c ∈ carrier R"
assumes "d ∈ nonzero R"
assumes "a ⊗ d ⊖ b ⊗ c = 𝟬"
shows "frac a b = frac c d"
proof-
have "frac a b ⊖⇘Frac R⇙ frac c d = frac (a ⊗ d ⊖ b ⊗ c) (b⊗d)"
by (simp add: a_minus_def assms(1) assms(2) assms(3) assms(4) frac_uminus local.frac_add nonzero_closed r_minus)
hence "frac a b ⊖⇘Frac R⇙ frac c d = 𝟬⇘Frac R⇙"
by (metis Frac_def assms(2) assms(4) assms(5) eq_obj_rng_of_frac.fraction_zero'
eq_obj_rng_of_frac_nonzero fraction_def local.integral nonzero_memE(1) nonzero_memE(2)
nonzero_memI nonzero_mult_closed)
thus ?thesis
by (meson assms(1) assms(2) assms(3) assms(4) field.is_ring frac_closed fraction_field_is_field ring.r_right_minus_eq)
qed
lemma(in domain_frac) frac_eqI':
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
assumes "c ∈ carrier R"
assumes "d ∈ nonzero R"
assumes "a ⊗ d = b ⊗ c"
shows "frac a b = frac c d"
using assms frac_eqI[of a b c d]
by (simp add: nonzero_closed)
lemma(in domain_frac) frac_cancel_l:
assumes "a ∈nonzero R"
assumes "b ∈nonzero R"
assumes "c ∈carrier R"
shows "frac (a ⊗ c) (a ⊗ b) = frac c b"
proof-
have 0: "frac (a ⊗c) (a ⊗b) =(frac b b) ⊗⇘Frac R⇙ (frac c b)"
by (metis (no_types, lifting) assms(1) assms(2) assms(3)
frac_mult frac_one mem_Collect_eq nonzero_def)
have 1: "frac b b = 𝟭⇘Frac R⇙"
by (simp add: assms(2) frac_one)
show ?thesis using 0 1
using Frac_def assms(2) assms(3) eq_obj_rng_of_frac.rng_rng_of_frac
eq_obj_rng_of_frac_nonzero frac_closed ring.ring_simprules(12)
by (simp add: Frac_def eq_obj_rng_of_frac.rng_rng_of_frac ring.ring_simprules(12))
qed
lemma(in domain_frac) frac_cancel_r:
assumes "a ∈nonzero R"
assumes "b ∈nonzero R"
assumes "c ∈carrier R"
shows "frac (c ⊗ a) (b ⊗ a) = frac c b"
by (metis (no_types, lifting) Localization.submonoid.subset assms(1)
assms(2) assms(3) frac_cancel_l m_comm nonzero_is_submonoid subsetCE)
lemma(in domain_frac) frac_cancel_lr:
assumes "a ∈nonzero R"
assumes "b ∈nonzero R"
assumes "c ∈carrier R"
shows "frac (a ⊗ c) (b ⊗ a) = frac c b"
by (metis (no_types, lifting) Localization.submonoid.subset assms(1)
assms(2) assms(3) frac_cancel_l m_comm nonzero_is_submonoid subsetCE)
lemma(in domain_frac) frac_cancel_rl:
assumes "a ∈nonzero R"
assumes "b ∈nonzero R"
assumes "c ∈carrier R"
shows "frac (c ⊗ a) (a ⊗ b) = frac c b"
by (metis (no_types, lifting) Localization.submonoid.subset assms(1)
assms(2) assms(3) frac_cancel_l m_comm nonzero_is_submonoid subsetCE)
lemma(in domain_frac) i_mult:
assumes "a ∈ carrier R"
assumes "c ∈ carrier R"
assumes "d ∈ nonzero R"
shows "(ι a) ⊗⇘Frac R⇙ (frac c d) = frac (a ⊗ c) d"
proof-
have "(ι a) ⊗⇘Frac R⇙ (frac c d) = (frac a 𝟭) ⊗⇘Frac R⇙ (frac c d)"
by (simp add: assms(1) inc_equation)
thus ?thesis
by (metis (mono_tags, lifting) assms(1) assms(2) assms(3) cring_simprules(12)
cring_simprules(6) frac_mult local.one_not_zero mem_Collect_eq nonzero_def)
qed
lemma(in domain_frac) frac_eqE:
assumes "a ∈ carrier R"
assumes "b ∈ nonzero R"
assumes "c ∈ carrier R"
assumes "d ∈ nonzero R"
assumes "frac a b = frac c d"
shows "a ⊗ d = b ⊗ c"
proof-
have "(ι b) ⊗⇘Frac R⇙ (frac a b) = (ι b) ⊗⇘Frac R⇙ (frac c d)"
by (simp add: assms(5))
hence "(frac (a ⊗ b) b) = (frac (c ⊗ b) d)"
using i_mult
by (metis (no_types, lifting) Localization.submonoid.subset assms(1)
assms(2) assms(3) assms(4) m_comm nonzero_is_submonoid subsetCE)
hence "(frac a 𝟭) = (frac (c ⊗ b) d)"
by (smt assms(1) assms(2) frac_cancel_r l_one mem_Collect_eq nonzero_def one_closed zero_not_one)
hence "(ι d) ⊗⇘Frac R⇙(frac a 𝟭) =(ι d) ⊗⇘Frac R⇙ (frac (c ⊗ b) d)"
by auto
hence "(frac (a ⊗ d) 𝟭) =(frac ((c ⊗ b)⊗ d) d)"
using i_mult
by (smt Localization.submonoid.m_closed Localization.submonoid.subset assms(1) assms(2) assms(3)
assms(4) cring_simprules(27) cring_simprules(6) local.one_not_zero m_comm
mem_Collect_eq nonzero_def nonzero_is_submonoid)
hence "(frac (a ⊗ d) 𝟭) =(frac (c ⊗ b) 𝟭)"
by (smt Localization.submonoid.subset assms(2) assms(3) assms(4) cring_simprules(5)
cring_simprules(6) frac_one i_mult inc_equation inc_is_hom nonzero_is_submonoid
r_one ring_hom_mult ring_hom_one subsetCE)
thus ?thesis using assms
unfolding fraction_def
by (simp add: fraction_def inc_equation inc_inj2 m_comm nonzero_closed)
qed
lemma(in domain_frac) frac_add_common_denom:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
assumes "c ∈ nonzero R"
shows "(frac a c) ⊕⇘Frac R⇙ (frac b c) = frac (a ⊕ b) c"
proof-
have "(frac a c) ⊕⇘Frac R⇙ (frac b c) = frac ((a ⊗ c) ⊕ (b ⊗ c)) (c ⊗ c)"
using assms(1) assms(2) assms(3) domain_frac.frac_add domain_axioms frac_eqE local.frac_add
by auto
hence "(frac a c) ⊕⇘Frac R⇙ (frac b c) = frac ((a ⊕ b) ⊗ c) (c ⊗ c)"
by (metis Localization.submonoid.subset assms(1) assms(2) assms(3) l_distr nonzero_is_submonoid subsetCE)
thus ?thesis
by (simp add: assms(1) assms(2) assms(3) frac_cancel_r)
qed
lemma(in domain_frac) common_denominator:
assumes "x ∈ carrier (Frac R)"
assumes "y ∈ carrier (Frac R)"
obtains a b c where
"a ∈ carrier R"
"b ∈ carrier R"
"c ∈ nonzero R"
"x = frac a c"
"y = frac b c"
proof-
obtain x1 x2 where X1: "x1 ∈ carrier R" and X2: "x2 ∈ nonzero R" and Fx: "x = frac x1 x2"
by (meson assms(1) numer_denom_facts(1) numer_denom_facts(2) numer_denom_facts(3))
obtain y1 y2 where Y1: "y1 ∈ carrier R" and Y2: "y2 ∈ nonzero R" and Fy: "y = frac y1 y2"
by (meson assms(2) numer_denom_facts(1) numer_denom_facts(2) numer_denom_facts(3))
let ?a = "x1 ⊗ y2"
let ?b = "y1 ⊗ x2"
let ?c = "x2 ⊗ y2"
have 0: "?a ∈ carrier R"
using X1 Y2 by (simp add: nonzero_def)
have 1: "?b ∈ carrier R" using Y1 X2
by (simp add: nonzero_def)
have 2: "?c ∈ nonzero R" using X2 Y2
by (simp add: Localization.submonoid.m_closed nonzero_is_submonoid)
have 3: "x = frac ?a ?c"
using Fx X1 X2 Y2 frac_cancel_r by auto
have 4: "y = frac ?b ?c"
using Fy X2 Y1 Y2 frac_cancel_rl by auto
thus ?thesis using 0 1 2 3 4
using that by blast
qed
sublocale domain_frac < F: field "Frac R"
by (simp add: fraction_field_is_field)
text‹Inclusions of natural numbers into \texttt{(Frac R)}:›
lemma(in domain_frac) nat_0:
"[(0::nat)]⋅𝟭 = 𝟬"
by simp
lemma(in domain_frac) nat_suc:
"[Suc n]⋅𝟭 = 𝟭 ⊕ [n]⋅𝟭"
using add.nat_pow_Suc2 by auto
lemma(in domain_frac) nat_inc_rep:
fixes n::nat
shows "[n]⋅⇘Frac R⇙ 𝟭⇘Frac R⇙ = frac ([n]⋅𝟭) 𝟭"
proof(induction n)
case 0
have "[(0::nat)] ⋅⇘Frac R⇙ 𝟭⇘Frac R⇙ = 𝟬⇘Frac R⇙"
using fraction_field_is_domain
by (simp add: domain_frac.intro domain_frac.nat_0)
thus ?case
by (simp add: Frac_def eq_obj_rng_of_frac.fraction_zero eq_obj_rng_of_frac_nonzero fraction_def)
next
case (Suc n)
assume A: "[n] ⋅⇘Frac R⇙ 𝟭⇘Frac R⇙ = frac ([n] ⋅ 𝟭) 𝟭"
have "[Suc n] ⋅⇘Frac R⇙ 𝟭⇘Frac R⇙ = 𝟭⇘Frac R⇙ ⊕⇘Frac R⇙ [n] ⋅⇘Frac R⇙ 𝟭⇘Frac R⇙"
using F.add.nat_pow_Suc2 by auto
hence "[Suc n] ⋅⇘Frac R⇙ 𝟭⇘Frac R⇙ = (frac 𝟭 𝟭) ⊕⇘Frac R⇙ (frac ([n] ⋅ 𝟭) 𝟭)"
by (simp add: Suc.IH frac_one nonzero_def)
hence "[Suc n] ⋅⇘Frac R⇙ 𝟭⇘Frac R⇙ = (frac (𝟭⊕[n] ⋅ 𝟭) 𝟭)"
by (simp add: frac_add_common_denom nonzero_def)
thus ?case
using nat_suc by auto
qed
lemma(in domain_frac) pow_0:
assumes "a ∈ nonzero R"
shows "a[^](0::nat) = 𝟭"
by simp
lemma(in domain_frac) pow_suc:
assumes "a ∈ carrier R"
shows "a[^](Suc n) = a ⊗(a[^]n)"
using assms nat_pow_Suc2 by auto
lemma(in domain_frac) nat_inc_add:
"[((n::nat) + (m::nat))]⋅𝟭 = [n]⋅𝟭 ⊕ [m]⋅𝟭"
using domain_def add_pow_def
by (simp add: add.nat_pow_mult)
lemma(in domain_frac) int_inc_add:
"[((n::int) + (m::int))]⋅𝟭 = [n]⋅𝟭 ⊕ [m]⋅𝟭"
using domain_def add_pow_def
by (simp add: add.int_pow_mult)
lemma(in domain_frac) nat_inc_mult:
"[((n::nat) * (m::nat))]⋅𝟭 = [n]⋅𝟭 ⊗ [m]⋅𝟭"
using domain_def add_pow_def
by (simp add: Groups.mult_ac(2) add.nat_pow_pow add_pow_ldistr)
lemma(in domain_frac) int_inc_mult:
"[((n::int) * (m::int))]⋅𝟭 = [n]⋅𝟭 ⊗ [m]⋅𝟭"
using domain_def add_pow_def
by (simp add: Groups.mult_ac(2) add.int_pow_pow add_pow_ldistr_int)
subsection‹Facts About Ring Units›
lemma(in ring) Units_nonzero:
assumes "u ∈ Units R"
assumes "𝟭⇘R⇙ ≠ 𝟬⇘R⇙"
shows "u ∈ nonzero R"
proof-
have "u ∈carrier R"
using Units_closed assms by auto
have "u ≠𝟬"
using Units_r_inv_ex assms(1) assms(2)
by force
thus ?thesis
by (simp add: ‹u ∈ carrier R› nonzero_def)
qed
lemma(in ring) Units_inverse:
assumes "u ∈ Units R"
shows "inv u ∈ Units R"
by (simp add: assms)
lemma(in cring) invI:
assumes "x ∈ carrier R"
assumes "y ∈ carrier R"
assumes "x ⊗⇘R⇙ y = 𝟭⇘R⇙"
shows "y = inv ⇘R⇙ x"
"x = inv ⇘R⇙ y"
using assms(1) assms(2) assms(3) is_invI
by auto
lemma(in cring) inv_cancelR:
assumes "x ∈ Units R"
assumes "y ∈ carrier R"
assumes "z ∈ carrier R"
assumes "y = x ⊗⇘R⇙ z"
shows "inv⇘R⇙ x ⊗⇘R⇙ y = z"
"y ⊗⇘R⇙ (inv⇘R⇙ x) = z"
apply (metis Units_closed assms(1) assms(3) assms(4) cring.cring_simprules(12)
is_cring m_assoc monoid.Units_inv_closed monoid.Units_l_inv monoid_axioms)
by (metis Units_closed assms(1) assms(3) assms(4) m_assoc m_comm monoid.Units_inv_closed
monoid.Units_r_inv monoid.r_one monoid_axioms)
lemma(in cring) inv_cancelL:
assumes "x ∈ Units R"
assumes "y ∈ carrier R"
assumes "z ∈ carrier R"
assumes "y = z ⊗⇘R⇙ x"
shows "inv⇘R⇙ x ⊗⇘R⇙ y = z"
"y ⊗⇘R⇙ (inv⇘R⇙ x) = z"
apply (simp add: Units_closed assms(1) assms(3) assms(4) m_lcomm)
by (simp add: Units_closed assms(1) assms(3) assms(4) m_assoc)
lemma(in domain_frac) nat_pow_nonzero:
assumes "x ∈nonzero R"
shows "x[^](n::nat) ∈ nonzero R"
unfolding nonzero_def
apply(induction n)
using assms integral_iff nonzero_closed zero_not_in_nonzero by auto
lemma(in monoid) Units_int_pow_closed:
assumes "x ∈ Units G"
shows "x[^](n::int) ∈ Units G"
by (metis Units_pow_closed assms int_pow_def2 monoid.Units_inv_Units monoid_axioms)
subsection‹Facts About Fraction Field Units›
lemma(in domain_frac) frac_nonzero_Units:
"nonzero (Frac R) = Units (Frac R)"
unfolding nonzero_def using F.field_Units
by blast
lemma(in domain_frac) frac_nonzero_inv_Unit:
assumes "b ∈ nonzero (Frac R)"
shows "inv⇘Frac R⇙ b ∈ Units (Frac R)"
using assms frac_nonzero_Units
by simp
lemma(in domain_frac) frac_nonzero_inv_closed:
assumes "b ∈ nonzero (Frac R)"
shows "inv⇘Frac R⇙ b ∈ carrier (Frac R)"
using frac_nonzero_inv_Unit
by (simp add: Units_def assms)
lemma(in domain_frac) frac_nonzero_inv:
assumes "b ∈ nonzero (Frac R)"
shows "b ⊗⇘Frac R⇙ inv ⇘Frac R⇙ b = 𝟭⇘Frac R⇙"
"inv ⇘Frac R⇙ b ⊗⇘Frac R⇙ b = 𝟭⇘Frac R⇙"
using frac_nonzero_Units assms by auto
lemma(in domain_frac) fract_cancel_right[simp]:
assumes "a ∈ carrier (Frac R)"
assumes "b ∈ nonzero (Frac R)"
shows "b ⊗⇘Frac R⇙ (a ⊗⇘Frac R⇙ inv⇘Frac R⇙ b) = a"
by (metis F.Units_inv_inv F.inv_cancelL(1) F.m_closed assms(1) assms(2) frac_nonzero_Units frac_nonzero_inv_Unit frac_nonzero_inv_closed)
lemma(in domain_frac) fract_cancel_left[simp]:
assumes "a ∈ carrier (Frac R)"
assumes "b ∈ nonzero (Frac R)"
shows "(a ⊗⇘Frac R⇙ inv⇘Frac R⇙ b) ⊗⇘Frac R⇙ b = a"
by (metis Diff_iff assms(1) assms(2) cring.cring_simprules(14) cring.cring_simprules(5)
domain.axioms(1) frac_nonzero_Units frac_nonzero_inv_closed fract_cancel_right
fraction_field_is_domain units_of_fraction_field)
lemma(in domain_frac) fract_mult_inv:
assumes "b ∈ nonzero (Frac R)"
assumes "d ∈ nonzero (Frac R)"
shows "(inv⇘Frac R⇙ b) ⊗⇘Frac R⇙ (inv⇘Frac R⇙ d) = (inv⇘Frac R⇙ (b ⊗⇘Frac R⇙d))"
by (metis F.Units_inv_closed F.Units_m_closed F.inv_cancelR(2) F.nonzero_closed assms(1) assms(2) frac_nonzero_Units)
lemma(in domain_frac) fract_mult:
assumes "a ∈ carrier (Frac R)"
assumes "b ∈ nonzero (Frac R)"
assumes "c ∈ carrier (Frac R)"
assumes "d ∈ nonzero (Frac R)"
shows "(a ⊗⇘Frac R⇙ inv⇘Frac R⇙ b) ⊗⇘Frac R⇙ (c ⊗⇘Frac R⇙ inv⇘Frac R⇙ d) = ((a ⊗⇘Frac R⇙ c)⊗⇘Frac R⇙ inv⇘Frac R⇙ (b ⊗⇘Frac R⇙d))"
using F.m_assoc F.m_lcomm assms(1) assms(2) assms(3) assms(4) frac_nonzero_Units fract_mult_inv by auto
lemma(in domain_frac) Frac_nat_pow_nonzero:
assumes "x ∈ nonzero (Frac R)"
shows "x[^]⇘Frac R⇙(n::nat) ∈ nonzero (Frac R)"
by (simp add: assms domain_frac.intro domain_frac.nat_pow_nonzero fraction_field_is_domain)
lemma(in domain_frac) Frac_nonzero_nat_pow:
assumes "x ∈ carrier (Frac R)"
assumes "n > 0"
assumes "x[^]⇘Frac R⇙(n::nat) ∈ nonzero (Frac R)"
shows "x ∈ nonzero (Frac R)"
proof(rule ccontr)
assume "x ∉ nonzero (Frac R)"
hence 0: "x = 𝟬⇘Frac R⇙"
by (simp add: assms(1) nonzero_def)
have "x[^]⇘Frac R⇙(n::nat) = 𝟬⇘Frac R⇙"
proof-
obtain k where "n = Suc k"
using assms(2) lessE by blast
hence 00: "x[^]⇘Frac R⇙(n::nat) = x[^]⇘Frac R⇙k ⊗⇘Frac R⇙ x"
by simp
have "x[^]⇘Frac R⇙k ∈ carrier (Frac R)"
using assms monoid.nat_pow_closed[of "Frac R" x k]
by (meson field.is_ring fraction_field_is_field ring_def)
thus ?thesis using 0 assms
using "00" cring.cring_simprules(27) domain.axioms(1) fraction_field_is_domain by fastforce
qed
thus False
using "0" ‹x ∉ nonzero (Frac R)› assms(3) by auto
qed
lemma(in domain_frac) Frac_int_pow_nonzero:
assumes "x ∈ nonzero (Frac R)"
shows "x[^]⇘Frac R⇙(n::int) ∈ nonzero (Frac R)"
using assms field.is_ring frac_nonzero_Units fraction_field_is_field monoid.Units_pow_closed[of "Frac R" x]
by (simp add: field.is_ring monoid.Units_int_pow_closed ring.is_monoid)
lemma(in domain_frac) Frac_nonzero_int_pow:
assumes "x ∈ carrier (Frac R)"
assumes "n > 0"
assumes "x[^]⇘Frac R⇙(n::int) ∈ nonzero (Frac R)"
shows "x ∈ nonzero (Frac R)"
by (metis (mono_tags, opaque_lifting) Frac_nonzero_nat_pow assms int_pow_int pos_int_cases)
lemma(in domain_frac) numer_denom_frac[simp]:
assumes "a ∈ nonzero R"
assumes "b ∈ nonzero R"
shows "frac (numer (frac a b)) (denom (frac a b)) = frac a b"
using assms(1) assms(2) domain_frac.numer_denom_facts(1)
domain_axioms frac_closed nonzero_closed numer_denom_facts(1) by auto
lemma(in domain_frac) numer_denom_swap:
assumes "a ∈ nonzero R"
assumes "b ∈ nonzero R"
shows "a ⊗ (denom (frac a b)) = b ⊗ (numer (frac a b))"
using numer_denom_frac[of a b] assms
by (simp add: frac_closed frac_eqE nonzero_closed numer_denom_facts(2) numer_denom_facts(3))
lemma(in domain_frac) numer_nonzero:
assumes "a ∈ nonzero (Frac R)"
shows "numer a ∈ nonzero R"
using assms numer_denom_facts(4)[of a] zero_not_in_nonzero[of R]
by (simp add: frac_nonzero_Units nonzero_memI numer_denom_facts(2) units_of_fraction_field)
lemma(in domain_frac) fraction_zero[simp]:
assumes "b ∈ nonzero R"
shows "frac 𝟬 b = 𝟬⇘Frac R⇙"
by (metis Frac_def assms eq_obj_rng_of_frac.fraction_zero' eq_obj_rng_of_frac_nonzero fraction_def nonzero_memE(2))
end