Theory Characteristic

section ‹The characteristic of a ring; finite domains have prime characteristic›

theory Characteristic
  imports Ring_Theory "HOL-Computational_Algebra.Primes"
begin

text ‹The natural-number multiples @{text "n ⋅ 𝟭"} of the unit form a ring homomorphism
  @{text "ℕ → R"}.  Its kernel determines the ∗‹characteristic› of the ring; for a finite
  integral domain the characteristic is a prime, and the multiples @{text "n ⋅ 𝟭"} form the prime
  subfield.  This is the first step toward the structural theorem that a finite field has
  prime-power order.›

context Ring
begin

text ‹The @{term n}-fold sum @{text "𝟭 + … + 𝟭"} (@{term n} summands), i.e. the image of @{term n}
  under the canonical map @{text "ℕ → R"}.›
definition natmult :: "nat ⇒ 'a"
  where "natmult n = (((+) 𝟭) ^^ n) 𝟬"

lemma natmult_0 [simp]: "natmult 0 = 𝟬"
  by (simp add: natmult_def)

lemma natmult_Suc [simp]: "natmult (Suc n) = 𝟭 + natmult n"
  by (simp add: natmult_def)

lemma natmult_closed [simp]: "natmult n ∈ R"
  by (induct n) auto

lemma natmult_1 [simp]: "natmult 1 = 𝟭"
  by simp

text ‹Additivity: @{text "natmult (m + n) = natmult m + natmult n"}.›
lemma natmult_add: "natmult (m + n) = natmult m + natmult n"
  by (induct m) (auto simp: additive.associative)

text ‹Multiplicativity: @{text "natmult (m * n) = natmult m ⋅ natmult n"}.›
lemma natmult_mult: "natmult (m * n) = natmult m ⋅ natmult n"
by (induct m) (auto simp: natmult_add distributive)

text ‹Cancellation across a difference: if two multiples agree, the multiple of their difference
  vanishes.›
lemma natmult_diff_zero:
  assumes "m ≤ n" and "natmult m = natmult n"
  shows "natmult (n - m) = 𝟬"
proof -
  have "natmult m + natmult (n - m) = natmult n"
    using natmult_add[of m "n - m"] le_add_diff_inverse[OF assms(1)] by simp
  also have "… = natmult m + 𝟬" using assms by (simp add: additive.right_unit)
  finally have "natmult m + natmult (n - m) = natmult m + 𝟬" .
  then show ?thesis
    using additive.invertible_left_cancel[of "natmult m" "natmult (n - m)" 𝟬] by simp
qed

end

context integral_domain
begin

text ‹The ∗‹characteristic›: the least positive @{term n} with @{text "n ⋅ 𝟭 = 𝟬"} (or @{text 0} if
  no such @{term n} exists).›
definition characteristic :: nat
  where "characteristic = (LEAST n. 0 < n ∧ natmult n = 𝟬)"

text ‹In a ∗‹finite› integral domain the map @{term natmult} cannot be injective, so some positive
  multiple of @{term 𝟭} vanishes.›
lemma finite_natmult_not_inj:
  assumes "finite R" shows "∃n. 0 < n ∧ natmult n = 𝟬"
proof -
  have "¬ inj natmult"
    by (meson assms image_subsetI infinite_iff_countable_subset natmult_closed)
  then obtain i j where ij: "i ≠ j" and eq: "natmult i = natmult j" by (auto simp: inj_def)
  show ?thesis
  proof (cases "i < j")
    case True
    then have "natmult (j - i) = 𝟬" using eq by (simp add: natmult_diff_zero)
    with True show ?thesis
      using zero_less_diff by blast
  next
    case False
    then have "natmult (i - j) = 𝟬"
      by (simp add: eq natmult_diff_zero)
    then show ?thesis
      by (meson False ij linorder_cases zero_less_diff)
  qed
qed

lemma characteristic_pos:
  assumes "finite R" shows "0 < characteristic ∧ natmult characteristic = 𝟬"
  unfolding characteristic_def
  using LeastI_ex[OF finite_natmult_not_inj[OF assms]] .

lemma characteristic_least:
  "⟦ 0 < n; natmult n = 𝟬 ⟧ ⟹ characteristic ≤ n"
  unfolding characteristic_def by (rule Least_le) simp

text ‹The characteristic exceeds @{text 1}: @{text "1 ⋅ 𝟭 = 𝟭 ≠ 𝟬"} by nontriviality.›
lemma characteristic_gt_1:
  assumes "finite R" shows "1 < characteristic"
  by (metis assms characteristic_pos nontrivial less_one nat_neq_iff natmult_1)

text ‹∗‹The characteristic of a finite integral domain is prime.›  If it factored as
  @{term "characteristic = a * b"} nontrivially, then @{text "natmult a ⋅ natmult b = 𝟬"} would
  force one factor's multiple to vanish, contradicting minimality.›
theorem characteristic_prime:
  assumes finR: "finite R" shows "prime characteristic"
proof (unfold prime_nat_iff, intro conjI allI impI)
  show "1 < characteristic" using characteristic_gt_1[OF finR] .
next
  fix m assume mdvd: "m dvd characteristic"
  then obtain k where ch: "characteristic = m * k" by (rule dvdE)
  have chz: "natmult characteristic = 𝟬" using characteristic_pos[OF finR] by simp
  have "natmult m ⋅ natmult k = 𝟬" using chz ch by (simp add: natmult_mult)
  then have "natmult m = 𝟬 ∨ natmult k = 𝟬" using no_zero_divisors by simp
  ― ‹Both @{term m} and @{term k} are positive (the product is positive).›
  have cpos: "0 < characteristic" using characteristic_pos[OF finR] by simp
  have mpos: "0 < m" and kpos: "0 < k" using ch cpos by auto
  then show "m = 1 ∨ m = characteristic"
  proof (cases "natmult m = 𝟬")
    case True
    then show ?thesis
      using characteristic_least cpos dvd_imp_le le_antisym mdvd mpos by presburger
  next
    case False
    then have nk: "natmult k = 𝟬" using ‹natmult m = 𝟬 ∨ natmult k = 𝟬› by simp
    have kdvd: "k dvd characteristic" using ch by auto
    have keq: "k = characteristic"
      by (simp add: characteristic_least cpos dvd_imp_le kdvd kpos le_antisym nk)
    then show ?thesis
      using ch cpos by force
  qed
qed

end

end