Theory Prime_Subfield
section ‹The prime subfield of a finite integral domain›
theory Prime_Subfield
imports Characteristic GF_p Divisibility_Theory
begin
subsection ‹Finite integral domains›
text ‹A finite integral domain is a field. Multiplication by a nonzero element is an
injective self-map of the finite carrier, hence surjective; a preimage of the unit is a
multiplicative inverse.›
theorem (in integral_domain) finite_integral_domain_imp_field:
assumes fin: "finite R"
shows "Field R (+) (⋅) 𝟬 𝟭"
proof (rule Field.intro[OF commutative_ring_axioms nontrivial_ring_axioms])
show "Field_axioms R (⋅) 𝟬 𝟭"
proof
fix a
assume aR: "a ∈ R" and anz: "a ≠ 𝟬"
have inj: "inj_on ((⋅) a) R"
by (rule inj_onI) (rule mult_cancel_left[OF aR _ _ anz])
have closed: "((⋅) a) ` R ⊆ R"
using aR by (blast intro: multiplicative.composition_closed)
have "𝟭 ∈ (⋅) a ` R"
using endo_inj_surj[OF fin closed inj] multiplicative.unit_closed by simp
then obtain b where bR: "b ∈ R" and ab: "a ⋅ b = 𝟭" by blast
have ba: "b ⋅ a = 𝟭"
using multiplicative.commutative[OF bR aR] ab by simp
show "multiplicative.invertible a"
by (rule multiplicative.invertibleI[OF ab ba bR])
qed
qed
text ‹The characteristic map factors through the existing concrete field
‹GF(characteristic)›. Its image is the canonical prime subfield of the finite
domain. This is the bridge between the carrier-set ring hierarchy and the finite-field
constructions.›
locale finite_integral_domain = integral_domain +
assumes finite_carrier: "finite R"
begin
definition prime_subfield :: "'a set"
where "prime_subfield = natmult ` {0..<characteristic}"
definition characteristic_embedding :: "nat ⇒ 'a"
where "characteristic_embedding = restrict natmult {0..<characteristic}"
lemma natmult_characteristic_multiple:
shows "natmult (k * characteristic) = 𝟬"
proof -
have "natmult characteristic = 𝟬" using characteristic_pos[OF finite_carrier] by simp
then show ?thesis by (simp add: natmult_mult)
qed
lemma natmult_mod_characteristic:
shows "natmult (n mod characteristic) = natmult n"
proof -
have n: "n = n div characteristic * characteristic + n mod characteristic"
using div_mult_mod_eq[of n characteristic] by simp
have "natmult n = natmult (n div characteristic * characteristic + n mod characteristic)"
by (rule arg_cong[OF n])
also have "… = natmult (n div characteristic * characteristic) + natmult (n mod characteristic)"
by (rule natmult_add)
also have "… = natmult (n mod characteristic)"
using natmult_characteristic_multiple by simp
finally show ?thesis by (rule sym)
qed
lemma natmult_inj_on_characteristic:
shows "inj_on natmult {0..<characteristic}"
proof (rule inj_onI)
fix m n
assume m: "m ∈ {0..<characteristic}" and n: "n ∈ {0..<characteristic}"
and eq: "natmult m = natmult n"
show "m = n"
proof (rule ccontr)
assume "m ≠ n"
consider (mn) "m < n" | (nm) "n < m" using ‹m ≠ n› by linarith
then show False
proof cases
case mn
have pos: "0 < n - m" using mn by simp
have zero: "natmult (n - m) = 𝟬"
using natmult_diff_zero[OF less_imp_le[OF mn] eq] .
have "characteristic ≤ n - m" by (rule characteristic_least[OF pos zero])
moreover have "n - m < characteristic" using n by simp
ultimately show False by simp
next
case nm
have pos: "0 < m - n" using nm by simp
have zero: "natmult (m - n) = 𝟬"
using natmult_diff_zero[OF less_imp_le[OF nm] eq[symmetric]] .
have "characteristic ≤ m - n" by (rule characteristic_least[OF pos zero])
moreover have "m - n < characteristic" using m by simp
ultimately show False by simp
qed
qed
qed
lemma characteristic_embedding_add:
assumes m: "m ∈ {0..<characteristic}" and n: "n ∈ {0..<characteristic}"
shows "characteristic_embedding (gfp_add characteristic m n) =
characteristic_embedding m + characteristic_embedding n"
proof -
have cgt1: "characteristic > 1"
using characteristic_prime[OF finite_carrier] by (simp add: prime_nat_iff)
have closed: "gfp_add characteristic m n ∈ {0..<characteristic}"
by (rule gfp_add_closed[OF cgt1])
have "characteristic_embedding (gfp_add characteristic m n) =
natmult ((m + n) mod characteristic)"
using m n closed by (simp add: characteristic_embedding_def gfp_add_def)
also have "… = natmult (m + n)" by (rule natmult_mod_characteristic)
also have "… = natmult m + natmult n" by (rule natmult_add)
also have "… = characteristic_embedding m + characteristic_embedding n"
using m n by (simp add: characteristic_embedding_def)
finally show ?thesis .
qed
lemma characteristic_embedding_mult:
assumes m: "m ∈ {0..<characteristic}" and n: "n ∈ {0..<characteristic}"
shows "characteristic_embedding (gfp_mult characteristic m n) =
characteristic_embedding m ⋅ characteristic_embedding n"
proof -
have cgt1: "characteristic > 1"
using characteristic_prime[OF finite_carrier] by (simp add: prime_nat_iff)
have closed: "gfp_mult characteristic m n ∈ {0..<characteristic}"
by (rule gfp_mult_closed[OF cgt1])
have "characteristic_embedding (gfp_mult characteristic m n) =
natmult ((m * n) mod characteristic)"
using m n closed by (simp add: characteristic_embedding_def gfp_mult_def)
also have "… = natmult (m * n)" by (rule natmult_mod_characteristic)
also have "… = natmult m ⋅ natmult n" by (rule natmult_mult)
also have "… = characteristic_embedding m ⋅ characteristic_embedding n"
using m n by (simp add: characteristic_embedding_def)
finally show ?thesis .
qed
theorem characteristic_embedding_monomorphism:
shows "ring_monomorphism characteristic_embedding
{0..<characteristic} (gfp_add characteristic) (gfp_mult characteristic) 0 1
R (+) (⋅) 𝟬 𝟭"
proof (intro ring_monomorphism.intro)
interpret GF: Field "{0..<characteristic}" "gfp_add characteristic" "gfp_mult characteristic" 0 1
by (rule gfp_field[OF characteristic_prime[OF finite_carrier]])
show "ring_homomorphism characteristic_embedding
{0..<characteristic} (gfp_add characteristic) (gfp_mult characteristic) 0 1
R (+) (⋅) 𝟬 𝟭"
proof (intro ring_homomorphism.intro)
show "Set_Theory.map characteristic_embedding {0..<characteristic} R"
by unfold_locales (auto simp: characteristic_embedding_def)
show "Ring {0..<characteristic} (gfp_add characteristic) (gfp_mult characteristic) 0 1"
by (rule GF.Ring_axioms)
show "Ring R (+) (⋅) 𝟬 𝟭" by (rule Ring_axioms)
show "group_homomorphism characteristic_embedding
{0..<characteristic} (gfp_add characteristic) 0 R (+) 𝟬"
proof
show "characteristic_embedding ∈ {0..<characteristic} →⇩E R"
by (auto simp: characteristic_embedding_def)
show "⋀x y. ⟦x ∈ {0..<characteristic}; y ∈ {0..<characteristic}⟧ ⟹
characteristic_embedding (gfp_add characteristic x y) =
characteristic_embedding x + characteristic_embedding y"
by (rule characteristic_embedding_add)
show "characteristic_embedding 0 = 𝟬"
using characteristic_pos[OF finite_carrier] by (simp add: characteristic_embedding_def)
qed
show "Monoid_homomorphism characteristic_embedding
{0..<characteristic} (gfp_mult characteristic) 1 R (⋅) 𝟭"
proof
show "characteristic_embedding ∈ {0..<characteristic} →⇩E R"
by (auto simp: characteristic_embedding_def)
show "⋀x y. ⟦x ∈ {0..<characteristic}; y ∈ {0..<characteristic}⟧ ⟹
characteristic_embedding (gfp_mult characteristic x y) =
characteristic_embedding x ⋅ characteristic_embedding y"
by (rule characteristic_embedding_mult)
show "characteristic_embedding 1 = 𝟭"
using characteristic_prime[OF finite_carrier]
by (simp add: characteristic_embedding_def prime_nat_iff)
qed
qed
show "injective_map characteristic_embedding {0..<characteristic} R"
proof
show "characteristic_embedding ∈ {0..<characteristic} →⇩E R"
by (auto simp: characteristic_embedding_def)
show "inj_on characteristic_embedding {0..<characteristic}"
using natmult_inj_on_characteristic
by (simp add: characteristic_embedding_def inj_on_def)
qed
qed
lemma characteristic_embedding_image:
"characteristic_embedding ` {0..<characteristic} = prime_subfield"
by (auto simp: characteristic_embedding_def prime_subfield_def)
theorem prime_subfield_subring:
shows "Subring prime_subfield R (+) (⋅) 𝟬 𝟭"
proof -
interpret E: ring_monomorphism characteristic_embedding
"{0..<characteristic}" "gfp_add characteristic" "gfp_mult characteristic" 0 1
R addition multiplication zero unit
by (rule characteristic_embedding_monomorphism)
show ?thesis using E.image.Subring_axioms by (simp add: characteristic_embedding_image)
qed
theorem prime_subfield_field:
shows "Field prime_subfield (+) (⋅) 𝟬 𝟭"
proof -
interpret P: Subring prime_subfield R addition multiplication zero unit
by (rule prime_subfield_subring)
have ag: "Abelian_Group prime_subfield (+) 𝟬"
proof -
interpret A: Group prime_subfield addition zero
by (rule P.additive.sub.Group_axioms)
show ?thesis
proof
fix x y
assume x: "x ∈ prime_subfield" and y: "y ∈ prime_subfield"
show "x + y = y + x"
by (rule additive.commutative[OF
subsetD[OF P.additive.subset x] subsetD[OF P.additive.subset y]])
qed
qed
have ring: "Ring prime_subfield (+) (⋅) 𝟬 𝟭"
proof (intro Ring.intro)
show "Abelian_Group prime_subfield (+) 𝟬" by (rule ag)
show "Monoid prime_subfield (⋅) 𝟭"
by (rule P.multiplicative.sub.Monoid_axioms)
show "Ring_axioms prime_subfield (+) (⋅)"
proof
fix a b c
assume a: "a ∈ prime_subfield" and b: "b ∈ prime_subfield"
and c: "c ∈ prime_subfield"
show "a ⋅ (b + c) = a ⋅ b + a ⋅ c"
by (rule distributive(1)[OF subsetD[OF P.additive.subset a]
subsetD[OF P.additive.subset b] subsetD[OF P.additive.subset c]])
show "(b + c) ⋅ a = b ⋅ a + c ⋅ a"
by (rule distributive(2)[OF subsetD[OF P.additive.subset a]
subsetD[OF P.additive.subset b] subsetD[OF P.additive.subset c]])
qed
qed
have cr: "commutative_ring prime_subfield (+) (⋅) 𝟬 𝟭"
proof -
interpret S: Ring prime_subfield addition multiplication zero unit by (rule ring)
show ?thesis
proof
fix x y
assume x: "x ∈ prime_subfield" and y: "y ∈ prime_subfield"
show "x ⋅ y = y ⋅ x"
by (rule multiplicative.commutative[OF
subsetD[OF P.multiplicative.subset x]
subsetD[OF P.multiplicative.subset y]])
qed
qed
interpret C: commutative_ring prime_subfield addition multiplication zero unit by (rule cr)
have nt: "nontrivial_ring prime_subfield (+) (⋅) 𝟬 𝟭"
proof
show "𝟭 ≠ 𝟬" by (rule nontrivial)
qed
interpret N: nontrivial_ring prime_subfield addition multiplication zero unit by (rule nt)
have dom: "integral_domain prime_subfield (+) (⋅) 𝟬 𝟭"
proof
fix a b
assume a: "a ∈ prime_subfield" and b: "b ∈ prime_subfield"
and zero: "a ⋅ b = 𝟬"
show "a = 𝟬 ∨ b = 𝟬"
by (rule no_zero_divisors[OF subsetD[OF P.additive.subset a]
subsetD[OF P.additive.subset b] zero])
qed
interpret D: integral_domain prime_subfield addition multiplication zero unit by (rule dom)
have "finite prime_subfield" unfolding prime_subfield_def by simp
then show ?thesis by (rule D.finite_integral_domain_imp_field)
qed
theorem card_prime_subfield:
shows "card prime_subfield = characteristic"
unfolding prime_subfield_def
using natmult_inj_on_characteristic by (simp add: card_image)
end
end