# Theory 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"]
qed

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"
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
{fix J assume J_def : "subfield J R" "I ⊆ J"
have "generate_field (R ⦇ carrier := J ⦈) I ⊆ 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}
note incl_HK = this
{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)
note hyp = this
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] hyp
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] hyp
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)
note hyp = this
have h_K : "h ∈ (K - {𝟬})" using incl_HK[OF assms(2) assms(4)] hyp 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)] hyp 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
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. 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
```