Theory HOL-Algebra.Generated_Fields

(*  Title:      HOL/Algebra/Generated_Fields.thy
    Author:     Martin Baillon
*)

theory Generated_Fields
imports Generated_Rings Subrings Multiplicative_Group
begin

inductive_set
  generate_field :: "('a, 'b) ring_scheme β‡’ 'a set β‡’ 'a set"
  for R and H where
    one  : "πŸ­β‡˜R⇙ ∈ generate_field R H"
  | incl : "h ∈ H ⟹ h ∈ generate_field R H"
  | a_inv: "h ∈ generate_field R H ⟹ βŠ–β‡˜R⇙ h ∈ generate_field R H"
  | m_inv: "⟦ h ∈ generate_field R H; h β‰  πŸ¬β‡˜R⇙ ⟧ ⟹ invβ‡˜R⇙ h ∈ generate_field R H"
  | eng_add : "⟦ h1 ∈ generate_field R H; h2 ∈ generate_field R H ⟧ ⟹ h1 βŠ•β‡˜R⇙ h2 ∈ generate_field R H"
  | eng_mult: "⟦ h1 ∈ generate_field R H; h2 ∈ generate_field R H ⟧ ⟹ h1 βŠ—β‡˜R⇙ h2 ∈ generate_field R H"


subsectionβ€ΉBasic Properties of Generated Rings - First Partβ€Ί

lemma (in field) generate_field_in_carrier:
  assumes "H βŠ† carrier R"
  shows "h ∈ generate_field R H ⟹ h ∈ carrier R"
  apply (induction rule: generate_field.induct)
  using assms field_Units
  by blast+

lemma (in field) generate_field_incl:
  assumes "H βŠ† carrier R"
  shows "generate_field R H βŠ† carrier R"
  using generate_field_in_carrier[OF assms] by auto
       
lemma (in field) zero_in_generate: "πŸ¬β‡˜R⇙ ∈ generate_field R H"
  using one a_inv generate_field.eng_add one_closed r_neg
  by metis

lemma (in field) generate_field_is_subfield:
  assumes "H βŠ† carrier R"
  shows "subfield (generate_field R H) R"
proof (intro subfieldI', simp_all add: m_inv)
  show "subring (generate_field R H) R"
    by (auto intro: subringI[of "generate_field R H"]
             simp add: eng_add a_inv eng_mult one generate_field_in_carrier[OF assms])
qed

lemma (in field) generate_field_is_add_subgroup:
  assumes "H βŠ† carrier R"
  shows "subgroup (generate_field R H) (add_monoid R)"
  using subring.axioms(1)[OF subfieldE(1)[OF generate_field_is_subfield[OF assms]]] .

lemma (in field) generate_field_is_field :
  assumes "H βŠ† carrier R"
  shows "field (R ⦇ carrier := generate_field R H ⦈)"
  using subfield_iff generate_field_is_subfield assms by simp

lemma (in field) generate_field_min_subfield1:
  assumes "H βŠ† carrier R"
    and "subfield E R" "H βŠ† E"
  shows "generate_field R H βŠ† E"
proof
  fix h
  assume h: "h ∈ generate_field R H"
  show "h ∈ E"
    using h and assms(3) and subfield_m_inv[OF assms(2)]
    by (induct rule: generate_field.induct)
       (auto simp add: subringE(3,5-7)[OF subfieldE(1)[OF assms(2)]])
qed

lemma (in field) generate_fieldI:
  assumes "H βŠ† carrier R"
    and "subfield E R" "H βŠ† E"
    and "β‹€K. ⟦ subfield K R; H βŠ† K ⟧ ⟹ E βŠ† K"
  shows "E = generate_field R H"
proof
  show "E βŠ† generate_field R H"
    using assms generate_field_is_subfield generate_field.incl by (metis subset_iff)
  show "generate_field R H βŠ† E"
    using generate_field_min_subfield1[OF assms(1-3)] by simp
qed

lemma (in field) generate_fieldE:
  assumes "H βŠ† carrier R" and "E = generate_field R H"
  shows "subfield E R" and "H βŠ† E" and "β‹€K. ⟦ subfield K R; H βŠ† K ⟧ ⟹ E βŠ† K"
proof -
  show "subfield E R" using assms generate_field_is_subfield by simp
  show "H βŠ† E" using assms(2) by (simp add: generate_field.incl subsetI)
  show "β‹€K. subfield K R  ⟹ H βŠ† K ⟹ E βŠ† K"
    using assms generate_field_min_subfield1 by auto
qed

lemma (in field) generate_field_min_subfield2:
  assumes "H βŠ† carrier R"
  shows "generate_field R H = β‹‚{K. subfield K R ∧ H βŠ† K}"
proof
  have "subfield (generate_field R H) R ∧ H βŠ† generate_field R H"
    by (simp add: assms generate_fieldE(2) generate_field_is_subfield)
  thus "β‹‚{K. subfield K R ∧ H βŠ† K} βŠ† generate_field R H" by blast
next
  have "β‹€K. subfield K R ∧ H βŠ† K ⟹ generate_field R H βŠ† K"
    by (simp add: assms generate_field_min_subfield1)
  thus "generate_field R H βŠ† β‹‚{K. subfield K R ∧ H βŠ† K}" by blast
qed

lemma (in field) mono_generate_field:
  assumes "I βŠ† J" and "J βŠ† carrier R"
  shows "generate_field R I βŠ† generate_field R J"
proof-
  have "I βŠ† generate_field R J "
    using assms generate_fieldE(2) by blast
  thus "generate_field R I βŠ† generate_field R J"
    using generate_field_min_subfield1[of I "generate_field R J"] assms generate_field_is_subfield[OF assms(2)]
    by blast
qed


lemma (in field) subfield_gen_incl :
  assumes "subfield H R"
    and  "subfield K R"
    and "I βŠ† H"
    and "I βŠ† K"
  shows "generate_field (R⦇carrier := K⦈) I βŠ† generate_field (R⦇carrier := H⦈) I"
proof
  have incl_HK: "generate_field (R ⦇ carrier := J ⦈) I βŠ† J"
    if J_def : "subfield J R" "I βŠ† J" for J
    using field.mono_generate_field[of "(R⦇carrier := J⦈)" I J] subfield_iff(2)[OF J_def(1)]
      field.generate_field_in_carrier[of "R⦇carrier := J⦈"]  field_axioms J_def
    by auto

  fix x
  have "x ∈ generate_field (R⦇carrier := K⦈) I ⟹ x ∈ generate_field (R⦇carrier := H⦈) I"
  proof (induction  rule : generate_field.induct)
    case one
    have "πŸ­β‡˜R⦇carrier := Hβ¦ˆβ‡™ βŠ— πŸ­β‡˜R⦇carrier := Kβ¦ˆβ‡™ = πŸ­β‡˜R⦇carrier := Hβ¦ˆβ‡™" by simp
    moreover have "πŸ­β‡˜R⦇carrier := Hβ¦ˆβ‡™ βŠ— πŸ­β‡˜R⦇carrier := Kβ¦ˆβ‡™ = πŸ­β‡˜R⦇carrier := Kβ¦ˆβ‡™" by simp
    ultimately show ?case using assms generate_field.one by metis
  next
    case (incl h)
    thus ?case using generate_field.incl by force
  next
    case (a_inv h)
    have "a_inv (R⦇carrier := K⦈) h = a_inv R h" 
      using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] a_inv
        subring.axioms(1)[OF subfieldE(1)[OF assms(2)]]
      unfolding comm_group_def a_inv_def by auto
    moreover have "a_inv (R⦇carrier := H⦈) h = a_inv R h"
      using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] a_inv
        subring.axioms(1)[OF subfieldE(1)[OF assms(1)]]
      unfolding  comm_group_def a_inv_def by auto
    ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce
  next
    case (m_inv h) 
    have h_K : "h ∈ (K - {𝟬})" using incl_HK[OF assms(2) assms(4)] m_inv by auto
    hence "m_inv (R⦇carrier := K⦈) h = m_inv R h" 
      using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]]
        group.m_inv_consistent[of "mult_of R" "K - {𝟬}"] field_mult_group units_of_inv
        subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp
      by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2))
    moreover have h_H : "h ∈ (H - {𝟬})" using incl_HK[OF assms(1) assms(3)] m_inv by auto
    hence "m_inv (R⦇carrier := H⦈) h = m_inv R h"
      using  field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]]
        group.m_inv_consistent[of "mult_of R" "H - {𝟬}"] field_mult_group 
        subgroup_mult_of[OF assms(1)]  unfolding mult_of_def apply simp
      by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def)
    ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce
  next
    case (eng_add h1 h2)
    thus ?case using incl_HK assms generate_field.eng_add by force
  next
    case (eng_mult h1 h2)
    thus ?case using generate_field.eng_mult by force
  qed
  thus "x ∈ generate_field (R⦇carrier := K⦈) I ⟹ x ∈ generate_field (R⦇carrier := H⦈) I"
    by auto
qed

lemma (in field) subfield_gen_equality:
  assumes "subfield H R" "K βŠ† H"
  shows "generate_field R K = generate_field (R ⦇ carrier := H ⦈) K"
  using subfield_gen_incl[OF assms(1) carrier_is_subfield assms(2)] assms subringE(1)
        subfield_gen_incl[OF carrier_is_subfield assms(1) _ assms(2)] subfieldE(1)[OF assms(1)]
  by force

end