|
1 (* ************************************************************************** *) |
|
2 (* Title: Generated_Fields.thy *) |
|
3 (* Author: Martin Baillon *) |
|
4 (* ************************************************************************** *) |
|
5 |
|
6 theory Generated_Fields |
|
7 |
|
8 imports Generated_Rings Subrings Multiplicative_Group |
|
9 |
|
10 begin |
|
11 |
|
12 inductive_set |
|
13 generate_field :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
14 for R and H where |
|
15 one : "\<one>\<^bsub>R\<^esub> \<in> generate_field R H" |
|
16 | incl : "h \<in> H \<Longrightarrow> h \<in> generate_field R H" |
|
17 | a_inv: "h \<in> generate_field R H \<Longrightarrow> \<ominus>\<^bsub>R\<^esub> h \<in> generate_field R H" |
|
18 | m_inv: "\<lbrakk> h \<in> generate_field R H; h \<noteq> \<zero>\<^bsub>R\<^esub> \<rbrakk> \<Longrightarrow> inv\<^bsub>R\<^esub> h \<in> generate_field R H" |
|
19 | eng_add : "\<lbrakk> h1 \<in> generate_field R H; h2 \<in> generate_field R H \<rbrakk> \<Longrightarrow> h1 \<oplus>\<^bsub>R\<^esub> h2 \<in> generate_field R H" |
|
20 | eng_mult: "\<lbrakk> h1 \<in> generate_field R H; h2 \<in> generate_field R H \<rbrakk> \<Longrightarrow> h1 \<otimes>\<^bsub>R\<^esub> h2 \<in> generate_field R H" |
|
21 |
|
22 |
|
23 subsection\<open>Basic Properties of Generated Rings - First Part\<close> |
|
24 |
|
25 lemma (in field) generate_field_in_carrier: |
|
26 assumes "H \<subseteq> carrier R" |
|
27 shows "h \<in> generate_field R H \<Longrightarrow> h \<in> carrier R" |
|
28 apply (induction rule: generate_field.induct) |
|
29 using assms field_Units |
|
30 by blast+ |
|
31 |
|
32 lemma (in field) generate_field_incl: |
|
33 assumes "H \<subseteq> carrier R" |
|
34 shows "generate_field R H \<subseteq> carrier R" |
|
35 using generate_field_in_carrier[OF assms] by auto |
|
36 |
|
37 lemma (in field) zero_in_generate: "\<zero>\<^bsub>R\<^esub> \<in> generate_field R H" |
|
38 using one a_inv generate_field.eng_add one_closed r_neg |
|
39 by metis |
|
40 |
|
41 lemma (in field) generate_field_is_subfield: |
|
42 assumes "H \<subseteq> carrier R" |
|
43 shows "subfield (generate_field R H) R" |
|
44 proof (intro subfieldI', simp_all add: m_inv) |
|
45 show "subring (generate_field R H) R" |
|
46 by (auto intro: subringI[of "generate_field R H"] |
|
47 simp add: eng_add a_inv eng_mult one generate_field_in_carrier[OF assms]) |
|
48 qed |
|
49 |
|
50 lemma (in field) generate_field_is_add_subgroup: |
|
51 assumes "H \<subseteq> carrier R" |
|
52 shows "subgroup (generate_field R H) (add_monoid R)" |
|
53 using subring.axioms(1)[OF subfieldE(1)[OF generate_field_is_subfield[OF assms]]] . |
|
54 |
|
55 lemma (in field) generate_field_is_field : |
|
56 assumes "H \<subseteq> carrier R" |
|
57 shows "field (R \<lparr> carrier := generate_field R H \<rparr>)" |
|
58 using subfield_iff generate_field_is_subfield assms by simp |
|
59 |
|
60 lemma (in field) generate_field_min_subfield1: |
|
61 assumes "H \<subseteq> carrier R" |
|
62 and "subfield E R" "H \<subseteq> E" |
|
63 shows "generate_field R H \<subseteq> E" |
|
64 proof |
|
65 fix h |
|
66 assume h: "h \<in> generate_field R H" |
|
67 show "h \<in> E" |
|
68 using h and assms(3) and subfield_m_inv[OF assms(2)] |
|
69 by (induct rule: generate_field.induct) |
|
70 (auto simp add: subringE(3,5-7)[OF subfieldE(1)[OF assms(2)]]) |
|
71 qed |
|
72 |
|
73 lemma (in field) generate_fieldI: |
|
74 assumes "H \<subseteq> carrier R" |
|
75 and "subfield E R" "H \<subseteq> E" |
|
76 and "\<And>K. \<lbrakk> subfield K R; H \<subseteq> K \<rbrakk> \<Longrightarrow> E \<subseteq> K" |
|
77 shows "E = generate_field R H" |
|
78 proof |
|
79 show "E \<subseteq> generate_field R H" |
|
80 using assms generate_field_is_subfield generate_field.incl by (metis subset_iff) |
|
81 show "generate_field R H \<subseteq> E" |
|
82 using generate_field_min_subfield1[OF assms(1-3)] by simp |
|
83 qed |
|
84 |
|
85 lemma (in field) generate_fieldE: |
|
86 assumes "H \<subseteq> carrier R" and "E = generate_field R H" |
|
87 shows "subfield E R" and "H \<subseteq> E" and "\<And>K. \<lbrakk> subfield K R; H \<subseteq> K \<rbrakk> \<Longrightarrow> E \<subseteq> K" |
|
88 proof - |
|
89 show "subfield E R" using assms generate_field_is_subfield by simp |
|
90 show "H \<subseteq> E" using assms(2) by (simp add: generate_field.incl subsetI) |
|
91 show "\<And>K. subfield K R \<Longrightarrow> H \<subseteq> K \<Longrightarrow> E \<subseteq> K" |
|
92 using assms generate_field_min_subfield1 by auto |
|
93 qed |
|
94 |
|
95 lemma (in field) generate_field_min_subfield2: |
|
96 assumes "H \<subseteq> carrier R" |
|
97 shows "generate_field R H = \<Inter>{K. subfield K R \<and> H \<subseteq> K}" |
|
98 proof |
|
99 have "subfield (generate_field R H) R \<and> H \<subseteq> generate_field R H" |
|
100 by (simp add: assms generate_fieldE(2) generate_field_is_subfield) |
|
101 thus "\<Inter>{K. subfield K R \<and> H \<subseteq> K} \<subseteq> generate_field R H" by blast |
|
102 next |
|
103 have "\<And>K. subfield K R \<and> H \<subseteq> K \<Longrightarrow> generate_field R H \<subseteq> K" |
|
104 by (simp add: assms generate_field_min_subfield1) |
|
105 thus "generate_field R H \<subseteq> \<Inter>{K. subfield K R \<and> H \<subseteq> K}" by blast |
|
106 qed |
|
107 |
|
108 lemma (in field) mono_generate_field: |
|
109 assumes "I \<subseteq> J" and "J \<subseteq> carrier R" |
|
110 shows "generate_field R I \<subseteq> generate_field R J" |
|
111 proof- |
|
112 have "I \<subseteq> generate_field R J " |
|
113 using assms generate_fieldE(2) by blast |
|
114 thus "generate_field R I \<subseteq> generate_field R J" |
|
115 using generate_field_min_subfield1[of I "generate_field R J"] assms generate_field_is_subfield[OF assms(2)] |
|
116 by blast |
|
117 qed |
|
118 |
|
119 |
|
120 lemma (in field) subfield_gen_incl : |
|
121 assumes "subfield H R" |
|
122 and "subfield K R" |
|
123 and "I \<subseteq> H" |
|
124 and "I \<subseteq> K" |
|
125 shows "generate_field (R\<lparr>carrier := K\<rparr>) I \<subseteq> generate_field (R\<lparr>carrier := H\<rparr>) I" |
|
126 proof |
|
127 {fix J assume J_def : "subfield J R" "I \<subseteq> J" |
|
128 have "generate_field (R \<lparr> carrier := J \<rparr>) I \<subseteq> J" |
|
129 using field.mono_generate_field[of "(R\<lparr>carrier := J\<rparr>)" I J] subfield_iff(2)[OF J_def(1)] |
|
130 field.generate_field_in_carrier[of "R\<lparr>carrier := J\<rparr>"] field_axioms J_def |
|
131 by auto} |
|
132 note incl_HK = this |
|
133 {fix x have "x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I" |
|
134 proof (induction rule : generate_field.induct) |
|
135 case one |
|
136 have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub>" by simp |
|
137 moreover have "\<one>\<^bsub>R\<lparr>carrier := H\<rparr>\<^esub> \<otimes> \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub> = \<one>\<^bsub>R\<lparr>carrier := K\<rparr>\<^esub>" by simp |
|
138 ultimately show ?case using assms generate_field.one by metis |
|
139 next |
|
140 case (incl h) thus ?case using generate_field.incl by force |
|
141 next |
|
142 case (a_inv h) |
|
143 note hyp = this |
|
144 have "a_inv (R\<lparr>carrier := K\<rparr>) h = a_inv R h" |
|
145 using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] hyp |
|
146 subring.axioms(1)[OF subfieldE(1)[OF assms(2)]] |
|
147 unfolding comm_group_def a_inv_def by auto |
|
148 moreover have "a_inv (R\<lparr>carrier := H\<rparr>) h = a_inv R h" |
|
149 using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] hyp |
|
150 subring.axioms(1)[OF subfieldE(1)[OF assms(1)]] |
|
151 unfolding comm_group_def a_inv_def by auto |
|
152 ultimately show ?case using generate_field.a_inv a_inv.IH by fastforce |
|
153 next |
|
154 case (m_inv h) |
|
155 note hyp = this |
|
156 have h_K : "h \<in> (K - {\<zero>})" using incl_HK[OF assms(2) assms(4)] hyp by auto |
|
157 hence "m_inv (R\<lparr>carrier := K\<rparr>) h = m_inv R h" |
|
158 using field.m_inv_mult_of[OF subfield_iff(2)[OF assms(2)]] |
|
159 group.m_inv_consistent[of "mult_of R" "K - {\<zero>}"] field_mult_group units_of_inv |
|
160 subgroup_mult_of subfieldE[OF assms(2)] unfolding mult_of_def apply simp |
|
161 by (metis h_K mult_of_def mult_of_is_Units subgroup.mem_carrier units_of_carrier assms(2)) |
|
162 moreover have h_H : "h \<in> (H - {\<zero>})" using incl_HK[OF assms(1) assms(3)] hyp by auto |
|
163 hence "m_inv (R\<lparr>carrier := H\<rparr>) h = m_inv R h" |
|
164 using field.m_inv_mult_of[OF subfield_iff(2)[OF assms(1)]] |
|
165 group.m_inv_consistent[of "mult_of R" "H - {\<zero>}"] field_mult_group |
|
166 subgroup_mult_of[OF assms(1)] unfolding mult_of_def apply simp |
|
167 by (metis h_H field_Units m_inv_mult_of mult_of_is_Units subgroup.mem_carrier units_of_def) |
|
168 ultimately show ?case using generate_field.m_inv m_inv.IH h_H by fastforce |
|
169 next |
|
170 case (eng_add h1 h2) |
|
171 thus ?case using incl_HK assms generate_field.eng_add by force |
|
172 next |
|
173 case (eng_mult h1 h2) |
|
174 thus ?case using generate_field.eng_mult by force |
|
175 qed} |
|
176 thus "\<And>x. x \<in> generate_field (R\<lparr>carrier := K\<rparr>) I \<Longrightarrow> x \<in> generate_field (R\<lparr>carrier := H\<rparr>) I" |
|
177 by auto |
|
178 qed |
|
179 |
|
180 lemma (in field) subfield_gen_equality: |
|
181 assumes "subfield H R" "K \<subseteq> H" |
|
182 shows "generate_field R K = generate_field (R \<lparr> carrier := H \<rparr>) K" |
|
183 using subfield_gen_incl[OF assms(1) carrier_is_subfield assms(2)] assms subringE(1) |
|
184 subfield_gen_incl[OF carrier_is_subfield assms(1) _ assms(2)] subfieldE(1)[OF assms(1)] |
|
185 by force |
|
186 |
|
187 |
|
188 |
|
189 end |
|
190 |