# 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]