Theory Closure_Extension
section ‹Extensions of a Field inside the Indexed Polynomial Ring›
theory Closure_Extension
imports Indexed_Poly Poly_Divisibility "HOL.Zorn"
begin
text ‹
Groundwork for the existence of an algebraic closure. Every extension needed for that is
generated by adjoining roots of polynomials over the base field ‹R›, so all of them can be built
inside ∗‹one› fixed type: the indexed polynomials of ‹Indexed_Poly› whose indeterminates are
indexed by pairs ‹(P, i)› --- a polynomial over ‹R› together with a natural number, so that each
polynomial has as many indeterminates available as it could have roots.
Fixing the type in advance is what makes Zorn's lemma applicable: the extensions then form a
∗‹set›, which can be ordered and exhausted. The alternative, iterating a quotient construction to
adjoin one root at a time, changes the type at every step --- a quotient of a ring over \<^typ>‹'a›
has carrier of type \<^typ>‹'a set› --- and so cannot be iterated by induction at all.
An extension is a triple ‹(K, ⊕, ⊗)›: a carrier with its own addition and multiplication. The
operations must be allowed to vary, because an extension realises a quotient ‹M[X]/(Q)›
concretely, by normal forms, and the modulus ‹Q› differs from step to step. The zero and the
unit, by contrast, are the same throughout: the constants ‹𝟬⇩I› and ‹𝟭⇩I›.
❙‹Why the operations are required to be undefined off the carrier.› Two extensions with the same
carrier and the same operations ∗‹on› that carrier are the same extension mathematically, but need
not be equal as triples if the operations disagree elsewhere --- and then the ordering below fails
antisymmetry, so it is not a partial order and Zorn does not apply. HOL-Algebra repairs this after
the fact with a ‹law_restrict› operator and a family of lemmas transporting field-ness,
homomorphisms and isomorphisms across it. Here it is part of what an extension is, which costs one
condition and no lemmas: in the carrier-set architecture the operations are parameters that can be
constrained, rather than record fields that are total by construction.
›
type_synonym 'a root_index = "(nat ⇒ 'a) × nat"
type_synonym 'a ipoly = "'a root_index multiset ⇒ 'a"
type_synonym 'a iop = "'a ipoly ⇒ 'a ipoly ⇒ 'a ipoly"
type_synonym 'a iext = "'a ipoly set × 'a iop × 'a iop"
abbreviation ecarrier :: "'a iext ⇒ 'a ipoly set" where "ecarrier E ≡ fst E"
abbreviation eadd :: "'a iext ⇒ 'a iop" where "eadd E ≡ fst (snd E)"
abbreviation emult :: "'a iext ⇒ 'a iop" where "emult E ≡ snd (snd E)"
subsection ‹Operations defined only on their carrier›
text ‹An operation is ∗‹restricted› to @{term K} when it is @{const undefined} unless both arguments
lie in @{term K}. This is the condition discussed above; the lemma after it is the only thing the
condition is ever used for, and replaces HOL-Algebra's ‹law_restrict› apparatus.›
definition op_restricted :: "'a ipoly set ⇒ 'a iop ⇒ bool"
where "op_restricted K f ⟷ (∀x y. (x ∉ K ∨ y ∉ K) ⟶ f x y = undefined)"
lemma op_restrictedI:
"(⋀x y. x ∉ K ∨ y ∉ K ⟹ f x y = undefined) ⟹ op_restricted K f"
by (simp add: op_restricted_def)
lemma op_restrictedD:
"⟦ op_restricted K f; x ∉ K ∨ y ∉ K ⟧ ⟹ f x y = undefined"
by (simp add: op_restricted_def)
text ‹Two operations restricted to the same carrier and agreeing on it are equal.›
lemma restricted_op_eqI:
assumes f: "op_restricted K f" and g: "op_restricted K g"
and eq: "⋀x y. ⟦ x ∈ K; y ∈ K ⟧ ⟹ f x y = g x y"
shows "f = g"
proof (rule ext, rule ext)
fix x y
show "f x y = g x y"
proof (cases "x ∈ K ∧ y ∈ K")
case True then show ?thesis using eq by simp
next
case False
then have "x ∉ K ∨ y ∉ K" by blast
then show ?thesis using op_restrictedD [OF f] op_restrictedD [OF g] by simp
qed
qed
context Ring
begin
subsection ‹Lifted polynomials›
text ‹A polynomial over @{term R} read as a polynomial over the ambient ring, coefficientwise.
Where HOL-Algebra maps a coefficient ∗‹list› through its constant embedding, a polynomial here is
already a function on exponents, so the lift is a composition.›
definition lift_poly :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a ipoly)"
where "lift_poly P = (λk. ipoly_const (P k))"
lemma lift_poly_apply [simp]: "lift_poly P k = ipoly_const (P k)"
by (simp add: lift_poly_def)
lemma lift_poly_coeff_closed: "P ∈ poly_carrier ⟹ lift_poly P k ∈ ipoly_carrier"
by (simp add: ipoly_const_closed poly_carrier_coeff_closed)
subsection ‹What it is to be an extension›
text ‹Evaluation in an extension, at that extension's own operations.›
abbreviation eeval :: "'a iext ⇒ 'a ipoly ⇒ (nat ⇒ 'a ipoly) ⇒ 'a ipoly"
where "eeval E ≡ Ring.eval (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
text ‹Evaluation in the ∗‹ambient› indexed polynomial ring. A locale prefix is not available here:
we are inside @{locale Ring} already, and interpreting the indexed polynomial ring as a
@{locale Ring} at this point would be self-referential. An abbreviation costs nothing and hides the
five parameters just as well.›
abbreviation ieval :: "'a ipoly ⇒ (nat ⇒ 'a ipoly) ⇒ 'a ipoly"
where "ieval ≡ Ring.eval ipoly_carrier (⊕⇩I) (⊗⇩I) 𝟬⇩I 𝟭⇩I"
text ‹An extension is closed under the roots it mentions: whenever one of its elements involves the
indeterminate @{term "(P, i)"}, that indeterminate belongs to the extension, and is a root of
@{term P} there. This is the condition that forces a ∗‹maximal› extension to split every
polynomial --- an unsplit polynomial leaves some index unused, and adjoining a root at it yields a
strictly larger extension.›
definition root_closed :: "'a iext ⇒ bool"
where "root_closed E ⟷
(∀𝒫 ∈ ecarrier E. ∀P ∈ poly_carrier. ∀i.
¬ index_free 𝒫 (P, i) ⟶
ivar (P, i) ∈ ecarrier E ∧ eeval E (ivar (P, i)) (lift_poly P) = 𝟬⇩I)"
lemma root_closedI:
"(⋀𝒫 P i. ⟦ 𝒫 ∈ ecarrier E; P ∈ poly_carrier; ¬ index_free 𝒫 (P, i) ⟧
⟹ ivar (P, i) ∈ ecarrier E ∧ eeval E (ivar (P, i)) (lift_poly P) = 𝟬⇩I)
⟹ root_closed E"
unfolding root_closed_def by blast
lemma root_closed_mem:
"⟦ root_closed E; 𝒫 ∈ ecarrier E; P ∈ poly_carrier; ¬ index_free 𝒫 (P, i) ⟧
⟹ ivar (P, i) ∈ ecarrier E"
unfolding root_closed_def by blast
lemma root_closed_eval:
"⟦ root_closed E; 𝒫 ∈ ecarrier E; P ∈ poly_carrier; ¬ index_free 𝒫 (P, i) ⟧
⟹ eeval E (ivar (P, i)) (lift_poly P) = 𝟬⇩I"
unfolding root_closed_def by blast
text ‹An extension of @{term R} inside the indexed polynomial ring: a field of indexed polynomials
over @{term R} that contains the constants, induces on them the ring operations of @{term R}, and
is closed under the roots it mentions.›
definition is_extension :: "'a iext ⇒ bool"
where "is_extension E ⟷
Field (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I
∧ ecarrier E ⊆ ipoly_carrier
∧ (∀a ∈ R. ipoly_const a ∈ ecarrier E)
∧ (∀a ∈ R. ∀b ∈ R. eadd E (ipoly_const a) (ipoly_const b) = ipoly_const (a + b))
∧ (∀a ∈ R. ∀b ∈ R. emult E (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b))
∧ root_closed E
∧ op_restricted (ecarrier E) (eadd E)
∧ op_restricted (ecarrier E) (emult E)"
definition extensions :: "'a iext set"
where "extensions = {E. is_extension E}"
lemma extensions_iff [simp]: "E ∈ extensions ⟷ is_extension E"
by (simp add: extensions_def)
text ‹The component facts, so that clients never unfold @{const is_extension}.›
lemma is_extension_field: "is_extension E ⟹ Field (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
by (simp add: is_extension_def)
lemma is_extension_subset: "is_extension E ⟹ ecarrier E ⊆ ipoly_carrier"
by (simp add: is_extension_def)
lemma is_extension_carrier_closed: "⟦ is_extension E; x ∈ ecarrier E ⟧ ⟹ x ∈ ipoly_carrier"
using is_extension_subset by blast
lemma is_extension_const_mem: "⟦ is_extension E; a ∈ R ⟧ ⟹ ipoly_const a ∈ ecarrier E"
by (simp add: is_extension_def)
lemma is_extension_const_add:
"⟦ is_extension E; a ∈ R; b ∈ R ⟧
⟹ eadd E (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
by (simp add: is_extension_def)
lemma is_extension_const_mult:
"⟦ is_extension E; a ∈ R; b ∈ R ⟧
⟹ emult E (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)"
by (simp add: is_extension_def)
lemma is_extension_root_closed: "is_extension E ⟹ root_closed E"
by (simp add: is_extension_def)
lemma is_extension_restricted:
"is_extension E ⟹ op_restricted (ecarrier E) (eadd E)"
"is_extension E ⟹ op_restricted (ecarrier E) (emult E)"
by (simp_all add: is_extension_def)
lemma is_extensionI:
assumes "Field (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
and "ecarrier E ⊆ ipoly_carrier"
and "⋀a. a ∈ R ⟹ ipoly_const a ∈ ecarrier E"
and "⋀a b. ⟦ a ∈ R; b ∈ R ⟧
⟹ eadd E (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
and "⋀a b. ⟦ a ∈ R; b ∈ R ⟧
⟹ emult E (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)"
and "root_closed E"
and "op_restricted (ecarrier E) (eadd E)"
and "op_restricted (ecarrier E) (emult E)"
shows "is_extension E"
unfolding is_extension_def using assms by blast
subsection ‹The ordering by inclusion›
text ‹One extension extends another when its carrier is contained in the other's and its operations
agree with the other's wherever the smaller one is defined.›
definition ext_le :: "'a iext ⇒ 'a iext ⇒ bool"
where "ext_le E F ⟷ ecarrier E ⊆ ecarrier F
∧ (∀x ∈ ecarrier E. ∀y ∈ ecarrier E.
eadd E x y = eadd F x y ∧ emult E x y = emult F x y)"
lemma ext_leI:
"⟦ ecarrier E ⊆ ecarrier F;
⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ eadd E x y = eadd F x y;
⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ emult E x y = emult F x y ⟧
⟹ ext_le E F"
unfolding ext_le_def by blast
lemma ext_le_carrier: "ext_le E F ⟹ ecarrier E ⊆ ecarrier F"
by (simp add: ext_le_def)
lemma ext_le_add: "⟦ ext_le E F; x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ eadd E x y = eadd F x y"
unfolding ext_le_def by blast
lemma ext_le_mult: "⟦ ext_le E F; x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ emult E x y = emult F x y"
unfolding ext_le_def by blast
lemma ext_le_refl: "ext_le E E"
by (simp add: ext_le_def)
lemma ext_le_trans:
assumes EF: "ext_le E F" and FG: "ext_le F G" shows "ext_le E G"
proof (rule ext_leI)
show sub: "ecarrier E ⊆ ecarrier G"
by (rule subset_trans [OF ext_le_carrier [OF EF] ext_le_carrier [OF FG]])
fix x y assume xy: "x ∈ ecarrier E" "y ∈ ecarrier E"
then have xyF: "x ∈ ecarrier F" "y ∈ ecarrier F"
using ext_le_carrier [OF EF] by auto
show "eadd E x y = eadd G x y"
using ext_le_add [OF EF xy(1) xy(2)] ext_le_add [OF FG xyF(1) xyF(2)] by simp
show "emult E x y = emult G x y"
using ext_le_mult [OF EF xy(1) xy(2)] ext_le_mult [OF FG xyF(1) xyF(2)] by simp
qed
text ‹Antisymmetry is where restrictedness earns its place: equal carriers and agreement on them
settle the operations there, and off the carrier both are @{const undefined}.›
lemma ext_le_antisym:
assumes E: "is_extension E" and F: "is_extension F"
and EF: "ext_le E F" and FE: "ext_le F E"
shows "E = F"
proof -
have K: "ecarrier E = ecarrier F"
by (rule subset_antisym [OF ext_le_carrier [OF EF] ext_le_carrier [OF FE]])
have rF: "op_restricted (ecarrier E) (eadd F)" "op_restricted (ecarrier E) (emult F)"
using is_extension_restricted [OF F] K by simp_all
have "eadd E = eadd F"
by (rule restricted_op_eqI [OF is_extension_restricted(1) [OF E] rF(1) ext_le_add [OF EF]])
moreover have "emult E = emult F"
by (rule restricted_op_eqI [OF is_extension_restricted(2) [OF E] rF(2) ext_le_mult [OF EF]])
ultimately have "(ecarrier E, eadd E, emult E) = (ecarrier F, eadd F, emult F)"
using K by simp
then show ?thesis by simp
qed
theorem ext_partial_order: "partial_order_on extensions (relation_of ext_le extensions)"
proof (rule partial_order_on_relation_ofI)
show "⋀E. E ∈ extensions ⟹ ext_le E E" by (rule ext_le_refl)
show "⋀E F G. ⟦ E ∈ extensions; F ∈ extensions; G ∈ extensions; ext_le E F; ext_le F G ⟧
⟹ ext_le E G"
by (rule ext_le_trans)
show "⋀E F. ⟦ E ∈ extensions; F ∈ extensions; ext_le E F; ext_le F E ⟧ ⟹ E = F"
by (metis extensions_iff ext_le_antisym)
qed
subsection ‹Powers and evaluation transfer along the ordering›
text ‹A power or an evaluation of an element of the smaller extension is the same whether computed
there or in the larger one. Nothing beyond ring-ness of the two, carrier inclusion, and agreement
of the operations on the smaller carrier is used --- that is, exactly @{const ext_le} --- so the
same two lemmas serve the union of a chain and the adjunction of a root.
There is no such fact one level down: @{term "commutative_monoid.fincomp"} depends on the
∗‹carrier› as well as the operation, through its @{text M_ify}, so
@{thm [source] commutative_monoid.fincomp_cong'}, which stays inside one monoid, does not apply.
@{thm [source] fincomp_transfer} is what bridges the two carriers.›
lemma ext_le_rpow:
assumes RE: "Ring (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
and RF: "Ring (ecarrier F) (eadd F) (emult F) 𝟬⇩I 𝟭⇩I"
and le: "ext_le E F" and a: "a ∈ ecarrier E"
shows "Ring.rpow (emult F) 𝟭⇩I a n = Ring.rpow (emult E) 𝟭⇩I a n"
proof (induct n)
case 0
show ?case by (simp add: Ring.rpow_0 [OF RE] Ring.rpow_0 [OF RF])
next
case (Suc n)
have cl: "Ring.rpow (emult E) 𝟭⇩I a n ∈ ecarrier E" by (rule Ring.rpow_closed [OF RE a])
have "Ring.rpow (emult F) 𝟭⇩I a (Suc n) = emult F a (Ring.rpow (emult F) 𝟭⇩I a n)"
by (rule Ring.rpow_Suc [OF RF])
also have "… = emult F a (Ring.rpow (emult E) 𝟭⇩I a n)" using Suc by simp
also have "… = emult E a (Ring.rpow (emult E) 𝟭⇩I a n)"
by (rule ext_le_mult [OF le a cl, symmetric])
also have "… = Ring.rpow (emult E) 𝟭⇩I a (Suc n)" by (rule Ring.rpow_Suc [OF RE, symmetric])
finally show ?case .
qed
lemma ext_le_eval:
assumes RE: "Ring (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
and RF: "Ring (ecarrier F) (eadd F) (emult F) 𝟬⇩I 𝟭⇩I"
and le: "ext_le E F" and a: "a ∈ ecarrier E" and p: "⋀k. p k ∈ ecarrier E"
shows "eeval F a p = eeval E a p"
proof -
interpret E: Ring "ecarrier E" "eadd E" "emult E" "𝟬⇩I" "𝟭⇩I" by (rule RE)
have cl: "Ring.rpow (emult E) 𝟭⇩I a i ∈ ecarrier E" for i by (rule Ring.rpow_closed [OF RE a])
have summand: "emult F (p i) (Ring.rpow (emult F) 𝟭⇩I a i)
= emult E (p i) (Ring.rpow (emult E) 𝟭⇩I a i)" for i
using ext_le_rpow [OF RE RF le a] ext_le_mult [OF le p cl] by simp
have inE: "(λi. emult E (p i) (Ring.rpow (emult E) 𝟭⇩I a i)) ∈ A → ecarrier E" for A
using p cl by auto
have "eeval F a p
= commutative_monoid.fincomp (ecarrier F) (eadd F) 𝟬⇩I
(λi. emult F (p i) (Ring.rpow (emult F) 𝟭⇩I a i)) {..Ring.degree 𝟬⇩I p}"
by (rule Ring.eval_def [OF RF])
also have "… = commutative_monoid.fincomp (ecarrier F) (eadd F) 𝟬⇩I
(λi. emult E (p i) (Ring.rpow (emult E) 𝟭⇩I a i)) {..Ring.degree 𝟬⇩I p}"
using summand by simp
also have "… = commutative_monoid.fincomp (ecarrier E) (eadd E) 𝟬⇩I
(λi. emult E (p i) (Ring.rpow (emult E) 𝟭⇩I a i)) {..Ring.degree 𝟬⇩I p}"
proof (rule fincomp_transfer [symmetric])
show "commutative_monoid (ecarrier E) (eadd E) 𝟬⇩I"
using RE by (simp add: Ring_def Abelian_Group_def)
show "commutative_monoid (ecarrier F) (eadd F) 𝟬⇩I"
using RF by (simp add: Ring_def Abelian_Group_def)
show "ecarrier E ⊆ ecarrier F" by (rule ext_le_carrier [OF le])
show "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ eadd E x y = eadd F x y"
by (rule ext_le_add [OF le])
show "(λi. emult E (p i) (Ring.rpow (emult E) 𝟭⇩I a i)) ∈ {..Ring.degree 𝟬⇩I p} → ecarrier E"
by (rule inE)
qed
also have "… = eeval E a p" by (rule Ring.eval_def [OF RE, symmetric])
finally show ?thesis .
qed
subsection ‹The base extension›
text ‹The constants form an extension: a copy of @{term R} inside the indexed polynomial ring,
carrying the ambient operations restricted to it. Besides supplying the upper bound Zorn needs for
the ∗‹empty› chain, this is the check that @{const is_extension} is satisfiable at all --- a
condition as encoded as @{const root_closed} could easily be vacuous, and then everything proved
from it would be too. Here @{const root_closed} holds vacuously ∗‹by design›: a constant involves
no indeterminate, so its hypothesis is never met.›
definition base_ext :: "'a iext"
where "base_ext =
(ipoly_const ` R,
(λx y. if x ∈ ipoly_const ` R ∧ y ∈ ipoly_const ` R then x ⊕⇩I y else undefined),
(λx y. if x ∈ ipoly_const ` R ∧ y ∈ ipoly_const ` R then x ⊗⇩I y else undefined))"
lemma base_ext_carrier [simp]: "ecarrier base_ext = ipoly_const ` R"
by (simp add: base_ext_def)
lemma base_ext_add:
assumes "a ∈ R" and "b ∈ R"
shows "eadd base_ext (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
using assms by (simp add: base_ext_def ipoly_const_add)
lemma base_ext_mult:
assumes "a ∈ R" and "b ∈ R"
shows "emult base_ext (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)"
using assms by (simp add: base_ext_def ipoly_const_mult)
lemma base_ext_restricted:
"op_restricted (ecarrier base_ext) (eadd base_ext)"
"op_restricted (ecarrier base_ext) (emult base_ext)"
by (auto simp: base_ext_def intro!: op_restrictedI)
subsection ‹Unions of chains›
text ‹A chain of extensions: a subset of @{const extensions} any two of whose members are comparable.
Its union is again an extension, and is an upper bound --- which is what Zorn's lemma asks for.›
definition ext_chain :: "'a iext set ⇒ bool"
where "ext_chain C ⟷ C ⊆ extensions ∧ (∀E ∈ C. ∀F ∈ C. ext_le E F ∨ ext_le F E)"
lemma ext_chainD_extension: "⟦ ext_chain C; E ∈ C ⟧ ⟹ is_extension E"
unfolding ext_chain_def by auto
lemma ext_chainD_comparable: "⟦ ext_chain C; E ∈ C; F ∈ C ⟧ ⟹ ext_le E F ∨ ext_le F E"
unfolding ext_chain_def by blast
text ‹The union carries, on each pair of elements, the operations of any member containing both;
the chain condition makes the choice immaterial.›
definition ext_Union :: "'a iext set ⇒ 'a iext"
where "ext_Union C =
(⋃ (ecarrier ` C),
(λx y. if x ∈ ⋃ (ecarrier ` C) ∧ y ∈ ⋃ (ecarrier ` C)
then eadd (SOME E. E ∈ C ∧ x ∈ ecarrier E ∧ y ∈ ecarrier E) x y else undefined),
(λx y. if x ∈ ⋃ (ecarrier ` C) ∧ y ∈ ⋃ (ecarrier ` C)
then emult (SOME E. E ∈ C ∧ x ∈ ecarrier E ∧ y ∈ ecarrier E) x y else undefined))"
lemma ext_Union_carrier [simp]: "ecarrier (ext_Union C) = ⋃ (ecarrier ` C)"
by (simp add: ext_Union_def)
lemma ext_Union_restricted:
"op_restricted (ecarrier (ext_Union C)) (eadd (ext_Union C))"
"op_restricted (ecarrier (ext_Union C)) (emult (ext_Union C))"
by (auto simp: ext_Union_def intro!: op_restrictedI)
context
fixes C :: "'a iext set"
assumes chain: "ext_chain C"
begin
lemma chain_field: "E ∈ C ⟹ Field (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
using chain by (simp add: ext_chainD_extension is_extension_field)
text ‹Two elements of the union lie in a common member: the larger of two members containing them.›
lemma chain_common2:
assumes "x ∈ ecarrier (ext_Union C)" and "y ∈ ecarrier (ext_Union C)"
shows "∃E ∈ C. x ∈ ecarrier E ∧ y ∈ ecarrier E"
proof -
from assms obtain E F where E: "E ∈ C" "x ∈ ecarrier E" and F: "F ∈ C" "y ∈ ecarrier F"
by auto
from ext_chainD_comparable [OF chain E(1) F(1)] show ?thesis
proof
assume "ext_le E F"
then have "x ∈ ecarrier F" using E(2) ext_le_carrier by blast
then show ?thesis using F by blast
next
assume "ext_le F E"
then have "y ∈ ecarrier E" using F(2) ext_le_carrier by blast
then show ?thesis using E by blast
qed
qed
lemma chain_common3:
assumes "x ∈ ecarrier (ext_Union C)" and "y ∈ ecarrier (ext_Union C)"
and "z ∈ ecarrier (ext_Union C)"
shows "∃E ∈ C. x ∈ ecarrier E ∧ y ∈ ecarrier E ∧ z ∈ ecarrier E"
proof -
from chain_common2 [OF assms(1,2)] obtain E
where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E" by blast
from assms(3) obtain F where F: "F ∈ C" "z ∈ ecarrier F" by auto
from ext_chainD_comparable [OF chain E(1) F(1)] show ?thesis
proof
assume "ext_le E F"
then have "x ∈ ecarrier F" "y ∈ ecarrier F" using E ext_le_carrier by blast+
then show ?thesis using F by blast
next
assume "ext_le F E"
then have "z ∈ ecarrier E" using F(2) ext_le_carrier by blast
then show ?thesis using E by blast
qed
qed
text ‹The union's operations agree with those of any member containing both arguments.›
lemma ext_Union_ops:
assumes E: "E ∈ C" and x: "x ∈ ecarrier E" and y: "y ∈ ecarrier E"
shows "eadd (ext_Union C) x y = eadd E x y"
and "emult (ext_Union C) x y = emult E x y"
proof -
have mem: "x ∈ ⋃ (ecarrier ` C)" "y ∈ ⋃ (ecarrier ` C)" using E x y by auto
have ex: "∃F. F ∈ C ∧ x ∈ ecarrier F ∧ y ∈ ecarrier F" using E x y by blast
let ?F = "SOME F. F ∈ C ∧ x ∈ ecarrier F ∧ y ∈ ecarrier F"
have F: "?F ∈ C" and xF: "x ∈ ecarrier ?F" and yF: "y ∈ ecarrier ?F"
using someI_ex [OF ex] by auto
have or: "ext_le E ?F ∨ ext_le ?F E" by (rule ext_chainD_comparable [OF chain E F])
have a: "eadd E x y = eadd ?F x y"
proof (cases "ext_le E ?F")
case True then show ?thesis using x y by (simp add: ext_le_add)
next
case False
then have "ext_le ?F E" using or by blast
then show ?thesis using xF yF by (simp add: ext_le_add)
qed
have m: "emult E x y = emult ?F x y"
proof (cases "ext_le E ?F")
case True then show ?thesis using x y by (simp add: ext_le_mult)
next
case False
then have "ext_le ?F E" using or by blast
then show ?thesis using xF yF by (simp add: ext_le_mult)
qed
show "eadd (ext_Union C) x y = eadd E x y"
using mem a by (simp add: ext_Union_def)
show "emult (ext_Union C) x y = emult E x y"
using mem m by (simp add: ext_Union_def)
qed
lemma ext_Union_upper_bound: "E ∈ C ⟹ ext_le E (ext_Union C)"
by (rule ext_leI) (auto simp: ext_Union_ops)
text ‹Every member's carrier contains ‹𝟬⇩I› and ‹𝟭⇩I›, being an extension of @{term R}.›
lemma chain_zero_one_mem:
assumes E: "E ∈ C" shows "𝟬⇩I ∈ ecarrier E" and "𝟭⇩I ∈ ecarrier E"
proof -
have ext: "is_extension E" using chain E by (rule ext_chainD_extension)
have "ipoly_const 𝟬 ∈ ecarrier E"
by (rule is_extension_const_mem [OF ext additive.unit_closed])
moreover have "ipoly_const 𝟭 ∈ ecarrier E"
by (rule is_extension_const_mem [OF ext multiplicative.unit_closed])
ultimately show "𝟬⇩I ∈ ecarrier E" and "𝟭⇩I ∈ ecarrier E" by simp_all
qed
text ‹The field laws of a single member, extracted through one interpretation so that the union's
proof below can cite them without re-interpreting for every axiom.›
lemma chain_member:
assumes E: "E ∈ C"
shows chain_add_closed: "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧
⟹ eadd E x y ∈ ecarrier E"
and chain_mult_closed: "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧
⟹ emult E x y ∈ ecarrier E"
and chain_add_assoc: "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ eadd E (eadd E x y) z = eadd E x (eadd E y z)"
and chain_mult_assoc: "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ emult E (emult E x y) z = emult E x (emult E y z)"
and chain_add_zero: "⋀x. x ∈ ecarrier E ⟹ eadd E 𝟬⇩I x = x"
and chain_add_zero': "⋀x. x ∈ ecarrier E ⟹ eadd E x 𝟬⇩I = x"
and chain_mult_one: "⋀x. x ∈ ecarrier E ⟹ emult E 𝟭⇩I x = x"
and chain_mult_one': "⋀x. x ∈ ecarrier E ⟹ emult E x 𝟭⇩I = x"
and chain_add_comm: "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧
⟹ eadd E x y = eadd E y x"
and chain_mult_comm: "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧
⟹ emult E x y = emult E y x"
and chain_distrib: "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ emult E x (eadd E y z) = eadd E (emult E x y) (emult E x z)"
and chain_distrib': "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ emult E (eadd E y z) x = eadd E (emult E y x) (emult E z x)"
and chain_add_inv: "⋀x. x ∈ ecarrier E
⟹ ∃y ∈ ecarrier E. eadd E x y = 𝟬⇩I ∧ eadd E y x = 𝟬⇩I"
and chain_mult_inv: "⋀x. ⟦ x ∈ ecarrier E; x ≠ 𝟬⇩I ⟧
⟹ ∃y ∈ ecarrier E. emult E x y = 𝟭⇩I ∧ emult E y x = 𝟭⇩I"
proof -
interpret E: Field "ecarrier E" "eadd E" "emult E" "𝟬⇩I" "𝟭⇩I"
by (rule chain_field [OF E])
show "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ eadd E x y ∈ ecarrier E" by simp
show "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ emult E x y ∈ ecarrier E" by simp
show "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ eadd E (eadd E x y) z = eadd E x (eadd E y z)"
by (simp add: E.additive.associative)
show "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ emult E (emult E x y) z = emult E x (emult E y z)"
by (simp add: E.multiplicative.associative)
show "⋀x. x ∈ ecarrier E ⟹ eadd E 𝟬⇩I x = x" by simp
show "⋀x. x ∈ ecarrier E ⟹ eadd E x 𝟬⇩I = x" by simp
show "⋀x. x ∈ ecarrier E ⟹ emult E 𝟭⇩I x = x" by simp
show "⋀x. x ∈ ecarrier E ⟹ emult E x 𝟭⇩I = x" by simp
show "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ eadd E x y = eadd E y x"
by (simp add: E.additive.commutative)
show "⋀x y. ⟦ x ∈ ecarrier E; y ∈ ecarrier E ⟧ ⟹ emult E x y = emult E y x"
by (simp add: E.multiplicative.commutative)
show "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ emult E x (eadd E y z) = eadd E (emult E x y) (emult E x z)"
by (simp add: E.distributive(1))
show "⋀x y z. ⟦ x ∈ ecarrier E; y ∈ ecarrier E; z ∈ ecarrier E ⟧
⟹ emult E (eadd E y z) x = eadd E (emult E y x) (emult E z x)"
by (simp add: E.distributive(2))
show "⋀x. x ∈ ecarrier E ⟹ ∃y ∈ ecarrier E. eadd E x y = 𝟬⇩I ∧ eadd E y x = 𝟬⇩I"
proof -
fix x assume x: "x ∈ ecarrier E"
have "E.additive.inverse x ∈ ecarrier E" using x by simp
moreover have "eadd E x (E.additive.inverse x) = 𝟬⇩I"
using x by (simp add: E.additive.invertible_right_inverse)
moreover have "eadd E (E.additive.inverse x) x = 𝟬⇩I"
using x by (simp add: E.additive.invertible_left_inverse)
ultimately show "∃y ∈ ecarrier E. eadd E x y = 𝟬⇩I ∧ eadd E y x = 𝟬⇩I" by blast
qed
show "⋀x. ⟦ x ∈ ecarrier E; x ≠ 𝟬⇩I ⟧
⟹ ∃y ∈ ecarrier E. emult E x y = 𝟭⇩I ∧ emult E y x = 𝟭⇩I"
proof -
fix x assume x: "x ∈ ecarrier E" and xnz: "x ≠ 𝟬⇩I"
have inv: "E.multiplicative.invertible x" by (rule E.field_inverse [OF x xnz])
have "E.multiplicative.inverse x ∈ ecarrier E"
by (rule E.multiplicative.invertible_inverse_closed [OF inv x])
moreover have "emult E x (E.multiplicative.inverse x) = 𝟭⇩I"
by (rule E.multiplicative.invertible_right_inverse [OF inv x])
moreover have "emult E (E.multiplicative.inverse x) x = 𝟭⇩I"
by (rule E.multiplicative.invertible_left_inverse [OF inv x])
ultimately show "∃y ∈ ecarrier E. emult E x y = 𝟭⇩I ∧ emult E y x = 𝟭⇩I" by blast
qed
qed
text ‹The union of a nonempty chain is a field. Each axiom involves at most three elements, which
a common member accommodates; there the axiom holds, and the union's operations agree with that
member's.›
lemma ext_Union_field:
assumes ne: "C ≠ {}" and nz: "𝟭 ≠ 𝟬"
shows "Field (ecarrier (ext_Union C)) (eadd (ext_Union C)) (emult (ext_Union C)) 𝟬⇩I 𝟭⇩I"
proof -
obtain E0 where E0: "E0 ∈ C" using ne by blast
have zmem: "𝟬⇩I ∈ ecarrier (ext_Union C)"
using E0 chain_zero_one_mem(1) [OF E0] unfolding ext_Union_carrier by blast
have omem: "𝟭⇩I ∈ ecarrier (ext_Union C)"
using E0 chain_zero_one_mem(2) [OF E0] unfolding ext_Union_carrier by blast
have grp: "Group (ecarrier (ext_Union C)) (eadd (ext_Union C)) 𝟬⇩I"
proof (rule GroupI)
fix x y assume "x ∈ ecarrier (ext_Union C)" and "y ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E"
using chain_common2 by blast
then show "eadd (ext_Union C) x y ∈ ecarrier (ext_Union C)"
using ext_Union_ops(1) [OF E] chain_add_closed [OF E(1)] by auto
next
show "𝟬⇩I ∈ ecarrier (ext_Union C)" by (rule zmem)
next
fix x y z
assume "x ∈ ecarrier (ext_Union C)" "y ∈ ecarrier (ext_Union C)" "z ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E" "z ∈ ecarrier E"
using chain_common3 by blast
have "eadd E x y ∈ ecarrier E" and "eadd E y z ∈ ecarrier E"
using chain_add_closed [OF E(1)] E by auto
then show "eadd (ext_Union C) (eadd (ext_Union C) x y) z
= eadd (ext_Union C) x (eadd (ext_Union C) y z)"
using ext_Union_ops(1) [OF E(1)] E chain_add_assoc [OF E(1)] by simp
next
fix x assume "x ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" by auto
then show "eadd (ext_Union C) 𝟬⇩I x = x"
using ext_Union_ops(1) [OF E(1) chain_zero_one_mem(1) [OF E(1)] E(2)]
chain_add_zero [OF E(1) E(2)] by simp
next
fix x assume "x ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" by auto
then show "eadd (ext_Union C) x 𝟬⇩I = x"
using ext_Union_ops(1) [OF E(1) E(2) chain_zero_one_mem(1) [OF E(1)]]
chain_add_zero' [OF E(1) E(2)] by simp
next
fix x assume "x ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" by auto
from chain_add_inv [OF E(1) E(2)] obtain y
where y: "y ∈ ecarrier E" "eadd E x y = 𝟬⇩I" "eadd E y x = 𝟬⇩I" by blast
then show "∃v ∈ ecarrier (ext_Union C).
eadd (ext_Union C) x v = 𝟬⇩I ∧ eadd (ext_Union C) v x = 𝟬⇩I"
using ext_Union_ops(1) [OF E(1) E(2) y(1)] ext_Union_ops(1) [OF E(1) y(1) E(2)] E by auto
qed
interpret Uadd: Group "ecarrier (ext_Union C)" "eadd (ext_Union C)" "𝟬⇩I" by (rule grp)
interpret Uadd: Abelian_Group "ecarrier (ext_Union C)" "eadd (ext_Union C)" "𝟬⇩I"
proof unfold_locales
fix x y assume "x ∈ ecarrier (ext_Union C)" and "y ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E"
using chain_common2 by blast
then show "eadd (ext_Union C) x y = eadd (ext_Union C) y x"
using ext_Union_ops(1) [OF E(1) E(2) E(3)] ext_Union_ops(1) [OF E(1) E(3) E(2)]
chain_add_comm [OF E(1) E(2) E(3)] by simp
qed
interpret Umult: commutative_monoid "ecarrier (ext_Union C)" "emult (ext_Union C)" "𝟭⇩I"
proof unfold_locales
fix x y assume "x ∈ ecarrier (ext_Union C)" and "y ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E"
using chain_common2 by blast
then show "emult (ext_Union C) x y ∈ ecarrier (ext_Union C)"
using ext_Union_ops(2) [OF E] chain_mult_closed [OF E(1)] by auto
next
show "𝟭⇩I ∈ ecarrier (ext_Union C)" by (rule omem)
next
fix x y z
assume "x ∈ ecarrier (ext_Union C)" "y ∈ ecarrier (ext_Union C)" "z ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E" "z ∈ ecarrier E"
using chain_common3 by blast
have "emult E x y ∈ ecarrier E" and "emult E y z ∈ ecarrier E"
using chain_mult_closed [OF E(1)] E by auto
then show "emult (ext_Union C) (emult (ext_Union C) x y) z
= emult (ext_Union C) x (emult (ext_Union C) y z)"
using ext_Union_ops(2) [OF E(1)] E chain_mult_assoc [OF E(1)] by simp
next
fix x assume "x ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" by auto
then show "emult (ext_Union C) 𝟭⇩I x = x"
using ext_Union_ops(2) [OF E(1) chain_zero_one_mem(2) [OF E(1)] E(2)]
chain_mult_one [OF E(1) E(2)] by simp
next
fix x assume "x ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" by auto
then show "emult (ext_Union C) x 𝟭⇩I = x"
using ext_Union_ops(2) [OF E(1) E(2) chain_zero_one_mem(2) [OF E(1)]]
chain_mult_one' [OF E(1) E(2)] by simp
next
fix x y assume "x ∈ ecarrier (ext_Union C)" and "y ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E"
using chain_common2 by blast
then show "emult (ext_Union C) x y = emult (ext_Union C) y x"
using ext_Union_ops(2) [OF E(1) E(2) E(3)] ext_Union_ops(2) [OF E(1) E(3) E(2)]
chain_mult_comm [OF E(1) E(2) E(3)] by simp
qed
show ?thesis
proof unfold_locales
fix x y z
assume "x ∈ ecarrier (ext_Union C)" "y ∈ ecarrier (ext_Union C)" "z ∈ ecarrier (ext_Union C)"
then obtain E where E: "E ∈ C" "x ∈ ecarrier E" "y ∈ ecarrier E" "z ∈ ecarrier E"
using chain_common3 by blast
have cl: "eadd E y z ∈ ecarrier E" "emult E x y ∈ ecarrier E" "emult E x z ∈ ecarrier E"
"emult E y x ∈ ecarrier E" "emult E z x ∈ ecarrier E"
using chain_add_closed [OF E(1)] chain_mult_closed [OF E(1)] E by auto
show "emult (ext_Union C) x (eadd (ext_Union C) y z)
= eadd (ext_Union C) (emult (ext_Union C) x y) (emult (ext_Union C) x z)"
using cl E ext_Union_ops(1) [OF E(1)] ext_Union_ops(2) [OF E(1)]
chain_distrib [OF E(1)] by simp
show "emult (ext_Union C) (eadd (ext_Union C) y z) x
= eadd (ext_Union C) (emult (ext_Union C) y x) (emult (ext_Union C) z x)"
using cl E ext_Union_ops(1) [OF E(1)] ext_Union_ops(2) [OF E(1)]
chain_distrib' [OF E(1)] by simp
next
show "𝟭⇩I ≠ 𝟬⇩I"
using nz by (auto simp: ipoly_one_def ipoly_zero_def fun_eq_iff)
next
fix x assume x: "x ∈ ecarrier (ext_Union C)" and xnz: "x ≠ 𝟬⇩I"
from x obtain E where E: "E ∈ C" "x ∈ ecarrier E" by auto
from chain_mult_inv [OF E(1) E(2) xnz] obtain y
where y: "y ∈ ecarrier E" "emult E x y = 𝟭⇩I" "emult E y x = 𝟭⇩I" by blast
have "emult (ext_Union C) x y = 𝟭⇩I" and "emult (ext_Union C) y x = 𝟭⇩I"
using ext_Union_ops(2) [OF E(1) E(2) y(1)] ext_Union_ops(2) [OF E(1) y(1) E(2)] y by simp_all
moreover have "y ∈ ecarrier (ext_Union C)" using E(1) y(1) by auto
ultimately show "Umult.invertible x"
by (blast intro: Umult.invertibleI)
qed
qed
subsection ‹Evaluation is the same in a member and in the union›
text ‹The remaining extension condition, @{const root_closed}, asserts that an indeterminate is a
∗‹root›, which is an equation about evaluation. Evaluation does not transfer between a member and
the union for free: @{const commutative_monoid.fincomp} depends on the carrier as well as the
operation (through @{const commutative_monoid.M_ify}), so @{thm [source] fincomp_transfer} is what
makes the two agree, given that every value involved stays inside the member.›
lemma chain_Ring:
assumes E: "E ∈ C" shows "Ring (ecarrier E) (eadd E) (emult E) 𝟬⇩I 𝟭⇩I"
using chain_field [OF E] by (simp add: Field_def commutative_ring_def)
lemma ext_Union_Ring:
assumes ne: "C ≠ {}" and nz: "𝟭 ≠ 𝟬"
shows "Ring (ecarrier (ext_Union C)) (eadd (ext_Union C)) (emult (ext_Union C)) 𝟬⇩I 𝟭⇩I"
using ext_Union_field [OF ne nz] by (simp add: Field_def commutative_ring_def)
text ‹The chain case is now just the ordering case at @{thm [source] ext_Union_upper_bound}.›
lemma rpow_transfer:
assumes ne: "C ≠ {}" and nz: "𝟭 ≠ 𝟬" and E: "E ∈ C" and a: "a ∈ ecarrier E"
shows "Ring.rpow (emult (ext_Union C)) 𝟭⇩I a n = Ring.rpow (emult E) 𝟭⇩I a n"
by (rule ext_le_rpow [OF chain_Ring [OF E] ext_Union_Ring [OF ne nz]
ext_Union_upper_bound [OF E] a])
lemma ext_Union_eval:
assumes ne: "C ≠ {}" and nz: "𝟭 ≠ 𝟬" and E: "E ∈ C"
and a: "a ∈ ecarrier E" and p: "⋀k. p k ∈ ecarrier E"
shows "eeval (ext_Union C) a p = eeval E a p"
by (rule ext_le_eval [OF chain_Ring [OF E] ext_Union_Ring [OF ne nz]
ext_Union_upper_bound [OF E] a p])
subsection ‹The union of a nonempty chain is an extension›
lemma ext_Union_is_extension:
assumes ne: "C ≠ {}" and nz: "𝟭 ≠ 𝟬"
shows "is_extension (ext_Union C)"
proof (rule is_extensionI)
obtain E0 where E0: "E0 ∈ C" using ne by blast
have ext0: "is_extension E0" using chain E0 by (rule ext_chainD_extension)
show "Field (ecarrier (ext_Union C)) (eadd (ext_Union C)) (emult (ext_Union C)) 𝟬⇩I 𝟭⇩I"
by (rule ext_Union_field [OF ne nz])
show "ecarrier (ext_Union C) ⊆ ipoly_carrier"
using chain ext_chainD_extension is_extension_subset by (fastforce simp: ext_Union_def)
show "⋀a. a ∈ R ⟹ ipoly_const a ∈ ecarrier (ext_Union C)"
using E0 is_extension_const_mem [OF ext0] by auto
show "⋀a b. ⟦ a ∈ R; b ∈ R ⟧
⟹ eadd (ext_Union C) (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
proof -
fix a b assume ab: "a ∈ R" "b ∈ R"
have mem: "ipoly_const a ∈ ecarrier E0" "ipoly_const b ∈ ecarrier E0"
using ab is_extension_const_mem [OF ext0] by simp_all
show "eadd (ext_Union C) (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
using ext_Union_ops(1) [OF E0 mem(1) mem(2)]
is_extension_const_add [OF ext0 ab(1) ab(2)] by simp
qed
show "⋀a b. ⟦ a ∈ R; b ∈ R ⟧
⟹ emult (ext_Union C) (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)"
proof -
fix a b assume ab: "a ∈ R" "b ∈ R"
have mem: "ipoly_const a ∈ ecarrier E0" "ipoly_const b ∈ ecarrier E0"
using ab is_extension_const_mem [OF ext0] by simp_all
show "emult (ext_Union C) (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)"
using ext_Union_ops(2) [OF E0 mem(1) mem(2)]
is_extension_const_mult [OF ext0 ab(1) ab(2)] by simp
qed
show "root_closed (ext_Union C)"
proof (rule root_closedI)
fix 𝒫 P i
assume Pm: "𝒫 ∈ ecarrier (ext_Union C)" and Pc: "P ∈ poly_carrier"
and nif: "¬ index_free 𝒫 (P, i)"
from Pm obtain E where E: "E ∈ C" "𝒫 ∈ ecarrier E" by auto
have extE: "is_extension E" using chain E(1) by (rule ext_chainD_extension)
have rc: "root_closed E" by (rule is_extension_root_closed [OF extE])
have mem: "ivar (P, i) ∈ ecarrier E" by (rule root_closed_mem [OF rc E(2) Pc nif])
have ev: "eeval E (ivar (P, i)) (lift_poly P) = 𝟬⇩I"
by (rule root_closed_eval [OF rc E(2) Pc nif])
have coeff: "lift_poly P k ∈ ecarrier E" for k
using Pc extE by (simp add: is_extension_const_mem poly_carrier_coeff_closed)
have "eeval (ext_Union C) (ivar (P, i)) (lift_poly P) = eeval E (ivar (P, i)) (lift_poly P)"
by (rule ext_Union_eval [OF ne nz E(1) mem coeff])
then show "ivar (P, i) ∈ ecarrier (ext_Union C)
∧ eeval (ext_Union C) (ivar (P, i)) (lift_poly P) = 𝟬⇩I"
using mem E(1) ev by auto
qed
show "op_restricted (ecarrier (ext_Union C)) (eadd (ext_Union C))"
by (rule ext_Union_restricted(1))
show "op_restricted (ecarrier (ext_Union C)) (emult (ext_Union C))"
by (rule ext_Union_restricted(2))
qed
end
end
section ‹Transporting a Field Structure along an Injection›
context Field
begin
text ‹A field structure transports along a map injective on the carrier, given operations on the
image that make the map a homomorphism there. Only the behaviour ∗‹on the image› is constrained,
which is what makes the restricted operations of an extension free of charge: no separate lemma is
needed to see that restricting a field's operations to its own carrier leaves a field. The same
lemma will serve when a root is adjoined, since that too realises a field as the image of an
injection.›
lemma field_image_transport:
fixes h :: "'a ⇒ 'b" and hadd hmult :: "'b ⇒ 'b ⇒ 'b"
assumes inj: "inj_on h R"
and ha: "⋀a b. ⟦ a ∈ R; b ∈ R ⟧ ⟹ hadd (h a) (h b) = h (a + b)"
and hm: "⋀a b. ⟦ a ∈ R; b ∈ R ⟧ ⟹ hmult (h a) (h b) = h (a ⋅ b)"
shows "Field (h ` R) hadd hmult (h 𝟬) (h 𝟭)"
proof -
have grp: "Group (h ` R) hadd (h 𝟬)"
proof (rule GroupI)
show "⋀x y. ⟦ x ∈ h ` R; y ∈ h ` R ⟧ ⟹ hadd x y ∈ h ` R"
using ha by force
show "h 𝟬 ∈ h ` R" by simp
show "⋀x y z. ⟦ x ∈ h ` R; y ∈ h ` R; z ∈ h ` R ⟧
⟹ hadd (hadd x y) z = hadd x (hadd y z)"
using ha by (clarsimp simp: additive.associative)
show "⋀x. x ∈ h ` R ⟹ hadd (h 𝟬) x = x" using ha by force
show "⋀x. x ∈ h ` R ⟹ hadd x (h 𝟬) = x" using ha by force
show "⋀x. x ∈ h ` R ⟹ ∃y ∈ h ` R. hadd x y = h 𝟬 ∧ hadd y x = h 𝟬"
proof -
fix x assume "x ∈ h ` R"
then obtain a where a: "a ∈ R" and xa: "x = h a" by blast
then have na: "- a ∈ R" by (simp add: additive.invertible_inverse_closed)
have "hadd (h a) (h (- a)) = h 𝟬"
using ha [OF a na] a by (simp add: additive.invertible_right_inverse)
moreover have "hadd (h (- a)) (h a) = h 𝟬"
using ha [OF na a] a by (simp add: additive.invertible_left_inverse)
ultimately show "∃y ∈ h ` R. hadd x y = h 𝟬 ∧ hadd y x = h 𝟬"
using na xa by blast
qed
qed
interpret hadd: Group "h ` R" hadd "h 𝟬" by (rule grp)
interpret hadd: Abelian_Group "h ` R" hadd "h 𝟬"
proof unfold_locales
fix x y assume "x ∈ h ` R" and "y ∈ h ` R"
then show "hadd x y = hadd y x"
using ha by (clarsimp simp: additive.commutative)
qed
interpret hmult: commutative_monoid "h ` R" hmult "h 𝟭"
proof unfold_locales
show "⋀x y. ⟦ x ∈ h ` R; y ∈ h ` R ⟧ ⟹ hmult x y ∈ h ` R"
using hm by force
show "h 𝟭 ∈ h ` R" by simp
show "⋀x y z. ⟦ x ∈ h ` R; y ∈ h ` R; z ∈ h ` R ⟧
⟹ hmult (hmult x y) z = hmult x (hmult y z)"
using hm by (clarsimp simp: multiplicative.associative)
show "⋀x. x ∈ h ` R ⟹ hmult (h 𝟭) x = x" using hm by force
show "⋀x. x ∈ h ` R ⟹ hmult x (h 𝟭) = x" using hm by force
show "⋀x y. ⟦ x ∈ h ` R; y ∈ h ` R ⟧ ⟹ hmult x y = hmult y x"
using hm by (clarsimp simp: multiplicative.commutative)
qed
have distrib: "⋀x y z. ⟦ x ∈ h ` R; y ∈ h ` R; z ∈ h ` R ⟧
⟹ hmult x (hadd y z) = hadd (hmult x y) (hmult x z)"
using ha hm by (clarsimp simp: distributive)
have distrib': "⋀x y z. ⟦ x ∈ h ` R; y ∈ h ` R; z ∈ h ` R ⟧
⟹ hmult (hadd y z) x = hadd (hmult y x) (hmult z x)"
using ha hm by (clarsimp simp: distributive)
have nz: "h 𝟭 ≠ h 𝟬"
using inj nontrivial by (simp add: inj_on_eq_iff)
show ?thesis
proof unfold_locales
show "⋀x y z. ⟦ x ∈ h ` R; y ∈ h ` R; z ∈ h ` R ⟧
⟹ hmult x (hadd y z) = hadd (hmult x y) (hmult x z)"
by (rule distrib)
show "⋀x y z. ⟦ x ∈ h ` R; y ∈ h ` R; z ∈ h ` R ⟧
⟹ hmult (hadd y z) x = hadd (hmult y x) (hmult z x)"
by (rule distrib')
show "h 𝟭 ≠ h 𝟬" by (rule nz)
show "⋀x. ⟦ x ∈ h ` R; x ≠ h 𝟬 ⟧ ⟹ hmult.invertible x"
proof -
fix x assume x: "x ∈ h ` R" and xnz: "x ≠ h 𝟬"
then obtain a where a: "a ∈ R" and xa: "x = h a" by blast
with xnz have anz: "a ≠ 𝟬" by blast
have inv: "multiplicative.invertible a" by (rule field_inverse [OF a anz])
have ia: "multiplicative.inverse a ∈ R"
by (rule multiplicative.invertible_inverse_closed [OF inv a])
have "hmult (h a) (h (multiplicative.inverse a)) = h 𝟭"
using hm [OF a ia] multiplicative.invertible_right_inverse [OF inv a] by simp
moreover have "hmult (h (multiplicative.inverse a)) (h a) = h 𝟭"
using hm [OF ia a] multiplicative.invertible_left_inverse [OF inv a] by simp
moreover have "h (multiplicative.inverse a) ∈ h ` R" using ia by simp
ultimately show "hmult.invertible x"
using xa by (blast intro: hmult.invertibleI)
qed
qed
qed
subsection ‹The base extension is an extension›
theorem is_extension_base_ext: "is_extension base_ext"
proof (rule is_extensionI)
have "Field (ipoly_const ` R) (eadd base_ext) (emult base_ext) (ipoly_const 𝟬) (ipoly_const 𝟭)"
by (rule field_image_transport [OF ipoly_const_inj_on base_ext_add base_ext_mult])
then show "Field (ecarrier base_ext) (eadd base_ext) (emult base_ext) 𝟬⇩I 𝟭⇩I" by simp
show "ecarrier base_ext ⊆ ipoly_carrier"
using ipoly_const_closed by auto
show "⋀a. a ∈ R ⟹ ipoly_const a ∈ ecarrier base_ext" by simp
show "⋀a b. ⟦ a ∈ R; b ∈ R ⟧
⟹ eadd base_ext (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)"
by (rule base_ext_add)
show "⋀a b. ⟦ a ∈ R; b ∈ R ⟧
⟹ emult base_ext (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)"
by (rule base_ext_mult)
show "root_closed base_ext"
by (rule root_closedI) auto
show "op_restricted (ecarrier base_ext) (eadd base_ext)" by (rule base_ext_restricted(1))
show "op_restricted (ecarrier base_ext) (emult base_ext)" by (rule base_ext_restricted(2))
qed
corollary extensions_non_empty: "extensions ≠ {}"
using is_extension_base_ext by auto
subsection ‹A maximal extension exists›
text ‹Zorn's lemma applies: the extensions form a set, partially ordered by @{const ext_le}, in which
every chain has an upper bound --- the union of a nonempty chain, and @{const base_ext} for the
empty one. Maximality is what will force every polynomial over @{term R} to split, since an
unsplit polynomial leaves an index free at which a root could be adjoined.›
theorem exists_maximal_extension:
"∃M ∈ extensions. ∀L ∈ extensions. ext_le M L ⟶ L = M"
proof (rule predicate_Zorn [OF ext_partial_order])
fix D assume D: "D ∈ Chains (relation_of ext_le extensions)"
then have sub: "D ⊆ extensions" by (rule Chains_relation_of)
have ch: "ext_chain D"
using D sub unfolding ext_chain_def Chains_def relation_of_def by auto
show "∃u ∈ extensions. ∀a ∈ D. ext_le a u"
proof (cases "D = {}")
case True
have "base_ext ∈ extensions" by (simp add: is_extension_base_ext)
with True show ?thesis by blast
next
case False
have "is_extension (ext_Union D)"
by (rule ext_Union_is_extension [OF ch False nontrivial])
moreover have "∀a ∈ D. ext_le a (ext_Union D)"
using ext_Union_upper_bound [OF ch] by blast
ultimately show ?thesis by auto
qed
qed
subsection ‹A fresh index always exists›
text ‹Towards @{text exists_root}: for any nonzero polynomial @{term P} over @{term R} there is an
index @{term i} that no element of a given extension involves. This is the step that makes room
for a new root, and it is where the choice of indexed polynomials as the ambient type pays off ---
no cardinality argument is needed, only the observation that an extension ∗‹mentioning› every index
would contain a root of @{term P} for each of them, and a nonzero polynomial over a field has only
finitely many roots.›
lemma exists_fresh_index:
assumes M: "is_extension M" and P: "P ∈ poly_carrier" and Pnz: "P ≠ 𝟬⇩P"
shows "∃i. ∀𝒫 ∈ ecarrier M. index_free 𝒫 (P, i)"
proof (rule ccontr)
assume "¬ (∃i. ∀𝒫 ∈ ecarrier M. index_free 𝒫 (P, i))"
then have bad: "∃𝒫 ∈ ecarrier M. ¬ index_free 𝒫 (P, i)" for i by blast
interpret M: Field "ecarrier M" "eadd M" "emult M" "𝟬⇩I" "𝟭⇩I"
by (rule is_extension_field [OF M])
have rc: "root_closed M" by (rule is_extension_root_closed [OF M])
have root: "ivar (P, i) ∈ ecarrier M ∧ M.eval (ivar (P, i)) (lift_poly P) = 𝟬⇩I" for i
proof -
obtain 𝒫 where "𝒫 ∈ ecarrier M" and "¬ index_free 𝒫 (P, i)" using bad by blast
then show ?thesis
using root_closed_mem [OF rc _ P] root_closed_eval [OF rc _ P] by blast
qed
have lc: "lift_poly P ∈ M.poly_carrier"
proof (rule M.poly_carrierI)
have "{k. lift_poly P k ≠ 𝟬⇩I} ⊆ {k. P k ≠ 𝟬}"
by (auto simp: lift_poly_def ipoly_const_def ipoly_zero_def)
then show "finite {k. lift_poly P k ≠ 𝟬⇩I}"
using poly_carrier_finite [OF P] by (rule finite_subset)
show "⋀k. lift_poly P k ∈ ecarrier M"
using P M by (simp add: is_extension_const_mem poly_carrier_coeff_closed)
qed
have lnz: "lift_poly P ≠ M.poly_zero"
proof -
obtain k where k: "P k ≠ 𝟬" using Pnz by (auto simp: poly_zero_def fun_eq_iff)
then have "ipoly_const (P k) ≠ 𝟬⇩I"
by (metis ipoly_const_coeff ipoly_zero_def)
then show ?thesis by (auto simp: lift_poly_def M.poly_zero_def fun_eq_iff)
qed
have fin: "finite {a ∈ ecarrier M. M.eval a (lift_poly P) = 𝟬⇩I}"
using M.card_roots_le_degree [OF lc lnz] by blast
have inj: "inj (λi. ivar (P, i) :: 'a ipoly)"
using ivar_inj [OF nontrivial] by (auto simp: inj_on_def)
have "range (λi. ivar (P, i) :: 'a ipoly)
⊆ {a ∈ ecarrier M. M.eval a (lift_poly P) = 𝟬⇩I}"
using root by blast
with fin inj show False
by (meson finite_subset finite_imageD infinite_UNIV_nat)
qed
end
subsection ‹Transporting a field onto its image, with restricted operations›
text ‹An injective image of a field carries a field structure, and the operations obtained by
∗‹transport› --- undo the injection, operate, redo it --- are automatically the restricted ones an
extension requires. Nothing is assumed about how @{term h} interacts with the ambient operations,
which is the point: an extension's addition need not be the ambient addition, and
@{const Ring.is_extension} does not require it to be. Choosing the operations by transport sidesteps
the question instead of forcing a stronger definition.›
lemma field_transport_restricted:
fixes A :: "'b set" and add mult :: "'b ⇒ 'b ⇒ 'b" and z u :: 'b
and h :: "'b ⇒ 'a ipoly"
assumes F: "Field A add mult z u" and inj: "inj_on h A"
defines "K ≡ h ` A"
and "hadd ≡ (λx y. if x ∈ h ` A ∧ y ∈ h ` A
then h (add (inv_into A h x) (inv_into A h y)) else undefined)"
and "hmult ≡ (λx y. if x ∈ h ` A ∧ y ∈ h ` A
then h (mult (inv_into A h x) (inv_into A h y)) else undefined)"
shows field_transport_field: "Field K hadd hmult (h z) (h u)"
and field_transport_add_restricted: "op_restricted K hadd"
and field_transport_mult_restricted: "op_restricted K hmult"
proof -
have undo: "inv_into A h (h a) = a" if "a ∈ A" for a
using inj that by (rule inv_into_f_f)
have ha: "hadd (h a) (h b) = h (add a b)" if "a ∈ A" "b ∈ A" for a b
unfolding hadd_def using that undo by simp
have hm: "hmult (h a) (h b) = h (mult a b)" if "a ∈ A" "b ∈ A" for a b
unfolding hmult_def using that undo by simp
show "Field K hadd hmult (h z) (h u)"
unfolding K_def by (rule Field.field_image_transport [OF F inj ha hm])
show "op_restricted K hadd"
by (rule op_restrictedI) (auto simp: hadd_def K_def)
show "op_restricted K hmult"
by (rule op_restrictedI) (auto simp: hmult_def K_def)
qed
section ‹Working Inside a Fixed Extension›
text ‹Adjoining a root needs the polynomial machinery of the extension's own coefficient field ---
‹pmod›, ‹poly_carrier›, ‹degree› at @{term "ecarrier M"}. Fixing @{term M} in a locale and
discharging @{locale Field} for it once, by @{thm [source] Ring.is_extension_field}, makes all of it
available under the @{text M} prefix throughout, ∗‹including inside definitions›.
@{command interpret} would not serve, being a proof-body command, but @{command sublocale} is its
declaration-level counterpart, so no definition here has to spell out the five locale parameters.›
locale field_extension = Field +
fixes M :: "'a iext"
assumes is_ext: "is_extension M"
sublocale field_extension ⊆ M: Field "ecarrier M" "eadd M" "emult M" "𝟬⇩I" "𝟭⇩I"
by (rule is_extension_field [OF is_ext])
context field_extension
begin
text ‹The realisation map: reduce a polynomial over @{term M} modulo @{term Q}, then read the
remainder off at the fresh indeterminate, using the ∗‹ambient› operations. Both prefixes now read
naturally.›
definition realise :: "'a root_index ⇒ (nat ⇒ 'a ipoly) ⇒ (nat ⇒ 'a ipoly) ⇒ 'a ipoly"
where "realise j Q S = ieval (ivar j) (M.pmod S Q)"
text ‹A polynomial over @{term M} is also one over the ambient ring, its carrier being contained
there. Note that the two rings share their zero, so they also share @{term Ring.degree} and
@{term Ring.poly_zero}: no translation of degrees is needed anywhere below.›
lemma coeff_ipoly_closed: "S ∈ M.poly_carrier ⟹ S k ∈ ipoly_carrier"
using is_extension_subset [OF is_ext] M.poly_carrier_coeff_closed by blast
lemma low_poly_ambient:
assumes S: "S ∈ M.low_poly d" shows "S ∈ Ring.poly_carrier ipoly_carrier 𝟬⇩I"
proof (rule Ring.poly_carrierI [OF ipoly_ring])
have Sc: "S ∈ M.poly_carrier" using S by (rule M.low_poly_closed)
show "finite {i. S i ≠ 𝟬⇩I}" using Sc by (rule M.poly_carrier_finite)
show "⋀i. S i ∈ ipoly_carrier" using Sc by (rule coeff_ipoly_closed)
qed
text ‹On the remainders the realisation is a sum over the ∗‹fixed› range @{term "{..d}"} rather than
over each polynomial's own degree. A common range is what @{thm [source] ieval_ivar_inj} needs, and
enlarging the range past the degree is harmless.›
lemma ieval_low_fincomp:
assumes S: "S ∈ M.low_poly d"
shows "ieval (ivar j) S
= commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. S k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..d}"
proof (rule Ring.eval_fincomp_le [OF ipoly_ring low_poly_ambient [OF S] ivar_closed])
have "S = M.poly_zero ∨ Ring.degree 𝟬⇩I S < d"
using S M.low_poly_iff_degree [OF M.low_poly_closed [OF S]] by blast
then show "Ring.degree 𝟬⇩I S ≤ d"
using M.degree_zero by fastforce
qed
text ‹∗‹The realisation is injective on the remainders.› This is the point of a ∗‹fresh› index: every
coefficient lies in @{term M} and so is index-free at @{term j}, which is exactly the hypothesis
under which @{thm [source] ieval_ivar_inj} reads the coefficients back off. Above the range the two
remainders agree trivially, both coefficients being zero.›
lemma ieval_inj_on_low:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
shows "inj_on (ieval (ivar j)) (M.low_poly d)"
proof (rule inj_onI)
fix S T
assume S: "S ∈ M.low_poly d" and T: "T ∈ M.low_poly d"
and eq: "ieval (ivar j) S = ieval (ivar j) T"
have Sc: "S ∈ M.poly_carrier" and Tc: "T ∈ M.poly_carrier"
using S T by (blast intro: M.low_poly_closed)+
have Sip: "S k ∈ ipoly_carrier" and Tip: "T k ∈ ipoly_carrier" for k
using Sc Tc by (blast intro: coeff_ipoly_closed)+
have Sf: "index_free (S k) j" and Tf: "index_free (T k) j" for k
using fresh Sc Tc by (blast intro: M.poly_carrier_coeff_closed)+
have sums: "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. S k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..d}
= commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. T k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..d}"
using ieval_low_fincomp [OF S] ieval_low_fincomp [OF T] eq by simp
show "S = T"
proof (rule ext)
fix k
show "S k = T k"
proof (cases "k ≤ d")
case True
show ?thesis by (rule ieval_ivar_inj [OF Sip Sf Tip Tf sums True])
next
case False
then have "S k = 𝟬⇩I" and "T k = 𝟬⇩I"
using S T unfolding M.low_poly_def by auto
then show ?thesis by simp
qed
qed
qed
text ‹∗‹The extension obtained by adjoining a root.› The carrier is the image of the remainders
modulo @{term Q} under evaluation at the fresh indeterminate; the operations are the transported
ones. Reduction modulo @{term Q} has to live in the multiplication, since the realisation of
@{term Q} itself is not zero in the ambient ring --- which is exactly why an extension carries its
own operations rather than inheriting the ambient ones.›
definition adjoin_carrier :: "'a root_index ⇒ (nat ⇒ 'a ipoly) ⇒ 'a ipoly set"
where "adjoin_carrier j Q = ieval (ivar j) ` M.low_poly (M.degree Q)"
definition adjoin :: "'a root_index ⇒ (nat ⇒ 'a ipoly) ⇒ 'a iext"
where "adjoin j Q =
(adjoin_carrier j Q,
(λx y. if x ∈ adjoin_carrier j Q ∧ y ∈ adjoin_carrier j Q
then ieval (ivar j)
(M.poly_add (inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) x)
(inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y))
else undefined),
(λx y. if x ∈ adjoin_carrier j Q ∧ y ∈ adjoin_carrier j Q
then ieval (ivar j)
(M.pmod (M.poly_mult
(inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) x)
(inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y)) Q)
else undefined))"
lemma adjoin_carrier_eq [simp]: "ecarrier (adjoin j Q) = adjoin_carrier j Q"
by (simp add: adjoin_def)
text ‹The field structure and the restrictedness of both operations come together, by transporting
@{thm [source] Field.remainder_field} along the realisation, which
@{thm [source] ieval_inj_on_low} shows to be injective on the remainders. The zero and the unit
land on @{term "𝟬⇩I"} and @{term "𝟭⇩I"} because evaluation sends the zero and unit polynomials
there.›
text ‹The realisation sends the zero, the unit and the variable of the polynomial ring over
@{term M} to
@{term "𝟬⇩I"}, @{term "𝟭⇩I"} and the fresh indeterminate. The first two are what make the
transported field structure have the zero and unit that @{const is_extension} demands; the third is
what exhibits @{term "ivar j"} as an element of the adjoined carrier.›
lemma ieval_poly_zero: "ieval (ivar j) M.poly_zero = 𝟬⇩I"
by (rule Ring.eval_zero [OF ipoly_ring ivar_closed])
lemma ieval_poly_one: "ieval (ivar j) M.poly_one = 𝟭⇩I"
by (rule Ring.eval_one [OF ipoly_ring ivar_closed])
lemma ieval_poly_var: "ieval (ivar j) M.var = ivar j"
by (rule Ring.eval_var [OF ipoly_ring ivar_closed])
text ‹Nontriviality of the ambient indexed ring, taken from @{term R} rather than from @{term M}:
a statement about @{term "𝟭⇩I"} and @{term "𝟬⇩I"} alone is generalised over the index type and so
cannot be derived from a hypothesis where that type is pinned.›
lemma ipoly_one_neq_zero: "(𝟭⇩I :: 'a root_index multiset ⇒ 'a) ≠ 𝟬⇩I"
proof -
have one: "𝟭 ∈ R" and zero: "𝟬 ∈ R" by simp_all
have "(ipoly_const 𝟭 :: 'a root_index multiset ⇒ 'a) ≠ ipoly_const 𝟬"
using inj_on_eq_iff [OF ipoly_const_inj_on one zero] nontrivial by simp
then show ?thesis by simp
qed
lemma var_low:
assumes d2: "2 ≤ M.degree Q" shows "M.var ∈ M.low_poly (M.degree Q)"
proof -
have "M.degree M.var = 1" by (rule M.degree_var [OF ipoly_one_neq_zero])
with d2 show ?thesis using M.var_closed by (simp add: M.low_poly_iff_degree)
qed
text ‹The constants of @{term M} sit inside the adjoined carrier, realised by the constant
polynomials, and the transported operations restrict to @{term M}'s own there. So @{term M} lies
below the adjoined extension in the ordering --- which is what carries @{term M}'s root witnesses
upwards, by @{thm [source] Ring.ext_le_eval}.›
lemma M_Ring: "Ring (ecarrier M) (eadd M) (emult M) 𝟬⇩I 𝟭⇩I"
using is_extension_field [OF is_ext] by (simp add: Field_def commutative_ring_def)
lemma adjoin_rep:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and S: "S ∈ M.low_poly (M.degree Q)"
shows "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) (ieval (ivar j) S) = S"
using ieval_inj_on_low [OF fresh] S by (rule inv_into_f_f)
lemma ieval_poly_const:
assumes y: "y ∈ ipoly_carrier" shows "ieval (ivar j) (M.poly_const y) = y"
by (rule Ring.eval_const [OF ipoly_ring ivar_closed y])
lemma const_low:
assumes irr: "M.poly_irreducible Q" and y: "y ∈ ecarrier M"
shows "M.poly_const y ∈ M.low_poly (M.degree Q)"
proof -
have dpos: "0 < M.degree Q" using irr by (rule M.poly_irreducible_degree_pos)
have c: "M.poly_const y ∈ M.poly_carrier" using y by (rule M.poly_const_closed)
have "M.degree (M.poly_const y) = 0" using M.degree_const_le by (simp add: le_zero_eq)
with dpos show ?thesis using c by (simp add: M.low_poly_iff_degree)
qed
lemma const_rep:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q" and y: "y ∈ ecarrier M"
shows "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y = M.poly_const y"
proof -
have yip: "y ∈ ipoly_carrier" using is_ext y by (rule is_extension_carrier_closed)
have "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) (ieval (ivar j) (M.poly_const y))
= M.poly_const y"
by (rule adjoin_rep [OF fresh const_low [OF irr y]])
then show ?thesis using ieval_poly_const [OF yip] by simp
qed
lemma ecarrier_subset_adjoin:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
shows "ecarrier M ⊆ adjoin_carrier j Q"
proof
fix y assume y: "y ∈ ecarrier M"
have yip: "y ∈ ipoly_carrier" using is_ext y by (rule is_extension_carrier_closed)
have "y = ieval (ivar j) (M.poly_const y)" using ieval_poly_const [OF yip] by simp
then show "y ∈ adjoin_carrier j Q"
unfolding adjoin_carrier_def using const_low [OF irr y] by blast
qed
lemma ext_le_adjoin:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
shows "ext_le M (adjoin j Q)"
proof (rule ext_leI)
show "ecarrier M ⊆ ecarrier (adjoin j Q)"
using ecarrier_subset_adjoin [OF fresh irr] by simp
next
fix y y' assume y: "y ∈ ecarrier M" and y': "y' ∈ ecarrier M"
have K: "y ∈ adjoin_carrier j Q" "y' ∈ adjoin_carrier j Q"
using ecarrier_subset_adjoin [OF fresh irr] y y' by blast+
have ry: "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y = M.poly_const y"
and ry': "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y' = M.poly_const y'"
using const_rep [OF fresh irr y] const_rep [OF fresh irr y'] by blast+
have sum: "eadd M y y' ∈ ecarrier M" using M.additive.composition_closed y y' by simp
have "eadd (adjoin j Q) y y'
= ieval (ivar j) (M.poly_add (M.poly_const y) (M.poly_const y'))"
unfolding adjoin_def using K ry ry' by simp
also have "M.poly_add (M.poly_const y) (M.poly_const y') = M.poly_const (eadd M y y')"
by (rule M.poly_const_add [OF y y'])
also have "ieval (ivar j) (M.poly_const (eadd M y y')) = eadd M y y'"
using is_extension_carrier_closed [OF is_ext sum] by (rule ieval_poly_const)
finally show "eadd M y y' = eadd (adjoin j Q) y y'" by simp
next
fix y y' assume y: "y ∈ ecarrier M" and y': "y' ∈ ecarrier M"
have K: "y ∈ adjoin_carrier j Q" "y' ∈ adjoin_carrier j Q"
using ecarrier_subset_adjoin [OF fresh irr] y y' by blast+
have ry: "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y = M.poly_const y"
and ry': "inv_into (M.low_poly (M.degree Q)) (ieval (ivar j)) y' = M.poly_const y'"
using const_rep [OF fresh irr y] const_rep [OF fresh irr y'] by blast+
have prod: "emult M y y' ∈ ecarrier M" using M.multiplicative.composition_closed y y' by simp
have Qc: "Q ∈ M.poly_carrier" using irr by (rule M.poly_irreducibleD_carrier)
have Qnz: "Q ≠ M.poly_zero" using irr by (rule M.poly_irreducibleD_nonzero)
have "emult (adjoin j Q) y y'
= ieval (ivar j)
(M.pmod (M.poly_mult (M.poly_const y) (M.poly_const y')) Q)"
unfolding adjoin_def using K ry ry' by simp
also have "M.poly_mult (M.poly_const y) (M.poly_const y') = M.poly_const (emult M y y')"
by (rule M.poly_const_mult [OF y y'])
also have "M.pmod (M.poly_const (emult M y y')) Q = M.poly_const (emult M y y')"
proof (rule M.pmod_small [OF Qc Qnz M.poly_const_closed [OF prod]])
have "M.degree (M.poly_const (emult M y y')) = 0"
using M.degree_const_le by (simp add: le_zero_eq)
then show "M.poly_const (emult M y y') = M.poly_zero
∨ M.degree (M.poly_const (emult M y y')) < M.degree Q"
using M.poly_irreducible_degree_pos [OF irr] by simp
qed
also have "ieval (ivar j) (M.poly_const (emult M y y')) = emult M y y'"
using is_extension_carrier_closed [OF is_ext prod] by (rule ieval_poly_const)
finally show "emult M y y' = emult (adjoin j Q) y y'" by simp
qed
lemma adjoin_field:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
shows "Field (ecarrier (adjoin j Q)) (eadd (adjoin j Q)) (emult (adjoin j Q))
(ieval (ivar j) M.poly_zero) (ieval (ivar j) M.poly_one)"
and "op_restricted (ecarrier (adjoin j Q)) (eadd (adjoin j Q))"
and "op_restricted (ecarrier (adjoin j Q)) (emult (adjoin j Q))"
using field_transport_restricted
[OF M.remainder_field [OF irr] ieval_inj_on_low [OF fresh]]
by (simp_all add: adjoin_def adjoin_carrier_def)
text ‹The adjoined field, with the zero and unit @{const is_extension} demands.›
lemma adjoin_field_zero_one:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
shows "Field (ecarrier (adjoin j Q)) (eadd (adjoin j Q)) (emult (adjoin j Q))
𝟬⇩I 𝟭⇩I"
using adjoin_field (1) [OF fresh irr] ieval_poly_zero ieval_poly_one by simp
lemma adjoin_Ring:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
shows "Ring (ecarrier (adjoin j Q)) (eadd (adjoin j Q)) (emult (adjoin j Q))
𝟬⇩I 𝟭⇩I"
using adjoin_field_zero_one [OF fresh irr] by (simp add: Field_def commutative_ring_def)
lemma lift_poly_M_carrier:
assumes P: "P ∈ poly_carrier" shows "lift_poly P ∈ M.poly_carrier"
proof (rule M.poly_carrierI)
have "{k. lift_poly P k ≠ 𝟬⇩I} ⊆ {k. P k ≠ 𝟬}"
by (auto simp: lift_poly_def ipoly_const_def ipoly_zero_def)
then show "finite {k. lift_poly P k ≠ 𝟬⇩I}"
using poly_carrier_finite [OF P] by (rule finite_subset)
show "⋀k. lift_poly P k ∈ ecarrier M"
using P is_ext by (simp add: is_extension_const_mem poly_carrier_coeff_closed)
qed
text ‹∗‹Root-closedness at the adjoined index itself.› The fresh indeterminate is the realisation of
the variable, so it lies in the carrier once the modulus has degree at least two. And it is a root:
@{thm [source] eval_transport} moves the evaluation into the field of remainders, where
@{thm [source] eval_remainder_at_var} identifies it with the reduction of the polynomial --- which
vanishes precisely because the modulus divides it.›
lemma root_closed_adjoin_self:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
and dvd: "M.poly_dvd Q (lift_poly (fst j))"
and Pj: "fst j ∈ poly_carrier"
and d2: "2 ≤ M.degree Q"
shows "ivar j ∈ ecarrier (adjoin j Q)
∧ eeval (adjoin j Q) (ivar j) (lift_poly (fst j)) = 𝟬⇩I"
proof -
have varlow: "M.var ∈ M.low_poly (M.degree Q)" by (rule var_low [OF d2])
have "ivar j = ieval (ivar j) M.var" by (rule ieval_poly_var [symmetric])
then have "ivar j ∈ ieval (ivar j) ` M.low_poly (M.degree Q)" using varlow by blast
then have mem: "ivar j ∈ ecarrier (adjoin j Q)" by (simp add: adjoin_carrier_def)
have RA: "Ring (M.low_poly (M.degree Q)) (M.poly_add)
(λS T. M.pmod (M.poly_mult S T) Q) M.poly_zero M.poly_one"
using M.remainder_field [OF irr] by (simp add: Field_def commutative_ring_def)
have RK: "Ring (ieval (ivar j) ` M.low_poly (M.degree Q))
(eadd (adjoin j Q)) (emult (adjoin j Q))
(ieval (ivar j) M.poly_zero) (ieval (ivar j) M.poly_one)"
using adjoin_Ring [OF fresh irr] ieval_poly_zero ieval_poly_one
by (simp add: adjoin_carrier_def)
have ha: "ieval (ivar j) (M.poly_add S T)
= eadd (adjoin j Q) (ieval (ivar j) S) (ieval (ivar j) T)"
if ST: "S ∈ M.low_poly (M.degree Q)" "T ∈ M.low_poly (M.degree Q)" for S T
unfolding adjoin_def
using ST adjoin_rep [OF fresh ST(1)] adjoin_rep [OF fresh ST(2)]
by (simp add: adjoin_carrier_def)
have hm: "ieval (ivar j) (M.pmod (M.poly_mult S T) Q)
= emult (adjoin j Q) (ieval (ivar j) S) (ieval (ivar j) T)"
if ST: "S ∈ M.low_poly (M.degree Q)" "T ∈ M.low_poly (M.degree Q)" for S T
unfolding adjoin_def
using ST adjoin_rep [OF fresh ST(1)] adjoin_rep [OF fresh ST(2)]
by (simp add: adjoin_carrier_def)
have liftc: "lift_poly (fst j) ∈ M.poly_carrier" by (rule lift_poly_M_carrier [OF Pj])
have coeffM: "lift_poly (fst j) k ∈ ecarrier M" for k
using liftc by (rule M.poly_carrier_coeff_closed)
have constlow: "M.poly_const (lift_poly (fst j) k) ∈ M.low_poly (M.degree Q)" for k
using const_low [OF irr coeffM] .
have hconst: "ieval (ivar j) (M.poly_const (lift_poly (fst j) k)) = lift_poly (fst j) k" for k
using ieval_poly_const [OF is_extension_carrier_closed [OF is_ext coeffM]] .
have hfun: "(λk. ieval (ivar j) (M.poly_const (lift_poly (fst j) k))) = lift_poly (fst j)"
by (rule ext) (rule hconst)
note transport =
eval_transport [OF RA RK ha hm ieval_inj_on_low [OF fresh] varlow constlow]
note evalrem = M.eval_remainder_at_var [OF irr d2 liftc]
have pmodz: "M.pmod (lift_poly (fst j)) Q = M.poly_zero"
using dvd M.poly_dvd_iff_pmod_zero
[OF M.poly_irreducibleD_carrier [OF irr] M.poly_irreducibleD_nonzero [OF irr] liftc]
by simp
have step1: "eeval (adjoin j Q) (ivar j) (lift_poly (fst j))
= Ring.eval (ieval (ivar j) ` M.low_poly (M.degree Q))
(eadd (adjoin j Q)) (emult (adjoin j Q))
(ieval (ivar j) M.poly_zero) (ieval (ivar j) M.poly_one)
(ieval (ivar j) M.var)
(λk. ieval (ivar j) (M.poly_const (lift_poly (fst j) k)))"
unfolding adjoin_carrier_eq adjoin_carrier_def hfun
ieval_poly_zero ieval_poly_one ieval_poly_var
by rule
have "eeval (adjoin j Q) (ivar j) (lift_poly (fst j))
= ieval (ivar j)
(Ring.eval (M.low_poly (M.degree Q)) (M.poly_add)
(λS T. M.pmod (M.poly_mult S T) Q) M.poly_zero M.poly_one
M.var (λk. M.poly_const (lift_poly (fst j) k)))"
unfolding step1 by (rule transport)
also have "… = ieval (ivar j) M.poly_zero" using evalrem pmodz by simp
also have "… = 𝟬⇩I" by (rule ieval_poly_zero)
finally have "eeval (adjoin j Q) (ivar j) (lift_poly (fst j)) = 𝟬⇩I" .
with mem show ?thesis by blast
qed
text ‹∗‹Root-closedness at an index other than the adjoined one.› An element of the adjoined carrier
that involves such an index must have a coefficient involving it --- removing copies of the adjoined
index cannot remove a different one --- and that coefficient lies in @{term M}, where
root-closedness applies. @{thm [source] Ring.ext_le_eval} then carries the root upwards.›
lemma root_closed_adjoin_other:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
and S: "S ∈ M.low_poly (M.degree Q)"
and P': "P' ∈ poly_carrier" and ne: "(P', i') ≠ j"
and nf: "¬ index_free (ieval (ivar j) S) (P', i')"
shows "ivar (P', i') ∈ ecarrier (adjoin j Q)
∧ eeval (adjoin j Q) (ivar (P', i')) (lift_poly P') = 𝟬⇩I"
proof -
have Sc: "S ∈ M.poly_carrier" using S by (rule M.low_poly_closed)
have Sip: "S k ∈ ipoly_carrier" for k using Sc by (rule coeff_ipoly_closed)
have SM: "S k ∈ ecarrier M" for k using Sc by (rule M.poly_carrier_coeff_closed)
have Sf: "index_free (S k) j" for k using fresh SM by blast
obtain m where m: "(P', i') ∈# m" and nz: "ieval (ivar j) S m ≠ 𝟬"
using nf unfolding index_free_def by blast
have val: "ieval (ivar j) S m
= (if count m j ≤ M.degree Q
then S (count m j) (m - replicate_mset (count m j) j) else 𝟬)"
using ieval_low_fincomp [OF S] ieval_ivar [OF Sip Sf] by simp
with nz have cnz: "S (count m j) (m - replicate_mset (count m j) j) ≠ 𝟬"
by (auto split: if_split_asm)
have inm: "(P', i') ∈# m - replicate_mset (count m j) j"
using m ne by (simp add: in_diff_count count_replicate_mset)
then have nfS: "¬ index_free (S (count m j)) (P', i')"
using cnz unfolding index_free_def by blast
have rc: "root_closed M" using is_ext by (rule is_extension_root_closed)
have mem: "ivar (P', i') ∈ ecarrier M" by (rule root_closed_mem [OF rc SM P' nfS])
have rootM: "eeval M (ivar (P', i')) (lift_poly P') = 𝟬⇩I"
by (rule root_closed_eval [OF rc SM P' nfS])
have "eeval (adjoin j Q) (ivar (P', i')) (lift_poly P')
= eeval M (ivar (P', i')) (lift_poly P')"
proof (rule ext_le_eval [OF M_Ring adjoin_Ring [OF fresh irr] ext_le_adjoin [OF fresh irr] mem])
show "⋀k. lift_poly P' k ∈ ecarrier M"
using P' is_extension_const_mem [OF is_ext] poly_carrier_coeff_closed by simp
qed
with rootM mem ecarrier_subset_adjoin [OF fresh irr] show ?thesis by auto
qed
text ‹∗‹The adjoined extension is root-closed.› The two cases above, joined by the observation that
the adjoined index can only be involved at all when the modulus is nonlinear: were its degree at most
one the remainders would be constants, so every element of the carrier would lie in @{term M} and be
index-free at the fresh index by freshness.›
lemma root_closed_adjoin:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
and dvd: "M.poly_dvd Q (lift_poly (fst j))"
and Pj: "fst j ∈ poly_carrier"
shows "root_closed (adjoin j Q)"
proof (rule root_closedI)
fix 𝒫 P' i'
assume Pmem: "𝒫 ∈ ecarrier (adjoin j Q)" and P': "P' ∈ poly_carrier"
and nf: "¬ index_free 𝒫 (P', i')"
obtain S where S: "S ∈ M.low_poly (M.degree Q)" and Peq: "𝒫 = ieval (ivar j) S"
using Pmem unfolding adjoin_carrier_eq adjoin_carrier_def by blast
show "ivar (P', i') ∈ ecarrier (adjoin j Q)
∧ eeval (adjoin j Q) (ivar (P', i')) (lift_poly P') = 𝟬⇩I"
proof (cases "(P', i') = j")
case False
show ?thesis
using root_closed_adjoin_other [OF fresh irr S P' False] nf Peq by simp
next
case True
have d2: "2 ≤ M.degree Q"
proof (rule ccontr)
assume "¬ 2 ≤ M.degree Q"
then have d1: "M.degree Q ≤ 1" by simp
have Sc: "S ∈ M.poly_carrier" using S by (rule M.low_poly_closed)
have "S = M.poly_zero ∨ M.degree S < M.degree Q"
using S M.low_poly_iff_degree [OF Sc] by blast
then have dS: "M.degree S = 0" using d1 M.degree_zero by fastforce
have "S = M.poly_const (S 0)" by (rule M.degree_zero_imp_const [OF Sc dS])
moreover have "S 0 ∈ ecarrier M" using Sc by (rule M.poly_carrier_coeff_closed)
ultimately have "𝒫 = S 0"
using Peq ieval_poly_const [OF is_extension_carrier_closed [OF is_ext]] by metis
then have "index_free 𝒫 j" using fresh ‹S 0 ∈ ecarrier M› by simp
with nf True show False by simp
qed
have Pfst: "P' = fst j" using True by (metis fst_conv)
show ?thesis
using root_closed_adjoin_self [OF fresh irr dvd Pj d2] True Pfst by simp
qed
qed
text ‹∗‹The adjoined triple is an extension.› Everything is now in place: the field structure and the
restrictedness of both operations come from the transport, root-closedness from the two cases above,
and the conditions on the constants from the fact that @{term M} lies below, its own agreement with
@{term R} on constants carrying over.›
theorem is_extension_adjoin:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q"
and dvd: "M.poly_dvd Q (lift_poly (fst j))"
and Pj: "fst j ∈ poly_carrier"
shows "is_extension (adjoin j Q)"
proof (rule is_extensionI)
show "Field (ecarrier (adjoin j Q)) (eadd (adjoin j Q)) (emult (adjoin j Q)) 𝟬⇩I 𝟭⇩I"
by (rule adjoin_field_zero_one [OF fresh irr])
show "ecarrier (adjoin j Q) ⊆ ipoly_carrier"
proof
fix y assume "y ∈ ecarrier (adjoin j Q)"
then obtain S where S: "S ∈ M.low_poly (M.degree Q)" and yeq: "y = ieval (ivar j) S"
unfolding adjoin_carrier_eq adjoin_carrier_def by blast
show "y ∈ ipoly_carrier"
using yeq Ring.eval_closed [OF ipoly_ring low_poly_ambient [OF S] ivar_closed] by simp
qed
next
fix a assume a: "a ∈ R"
have "ipoly_const a ∈ ecarrier M" using is_ext a by (rule is_extension_const_mem)
then have "ipoly_const a ∈ adjoin_carrier j Q"
using ecarrier_subset_adjoin [OF fresh irr] by blast
then show "ipoly_const a ∈ ecarrier (adjoin j Q)" by simp
next
fix a b assume a: "a ∈ R" and b: "b ∈ R"
have mem: "ipoly_const a ∈ ecarrier M" "ipoly_const b ∈ ecarrier M"
using is_ext a b by (blast intro: is_extension_const_mem)+
have "eadd (adjoin j Q) (ipoly_const a) (ipoly_const b)
= eadd M (ipoly_const a) (ipoly_const b)"
by (rule ext_le_add [OF ext_le_adjoin [OF fresh irr] mem(1) mem(2), symmetric])
also have "… = ipoly_const (a + b)" using is_ext a b by (rule is_extension_const_add)
finally show "eadd (adjoin j Q) (ipoly_const a) (ipoly_const b) = ipoly_const (a + b)" .
next
fix a b assume a: "a ∈ R" and b: "b ∈ R"
have mem: "ipoly_const a ∈ ecarrier M" "ipoly_const b ∈ ecarrier M"
using is_ext a b by (blast intro: is_extension_const_mem)+
have "emult (adjoin j Q) (ipoly_const a) (ipoly_const b)
= emult M (ipoly_const a) (ipoly_const b)"
by (rule ext_le_mult [OF ext_le_adjoin [OF fresh irr] mem(1) mem(2), symmetric])
also have "… = ipoly_const (a ⋅ b)" using is_ext a b by (rule is_extension_const_mult)
finally show "emult (adjoin j Q) (ipoly_const a) (ipoly_const b) = ipoly_const (a ⋅ b)" .
next
show "root_closed (adjoin j Q)" by (rule root_closed_adjoin [OF fresh irr dvd Pj])
next
show "op_restricted (ecarrier (adjoin j Q)) (eadd (adjoin j Q))"
by (rule adjoin_field (2) [OF fresh irr])
next
show "op_restricted (ecarrier (adjoin j Q)) (emult (adjoin j Q))"
by (rule adjoin_field (3) [OF fresh irr])
qed
text ‹And it is ∗‹strictly› larger: the fresh indeterminate involves its own index, whereas every
element of @{term M} is index-free there.›
lemma adjoin_strictly_larger:
assumes fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 j"
and irr: "M.poly_irreducible Q" and d2: "2 ≤ M.degree Q"
shows "adjoin j Q ≠ M"
proof -
have "ivar j = ieval (ivar j) M.var" by (rule ieval_poly_var [symmetric])
then have "ivar j ∈ ieval (ivar j) ` M.low_poly (M.degree Q)"
using var_low [OF d2] by blast
then have inC: "ivar j ∈ ecarrier (adjoin j Q)" by (simp add: adjoin_carrier_def)
have notinM: "ivar j ∉ ecarrier M"
proof
assume "ivar j ∈ ecarrier M"
then have "index_free (ivar j) j" by (rule fresh)
with not_index_free_ivar [OF nontrivial, of j] show False by simp
qed
show ?thesis
proof
assume eq: "adjoin j Q = M"
have "ivar j ∈ ecarrier M" using inC eq by simp
with notinM show False ..
qed
qed
subsection ‹Every polynomial over the base field splits in a maximal extension›
text ‹∗‹The point of maximality.› Factor the lifted polynomial into irreducibles over @{term M}. A
factor of degree two or more would let a root of ∗‹it› be adjoined at a fresh index --- giving a
strictly larger extension, which maximality forbids. So every factor is linear, and a product of
linear factors splits.
Note where each earlier piece enters: @{thm [source] exists_fresh_index} supplies the index,
@{thm [source] is_extension_adjoin} and @{thm [source] ext_le_adjoin} make the enlargement an
extension above @{term M}, @{thm [source] adjoin_strictly_larger} contradicts maximality, and
@{thm [source] Field.degree_one_splits} with @{thm [source] Field.splits_poly_prod} assembles the
conclusion.›
theorem exists_root:
assumes max: "⋀L. ⟦ is_extension L; ext_le M L ⟧ ⟹ L = M"
and P: "P ∈ poly_carrier"
shows "M.splits (lift_poly P)"
proof -
have liftc: "lift_poly P ∈ M.poly_carrier" by (rule lift_poly_M_carrier [OF P])
show ?thesis
proof (cases "lift_poly P = M.poly_zero")
case True
then show ?thesis by (simp add: M.splits_zero)
next
case nz: False
show ?thesis
proof (cases "M.poly_unit (lift_poly P)")
case True
then have "lift_poly P = M.poly_const (lift_poly P 0)"
using M.poly_unit_imp_const by blast
moreover have "lift_poly P 0 ∈ ecarrier M"
using liftc by (rule M.poly_carrier_coeff_closed)
ultimately show ?thesis using M.splits_const by metis
next
case nu: False
obtain fs where firr: "⋀f. f ∈ set fs ⟹ M.poly_irreducible f"
and prod: "lift_poly P = M.poly_prod fs"
using M.factorization_into_irreducibles [OF liftc nz nu] by blast
have fc: "f ∈ M.poly_carrier" if "f ∈ set fs" for f
using firr [OF that] by (rule M.poly_irreducibleD_carrier)
have Pnz: "P ≠ 𝟬⇩P"
proof
assume "P = 𝟬⇩P"
then have "lift_poly P = M.poly_zero"
by (simp add: lift_poly_def poly_zero_def M.poly_zero_def)
with nz show False ..
qed
have deg1: "M.degree f = 1" if f: "f ∈ set fs" for f
proof (rule ccontr)
assume "M.degree f ≠ 1"
moreover have "0 < M.degree f"
using firr [OF f] by (rule M.poly_irreducible_degree_pos)
ultimately have d2: "2 ≤ M.degree f" by simp
obtain i where fresh: "⋀𝒫. 𝒫 ∈ ecarrier M ⟹ index_free 𝒫 (P, i)"
using exists_fresh_index [OF is_ext P Pnz] by blast
have dvd: "M.poly_dvd f (lift_poly (fst (P, i)))"
using prod M.poly_dvd_poly_prod [OF fc f] by simp
have Pj: "fst (P, i) ∈ poly_carrier" using P by simp
have "is_extension (adjoin (P, i) f)"
by (rule is_extension_adjoin [OF fresh firr [OF f] dvd Pj])
moreover have "ext_le M (adjoin (P, i) f)"
by (rule ext_le_adjoin [OF fresh firr [OF f]])
ultimately have "adjoin (P, i) f = M" by (rule max)
moreover have "adjoin (P, i) f ≠ M"
by (rule adjoin_strictly_larger [OF fresh firr [OF f] d2])
ultimately show False by simp
qed
have "M.splits f" if "f ∈ set fs" for f
by (rule M.degree_one_splits [OF fc [OF that] deg1 [OF that]])
then show ?thesis using prod M.splits_poly_prod by simp
qed
qed
qed
end
section ‹An Extension in which Every Base Polynomial Splits›
context Field
begin
text ‹Zorn gave a maximal extension; maximality makes every polynomial over @{term R} split in it.
Putting the two together is the whole of this step, exactly as it is in HOL-Algebra.›
theorem exists_extension_with_roots:
obtains M where "is_extension M"
and "⋀P. P ∈ poly_carrier
⟹ Field.splits (ecarrier M) (eadd M) (emult M) 𝟬⇩I 𝟭⇩I (lift_poly P)"
proof -
obtain M where Mext: "M ∈ extensions"
and Mmax: "∀L ∈ extensions. ext_le M L ⟶ L = M"
using exists_maximal_extension by blast
have ext: "is_extension M" using Mext by simp
interpret FE: field_extension R addition multiplication zero unit M
by unfold_locales (rule ext)
have max: "⋀L. ⟦ is_extension L; ext_le M L ⟧ ⟹ L = M"
using Mmax by simp
show thesis
proof (rule that [OF ext])
fix P assume P: "P ∈ poly_carrier"
show "Field.splits (ecarrier M) (eadd M) (emult M) 𝟬⇩I 𝟭⇩I (lift_poly P)"
by (rule FE.exists_root [OF max P])
qed
qed
end
end