Theory Subfield

(*TODO: move to HOL-Computational_Algebra.Field_as_Ring*)
section ‹Subfields and Field Homomorphisms (Type-Class Setting)›

theory Subfield
  imports "HOL-Computational_Algebra.Polynomial"
begin

text ‹
  We develop field-extension theory generically over an
  ambient field @{typ "'a :: field"}, taking a ∗‹subfield› to be a subset closed under the
  field operations..)
›

subsection ‹The subfield generated by a set›

inductive_set generate_field :: "'a :: field set ⇒ 'a set" for K :: "'a set" where
  generate_field_base [intro]:    "x ∈ K ⟹ x ∈ generate_field K"
| generate_field_0 [intro]:       "0 ∈ generate_field K"
| generate_field_1 [intro]:       "1 ∈ generate_field K"
| generate_field_minus [intro]:   "x ∈ generate_field K ⟹ -x ∈ generate_field K"
| generate_field_add [intro]:     "x ∈ generate_field K ⟹ y ∈ generate_field K ⟹ x + y ∈ generate_field K"
| generate_field_mult [intro]:    "x ∈ generate_field K ⟹ y ∈ generate_field K ⟹ x * y ∈ generate_field K"
| generate_field_inverse [intro]: "x ∈ generate_field K ⟹ inverse x ∈ generate_field K"

lemma subset_generate_field: "A ⊆ generate_field A"
  by (auto intro: generate_field_base)


subsection ‹The subfield locale›

locale Subfield =
  fixes K :: "'a :: field set"
  assumes zero_closed [intro, simp]: "0 ∈ K"
  assumes one_closed [intro, simp]: "1 ∈ K"
  assumes add_closed [intro]: "x ∈ K ⟹ y ∈ K ⟹ x + y ∈ K"
  assumes uminus_closed [intro]: "x ∈ K ⟹ -x ∈ K"
  assumes mult_closed [intro]: "x ∈ K ⟹ y ∈ K ⟹ x * y ∈ K"
  assumes inverse_closed [intro]: "x ∈ K ⟹ inverse x ∈ K"
begin

lemma diff_closed [intro]: "x ∈ K ⟹ y ∈ K ⟹ x - y ∈ K"
  using add_closed[of x "-y"] by auto

lemma divide_closed [intro]: "x ∈ K ⟹ y ∈ K ⟹ x / y ∈ K"
  using mult_closed[of x, OF _ inverse_closed[of y]] by (simp add: field_simps)

lemma power_closed [intro]: "x ∈ K ⟹ x ^ n ∈ K"
  by (induction n) auto

lemma of_nat_closed [intro]: "of_nat n ∈ K"
  by (induction n) auto

lemma of_int_closed [intro]: "of_int n ∈ K"
  by (induction n) auto

lemma sum_closed [intro]: "(⋀x. x ∈ A ⟹ f x ∈ K) ⟹ (∑x∈A. f x) ∈ K"
  by (induction A rule: infinite_finite_induct) auto

lemma prod_closed [intro]: "(⋀x. x ∈ A ⟹ f x ∈ K) ⟹ (∏x∈A. f x) ∈ K"
  by (induction A rule: infinite_finite_induct) auto

lemma cardK_gt1: 
  assumes "finite K" shows "card K > 1"
proof -
  have pair: "{0, 1} ⊆ K" by auto
  with card_mono[OF assms pair] show ?thesis by simp
qed

end

lemma subfield_generate_field [intro]:
  fixes A :: "'a :: field set"
  shows "Subfield (generate_field A)"
  by standard (auto intro: generate_field.intros)

lemma generate_field_least:
  assumes "Subfield K" "A ⊆ K"
  shows   "generate_field A ⊆ K"
proof
  fix x assume x: "x ∈ generate_field A"
  interpret Subfield K by fact
  from x show "x ∈ K"
    by induction (use assms(2) in auto)
qed

lemma generate_field_mono: "A ⊆ B ⟹ generate_field A ⊆ generate_field B"
  by (meson order.trans generate_field_least subfield_generate_field subset_generate_field)

lemma generate_field_mono': "A ⊆ B ⟹ x ∈ generate_field A ⟹ x ∈ generate_field B"
  using generate_field_mono by blast

lemma generate_field_collapse [simp]: "generate_field (generate_field X) = generate_field X"
  using generate_field_least subfield_generate_field subset_generate_field by blast

lemma generate_field_Un_collapse1 [simp]:
  "generate_field (generate_field A ∪ B) = generate_field (A ∪ B)"
proof
  show "generate_field (A ∪ B) ⊆ generate_field (generate_field A ∪ B)"
    using subset_generate_field by (intro generate_field_mono) auto
  thus "generate_field (generate_field A ∪ B) ⊆ generate_field (A ∪ B)"
    by (metis generate_field_least le_sup_iff subfield_generate_field subset_generate_field)
qed

lemma generate_field_Un_collapse2 [simp]:
  "generate_field (A ∪ generate_field B) = generate_field (A ∪ B)"
  using generate_field_Un_collapse1[of B A]
  by (simp add: Un_commute del: generate_field_Un_collapse1)


subsection ‹Field homomorphisms on a subfield›

locale field_hom_on = Subfield K for K :: "'a :: field set" +
  fixes f :: "'a ⇒ 'b :: field"
  assumes hom_0 [simp]: "f 0 = 0"
  assumes hom_1 [simp]: "f 1 = 1"
  assumes hom_add: "x ∈ K ⟹ y ∈ K ⟹ f (x + y) = f x + f y"
  assumes hom_mult: "x ∈ K ⟹ y ∈ K ⟹ f (x * y) = f x * f y"
begin

lemma hom_uminus: "x ∈ K ⟹ f (-x) = -f x"
  using hom_add[of x "-x"] by (simp add: uminus_closed add_eq_0_iff)

lemma hom_diff: "x ∈ K ⟹ y ∈ K ⟹ f (x - y) = f x - f y"
  using hom_add[of x "-y"] hom_uminus[of y] uminus_closed[of y] by simp

lemma hom_inverse: "x ∈ K - {0} ⟹ f (inverse x) = inverse (f x)"
  using hom_mult[of x "inverse x"]
  by (auto simp: uminus_closed add_eq_0_iff divide_simps divide_closed mult_ac)

lemma hom_inverse_all: "x ∈ K ⟹ f (inverse x) = inverse (f x)"
  by (cases "x = 0") (auto simp: hom_inverse)

lemma hom_divide: "x ∈ K ⟹ y ∈ K - {0} ⟹ f (x / y) = f x / f y"
  using hom_mult[of x "inverse y"] hom_inverse[of y] inverse_closed[of y]
  by (simp add: field_simps)

lemma kernel_triv: 
  assumes "u ∈ K - {0}" "f u = 0" 
  shows False 
  by (metis Diff_iff divide_self_if hom_1 hom_divide insert_iff one_neq_zero assms)

text ‹A field homomorphism is injective on its domain.›
lemma inj_on: "inj_on f K"
proof 
  fix x y assume "x ∈ K" "y ∈ K" "f x = f y"
  thus "x = y" using kernel_triv[of "x - y"] by (auto simp: hom_diff diff_closed)
qed

lemma generate_field_subK: "S ⊆ K ⟹ generate_field S ⊆ K" 
  using Subfield_axioms by (rule generate_field_least)

text ‹The image under @{term f} of the subfield generated by a subset @{term "S ⊆ K"} is
  contained in the subfield generated by the image @{term "f ` S"}: the homomorphism laws
  carry each generation step over (here @{term f} need only be a homomorphism on @{term K},
  and @{term "generate_field S ⊆ K"} keeps every intermediate element in range).›
lemma image_generate_field_subset:
  assumes S: "S ⊆ K"
  shows "f ` generate_field S ⊆ generate_field (f ` S)"
proof
  fix y assume "y ∈ f ` generate_field S"
  then obtain x where x: "x ∈ generate_field S" and yx: "y = f x" by blast
  from x have "f x ∈ generate_field (f ` S)"
  proof (induction rule: generate_field.induct)
    case (generate_field_minus x)
    then have "x ∈ K" using generate_field_subK S by auto
    then show ?case using generate_field_minus.IH by (simp add: hom_uminus generate_field.intros)
  next
    case (generate_field_add x y)
    then have "x ∈ K" "y ∈ K" using generate_field_subK S by auto
    then show ?case using generate_field_add.IH by (simp add: hom_add generate_field.intros)
  next
    case (generate_field_mult x y)
    then have "x ∈ K" "y ∈ K" using generate_field_subK S by auto
    then show ?case using generate_field_mult.IH by (simp add: hom_mult generate_field.intros)
  next
    case (generate_field_inverse x)
    then have "x ∈ K" using generate_field_subK S by auto
    then show ?case using generate_field_inverse.IH by (simp add: hom_inverse_all generate_field.intros)
  qed (auto simp: generate_field.intros)
  then show "y ∈ generate_field (f ` S)" using yx by simp
qed

text ‹The image of a generated subfield is itself a subfield (of the target type).›
lemma image_generate_field_subfield:
  assumes S: "S ⊆ K"
  shows "Subfield (f ` generate_field S)"
proof
  show "0 ∈ f ` generate_field S" using hom_0 by (metis generate_field_0 image_eqI)
  show "1 ∈ f ` generate_field S" using hom_1 by (metis generate_field_1 image_eqI)
next
  fix x y assume "x ∈ f ` generate_field S" "y ∈ f ` generate_field S"
  then obtain a b where a: "a ∈ generate_field S" "x = f a"
    and b: "b ∈ generate_field S" "y = f b" by blast
  have aK: "a ∈ K" and bK: "b ∈ K" using a b generate_field_subK S by auto
  show "x + y ∈ f ` generate_field S"
    by (metis a aK b bK generate_field.generate_field_add hom_add image_eqI)
  show "x * y ∈ f ` generate_field S"
    by (metis a aK b bK generate_field.generate_field_mult hom_mult image_iff)
next
  fix x assume "x ∈ f ` generate_field S"
  then obtain a where a: "a ∈ generate_field S" "x = f a" by blast
  have aK: "a ∈ K" using a generate_field_subK S by auto
  show "- x ∈ f ` generate_field S"
    by (metis a aK generate_field.generate_field_minus hom_uminus image_eqI)
  show "inverse x ∈ f ` generate_field S"
    by (metis a aK hom_inverse_all image_iff Subfield.inverse_closed subfield_generate_field)
qed

text ‹Hence the image of a generated subfield is exactly the subfield generated by the image.
  (Both sides live in the target type, so this is an unconditional naturality statement.)›
lemma image_generate_field_eq:
  assumes S: "S ⊆ K"
  shows "f ` generate_field S = generate_field (f ` S)"
  by (simp add: assms generate_field_least image_generate_field_subfield
      image_generate_field_subset image_mono order_antisym subset_generate_field)

end

end