Theory Artin_Degree
section ‹Artin's degree bound: the fixed field of a finite group has small index›
theory Artin_Degree
imports Artin Algebraic_Transitivity
begin
text ‹The results of ‹Artin› are phrased with explicit sums over an index set.
Here they are transported into the vector-space language of
‹Extension_Vector_Space›, where @{term "fixed_field K H ⊆ K"} is a
@{locale subfield_tower} and the size of the extension is measured by
@{const Vector_Space.lin_indep} and @{const Vector_Space.dimension}. The bridge in both directions
is @{thm [source] subfield_tower.vs_lincomb_eq_sum}: an abstract linear combination over a finite
set of vectors is an ordinary field sum.
The conclusion is ∗‹Artin's bound›: over the fixed field of a finite group @{term H} of
automorphisms, no more than @{term "card H"} elements of @{term K} can be linearly independent.
Together with Dedekind's lemma --- which gives the matching lower bound --- this is what pins the
order of the Galois group of @{term "fixed_field K H"} to exactly @{term "card H"}.›
notation plus (infixl ‹+› 65)
notation minus (infixl ‹-› 65)
unbundle uminus_syntax
subsection ‹The fixed field sits below ‹K› as a tower›
text ‹Both fields are native set-based subfields and one contains the other, so they form a
@{locale subfield_tower} --- the scalars being the fixed field and the vectors @{term K}.›
lemma fixed_field_tower:
assumes K: "Subfield K" and HG: "H ⊆ field_auto K F"
shows "subfield_tower (fixed_field K H) K"
using HG K
by (meson field_auto_fixed_field_subfield fixed_field_subset subfield_tower_axioms.intro
subfield_tower_def)
subsection ‹Artin's bound›
text ‹No set of more than @{term "card H"} elements of @{term K} is linearly independent over the
fixed field. The argument is the one sketched in ‹Artin›, now assembled:
@{thm [source] artin_lemma} produces a simultaneous dependence with coefficients in @{term K}, and
@{thm [source] artin_solution_over_fixed_field} pushes those coefficients down into the fixed field.
The simultaneous system is the key correction: no assumption that the vectors themselves are fixed
by @{term H} is needed.
Care is needed about which set indexes what. A ‹lin_indep› set is a set ∗‹of vectors›, and the
dependence lemmas index by an arbitrary type; we index the vectors by themselves, taking
@{term "J = B"} and @{term "x = id"}.
The statements live in a ∗‹context› fixing @{term K} and @{term H} and interpreting the tower. The
@{locale Vector_Space} locale has nine parameters, so spelling ‹lin_indep› out at the top level
would mean writing all of them; inside the context the interpretation supplies them and the
qualified ‹T.vs.› prefix works.›
context
fixes K F :: "'a :: field set" and H :: "('a ⇒ 'a) set"
assumes K: "Subfield K" and Hsub: "H ∈ galois_subgroups K F"
begin
lemma H_auto: "H ⊆ field_auto K F" using Hsub by (rule galois_subgroups_subset)
interpretation T: subfield_tower "fixed_field K H" K by (rule fixed_field_tower[OF K H_auto])
theorem artin_bound:
assumes finH: "finite H" and BK: "B ⊆ K"
and finB: "finite B" and lt: "card H < card B"
shows "¬ T.vs.lin_indep B"
proof
assume indep: "T.vs.lin_indep B"
have idH: "identity K ∈ H"
using Hsub by (metis Subgroup_def Submonoid.sub_unit_closed galois_subgroups_iff)
have xK: "⋀j. j ∈ B ⟹ id j ∈ K"
using BK by force
have dep: "∃c. (∀j. c j ∈ K) ∧ (∃j ∈ B. c j ≠ 0) ∧
(∀σ ∈ H. (∑j ∈ B. σ (id j) * c j) = 0)"
using artin_lemma[where x = id and J = B, OF K finH H_auto finB lt xK] .
have descended:
"∃c. (∀j ∈ B. c j ∈ fixed_field K H) ∧ (∃j ∈ B. c j ≠ 0) ∧ (∀σ ∈ H. (∑j ∈ B. σ (id j) * c j) = 0)"
by (intro xK K dep finB Hsub artin_solution_over_fixed_field[where F = F])
then obtain c where cfix: "⋀j. j ∈ B ⟹ c j ∈ fixed_field K H"
and cnz: "∃j ∈ B. c j ≠ 0"
and ceq_all: "∀σ ∈ H. (∑j ∈ B. σ (id j) * c j) = 0" by blast
have ceq: "(∑j ∈ B. j * c j) = 0"
proof -
have row: "(∑j ∈ B. identity K (id j) * c j) = 0"
using ceq_all idH by blast
moreover have "(∑j ∈ B. identity K (id j) * c j) = (∑j ∈ B. j * c j)"
using xK by force
ultimately show ?thesis by simp
qed
define e where "e ≡ restrict c B"
have eF: "e ∈ B →⇩E fixed_field K H" using cfix by (simp add: e_def)
have "T.vs.lincomb e B = (∑j ∈ B. e j * j)"
using finB BK eF by (intro T.vs_lincomb_eq_sum) auto
also have "… = 0"
by (simp add: ceq e_def mult.commute)
finally have lc0: "T.vs.lincomb e B = 0" .
have "∀v ∈ B. e v = 0" using indep eF lc0 by (simp add: T.vs.lin_indep_def)
then show False using cnz by (auto simp: e_def)
qed
text ‹Consequently a basis of @{term K} over the fixed field --- if there is one --- has at most
@{term "card H"} elements, so the degree is bounded by the group order.›
corollary artin_dimension_le:
assumes finH: "finite H" and basis: "T.vs.basis B"
shows "card B ≤ card H"
using T.vs.basis_def T.vs.basis_lin_indep artin_bound assms
by (meson linorder_le_less_linear)
text ‹And the same bound on the degree itself, since the dimension is the size of any basis
(@{thm [source] Vector_Space.dimension_eq_any_field} --- no finiteness of the base field needed).›
corollary artin_degree_le:
assumes finH: "finite H" and basis: "T.vs.basis B"
shows "T.vs.dimension ≤ card H"
using artin_dimension_le[where B = B, OF finH basis]
T.vs.dimension_eq_any_field[OF basis] by simp
end
subsection ‹The reverse bound: the Galois group is no larger than the degree›
text ‹Now the other inequality, and the one that needs Dedekind's lemma. Let @{term E} be an
intermediate field and @{term B} a basis of @{term K} over @{term E}. Then
@{term "field_auto K E"} has at most @{term "card B"} elements.
The argument is again the linear pigeonhole, with the roles of the two index sets exchanged.
Suppose there were more than @{term "card B"} automorphisms, and take a finite set @{term S} of
them of size @{term "card B + 1"}. Consider the system with ∗‹one equation per basis vector›
@{term "v ∈ B"} and one unknown per automorphism:
@{text "∑⇩σ a⇩σ σ(v) = 0"}. It has more unknowns than equations, so
@{thm [source] Subfield.underdetermined_solution} gives a nontrivial solution.
A solution of those finitely many equations already satisfies the corresponding relation at
∗‹every› point of @{term K}: an arbitrary @{term "z ∈ K"} is an @{term E}-combination of @{term B},
and each automorphism is @{term E}-linear (it is additive, multiplicative, and fixes @{term E}), so
the relation propagates from the basis to all of @{term K} by linearity. But then Dedekind's lemma
forces every coefficient to vanish --- contradicting nontriviality.
The propagation step is the only real work, and it is where the basis hypothesis is used.›
text ‹As before the statements sit inside a context, so that the tower's interpretation supplies the
nine parameters of @{locale Vector_Space} and ‹basis› can be written qualified. The tower is
∗‹interpreted› here rather than passed as an assumption: a hypothesis @{text "subfield_tower E K"}
would not bring ‹T.vs.basis› into scope for the statement itself.›
context
fixes K E :: "'a :: field set"
assumes K: "Subfield K" and Ebase: "subfield_tower E K"
begin
interpretation T: subfield_tower E K by (rule Ebase)
text ‹The base field lies inside the extension --- the tower's own axiom.›
lemma EK: "E ⊆ K" by (rule T.base_subset)
text ‹An automorphism fixing @{term E} is @{term E}-linear on linear combinations of a finite set of
vectors: it commutes with the sum, with the scalar products, and fixes the scalars.›
lemma field_auto_lincomb:
assumes s: "σ ∈ field_auto K E" and finB: "finite B" and BK: "B ⊆ K"
and c: "⋀v. v ∈ B ⟹ c v ∈ E"
shows "σ (∑v ∈ B. c v * v) = (∑v ∈ B. c v * σ v)"
proof -
have cK: "⋀v. v ∈ B ⟹ c v ∈ K" using c EK by blast
have "σ (∑v ∈ B. c v * v) = (∑v ∈ B. σ (c v * v))"
using cK BK by (intro field_auto_sum[OF K s]) (blast intro: Subfield.mult_closed[OF K])
also have "… = (∑v ∈ B. c v * σ v)"
using BK c cK s by (smt (cvc5, interleave) field_auto_mem_iff subset_iff sum.cong)
finally show ?thesis .
qed
text ‹Hence a relation among automorphisms that holds on a basis holds throughout @{term K}.›
lemma character_relation_from_basis:
assumes finS: "finite S" and SG: "S ⊆ field_auto K E"
and basis: "T.vs.basis B"
and rel: "∀v ∈ B. (∑σ ∈ S. a σ * σ v) = 0"
and z: "z ∈ K"
shows "(∑σ ∈ S. a σ * σ z) = 0"
proof -
have finB: "finite B" and BK: "B ⊆ K" using basis by (auto simp: T.vs.basis_def)
have "T.vs.spanning B" using basis by (rule T.vs.basis_spanning)
then obtain c where cE: "c ∈ B →⇩E E" and zeq: "z = T.vs.lincomb c B"
using z by (auto simp: T.vs.spanning_def)
have cEv: "⋀v. v ∈ B ⟹ c v ∈ E" using cE by auto
have zsum: "z = (∑v ∈ B. c v * v)"
using zeq cE T.vs_lincomb_eq_sum[OF finB BK] by auto
have "(∑σ ∈ S. a σ * σ z) = (∑σ ∈ S. a σ * (∑v ∈ B. c v * σ v))"
using SG finB BK cEv by (simp add: zsum field_auto_lincomb subset_iff)
also have "… = (∑σ ∈ S. ∑v ∈ B. c v * (a σ * σ v))"
by (simp add: sum_distrib_left mult.commute mult.left_commute)
also have "… = (∑v ∈ B. c v * (∑σ ∈ S. a σ * σ v))"
using sum.swap by (simp add: sum_distrib_left)
also have "… = 0" using rel by simp
finally show ?thesis .
qed
text ‹∗‹The reverse bound.› With a basis of size @{term "card B"}, there cannot be more than
@{term "card B"} distinct automorphisms of @{term K} fixing @{term E}.›
theorem galois_group_card_le:
assumes basis: "T.vs.basis B"
and finS: "finite S" and SG: "S ⊆ field_auto K E"
shows "card S ≤ card B"
proof (rule ccontr)
assume non: "¬ card S ≤ card B"
have finB: "finite B" and BK: "B ⊆ K" using basis by (auto simp: T.vs.basis_def)
have entries: "∀v ∈ B. ∀σ ∈ S. σ v ∈ K"
using SG BK by (blast intro: field_auto_closed)
have "∃a. (∀σ. a σ ∈ K) ∧ (∃σ ∈ S. a σ ≠ 0) ∧ (∀v ∈ B. (∑σ ∈ S. σ v * a σ) = 0)"
using Subfield.underdetermined_solution[OF K, where A = "λv σ. σ v" and I = B and J = S]
using entries finB finS non by force
then obtain a where anz: "∃σ ∈ S. a σ ≠ 0" and arel: "∀v ∈ B. (∑σ ∈ S. σ v * a σ) = 0"
by fastforce
have arel': "∀v ∈ B. (∑σ ∈ S. a σ * σ v) = 0"
using arel by (simp add: mult.commute)
have "⋀z. z ∈ K ⟹ (∑σ ∈ S. a σ * σ z) = 0"
by (rule character_relation_from_basis[OF finS SG basis arel'])
then show False using anz
using dedekind_independence[OF K, of S] finS SG by blast
qed
end
subsection ‹Artin's theorem›
text ‹The two bounds now meet. Let @{term H} be a finite group of automorphisms of @{term K}.
The uniform bound first extracts a basis @{term B} of @{term K} over @{term "fixed_field K H"}; write
‹G = field_auto K (fixed_field K H)› for the Galois group of the fixed field.
▪ @{thm [source] artin_dimension_le} gives @{term "card B ≤ card H"}: were there more basis
vectors than automorphisms, Artin's bound would make them dependent;
▪ @{thm [source] galois_group_card_le} gives @{term "card G ≤ card B"}: were there more
automorphisms than basis vectors, Dedekind's lemma would be contradicted;
▪ @{thm [source] galois_extension.le_galois_group_fixed_field} --- the unit of the adjunction, and
the one part needing no hypotheses --- gives @{term "H ⊆ G"}.
Chaining the first two bounds gives @{term "card G ≤ card H"}, and an inclusion between finite sets
of equal cardinality is an equality. So the kernel operator of the Galois correspondence is the
identity on finite subgroups: ∗‹every› automorphism fixing the fixed field of @{term H} already
belongs to @{term H}.
This is the converse half of the correspondence, and the hypothesis that does the work is
∗‹finiteness of @{term H}›; no basis, separability, or normality is assumed by the public theorem.›
text ‹Again a context, for the same reason as before: the locally extracted ‹basis› is a
@{locale Vector_Space} constant and can only be written qualified where an interpretation of the tower
is in scope. Here the tower is the one built from @{term H} itself.›
context
fixes K F :: "'a :: field set" and H :: "('a ⇒ 'a) set"
assumes K: "Subfield K" and Fsub: "Subfield F" and FK: "F ⊆ K"
and Hsub: "H ∈ galois_subgroups K F"
begin
lemma HG: "H ⊆ field_auto K F" using Hsub by (rule galois_subgroups_subset)
interpretation T: subfield_tower "fixed_field K H" K
by (rule fixed_field_tower[OF K HG])
theorem artin_fixed_field_degree_data:
assumes finH: "finite H"
shows "∃B. T.vs.basis B ∧ card B = card H ∧
finite (field_auto K (fixed_field K H)) ∧
card (field_auto K (fixed_field K H)) = card H"
proof -
interpret GE: galois_extension K F
by (rule galois_extension.intro[OF K Fsub FK])
have tower: "subfield_tower (fixed_field K H) K" by (rule fixed_field_tower[OF K HG])
have indep_bound: "⋀A. T.vs.lin_indep A ⟹ card A ≤ card H"
using Hsub K T.vs.lin_indep_def finH by (metis artin_bound linorder_not_less)
obtain B where basis: "T.vs.basis B"
using T.vs.basis_exists_of_independent_card_bound[where n = "card H"] indep_bound by blast
have le1: "card B ≤ card H"
by (rule artin_dimension_le[OF K Hsub finH basis])
have finG: "finite (field_auto K (fixed_field K H))"
using galois_group_card_le[OF K tower basis] infinite_arbitrarily_large
by (meson finite_if_finite_subsets_card_bdd)
have le2: "card (field_auto K (fixed_field K H)) ≤ card B"
by (rule galois_group_card_le[OF K tower basis finG subset_refl])
have card_le: "card (field_auto K (fixed_field K H)) ≤ card H" using le1 le2 by simp
have card_ge: "card H ≤ card (field_auto K (fixed_field K H))"
by (simp add: GE.le_galois_group_fixed_field Hsub card_mono finG)
have cardG: "card (field_auto K (fixed_field K H)) = card H"
using card_le card_ge by simp
have cardB: "card B = card H" using le1 le2 card_ge by simp
show ?thesis using basis cardB finG cardG by blast
qed
theorem artin_theorem:
assumes finH: "finite H"
shows "field_auto K (fixed_field K H) = H"
proof -
obtain B where basis: "T.vs.basis B" and cardB: "card B = card H"
and finG: "finite (field_auto K (fixed_field K H))"
and cardG: "card (field_auto K (fixed_field K H)) = card H"
using artin_fixed_field_degree_data[OF finH] by blast
interpret GE: galois_extension K F
by (rule galois_extension.intro[OF K Fsub FK])
show ?thesis
using GE.le_galois_group_fixed_field Hsub cardG finG by (metis card_subset_eq)
qed
end
text ‹With @{thm [source] artin_theorem} the kernel operator of the Galois
correspondence is the identity on finite subgroups. Together with the semi-inverse laws already in
‹Galois_Correspondence›, the correspondence restricts to a ∗‹bijection› between the finite subgroups
of the Galois group and those intermediate fields that arise as fixed fields.
The classical finite correspondence is assembled downstream in
‹Galois_Finite_Correspondence›. There separability and normality show that
every intermediate field is recovered from its relative automorphism group, while this theorem
supplies the inverse law for every subgroup.›
end