# Theory Field

```section βΉFinite FieldsβΊ

theory Field
imports
"Finite_Fields.Ring_Characteristic"
"HOL-Algebra.Ring_Divisibility"
"HOL-Algebra.IntRing"
begin

text βΉIn some applications it is more convenient to work with natural numbers instead of
@{term "ZFact p"} whose elements are cosets. To support that use case the following definition
introduces an additive and multiplicative structure on @{term "{..<p}"}. After verifying that
the function @{term "zfact_iso"} and its inverse are homomorphisms, the ring and field property
can be transfered from @{term "ZFact p"} to to the structure on @{term "{..<p}"}.βΊ

lemma zfact_iso_0:
assumes "n > 0"
shows "zfact_iso n 0 = π¬βZFact (int n)β"
proof -
let ?I = "Idlβπ΅β {int n}"
have ideal_I: "ideal ?I π΅"

interpret i:ideal "?I" "π΅" using ideal_I by simp
interpret s:ring_hom_ring "π΅" "ZFact (int n)" "(+>βπ΅β) ?I"
using i.rcos_ring_hom_ring ZFact_def by auto

show ?thesis
qed

lemma zfact_prime_is_field:
assumes "Factorial_Ring.prime (p :: nat)"
shows "field (ZFact (int p))"
using zfact_prime_is_finite_field[OF assms] finite_field_def by auto

definition mod_ring :: "nat => nat ring"
where "mod_ring n = β¦
carrier = {..<n},
mult = (Ξ» x y. (x * y) mod n),
one = 1,
zero = 0,
add = (Ξ» x y. (x + y) mod n) β¦"

definition zfact_iso_inv :: "nat β int set β nat" where
"zfact_iso_inv p = inv_into {..<p} (zfact_iso p)"

lemma zfact_iso_inv_0:
assumes n_ge_0: "n > 0"
shows "zfact_iso_inv n π¬βZFact (int n)β = 0"
unfolding zfact_iso_inv_def zfact_iso_0[OF n_ge_0, symmetric] using n_ge_0
by (rule inv_into_f_f[OF zfact_iso_inj], simp add:mod_ring_def)

lemma zfact_coset:
assumes n_ge_0: "n > 0"
assumes "x β carrier (ZFact (int n))"
defines "I β‘ Idlβπ΅β {int n}"
shows "x = I +>βπ΅β (int (zfact_iso_inv n x))"
proof -
have "x β zfact_iso n ` {..<n}"
using assms zfact_iso_ran by simp
hence "zfact_iso n (zfact_iso_inv n x) = x"
unfolding zfact_iso_inv_def by (rule f_inv_into_f)
thus ?thesis unfolding zfact_iso_def I_def by blast
qed

lemma zfact_iso_inv_is_ring_iso:
assumes n_ge_1: "n > 1"
shows "zfact_iso_inv n β ring_iso (ZFact (int n)) (mod_ring n)"
proof (rule ring_iso_memI)
interpret r:cring "(ZFact (int n))"
using ZFact_is_cring by simp

define I where "I = Idlβπ΅β {int n}"

have n_ge_0: "n > 0" using n_ge_1 by simp

interpret i:ideal "I" "π΅"
unfolding I_def using int.genideal_ideal by simp

interpret s:ring_hom_ring "π΅" "ZFact (int n)" "(+>βπ΅β) I"
using i.rcos_ring_hom_ring ZFact_def I_def by auto

show
"βx. x β carrier (ZFact (int n)) βΉ zfact_iso_inv n x β carrier (mod_ring n)"
proof -
fix x
assume "x β carrier (ZFact (int n))"
hence "zfact_iso_inv n x β {..<n}"
unfolding zfact_iso_inv_def
using zfact_iso_ran[OF n_ge_0] inv_into_into by metis

thus "zfact_iso_inv n x β carrier (mod_ring n)"
unfolding mod_ring_def by simp
qed

show "βx y. x β carrier (ZFact (int n)) βΉ y β carrier (ZFact (int n)) βΉ
zfact_iso_inv n (x ββZFact (int n)β y) =
zfact_iso_inv n x ββmod_ring nβ zfact_iso_inv n y"
proof -
fix x y
assume x_carr: "x β carrier (ZFact (int n))"
define x' where "x' = zfact_iso_inv n x"
assume y_carr: "y β carrier (ZFact (int n))"
define y' where "y' = zfact_iso_inv n y"
have "x ββZFact (int n)β y = (I +>βπ΅β (int x')) ββZFact (int n)β (I +>βπ΅β (int y'))"
unfolding x'_def y'_def
using x_carr y_carr zfact_coset[OF n_ge_0] I_def by simp
also have "... = (I +>βπ΅β (int x' * int y'))"
by simp
also have "... = (I +>βπ΅β (int ((x' * y') mod n)))"
unfolding I_def zmod_int by (rule int_cosetI[OF n_ge_0],simp)
also have "... = (I +>βπ΅β (x' ββmod_ring nβ y'))"
unfolding mod_ring_def by simp
also have "... = zfact_iso n (x' ββmod_ring nβ y')"
unfolding zfact_iso_def I_def by simp
finally have a:"x ββZFact (int n)β y = zfact_iso n (x' ββmod_ring nβ y')"
by simp
have b:"x' ββmod_ring nβ y' β {..<n}"
using mod_ring_def n_ge_0 by auto
have "zfact_iso_inv n (zfact_iso n (x' ββmod_ring nβ y')) = x' ββmod_ring nβ y'"
unfolding zfact_iso_inv_def
by (rule inv_into_f_f[OF zfact_iso_inj[OF n_ge_0] b])
thus
"zfact_iso_inv n (x ββZFact (int n)β y) =
zfact_iso_inv n x ββmod_ring nβ zfact_iso_inv n y"
using a x'_def y'_def by simp
qed

show "βx y. x β carrier (ZFact (int n)) βΉ y β carrier (ZFact (int n)) βΉ
zfact_iso_inv n (x ββZFact (int n)β y) =
zfact_iso_inv n x ββmod_ring nβ zfact_iso_inv n y"
proof -
fix x y
assume x_carr: "x β carrier (ZFact (int n))"
define x' where "x' = zfact_iso_inv n x"
assume y_carr: "y β carrier (ZFact (int n))"
define y' where "y' = zfact_iso_inv n y"
have "x ββZFact (int n)β y = (I +>βπ΅β (int x')) ββZFact (int n)β (I +>βπ΅β (int y'))"
unfolding x'_def y'_def
using x_carr y_carr zfact_coset[OF n_ge_0] I_def by simp
also have "... = (I +>βπ΅β (int x' + int y'))"
by simp
also have "... = (I +>βπ΅β (int ((x' + y') mod n)))"
unfolding I_def zmod_int by (rule int_cosetI[OF n_ge_0],simp)
also have "... = (I +>βπ΅β (x' ββmod_ring nβ y'))"
unfolding mod_ring_def by simp
also have "... = zfact_iso n (x' ββmod_ring nβ y')"
unfolding zfact_iso_def I_def by simp
finally have a:"x ββZFact (int n)β y = zfact_iso n (x' ββmod_ring nβ y')"
by simp
have b:"x' ββmod_ring nβ y' β {..<n}"
using mod_ring_def n_ge_0 by auto
have "zfact_iso_inv n (zfact_iso n (x' ββmod_ring nβ y')) = x' ββmod_ring nβ y'"
unfolding zfact_iso_inv_def
by (rule inv_into_f_f[OF zfact_iso_inj[OF n_ge_0] b])
thus
"zfact_iso_inv n (x ββZFact (int n)β y) =
zfact_iso_inv n x ββmod_ring nβ zfact_iso_inv n y"
using a x'_def y'_def by simp
qed

have "π­βZFact (int n)β = zfact_iso n (π­βmod_ring nβ)"
by (simp add:zfact_iso_def ZFact_def I_def[symmetric] mod_ring_def)

thus "zfact_iso_inv n π­βZFact (int n)β = π­βmod_ring nβ"
unfolding zfact_iso_inv_def mod_ring_def
using inv_into_f_f[OF zfact_iso_inj] n_ge_1 by simp

show "bij_betw (zfact_iso_inv n) (carrier (ZFact (int n))) (carrier (mod_ring n))"
using zfact_iso_inv_def mod_ring_def zfact_iso_bij[OF n_ge_0] bij_betw_inv_into
by force
qed

lemma mod_ring_finite:
"finite (carrier (mod_ring n))"

lemma mod_ring_carr:
"x β carrier (mod_ring n) β·  x < n"

lemma mod_ring_is_cring:
assumes n_ge_1: "n > 1"
shows "cring (mod_ring n)"
proof -
have n_ge_0: "n > 0" using n_ge_1 by simp

interpret cring "ZFact (int n)"
using ZFact_is_cring by simp

have "cring ((mod_ring n) β¦ zero := zfact_iso_inv n π¬βZFact (int n)β β¦)"
by (rule ring_iso_imp_img_cring[OF zfact_iso_inv_is_ring_iso[OF n_ge_1]])
moreover have
"(mod_ring n) β¦ zero := zfact_iso_inv n π¬βZFact (int n)β β¦ = mod_ring n"
using zfact_iso_inv_0[OF n_ge_0]
ultimately show ?thesis by simp
qed

lemma zfact_iso_is_ring_iso:
assumes n_ge_1: "n > 1"
shows "zfact_iso n β ring_iso (mod_ring n) (ZFact (int n))"
proof -
have r:"ring (ZFact (int n))"
using ZFact_is_cring cring.axioms(1) by blast

interpret s: ring "(mod_ring n)"
using mod_ring_is_cring cring.axioms(1) n_ge_1 by blast
have n_ge_0: "n > 0" using n_ge_1 by linarith

have
"inv_into (carrier (ZFact (int n))) (zfact_iso_inv n)
β ring_iso (mod_ring n) (ZFact (int n))"
using ring_iso_set_sym[OF r zfact_iso_inv_is_ring_iso[OF n_ge_1]] by simp
moreover have "βx. x β carrier (mod_ring n) βΉ
inv_into (carrier (ZFact (int n))) (zfact_iso_inv n) x = zfact_iso n x"
proof -
fix x
assume "x β carrier (mod_ring n)"
hence "x β {..<n}" by (simp add:mod_ring_def)
thus "inv_into (carrier (ZFact (int n))) (zfact_iso_inv n) x = zfact_iso n x"
unfolding zfact_iso_inv_def
qed

ultimately show ?thesis
using s.ring_iso_restrict by blast
qed

text βΉIf @{term "p"} is a prime than @{term "mod_ring p"} is a field:βΊ

lemma mod_ring_is_field:
assumes"Factorial_Ring.prime p"
shows "field (mod_ring p)"
proof -
have p_ge_0: "p > 0" using assms prime_gt_0_nat by blast
have p_ge_1: "p > 1" using assms prime_gt_1_nat by blast

interpret field "ZFact (int p)"
using zfact_prime_is_field[OF assms] by simp

have "field ((mod_ring p) β¦ zero := zfact_iso_inv p π¬βZFact (int p)β β¦)"
by (rule ring_iso_imp_img_field[OF zfact_iso_inv_is_ring_iso[OF p_ge_1]])

moreover have
"(mod_ring p) β¦ zero := zfact_iso_inv p π¬βZFact (int p)β β¦ = mod_ring p"
using zfact_iso_inv_0[OF p_ge_0]