Theory Ring_Theory
theory Ring_Theory
imports Group_Theory
begin
no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax
no_notation quotient (infixl ‹'/'/› 90)
section ‹Rings›
subsection ‹Definition and Elementary Properties›
text ‹Def 2.1›
text ‹p 86, ll 20--28›
locale Ring = additive: Abelian_Group R "(+)" 𝟬 + multiplicative: Monoid R "(⋅)" 𝟭
for R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›) +
assumes distributive: "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ a ⋅ (b + c) = a ⋅ b + a ⋅ c"
"⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ (b + c) ⋅ a = b ⋅ a + c ⋅ a"
begin
text ‹p 86, ll 20--28›
notation additive.inverse (‹- _› [66] 65)
abbreviation subtraction (infixl ‹-› 65) where "a - b ≡ a + (- b)"
end
text ‹Compact version based on the monoid type›
locale Ring' =
fixes additive multiplicative
assumes eq: "mcarrier additive = mcarrier multiplicative"
assumes Ring: "Ring (mcarrier additive) (mmult additive) (mmult multiplicative) (munit additive) (munit multiplicative)"
text ‹p 87, ll 10--12›
locale Subring =
additive: Subgroup S R "(+)" 𝟬 + multiplicative: Submonoid S R "(⋅)" 𝟭
for S and R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›)
context Ring begin
text ‹p 88, ll 26--28›
lemma right_zero [simp]:
assumes [simp]: "a ∈ R" shows "a ⋅ 𝟬 = 𝟬"
proof -
have "a ⋅ 𝟬 = a ⋅ (𝟬 + 𝟬)" by simp
also have "… = a ⋅ 𝟬 + a ⋅ 𝟬" by (simp add: distributive del: additive.left_unit additive.right_unit)
finally have "a ⋅ 𝟬 - a ⋅ 𝟬 = a ⋅ 𝟬 + a ⋅ 𝟬 - a ⋅ 𝟬" by simp
then show ?thesis by (simp add: additive.associative del: additive.invertible_left_cancel)
qed
text ‹p 88, l 29›
lemma left_zero [simp]:
assumes [simp]: "a ∈ R" shows "𝟬 ⋅ a = 𝟬"
proof -
have "𝟬 ⋅ a = (𝟬 + 𝟬) ⋅ a" by simp
also have "… = 𝟬 ⋅ a + 𝟬 ⋅ a" by (simp add: distributive del: additive.left_unit additive.right_unit)
finally have "𝟬 ⋅ a - 𝟬 ⋅ a = 𝟬 ⋅ a + 𝟬 ⋅ a - 𝟬 ⋅ a" by simp
then show ?thesis by (simp add: additive.associative del: additive.invertible_left_cancel)
qed
text ‹p 88, ll 29--30; p 89, ll 1--2›
lemma left_minus:
assumes [simp]: "a ∈ R" "b ∈ R" shows "(- a) ⋅ b = - a ⋅ b"
proof -
have "𝟬 = 𝟬 ⋅ b" by simp
also have "… = (a - a) ⋅ b" by simp
also have "… = a ⋅ b + (- a) ⋅ b" by (simp add: distributive del: additive.invertible_right_inverse)
finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + (- a) ⋅ b" by (simp add: additive.associative del: additive.invertible_left_inverse)
then show ?thesis by simp
qed
text ‹p 89, l 3›
lemma right_minus:
assumes [simp]: "a ∈ R" "b ∈ R" shows "a ⋅ (- b) = - a ⋅ b"
proof -
have "𝟬 = a ⋅ 𝟬" by simp
also have "… = a ⋅ (b - b)" by simp
also have "… = a ⋅ b + a ⋅ (- b)" by (simp add: distributive del: additive.invertible_right_inverse)
finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + a ⋅ (- b)" by (simp add: additive.associative del: additive.invertible_left_inverse)
then show ?thesis by simp
qed
end
subsection ‹Commutative rings, integral domains, and fields›
text ‹A commutative ring is a ring whose multiplication is commutative. We reuse the
@{locale commutative_monoid} structure on the multiplicative part, mirroring how
@{locale Abelian_Group} reuses @{locale commutative_monoid}.›
locale commutative_ring = Ring +
multiplicative: commutative_monoid R "(⋅)" 𝟭
begin
text ‹Associative-commutative normalisation bundles for the two operations, for on-demand use as
@{text "simp add: mult_ac"} / @{text "simp add: add_ac"}. The additive group is abelian, so it too
supplies the @{text ac} bundle.›
lemmas mult_ac = multiplicative.ac
lemmas add_ac = additive.ac
end
text ‹A nontrivial ring is one in which the unit and zero differ. Both integral domains
and fields require this, so we factor it into a common ancestor: that way the assumption
is inherited (and named @{text nontrivial}) by a single route, avoiding a duplicate when
a field is shown to be an integral domain or interpreted.›
locale nontrivial_ring = Ring +
assumes nontrivial: "𝟭 ≠ 𝟬"
text ‹An integral domain is a nontrivial commutative ring without zero divisors.›
locale integral_domain = commutative_ring + nontrivial_ring +
assumes no_zero_divisors: "⟦ a ∈ R; b ∈ R; a ⋅ b = 𝟬 ⟧ ⟹ a = 𝟬 ∨ b = 𝟬"
text ‹A field is a nontrivial commutative ring in which every nonzero element is
invertible. Invertibility is expressed through the multiplicative monoid's
@{const Monoid.invertible} predicate, so the multiplicative inverse and unit
machinery is available via the @{text multiplicative} prefix.›
locale Field = commutative_ring + nontrivial_ring +
assumes field_inverse: "⟦ a ∈ R; a ≠ 𝟬 ⟧ ⟹ multiplicative.invertible a"
begin
text ‹Every field is an integral domain.›
sublocale integral_domain
proof unfold_locales
fix a b assume a: "a ∈ R" and b: "b ∈ R" and ab: "a ⋅ b = 𝟬"
show "a = 𝟬 ∨ b = 𝟬"
proof (cases "a = 𝟬")
case False
then have inv: "multiplicative.invertible a" using a field_inverse by blast
then have ia: "multiplicative.inverse a ∈ R" using a by simp
have "b = multiplicative.inverse a ⋅ (a ⋅ b)"
using a b inv by (simp add: multiplicative.invertible_left_inverse2)
also have "… = multiplicative.inverse a ⋅ 𝟬" using ab by simp
also have "… = 𝟬" using ia by (rule right_zero)
finally have "b = 𝟬" .
then show ?thesis ..
qed simp
qed
end
subsection ‹Ideals, Quotient Rings›
text ‹p 101, ll 2--5›
locale ring_congruence = Ring +
additive: group_congruence R "(+)" 𝟬 E +
multiplicative: Monoid_congruence R "(⋅)" 𝟭 E
for E
begin
text ‹p 101, ll 2--5›
notation additive.quotient_composition (infixl ‹[+]› 65)
notation additive.quotient.inverse (‹[-] _› [66] 65)
notation multiplicative.quotient_composition (infixl ‹[⋅]› 70)
text ‹p 101, ll 5--11›
sublocale quotient: Ring "R / E" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭"
by unfold_locales
(auto simp: additive.Class_commutes_with_composition additive.associative additive.commutative
multiplicative.Class_commutes_with_composition distributive elim!: additive.quotient_ClassE)
end
text ‹p 101, ll 12--13›
locale subgroup_of_additive_group_of_ring =
additive: Subgroup I R "(+)" 𝟬 + Ring R "(+)" "(⋅)" 𝟬 𝟭
for I and R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›)
begin
text ‹p 101, ll 13--14›
definition "Ring_Congruence = {(a, b). a ∈ R ∧ b ∈ R ∧ a - b ∈ I}"
text ‹p 101, ll 13--14›
lemma Ring_CongruenceI: "⟦ a - b ∈ I; a ∈ R; b ∈ R ⟧ ⟹ (a, b) ∈ Ring_Congruence"
using Ring_Congruence_def by blast
text ‹p 101, ll 13--14›
lemma Ring_CongruenceD: "(a, b) ∈ Ring_Congruence ⟹ a - b ∈ I"
using Ring_Congruence_def by blast
text ‹
Jacobson's definition of Ring congruence deviates from that of group congruence; this complicates
the proof.
›
text ‹p 101, ll 12--14›
sublocale additive: subgroup_of_abelian_group I R "(+)" 𝟬
rewrites additive_congruence: "additive.Congruence = Ring_Congruence"
proof -
show "subgroup_of_abelian_group I R (+) 𝟬"
using additive.commutative additive.invertible_right_inverse2 by unfold_locales auto
then interpret additive: subgroup_of_abelian_group I R "(+)" 𝟬 .
{
fix a b
assume [simp]: "a ∈ R" "b ∈ R"
have "a - b ∈ I ⟷ - (a - b) ∈ I" by auto
also have "… ⟷ - a + b ∈ I" by (simp add: additive.commutative additive.inverse_composition_commute)
finally have "a - b ∈ I ⟷ - a + b ∈ I" .
}
then show "additive.Congruence = Ring_Congruence"
unfolding additive.Congruence_def Ring_Congruence_def by auto
qed
text ‹p 101, l 14›
notation additive.Left_Coset (infixl ‹+|› 65)
end
text ‹Def 2.2›
text ‹p 101, ll 21--22›
locale Ideal = subgroup_of_additive_group_of_ring +
assumes Ideal: "⟦ a ∈ R; b ∈ I ⟧ ⟹ a ⋅ b ∈ I" "⟦ a ∈ R; b ∈ I ⟧ ⟹ b ⋅ a ∈ I"
context subgroup_of_additive_group_of_ring begin
text ‹p 101, ll 14--17›
theorem multiplicative_congruence_implies_ideal:
assumes "Monoid_congruence R (⋅) 𝟭 Ring_Congruence"
shows "Ideal I R (+) (⋅) 𝟬 𝟭"
proof -
interpret multiplicative: Monoid_congruence R "(⋅)" 𝟭 Ring_Congruence by fact
show ?thesis
proof
fix a b
assume [simp]: "a ∈ R" "b ∈ I"
have congs: "(a, a) ∈ Ring_Congruence" "(b, 𝟬) ∈ Ring_Congruence"
by (auto simp: additive.ClassD additive.Class_unit_normal_subgroup)
from congs have "(a ⋅ b, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce
then show "a ⋅ b ∈ I" using additive.Class_unit_normal_subgroup by blast
from congs have "(b ⋅ a, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce
then show "b ⋅ a ∈ I" using additive.Class_unit_normal_subgroup by blast
qed
qed
end
context Ideal begin
text ‹p 101, ll 17--20›
theorem multiplicative_congruence [intro]:
assumes a: "(a, a') ∈ Ring_Congruence" and b: "(b, b') ∈ Ring_Congruence"
shows "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence"
proof -
note Ring_CongruenceI [intro] Ring_CongruenceD [dest]
from a b have [simp]: "a ∈ R" "a' ∈ R" "b ∈ R" "b' ∈ R" by auto
from a have [simp]: "a - a' ∈ I" ..
have "a ⋅ b - a' ⋅ b = (a - a') ⋅ b" by (simp add: distributive left_minus)
also have "… ∈ I" by (simp add: Ideal)
finally have ab: "a ⋅ b - a' ⋅ b ∈ I" .
from b have [simp]: "b - b' ∈ I" ..
have "a' ⋅ b - a' ⋅ b' = a' ⋅ (b - b')" by (simp add: distributive right_minus)
also have "… ∈ I" by (simp add: Ideal)
finally have a'b': "a' ⋅ b - a' ⋅ b' ∈ I" .
have "a ⋅ b - a' ⋅ b' = (a ⋅ b - a' ⋅ b) + (a' ⋅ b - a' ⋅ b')"
by (simp add: additive.associative) (simp add: additive.associative [symmetric])
also have "… ∈ I" using ab a'b' by simp
finally show "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence" by auto
qed
text ‹p 101, ll 23--24›
sublocale ring_congruence where E = Ring_Congruence
by unfold_locales (rule multiplicative_congruence)
end
text ‹p 101, ll 24--26›
locale quotient_ring = Ideal begin
text ‹p 101, ll 24--26›
sublocale quotient: Ring "R / (subgroup_of_additive_group_of_ring.Ring_Congruence I R (+) 𝟬)" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭" ..
text ‹p 101, l 26›
lemmas Left_Coset = additive.Left_CosetE
text ‹Equation 17 (1)›
text ‹p 101, l 28›
lemmas quotient_addition = additive.factor_composition
text ‹Equation 17 (2)›
text ‹p 101, l 29›
theorem quotient_multiplication [simp]:
"⟦ a ∈ R; b ∈ R ⟧ ⟹ (a +| I) [⋅] (b +| I) = a ⋅ b +| I"
using multiplicative.Class_commutes_with_composition additive.Class_is_Left_Coset by auto
text ‹p 101, l 30›
lemmas quotient_zero = additive.factor_unit
lemmas quotient_negative = additive.factor_inverse
end
subsection ‹Homomorphisms of Rings. Basic Theorems›
text ‹Def 2.3›
text ‹p 106, ll 7--9›
locale ring_homomorphism =
map η R R' + source: Ring R "(+)" "(⋅)" 𝟬 𝟭 + target: Ring R' "(+')" "(⋅')" "𝟬'" "𝟭'" +
additive: group_homomorphism η R "(+)" 𝟬 R' "(+')" "𝟬'" +
multiplicative: Monoid_homomorphism η R "(⋅)" 𝟭 R' "(⋅')" "𝟭'"
for η
and R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›)
and R' and addition' (infixl ‹+''› 65) and multiplication' (infixl ‹⋅''› 70) and zero' (‹𝟬''›) and unit' (‹𝟭''›)
text ‹p 106, l 17›
locale ring_epimorphism = ring_homomorphism + surjective_map η R R'
text ‹p 106, ll 14--18›
sublocale quotient_ring ⊆ natural: ring_epimorphism
where η = additive.Class and R' = "R / (subgroup_of_additive_group_of_ring.Ring_Congruence I R (+) 𝟬)" and addition' = "([+])" and multiplication' = "([⋅])"
and zero' = "additive.Class 𝟬" and unit' = "additive.Class 𝟭"
..
context ring_homomorphism begin
text ‹
Jacobson reasons via @{term "a - b ∈ additive.Ker"} being a congruence; we prefer the direct proof,
since it is very simple.
›
text ‹p 106, ll 19--21›
sublocale kernel: Ideal where I = additive.Ker
by unfold_locales (auto simp: additive.Ker_image multiplicative.commutes_with_composition)
end
text ‹p 106, l 22›
locale ring_monomorphism = ring_homomorphism + injective_map η R R'
context ring_homomorphism begin
text ‹p 106, ll 21--23›
theorem ring_monomorphism_iff_kernel_unit:
"ring_monomorphism η R (+) (⋅) 𝟬 𝟭 R' (+') (⋅') 𝟬' 𝟭' ⟷ additive.Ker = {𝟬}" (is "?monom ⟷ ?ker")
proof
assume ?monom then interpret ring_monomorphism . show ?ker by (simp add: additive.injective_iff_kernel_unit [symmetric])
next
assume ?ker then show ?monom by unfold_locales (simp add: additive.injective_iff_kernel_unit)
qed
end
text ‹p 106, ll 23--25›
sublocale ring_homomorphism ⊆ image: Subring "η ` R" R' "(+')" "(⋅')" "𝟬'" "𝟭'" ..
text ‹p 106, ll 26--27›
locale ideal_in_kernel =
ring_homomorphism + contained: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 for I +
assumes subset: "I ⊆ additive.Ker"
begin
text ‹p 106, ll 26--27›
notation contained.additive.quotient_composition (infixl ‹[+]› 65)
notation contained.multiplicative.quotient_composition (infixl ‹[⋅]› 70)
text ‹Provides @{text additive.induced}, which Jacobson calls $\bar{\eta}$.›
text ‹p 106, l 30›
sublocale additive: normal_subgroup_in_kernel η R "(+)" 𝟬 R' "(+')" "𝟬'" I
rewrites "normal_subgroup.Congruence I R addition zero = contained.Ring_Congruence"
by unfold_locales (rule subset contained.additive_congruence)+
text ‹Only the multiplicative part needs some work.›
text ‹p 106, ll 27--30›
sublocale induced: ring_homomorphism additive.induced "R / (subgroup_of_additive_group_of_ring.Ring_Congruence I R (+) 𝟬)" "([+])" "([⋅])" "contained.additive.Class 𝟬" "contained.additive.Class 𝟭"
using contained.multiplicative.Class_commutes_with_composition
by unfold_locales
(auto elim!: contained.additive.Left_CosetE simp: contained.additive.Class_is_Left_Coset multiplicative.commutes_with_composition multiplicative.commutes_with_unit)
text ‹p 106, l 30; p 107, ll 1--3›
text ‹
@{term additive.induced} denotes Jacobson's $\bar{\eta}$. We have the commutativity of the diagram, where
@{term additive.induced} is unique: @{thm [display] additive.factorization} @{thm [display] additive.uniqueness}
›
end
text ‹Fundamental Theorem of Homomorphisms of Rings›
text ‹p 107, l 6›
locale ring_homomorphism_fundamental = ring_homomorphism begin
text ‹p 107, l 6›
notation kernel.additive.quotient_composition (infixl ‹[+]› 65)
notation kernel.multiplicative.quotient_composition (infixl ‹[⋅]› 70)
text ‹p 107, l 6›
sublocale ideal_in_kernel where I = additive.Ker by unfold_locales rule
text ‹p 107, ll 8--9›
sublocale natural: ring_epimorphism
where η = kernel.additive.Class and R' = "R / (subgroup_of_additive_group_of_ring.Ring_Congruence additive.Ker R (+) 𝟬)"
and addition' = "kernel.additive.quotient_composition"
and multiplication' = "kernel.multiplicative.quotient_composition"
and zero' = "kernel.additive.Class 𝟬" and unit' = "kernel.additive.Class 𝟭"
..
text ‹p 107, l 9›
sublocale induced: ring_monomorphism
where η = additive.induced and R = "R / (subgroup_of_additive_group_of_ring.Ring_Congruence additive.Ker R (+) 𝟬)"
and addition = "kernel.additive.quotient_composition"
and multiplication = "kernel.multiplicative.quotient_composition"
and zero = "kernel.additive.Class 𝟬" and unit = "kernel.additive.Class 𝟭"
by unfold_locales (simp add: additive.induced_inj_on)
end
text ‹p 107, l 11›
locale ring_isomorphism = ring_homomorphism + bijective_map η R R' begin
text ‹p 107, l 11›
sublocale ring_monomorphism ..
sublocale ring_epimorphism ..
text ‹p 107, l 11›
lemma inverse_ring_isomorphism:
"ring_isomorphism (restrict (inv_into R η) R') R' (+') (⋅') 𝟬' 𝟭' R (+) (⋅) 𝟬 𝟭"
proof
fix x y
assume "x ∈ R'" and "y ∈ R'"
then obtain u v where *: "η u = x" "η v = y" "u ∈ R" "v ∈ R"
using surjective by blast
then show "restrict (inv_into R η) R' (x +' y) = restrict (inv_into R η) R' x + restrict (inv_into R η) R' y"
by (auto simp flip: additive.commutes_with_composition)
show "restrict (inv_into R η) R' (x ⋅' y) = restrict (inv_into R η) R' x ⋅ restrict (inv_into R η) R' y"
using * by (auto simp: inv_into_f_eq multiplicative.commutes_with_composition)
next
show "restrict (inv_into R η) R' 𝟬' = 𝟬"
using additive.commutes_with_unit by force
show "restrict (inv_into R η) R' 𝟭' = 𝟭"
using multiplicative.commutes_with_unit by auto
show "bij_betw (restrict (inv_into R η) R') R' R"
using bij_betw_inverse by blast
qed
end
text ‹p 107, l 11›
definition isomorphic_as_rings (infixl ‹≅⇩R› 50)
where "ℛ ≅⇩R ℛ' ⟷ (let (R, addition, multiplication, zero, unit) = ℛ; (R', addition', multiplication', zero', unit') = ℛ' in
(∃η. ring_isomorphism η R addition multiplication zero unit R' addition' multiplication' zero' unit'))"
text ‹p 107, l 11›
lemma isomorphic_as_rings_symmetric:
"(R, addition, multiplication, zero, unit) ≅⇩R (R', addition', multiplication', zero', unit') ⟹
(R', addition', multiplication', zero', unit') ≅⇩R (R, addition, multiplication, zero, unit)"
by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism)
context ring_homomorphism begin
text ‹Corollary›
text ‹p 107, ll 11--12›
theorem image_is_isomorphic_to_quotient_ring:
"∃K add mult zero one. Ideal K R (+) (⋅) 𝟬 𝟭 ∧ (η ` R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩R (R / (subgroup_of_additive_group_of_ring.Ring_Congruence K R (+) 𝟬), add, mult, zero, one)"
proof -
interpret image: ring_homomorphism_fundamental where R' = "η ` R"
by unfold_locales (auto simp: target.additive.commutative additive.commutes_with_composition
multiplicative.commutes_with_composition target.distributive multiplicative.commutes_with_unit)
have "ring_isomorphism image.additive.induced (R / (subgroup_of_additive_group_of_ring.Ring_Congruence additive.Ker R (+) 𝟬)) ([+]) ([⋅]) (kernel.additive.Class 𝟬) (kernel.additive.Class 𝟭) (η ` R) (+') (⋅') 𝟬' 𝟭'"
by unfold_locales (simp add: image.additive.induced_image bij_betw_def)
then have "(η ` R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩R (R / (subgroup_of_additive_group_of_ring.Ring_Congruence additive.Ker R (+) 𝟬), ([+]), ([⋅]), kernel.additive.Class 𝟬, kernel.additive.Class 𝟭)"
by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism)
moreover have "Ideal additive.Ker R (+) (⋅) 𝟬 𝟭" ..
ultimately show ?thesis by blast
qed
end
subsection ‹Abstract type of rings›
lemma trivial_Ring': "Ring' trivial_monoid trivial_monoid"
proof
qed (simp_all add: Monoid.mcarrier_monoid Monoid.munit_monoid trivial_Monoid
trivial_monoid_def Monoid.mmult_monoid trivial_Monoid trivial_Monoid_invertible)
lemma trivial_Ring: "Ring {undefined} (λx y. undefined) (λx y. undefined) undefined undefined"
proof -
have "commutative_monoid_axioms {undefined} (λx y. undefined)"
by (simp add: commutative_monoid_axioms.intro)
moreover have "Ring_axioms {undefined} (λx y. undefined) (λx y. undefined)"
by (simp add: Ring_axioms.intro)
ultimately show ?thesis
by (auto simp: Ring_def Abelian_Group_def commutative_monoid_def trivial_Group trivial_Monoid)
qed
typedef 'a ring = "{(addition::'a monoid, multiplication). Ring' addition multiplication}"
morphisms "dest_ring" "ring"
using trivial_Ring' by blast
declare dest_ring_inverse [simp]
definition "trivial_ring ≡ ring (trivial_monoid, trivial_monoid)"
definition radd where "radd m ≡ fst (dest_ring m)"
definition rmult where "rmult m ≡ snd (dest_ring m)"
definition rcarrier where "rcarrier m ≡ mcarrier (radd m)"
lemma ring_is_Ring [iff]: "Ring' (radd m) (rmult m)"
by (metis Product_Type.Collect_case_prodD dest_ring radd_def rmult_def)
lemma ring_collapse [simp]: "ring (radd r, rmult r) = r"
by (simp add: radd_def rmult_def)
text ‹Allows reference to the current ring space within the locale as a value›
definition (in Ring') "Self ≡ ring (additive, multiplicative)"
lemma (in Ring') radd_Self [simp]: "radd Self = additive"
by (simp add: Ring'_axioms Self_def radd_def ring_inverse)
lemma (in Ring') rmult_Self [simp]: "rmult Self = multiplicative"
by (simp add: Ring'_axioms Self_def ring_inverse rmult_def)
text ‹Further accessors, mirroring the @{typ "'a monoid"} type: the additive and
multiplicative operations and the two distinguished constants @{text 𝟬}, @{text 𝟭}
recovered from the component monoids. (We keep @{const radd}/@{const rmult} returning
whole @{typ "'a monoid"} values, as @{locale Ring'} is built on those.)›
definition radd_op where "radd_op m ≡ mmult (radd m)"
definition rmult_op where "rmult_op m ≡ mmult (rmult m)"
definition rzero where "rzero m ≡ munit (radd m)"
definition rone where "rone m ≡ munit (rmult m)"
text ‹The value really is a ring: the analogue of @{thm [source] monoid_is_Monoid}.›
lemma Ring_ring [iff]: "Ring (rcarrier m) (radd_op m) (rmult_op m) (rzero m) (rone m)"
using Ring'.Ring [OF ring_is_Ring [of m]]
by (simp add: rcarrier_def radd_op_def rmult_op_def rzero_def rone_def)
text ‹Computing the accessors of a ring built from its component monoids.›
lemma (in Ring') radd_ring [simp]: "radd (ring (additive, multiplicative)) = additive"
by (simp add: Ring'_axioms radd_def ring_inverse)
lemma (in Ring') rmult_ring [simp]: "rmult (ring (additive, multiplicative)) = multiplicative"
by (simp add: Ring'_axioms rmult_def ring_inverse)
lemma (in Ring') rcarrier_ring [simp]: "rcarrier (ring (additive, multiplicative)) = mcarrier additive"
by (simp add: rcarrier_def)
lemma (in Ring') rzero_ring [simp]: "rzero (ring (additive, multiplicative)) = munit additive"
by (simp add: rzero_def)
lemma (in Ring') rone_ring [simp]: "rone (ring (additive, multiplicative)) = munit multiplicative"
by (simp add: rone_def)
lemma (in Ring') radd_op_ring [simp]: "radd_op (ring (additive, multiplicative)) = mmult additive"
by (simp add: radd_op_def)
lemma (in Ring') rmult_op_ring [simp]: "rmult_op (ring (additive, multiplicative)) = mmult multiplicative"
by (simp add: rmult_op_def)
text ‹Within the mathematical @{locale Ring} locale, the component monoids form a
@{locale Ring'}, so the current ring can be referred to as a value.›
lemma (in Ring) Ring'_Self_components:
"Ring' (monoid (R, (+), 𝟬)) (monoid (R, (⋅), 𝟭))"
proof -
have a: "mcarrier (monoid (R, (+), 𝟬)) = R" "mmult (monoid (R, (+), 𝟬)) = (+)"
"munit (monoid (R, (+), 𝟬)) = 𝟬"
by (simp_all add: additive.mcarrier_monoid additive.mmult_monoid additive.munit_monoid)
have m: "mcarrier (monoid (R, (⋅), 𝟭)) = R" "mmult (monoid (R, (⋅), 𝟭)) = (⋅)"
"munit (monoid (R, (⋅), 𝟭)) = 𝟭"
by (simp_all add: multiplicative.mcarrier_monoid multiplicative.mmult_monoid multiplicative.munit_monoid)
show ?thesis
by (simp add: Ring'_def a m Ring_axioms)
qed
definition (in Ring) "Self ≡ ring (monoid (R, (+), 𝟬), monoid (R, (⋅), 𝟭))"
lemma (in Ring) rcarrier_Self [simp]: "rcarrier Self = R"
by (simp add: Self_def Ring'.rcarrier_ring Ring'_Self_components additive.mcarrier_monoid)
lemma (in Ring) rzero_Self [simp]: "rzero Self = 𝟬"
by (simp add: Self_def Ring'.rzero_ring Ring'_Self_components additive.munit_monoid)
lemma (in Ring) rone_Self [simp]: "rone Self = 𝟭"
by (simp add: Self_def Ring'.rone_ring Ring'_Self_components multiplicative.munit_monoid)
lemma (in Ring) radd_op_Self [simp]: "radd_op Self = (+)"
by (simp add: Self_def Ring'.radd_op_ring Ring'_Self_components additive.mmult_monoid)
lemma (in Ring) rmult_op_Self [simp]: "rmult_op Self = (⋅)"
by (simp add: Self_def Ring'.rmult_op_ring Ring'_Self_components multiplicative.mmult_monoid)
text ‹The one abstract @{typ "'a ring"} type serves all the ring-like structures: which
one a value belongs to is recorded by a predicate on its accessors. (We provide the
field predicate, used in Galois theory; the others follow the same shape.)›
definition is_field where
"is_field r ≡ Field (rcarrier r) (radd_op r) (rmult_op r) (rzero r) (rone r)"
lemma is_fieldI:
"Field (rcarrier r) (radd_op r) (rmult_op r) (rzero r) (rone r) ⟹ is_field r"
by (simp add: is_field_def)
lemma is_fieldD:
"is_field r ⟹ Field (rcarrier r) (radd_op r) (rmult_op r) (rzero r) (rone r)"
by (simp add: is_field_def)
subsection ‹Linking the locale-based field theory to Isabelle's type classes›
text ‹
Following the ‹Met_TC› pattern of ‹HOL-Analysis.Abstract_Metric_Spaces›
(where ‹interpretation Met_TC: Metric_space UNIV dist› feeds the type-class operations
into the locale), we interpret the locale-based @{locale Field} at an arbitrary
type-class field, with the whole type as carrier. This lets the locale-based
constructions to come (polynomials, splitting fields, Galois groups) be applied to
concrete type-class fields such as ‹real› and ‹complex›.
›
text ‹The additive-group, multiplicative-monoid and ring bridge lemmas need only the ring axioms,
so we state them at the weakest suitable type class @{class comm_ring_1} rather than @{class field}.
This lets the same bridge serve integral domains (e.g.\ ‹int›, in theory ‹IntRing›), not just fields.›
lemma add_group_TC: "Group (UNIV :: 'a :: group_add set) plus 0"
proof (rule GroupI)
fix u :: 'a
show "∃v ∈ UNIV. plus u v = 0 ∧ plus v u = 0" by (rule bexI [where x = "uminus u"]) simp_all
qed (auto simp: algebra_simps)
lemma add_abelian_TC: "Abelian_Group (UNIV :: 'a :: ab_group_add set) plus 0"
proof (rule Abelian_Group.intro [OF add_group_TC])
show "commutative_monoid UNIV plus (0::'a)"
by unfold_locales (simp_all add: ac_simps)
qed
lemma mult_monoid_TC: "Monoid (UNIV :: 'a :: monoid_mult set) (*) 1"
by unfold_locales (auto simp: ac_simps)
lemma mult_cmonoid_TC: "commutative_monoid (UNIV :: 'a :: comm_monoid_mult set) (*) 1"
by unfold_locales (auto simp: ac_simps)
lemma ring_TC: "Ring (UNIV :: 'a :: ring_1 set) plus times 0 1"
proof (intro Ring.intro add_abelian_TC)
show "Monoid (UNIV::'a set) (*) 1"
using mult_monoid_TC by blast
show "Ring_axioms (UNIV::'a set) plus (*)" by unfold_locales (auto simp: algebra_simps)
qed
lemma comm_ring_TC: "commutative_ring (UNIV :: 'a :: comm_ring_1 set) plus (*) 0 1"
by (rule commutative_ring.intro [OF ring_TC mult_cmonoid_TC])
text ‹At an integral domain, the locale @{locale integral_domain} holds: the type class provides
nontriviality (@{thm zero_neq_one}) and the absence of zero divisors (@{thm mult_eq_0_iff}).›
lemma idom_TC: "integral_domain (UNIV :: 'a :: idom set) plus (*) 0 1"
proof -
interpret R: commutative_ring "UNIV :: 'a set" "plus" "(*)" "0" "1" by (rule comm_ring_TC)
show ?thesis
proof (unfold_locales)
show "(1::'a) ≠ 0" by simp
next
fix a b :: 'a assume "a * b = 0" then show "a = 0 ∨ b = 0" by simp
qed
qed