Theory Artin
section ‹Artin's lemma: a finite automorphism group bounds the degree over its fixed field›
theory Artin
imports Galois_Correspondence Linear_System Iso_Extension_Tower
begin
text ‹Let ‹H› be a ∗‹finite› group of automorphisms of a subfield ‹K› of a field, and let
@{term "fixed_field K H"} be the subfield it fixes pointwise. ∗‹Artin's lemma› bounds the
extension ‹K› over that fixed field by the order of the group: any @{term "card H + 1"} elements
of ‹K› are linearly dependent over @{term "fixed_field K H"}.
The proof is the linear-algebra pigeonhole principle. Given elements @{text "x⇩1, …, x⇩n"} of
‹K› with @{text "n > card H"}, consider the homogeneous system
▪ one equation per automorphism @{text "σ ∈ H"}, namely @{text "∑⇩j σ(x⇩j) c⇩j = 0"},
in the unknowns @{term "c⇩j"}. There are more unknowns than equations, so
@{thm [source] Subfield.underdetermined_solution} supplies a nontrivial solution in ‹K› --- and
the equation belonging to the identity automorphism is precisely the required dependence
@{text "∑⇩j x⇩j c⇩j = 0"}.›
subsection ‹Artin's lemma›
text ‹The system to be solved has one equation per automorphism and one unknown per element, so its
coefficient matrix is @{term "λσ j. σ (x j)"}: a genuinely two-index family, indexed by
∗‹functions› on one side and by the element index on the other. This is exactly the shape
@{thm [source] Subfield.underdetermined_solution} was stated for, indices ranging over arbitrary
finite sets rather than initial segments.›
theorem artin_lemma:
fixes H :: "('a :: field ⇒ 'a) set" and x :: "'j ⇒ 'a"
assumes K: "Subfield K"
and finH: "finite H" and HG: "H ⊆ field_auto K F"
and finJ: "finite J" and card: "card H < card J"
and xK: "⋀j. j ∈ J ⟹ x j ∈ K"
shows "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∀σ ∈ H. (∑j ∈ J. σ (x j) * c j) = 0)"
proof -
interpret K: Subfield K by (rule K)
have entries: "∀σ ∈ H. ∀j ∈ J. σ (x j) ∈ K"
using HG xK by (blast intro: field_auto_closed)
show ?thesis
using K.underdetermined_solution
[where A = "λσ j. σ (x j)" and I = H and J = J, OF finH finJ card]
using entries by blast
qed
text ‹The advertised form: more than @{term "card H"} elements of @{term K} admit a nontrivial
vanishing @{term K}-linear combination against ∗‹every› automorphism of @{term H} at once, and in
particular --- taking the identity, which lies in every Galois group --- against the elements
themselves.›
corollary artin_lemma_dependence:
fixes H :: "('a :: field ⇒ 'a) set" and x :: "'j ⇒ 'a"
assumes K: "Subfield K"
and finH: "finite H" and HG: "H ⊆ field_auto K F" and id: "identity K ∈ H"
and finJ: "finite J" and card: "card H < card J"
and xJK: "x ` J ⊆ K"
shows "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∑j ∈ J. x j * c j) = 0"
proof -
have xK: "⋀j. j ∈ J ⟹ x j ∈ K" using xJK by blast
obtain c where cK: "∀j. c j ∈ K" and cnz: "∃j ∈ J. c j ≠ 0"
and ceq: "∀σ ∈ H. (∑j ∈ J. σ (x j) * c j) = 0"
using artin_lemma[where x = x, OF K finH HG finJ card xK] by blast
have "(∑j ∈ J. identity K (x j) * c j) = 0" using ceq id by blast
moreover have "⋀j. j ∈ J ⟹ identity K (x j) = x j" using xK by (simp add: identity_apply)
ultimately have "(∑j ∈ J. x j * c j) = 0" by simp
then show ?thesis using cK cnz by blast
qed
text ‹For a genuine Galois subgroup the identity premise is automatic. This is the convenient
interface for the later fixed-field argument, while @{thm [source] artin_lemma} deliberately
retains the extra generality of an arbitrary finite automorphism family.›
corollary artin_lemma_subgroup_dependence:
fixes H :: "('a :: field ⇒ 'a) set" and x :: "'j ⇒ 'a"
assumes K: "Subfield K"
and H: "H ∈ galois_subgroups K F" and finH: "finite H"
and finJ: "finite J" and card: "card H < card J"
and xJK: "x ` J ⊆ K"
shows "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∑j ∈ J. x j * c j) = 0"
proof -
interpret H: Subgroup H "field_auto K F" "compose K" "identity K"
using H by (simp add: galois_subgroups_iff)
show ?thesis
by (rule artin_lemma_dependence[OF K finH H.subset H.sub_unit_closed finJ card xJK])
qed
subsection ‹Transporting a dependence along an automorphism›
text ‹The step that will drive the descent to the fixed field: an automorphism carries a vanishing
linear combination to another vanishing linear combination, over the transported coefficients.
Multiplicativity handles each summand, additivity the sum, and @{thm [source] field_auto_zero} the
right-hand side.
This is the mechanism behind the minimality argument sketched at the end. If @{term c} is a
dependence among the @{term "x j"} with the fewest nonzero coefficients, normalised so that some
@{text "c k = 1"}, then @{text "λj. σ (c j)"} is another dependence, also with @{text "σ (c k) = 1"}
and supported in the same places. Their difference is a shorter dependence, so minimality forces it
to vanish, i.e. @{text "σ (c j) = c j"} for every @{text "σ ∈ H"} --- which is exactly to say that
the coefficients lie in @{term "fixed_field K H"}.›
lemma field_auto_transports_dependence:
assumes K: "Subfield K" and s: "σ ∈ field_auto K F"
and finJ: "finite J"
and xK: "⋀j. j ∈ J ⟹ x j ∈ K" and cK: "⋀j. j ∈ J ⟹ c j ∈ K"
and dep: "(∑j ∈ J. x j * c j) = 0"
shows "(∑j ∈ J. σ (x j) * σ (c j)) = 0"
proof -
interpret K: Subfield K by (rule K)
have "(∑j ∈ J. σ (x j) * σ (c j)) = (∑j ∈ J. σ (x j * c j))"
using xK cK by (simp add: field_auto_mult[OF s])
also have "… = σ (∑j ∈ J. x j * c j)"
using xK cK by (intro field_auto_sum[OF K s, symmetric]) (blast intro: K.mult_closed)
also have "… = 0" using dep field_auto_zero[OF K s] by simp
finally show ?thesis .
qed
text ‹Applying one subgroup automorphism to the coefficients preserves the simultaneous system.
For a target row @{term ρ}, apply @{term σ} to the row indexed by
‹compose K (inverse σ) ρ›; the group laws reduce the transformed row back to
@{term ρ}.›
lemma field_auto_transports_artin_solution:
fixes H :: "('a :: field ⇒ 'a) set"
assumes K: "Subfield K" and H: "H ∈ galois_subgroups K F"
and s: "σ ∈ H" and finJ: "finite J"
and xK: "⋀j. j ∈ J ⟹ x j ∈ K"
and cK: "⋀j. j ∈ J ⟹ c j ∈ K"
and equations: "∀ρ ∈ H. (∑j ∈ J. ρ (x j) * c j) = 0"
and "ρ ∈ H"
shows "(∑j ∈ J. ρ (x j) * σ (c j)) = 0"
proof -
interpret H: Subgroup H "field_auto K F" "compose K" "identity K"
using H by (simp add: galois_subgroups_iff)
let ?τ = "compose K (H.sub.inverse σ) ρ"
have invH: "H.sub.inverse σ ∈ H"
using s by simp
have t: "?τ ∈ H"
using invH ‹ρ ∈ H› by (rule H.sub.composition_closed)
have dep: "(∑j ∈ J. ?τ (x j) * c j) = 0"
using equations t by blast
have txK: "⋀j. j ∈ J ⟹ ?τ (x j) ∈ K"
using H.subset t xK by (blast intro: field_auto_closed)
have sAuto: "σ ∈ field_auto K F"
using H.subset s by blast
have transported: "(∑j ∈ J. σ (?τ (x j)) * σ (c j)) = 0"
using field_auto_transports_dependence[OF K sAuto finJ txK cK dep] .
have "⋀j. j ∈ J ⟹ σ (?τ (x j)) = ρ (x j)"
using H.sub.invertible H.sub.invertible_right_inverse2 ‹ρ ∈ H› s xK by (metis compose_eq)
with transported show "(∑j ∈ J. ρ (x j) * σ (c j)) = 0"
by simp
qed
subsection ‹Descending the coefficients to the fixed field›
text ‹The coefficients of a dependence can be taken to lie in the fixed field,
not merely in @{term K}.
The device is minimality. Among all nontrivial dependences of the @{term "x j"} choose one whose
∗‹support› @{term "{j ∈ J. c j ≠ 0}"} is smallest, and scale it so that some distinguished
coefficient equals @{term 1}. For @{text "σ ∈ H"} the transported family
@{text "λj. σ (c j)"} is again a dependence --- this is
@{thm [source] field_auto_transports_dependence}, and it needs @{term σ} to fix the @{term "x j"},
which is why the @{term "x j"} are taken in the fixed field's ∗‹ambient› position below.›
lemma dependence_difference:
fixes c d :: "'j ⇒ 'a :: field"
assumes finJ: "finite J"
and dep_c: "(∑j ∈ J. x j * c j) = 0" and dep_d: "(∑j ∈ J. x j * d j) = 0"
shows "(∑j ∈ J. x j * (c j - d j)) = 0"
by (simp add: dep_c dep_d right_diff_distrib' sum_subtractf)
text ‹The simultaneous system version of the minimal-support descent. Unlike the specialized
fixed-vector descent below, this does not assume that the vectors are fixed by
@{term H}: the equations contain every row @{term "ρ ∈ H"}, and
@{thm [source] field_auto_transports_artin_solution} transports a solution to another solution of
that same system. This is the form needed for the genuine Artin bound.›
theorem artin_solution_over_fixed_field:
fixes H :: "('a :: field ⇒ 'a) set" and x :: "'j ⇒ 'a"
assumes K: "Subfield K" and H: "H ∈ galois_subgroups K F"
and finJ: "finite J" and xK: "⋀j. j ∈ J ⟹ x j ∈ K"
and exsol: "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∀ρ ∈ H. (∑j ∈ J. ρ (x j) * c j) = 0)"
shows "∃c. (∀j ∈ J. c j ∈ fixed_field K H) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∀ρ ∈ H. (∑j ∈ J. ρ (x j) * c j) = 0)"
proof -
interpret KS: Subfield K by (rule K)
define Sol where
"Sol ≡ (λc :: 'j ⇒ 'a. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∀ρ ∈ H. (∑j ∈ J. ρ (x j) * c j) = 0))"
define supp where "supp ≡ (λc :: 'j ⇒ 'a. {j ∈ J. c j ≠ 0})"
define Q where "Q ≡ (λn. ∃c. Sol c ∧ card (supp c) = n)"
have "Q (LEAST n. Q n)" using exsol by (metis LeastI Sol_def Q_def)
then obtain c where solc: "Sol c" and cmin: "card (supp c) = (LEAST n. Q n)"
unfolding Q_def by blast
have minimal: "card (supp c) ≤ card (supp d)" if "Sol d" for d
by (metis Least_le Q_def cmin that)
from solc have cK: "⋀j. c j ∈ K" and ceq: "⋀ρ. ρ ∈ H ⟹ (∑j ∈ J. ρ (x j) * c j) = 0"
by (simp_all add: Sol_def)
from solc obtain k where kJ: "k ∈ J" and cknz: "c k ≠ 0"
by (auto simp: Sol_def)
define e where "e ≡ (λj. c j / c k)"
have eK: "⋀j. e j ∈ K" using cK by (simp add: e_def KS.divide_closed)
have ekeq1: "e k = 1" using cknz by (simp add: e_def)
have esupp: "supp e = supp c" using cknz by (auto simp: supp_def e_def)
have eeq: "(∑j ∈ J. ρ (x j) * e j) = 0" if r: "ρ ∈ H" for ρ
using ceq[OF r] by (simp add: e_def divide_simps flip: sum_divide_distrib)
have depe: "Sol e"
unfolding Sol_def using eK ekeq1 kJ eeq by (intro conjI allI bexI[of _ k]) (simp_all)
have fixed: "σ (e j) = e j" if s: "σ ∈ H" and jJ: "j ∈ J" for σ j
proof (rule ccontr)
assume ne: "σ (e j) ≠ e j"
have sG: "σ ∈ field_auto K F"
using H galois_subgroups_subset s by blast
define d where "d = (λi. e i - σ (e i))"
have eqe: "∀ρ ∈ H. (∑i ∈ J. ρ (x i) * e i) = 0"
using depe by (simp add: Sol_def)
have transported_all:
"∀ρ ∈ H. (∑i ∈ J. ρ (x i) * σ (e i)) = 0"
using field_auto_transports_artin_solution[OF K H s finJ xK eK eqe] by blast
have dep_d: "(∑i ∈ J. ρ (x i) * d i) = 0" if r: "ρ ∈ H" for ρ
using r eeq transported_all unfolding d_def
by (simp add: sum_subtractf right_diff_distrib)
have dK: "⋀i. d i ∈ K"
unfolding d_def using eK sG by (blast intro: KS.diff_closed field_auto_closed)
have depd: "Sol d"
using Sol_def dK d_def dep_d jJ ne by force
have dk: "d k = 0" using ekeq1 field_auto_one[OF sG] by (simp add: d_def)
have sub: "supp d ⊆ supp e - {k}"
using field_auto_zero K d_def dk sG supp_def by fastforce
have fin_e: "finite (supp e)" using finJ by (simp add: supp_def)
have k_e: "k ∈ supp e" using kJ ekeq1 by (simp add: supp_def)
have "card (supp d) ≤ card (supp e - {k})" using sub fin_e by (intro card_mono) blast
also have "… < card (supp e)"
using fin_e k_e by (meson card_Diff1_less)
finally show False using minimal[OF depd] esupp by simp
qed
show ?thesis
using Sol_def depe fixed by (smt (cvc5, dec_internal_enum_inst_sum) fixed_field_memI)
qed
text ‹Note that the @{term "x j"} are ∗‹fixed› by every @{text "σ ∈ H"}. This is essential and not a
technicality: @{thm [source] field_auto_transports_dependence} turns a dependence of the
@{term "x j"} into a dependence of the images @{term "σ (x j)"}, and only when those images are the
@{term "x j"} again is the result a dependence of the ∗‹same› family, so that subtracting it from
the original stays inside the system. In the intended application the roles are reversed from what
one might expect: it is the ∗‹vectors› that are taken over the fixed field and the
∗‹coefficients› that are unknown and must be shown to descend.
Also, @{term H} is closed under composition --- a subgroup of the Galois group --- which is what
makes @{text "σ (c j) = c j"} for all @{text "σ ∈ H"} equivalent to @{term "c j ∈ fixed_field K H"}.
In fact only membership of @{term "σ ` H ⊆ field_auto K F"} is used below; the group structure is
what makes the conclusion ∗‹mean› what it says.›
theorem dependence_over_fixed_field:
fixes H :: "('a :: field ⇒ 'a) set" and x :: "'j ⇒ 'a"
assumes K: "Subfield K"
and HG: "H ⊆ field_auto K F"
and finJ: "finite J"
and xK: "⋀j. j ∈ J ⟹ x j ∈ K"
and xfix: "⋀σ j. ⟦ σ ∈ H; j ∈ J ⟧ ⟹ σ (x j) = x j"
and exdep: "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∑j ∈ J. x j * c j) = 0"
shows "∃c. (∀j ∈ J. c j ∈ fixed_field K H) ∧ (∃j ∈ J. c j ≠ 0)
∧ (∑j ∈ J. x j * c j) = 0"
proof -
interpret K: Subfield K by (rule K)
define Dep where
"Dep ≡ (λc :: 'j ⇒ 'a. (∀j. c j ∈ K) ∧ (∃j ∈ J. c j ≠ 0) ∧ (∑j ∈ J. x j * c j) = 0)"
define supp where "supp ≡ (λc :: 'j ⇒ 'a. {j ∈ J. c j ≠ 0})"
define Q where "Q ≡ (λn. ∃c. Dep c ∧ card (supp c) = n)"
have "Q (LEAST n. Q n)" using exdep by (metis LeastI Dep_def Q_def)
then obtain c where depc: "Dep c" and cmin: "card (supp c) = (LEAST n. Q n)"
unfolding Q_def by blast
have minimal: "card (supp c) ≤ card (supp d)" if "Dep d" for d
by (metis Least_le Q_def cmin that)
from depc have cK: "⋀j. c j ∈ K" and ceq: "(∑j ∈ J. x j * c j) = 0"
by (simp_all add: Dep_def)
from depc obtain k where kJ: "k ∈ J" and cknz: "c k ≠ 0" by (auto simp: Dep_def)
define e where "e = (λj. c j / c k)"
have eK: "⋀j. e j ∈ K" using cK by (simp add: e_def K.divide_closed)
have ek: "e k = 1" using cknz by (simp add: e_def)
have esupp: "supp e = supp c" using cknz by (auto simp: supp_def e_def)
have eeq: "(∑j ∈ J. x j * e j) = 0"
using ceq e_def
by (metis (mono_tags, lifting) div_0 sum.cong sum_divide_distrib times_divide_eq_right)
have depe: "Dep e"
unfolding Dep_def using eK eeq by (intro conjI allI bexI[of _ k]) (simp_all add: ek kJ)
have fixed: "σ (e j) = e j" if s: "σ ∈ H" and jJ: "j ∈ J" for σ j
proof (rule ccontr)
assume ne: "¬ ?thesis"
have sG: "σ ∈ field_auto K F" using s HG by blast
define d where "d = (λi. e i - σ (e i))"
have "(∑i ∈ J. σ (x i) * σ (e i)) = 0"
using eeq eK xK by (intro field_auto_transports_dependence[OF K sG finJ]) auto
then have dep_t: "(∑i ∈ J. x i * σ (e i)) = 0" using xfix[OF s] by simp
have dep_d: "(∑i ∈ J. x i * d i) = 0"
unfolding d_def using eeq dep_t by (rule dependence_difference[OF finJ])
have dK: "⋀i. d i ∈ K"
unfolding d_def using eK sG by (blast intro: K.diff_closed field_auto_closed)
have dnz: "d j ≠ 0" using ne by (simp add: d_def)
have depd: "Dep d" using dK dnz jJ dep_d by (auto simp: Dep_def)
have dk: "d k = 0" using ek field_auto_one[OF sG] by (simp add: d_def)
have sub: "supp d ⊆ supp e - {k}"
using field_auto_zero Diff_iff K d_def dk empty_iff insert_iff mem_Collect_eq right_minus_eq
sG supp_def by fastforce
have fin_e: "finite (supp e)" using finJ by (simp add: supp_def)
have k_e: "k ∈ supp e" using kJ ek by (simp add: supp_def)
have "card (supp d) ≤ card (supp e - {k})" using sub fin_e by (intro card_mono) blast
also have "… < card (supp e)"
using fin_e k_e by (meson card_Diff1_less_iff)
finally show False using minimal[OF depd] esupp by simp
qed
show ?thesis
using Dep_def depe fixed by (metis (lifting) fixed_field_memI)
qed
subsection ‹Dedekind's lemma: distinct automorphisms are linearly independent›
text ‹The reverse direction. Distinct field automorphisms are linearly independent as functions:
if @{text "∑⇩σ a⇩σ σ(z) = 0"} for ∗‹every› @{term z} in @{term K}, with the @{term σ} pairwise
distinct, then all the coefficients @{term "a σ"} vanish.
The proof is by induction on the number of automorphisms involved, and the inductive step is a
small piece of cunning. Suppose the relation holds for a set @{term "insert σ⇩0 S"} and, for a
contradiction, that it is nontrivial. Pick @{term τ} in @{term S} and, since @{term τ} and
@{term σ⇩0} are distinct automorphisms, an element @{term y} of @{term K} with
@{term "σ⇩0 y ≠ τ y"}. Now evaluate the relation at @{term "y * z"} rather than at @{term z}: by
multiplicativity this multiplies the @{term σ}-th term by @{term "σ y"}. Subtracting
@{term "σ⇩0 y"} times the original relation annihilates the @{term σ⇩0} term, leaving a relation on
@{term S} alone whose @{term τ}-coefficient is @{term "a τ * (τ y - σ⇩0 y) ≠ 0"}.›
lemma character_relation_scaled:
assumes K: "Subfield K" and finS: "finite S"
and SG: "S ⊆ field_auto K F"
and rel: "⋀z. z ∈ K ⟹ (∑σ ∈ S. a σ * σ z) = 0"
and y: "y ∈ K" and z: "z ∈ K"
shows "(∑σ ∈ S. (a σ * σ y) * σ z) = 0"
proof -
interpret K: Subfield K by (rule K)
have mult: "σ (y * z) = σ y * σ z" if "σ ∈ S" for σ
using that SG y z by (blast intro: field_auto_mult)
have "(∑σ ∈ S. (a σ * σ y) * σ z) = (∑σ ∈ S. a σ * σ (y * z))"
by (simp add: mult mult.assoc)
also have "… = 0" using rel y z by (simp add: K.mult_closed)
finally show ?thesis .
qed
text ‹Dedekind's lemma. The coefficients are arbitrary field elements; no subfield hypothesis on
them is needed, and none is available in the intended application.›
theorem dedekind_independence:
fixes S :: "('a :: field ⇒ 'a) set" and a :: "('a ⇒ 'a) ⇒ 'a"
assumes K: "Subfield K"
shows "⟦ finite S; S ⊆ field_auto K F; ⋀z. z ∈ K ⟹ (∑σ ∈ S. a σ * σ z) = 0 ⟧
⟹ ∀σ ∈ S. a σ = 0"
proof (induction S arbitrary: a rule: finite_induct)
case empty then show ?case by simp
next
case (insert σ⇩0 S)
interpret K: Subfield K by (rule K)
note insG = insert.prems(1) and insrel = insert.prems(2)
have s0G: "σ⇩0 ∈ field_auto K F" and SG: "S ⊆ field_auto K F" using insG by auto
have rel: "⋀z. z ∈ K ⟹ a σ⇩0 * σ⇩0 z + (∑σ ∈ S. a σ * σ z) = 0"
using insrel insert.hyps by simp
have S_zero: "a τ = 0" if "τ ∈ S" for τ
proof (rule ccontr)
assume atnz: "¬ ?thesis"
have tG: "τ ∈ field_auto K F" using ‹τ ∈ S› SG by blast
have tne: "τ ≠ σ⇩0" using ‹τ ∈ S› insert.hyps by blast
obtain y where yK: "y ∈ K" and diff: "σ⇩0 y ≠ τ y"
using s0G tG tne by (metis (no_types, lifting) ext PiE_E field_auto_mem_iff)
define b where "b ≡ (λσ. a σ * (σ y - σ⇩0 y))"
have "(∑σ ∈ S. b σ * σ z) = 0" if zK: "z ∈ K" for z
proof -
have scaled: "(∑σ ∈ insert σ⇩0 S. (a σ * σ y) * σ z) = 0"
by (rule character_relation_scaled[OF K _ insG insrel yK zK]) (simp add: insert.hyps)
have "(∑σ ∈ insert σ⇩0 S. (a σ * σ⇩0 y) * σ z) = σ⇩0 y * (∑σ ∈ insert σ⇩0 S. a σ * σ z)"
by (simp add: sum_distrib_left mult.commute mult.left_commute)
also have "… = 0" using insrel zK by simp
finally have orig: "(∑σ ∈ insert σ⇩0 S. (a σ * σ⇩0 y) * σ z) = 0" .
have "(∑σ ∈ insert σ⇩0 S. b σ * σ z)
= (∑σ ∈ insert σ⇩0 S. (a σ * σ y) * σ z) - (∑σ ∈ insert σ⇩0 S. (a σ * σ⇩0 y) * σ z)"
unfolding b_def by (simp add: sum_subtractf left_diff_distrib right_diff_distrib mult.assoc)
also have "… = 0" using scaled orig by simp
finally have "(∑σ ∈ insert σ⇩0 S. b σ * σ z) = 0" .
then show ?thesis using insert.hyps
using b_def by force
qed
then show False using insert.IH[where a = b, OF SG] ‹τ ∈ S› atnz diff
by (force simp: b_def)
qed
have "a σ⇩0 * σ⇩0 1 + (∑σ ∈ S. a σ * σ 1) = 0" using rel K.one_closed by blast
moreover have "(∑σ ∈ S. a σ * σ 1) = 0" using S_zero by simp
ultimately have "a σ⇩0 = 0"
using field_auto_one[OF s0G] by simp
then show ?case using S_zero by blast
qed
text ‹This theory supplies the two difficult
ingredients for Artin's theorem: the pigeonhole dependence and the descent of its coefficients
into the fixed field. The vector-space degree assembly and the final finite-group equality live
in ‹Artin_Degree›.
The older ‹dependence_over_fixed_field› remains a useful specialization for a family of
vectors already fixed by @{term H}. The corrected simultaneous-system theorem
‹artin_solution_over_fixed_field› is the interface used by the degree layer, so the public
‹artin_theorem› no longer exposes either that fixed-vector premise or an explicit basis
premise.›
end