Theory Galois_Degree

section ‹The order of the Galois group of a finite normal separable extension›

theory Galois_Degree
  imports Galois_Action Extension_Properties Primitive_Element
begin

text ‹For a ∗‹simple normal› extension
  ‹K = F(a)› of complex fields (all conjugates of @{term a} --- the roots of its minimal
  polynomial --- already lying in @{term K}), the order of the Galois group equals the number of
  those conjugates,
  and, in characteristic ‹0› where the minimal polynomial is separable, this equals
  @{term "ext_degree F a"}.  The argument is the classical bijection @{term "λσ. σ a"} between
  @{term "field_auto K F"} and the conjugates of @{term a}: it is injective (an
  @{term F}-automorphism of @{term "F(a)"} is determined by where it sends @{term a}), lands among
  the conjugates (@{thm [source] field_auto_maps_root}), and is onto (the Galois action is transitive on
  the roots of an irreducible polynomial).

  The simple-extension calculation is the reusable core.  The final theorem combines it with the
  primitive-element theorem and the basis definition of extension degree to obtain
  ‹|Gal(K/F)| = [K:F]› for every finite normal separable extension in an algebraically closed
  ambient field.›

subsection ‹The minimal polynomial is irreducible over the base›

text ‹A minimal polynomial is irreducible over @{term F}: it is nonzero of positive degree and,
  by minimality, admits no factorisation over @{term F} into two positive-degree factors.›
lemma irreducible_over_minpoly:
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
  shows "irreducible_over F (minpoly F a)"
proof -
  have "minpoly F a ≠ 0" by (rule Subfield.minpoly_nonzero[OF sfF alg])
  moreover have "degree (minpoly F a) > 0"
    using Subfield.is_minpoly_minpoly Subfield.minpoly_degree_pos alg sfF by blast
  ultimately show ?thesis
    unfolding irreducible_over_def
    using alg sfF by (metis Subfield.is_minpoly_minpoly Subfield.minpoly_no_proper_factor)
qed

subsection ‹An ‹F›-automorphism of ‹F(a)› is determined by its value at ‹a››

text ‹Two @{term F}-automorphisms of the simple extension @{term "eval_img F a"} that agree at
  @{term a} agree everywhere.  Every element of @{term "eval_img F a"} is @{term "poly p a"} for
  some @{term "p ∈ poly_over F"}, and an @{term F}-automorphism commutes with such evaluation
  (@{thm [source] field_hom_on.poly_map_poly_hom}, together with @{thm [source] map_poly_fix} since
  the coefficients lie in @{term F}); so the common value at @{term a} fixes the value everywhere.›
lemma field_auto_determined_by_gen:
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
    and s: "σ ∈ field_auto (eval_img F a) F" and t: "τ ∈ field_auto (eval_img F a) F"
    and eq: "σ a = τ a"
  shows "σ = τ"
proof -
  define E where "E ≡ eval_img F a"
  have sfE: "Subfield E" unfolding E_def by (rule Subfield.subfield_eval_img[OF sfF alg])
  have FE: "F ⊆ E" unfolding E_def using Subfield.eval_img_base[OF sfF] by blast
  have aE: "a ∈ E" unfolding E_def by (rule Subfield.eval_img_self[OF sfF])
  have homs: "field_hom_on E σ"
    using E_def field_auto_imp_field_hom_on s sfE by blast
  have homt: "field_hom_on E τ"
    using E_def field_auto_imp_field_hom_on sfE t by blast
  have fixFs: "⋀x. x ∈ F ⟹ σ x = x" using s by (auto simp: field_auto_mem_iff)
  have fixFt: "⋀x. x ∈ F ⟹ τ x = x" using t by (auto simp: field_auto_mem_iff)
  ― ‹On the shared carrier @{term E} the two maps agree, elementwise.›
  have agree: "σ x = τ x" if xE: "x ∈ E" for x
  proof -
    obtain p where p: "p ∈ poly_over F" and xp: "x = poly p a" and pE: "p ∈ poly_over E"
      using xE poly_over_mono[OF FE] by (auto simp: E_def eval_img_def)
    ― ‹@{term σ} commutes with evaluation, and fixes the (‹F›-)coefficients.›
    have "σ x = poly (map_poly σ p) (σ a)"
      using field_hom_on.poly_map_poly_hom[OF homs pE aE] by (simp add: xp)
    also have "… = poly (map_poly τ p) (τ a)"
      using eq fixFs fixFt homs homt p sfF by (metis map_poly_fix)
    also have "… = τ x"
      using field_hom_on.poly_map_poly_hom[OF homt pE aE] by (simp add: xp)
    finally show ?thesis .
  qed
  ― ‹Both maps are extensional on @{term E}, so agreeing on @{term E} makes them equal.›
  then show ?thesis
    using s t unfolding E_def field_auto_mem_iff by (meson PiE_ext)
qed

subsection ‹The order of the Galois group of a simple normal extension›

text ‹∗‹Normality› of the simple extension: all conjugates of @{term a} lie in @{term "eval_img F a"}.
  Under this hypothesis, @{term "λσ. σ a"} is a bijection from @{term "field_auto (eval_img F a) F"}
  to the conjugate set, so the group order equals the number of conjugates.›
theorem galois_simple_normal_card:
  fixes F :: "complex set" and a :: complex
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
    and normal: "{r. poly (minpoly F a) r = 0} ⊆ eval_img F a"
  shows "card (field_auto (eval_img F a) F) = card {r. poly (minpoly F a) r = 0}"
proof -
  define m where "m ≡ minpoly F a"
  define E where "E ≡ eval_img F a"
  define R where "R ≡ {r. poly m r = 0}"
  have sfE: "Subfield E" unfolding E_def by (rule Subfield.subfield_eval_img[OF sfF alg])
  have mF: "m ∈ poly_over F" unfolding m_def by (rule Subfield.minpoly_over[OF sfF alg])
  have mnz: "m ≠ 0" unfolding m_def by (rule Subfield.minpoly_nonzero[OF sfF alg])
  have mroot: "poly m a = 0" unfolding m_def by (rule Subfield.minpoly_root[OF sfF alg])
  have irr: "irreducible_over F m" unfolding m_def by (rule irreducible_over_minpoly[OF sfF alg])
  have aR: "a ∈ R" using mroot by (simp add: R_def)
  have aE: "a ∈ E" unfolding E_def by (rule Subfield.eval_img_self[OF sfF])
  have FE: "F ⊆ E" unfolding E_def using Subfield.eval_img_base[OF sfF] by blast
  have RE: "R ⊆ E" using normal by (simp add: R_def m_def E_def)
  have finR: "finite R" unfolding R_def using mnz by (rule poly_roots_finite)
  ― ‹Normality makes @{term E} the splitting field @{term "generate_field (F ∪ R)"}.›
  have E_gen: "E = generate_field (F ∪ R)"
  proof (rule antisym)
    have "F ∪ {a} ⊆ F ∪ R" using aR by blast
    then show "E ⊆ generate_field (F ∪ R)"
      unfolding E_def
      using Subfield.eval_img_eq_generate_field[OF sfF alg] by (metis generate_field_mono)
    show "generate_field (F ∪ R) ⊆ E"
      using FE RE by (intro generate_field_least[OF sfE]) auto
  qed
  ― ‹Fundamental theorem of algebra: every positive-degree complex polynomial has a root.›
  have closed: "∃b. poly q b = 0" if "0 < degree q" for q :: "complex poly"
    using that by (intro fundamental_theorem_of_algebra) (simp add: constant_degree)
  ― ‹The bijection @{term "λσ. σ a"} from the Galois group to the conjugate set.›
  have "bij_betw (λσ. σ a) (field_auto E F) R"
    unfolding bij_betw_def
  proof
    show inj: "inj_on (λσ. σ a) (field_auto E F)"
      unfolding inj_on_def
      using field_auto_determined_by_gen[OF sfF alg] by (simp add: E_def)
    show "(λσ. σ a) ` field_auto E F = R"
    proof (rule antisym)
      ― ‹Well-defined: an automorphism sends @{term a} to a conjugate.›
      show "(λσ. σ a) ` field_auto E F ⊆ R"
        using FE R_def aE field_auto_maps_root mF mroot sfE sfF by blast
      ― ‹Onto: transitivity of the Galois action on the roots of the irreducible @{term m}.›
      show "R ⊆ (λσ. σ a) ` field_auto E F"
        using galois_action_transitive[OF sfF finR mF irr _ closed aR] E_gen aR 
        by (force simp add: R_def)
    qed
  qed
  then show ?thesis
    using E_def R_def bij_betw_same_card m_def by blast
qed

subsection ‹Separability in characteristic ‹0›: the number of conjugates is the degree›

text ‹@{const poly_over} is closed under formal differentiation: the coefficients of @{term "pderiv p"}
  are integer multiples of coefficients of @{term p} (@{thm [source] coeff_pderiv}), and a subfield
  contains all @{term "of_nat n"}.›
lemma (in Subfield) poly_over_pderiv:
  assumes "p ∈ poly_over K"
  shows "pderiv p ∈ poly_over K"
    using poly_overI assms mult_closed of_nat_closed poly_over_coeff by (metis coeff_pderiv)

text ‹In characteristic @{term 0} the minimal polynomial is ∗‹separable› (squarefree): it shares no
  root with its derivative.  As @{term "pderiv m"} has smaller degree than the irreducible @{term m},
  it is not a multiple of @{term m}, so B\'ezout over @{term F} gives @{term "u * m + v * pderiv m = 1"};
  evaluating this ∗‹polynomial identity› at any root @{term r} of @{term m} yields
  @{term "poly v r * poly (pderiv m) r = 1"}, so @{term "poly (pderiv m) r ≠ 0"}.›
lemma rsquarefree_minpoly:
  fixes F :: "'a :: field_char_0 set" and a :: 'a
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
  shows "rsquarefree (minpoly F a)"
proof -
  define m where "m ≡ minpoly F a"
  have ism: "is_minpoly F a m" unfolding m_def by (rule Subfield.is_minpoly_minpoly[OF sfF alg])
  have mdeg: "degree m > 0" unfolding m_def
    by (rule Subfield.minpoly_degree_pos[OF sfF Subfield.is_minpoly_minpoly[OF sfF alg]])
  have pmF: "pderiv m ∈ poly_over F"
    using Subfield.poly_over_pderiv is_minpoly_def ism sfF by blast
  ― ‹@{term "pderiv m"} is nonzero (positive degree, char ‹0›) of degree below @{term m}.›
  have pmnz: "pderiv m ≠ 0" using mdeg by (simp add: pderiv_eq_0_iff)
  have ndvd: "¬ m dvd pderiv m"
    by (simp add: mdeg)
  ― ‹B\'ezout over @{term F}: the coefficient identity holds as polynomials.›
  obtain u v where u: "u ∈ poly_over F" and v: "v ∈ poly_over F"
    and bez: "u * m + v * pderiv m = 1"
    using Subfield.minpoly_bezout[OF sfF ism pmF ndvd] by blast
  ― ‹No root of @{term m} is a root of @{term "pderiv m"}, so @{term m} is squarefree.›
  have "¬ (poly m r = 0 ∧ poly (pderiv m) r = 0)" for r
    using bez pmnz by (metis mult_cancel_left1 poly_squarefree_decomp rsquarefree_roots)
  then show ?thesis
    using m_def rsquarefree_roots by blast
qed

text ‹Hence, over @{typ complex}, a separable minimal polynomial that splits has exactly
  @{term "degree (minpoly F a)"} distinct roots: it decomposes as a product of the distinct linear
  factors @{term "[:-z, 1:]"} (@{thm [source] complex_poly_decompose_rsquarefree}), and the degree
  of that product is the number of factors.›
lemma card_conjugates_eq_degree:
  fixes F :: "complex set" and a :: complex
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
  shows "card {r. poly (minpoly F a) r = 0} = ext_degree F a"
proof -
  define m where "m ≡ minpoly F a"
  have mnz: "m ≠ 0"
    by (simp add: Subfield.minpoly_nonzero alg m_def sfF)
  have monic: "lead_coeff m = 1"
    by (simp add: Subfield.minpoly_monic alg m_def sfF)
  have "rsquarefree m"
    by (simp add: alg m_def rsquarefree_minpoly sfF)
  ― ‹Squarefree decomposition into distinct monic linear factors.›
  then have decomp: "smult (lead_coeff m) (∏z | poly m z = 0. [:- z, 1:]) = m"
   by (intro complex_poly_decompose_rsquarefree)
  have "degree m = degree (∏z | poly m z = 0. [:- z, 1:])"
    using decomp monic by (metis smult_1_left)
  also have "… = card {z. poly m z = 0}" 
    using mnz by (simp add: poly_roots_finite degree_prod_eq_sum_degree)
  finally show ?thesis by (simp add: ext_degree_def m_def)
qed

subsection ‹The headline: order of the Galois group of a simple normal extension›

text ‹∗‹The order of the Galois group of a simple normal extension equals the extension degree.›
  Combining the bijection @{thm [source] galois_simple_normal_card} with separability
  @{thm [source] card_conjugates_eq_degree}: for a simple normal complex extension @{term "F(a)"},
  \[ \bigl|\mathrm{field\_auto}\ (F(a))\ F\bigr| = \mathrm{ext\_degree}\ F\ a = \deg(\mathrm{minpoly}\ F\ a). \]
  This is ‹|Gal(K/F)| = [K:F]› in the simple normal (separable) case.›
theorem galois_simple_normal_degree:
  fixes F :: "complex set" and a :: complex
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
    and normal: "{r. poly (minpoly F a) r = 0} ⊆ eval_img F a"
  shows "card (field_auto (eval_img F a) F) = ext_degree F a"
  using galois_simple_normal_card[OF sfF alg normal] card_conjugates_eq_degree[OF sfF alg]
  by simp

subsection ‹Generic finite normal and separable extensions›

text ‹Normality of a simple extension identifies its automorphisms with the roots of the
  minimal polynomial.  The proof is the generic root-action argument: an automorphism is determined
  by the generator, maps the generator to a root, and transitivity supplies an automorphism for each
  root.›
theorem galois_simple_normal_card_alg_closed:
  fixes F :: "'a :: alg_closed_field set" and a :: 'a
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
    and normal: "{r. poly (minpoly F a) r = 0} ⊆ eval_img F a"
  shows "card (field_auto (eval_img F a) F) = card {r. poly (minpoly F a) r = 0}"
proof -
  define m where "m ≡ minpoly F a"
  define E where "E ≡ eval_img F a"
  define R where "R ≡ {r. poly m r = 0}"
  have sfE: "Subfield E"
    unfolding E_def by (rule Subfield.subfield_eval_img[OF sfF alg])
  have mF: "m ∈ poly_over F"
    unfolding m_def by (rule Subfield.minpoly_over[OF sfF alg])
  have mroot: "poly m a = 0"
    unfolding m_def by (rule Subfield.minpoly_root[OF sfF alg])
  have irr: "irreducible_over F m"
    unfolding m_def by (rule irreducible_over_minpoly[OF sfF alg])
  have aE: "a ∈ E"
    unfolding E_def by (rule Subfield.eval_img_self[OF sfF])
  have FE: "F ⊆ E"
    unfolding E_def using Subfield.eval_img_base[OF sfF] by blast
  have RE: "R ⊆ E"
    using normal by (simp add: R_def m_def E_def)
  have finR: "finite R"
    using R_def irr irreducible_over_def poly_roots_finite by blast
  have E_gen: "E = generate_field (F ∪ R)"
  proof (rule antisym)
    show "E ⊆ generate_field (F ∪ R)"
      using Subfield.eval_img_eq_generate_field[OF sfF alg] mroot
      by (simp add: E_def R_def generate_field_mono)
    show "generate_field (F ∪ R) ⊆ E"
      using FE RE by (intro generate_field_least[OF sfE]) auto
  qed
  have action_bij: "bij_betw (λσ. σ a) (field_auto E F) R"
    unfolding bij_betw_def
  proof
    show "inj_on (λσ. σ a) (field_auto E F)"
      unfolding inj_on_def
      using field_auto_determined_by_gen[OF sfF alg] by (simp add: E_def)
    show "(λσ. σ a) ` field_auto E F = R"
    proof
      show "(λσ. σ a) ` field_auto E F ⊆ R"
        using FE R_def aE field_auto_maps_root mF mroot sfE sfF by blast
      show "R ⊆ (λσ. σ a) ` field_auto E F"
        using E_gen mroot galois_action_transitive[OF sfF finR mF irr _ alg_closed_imp_poly_has_root] 
        by (force simp: R_def)
    qed
  qed
  then show ?thesis
    using E_def R_def bij_betw_same_card m_def by blast
qed

text ‹The simple normal argument is now available over every algebraically closed field.  The
  normality hypothesis says that all roots of the minimal polynomial lie in the simple extension;
  separability supplies squarefreeness, and the generic root action supplies the matching
  automorphism count.›
theorem galois_simple_normal_separable_degree:
  fixes F :: "'a :: alg_closed_field set" and a :: 'a
  assumes sfF: "Subfield F" and alg: "algebraic_over F a"
    and normal: "{r. poly (minpoly F a) r = 0} ⊆ eval_img F a"
    and sep: "separable_extension (eval_img F a) F"
  shows "card (field_auto (eval_img F a) F) = ext_degree F a"
proof -
  have card_group_roots:
      "card (field_auto (eval_img F a) F) = card {r. poly (minpoly F a) r = 0}"
    by (rule galois_simple_normal_card_alg_closed[OF sfF alg normal])
  have sep_minpoly: "rsquarefree (minpoly F a)"
    using Subfield.eval_img_self alg sep separable_extension_def sfF by blast
  have minpoly0: "minpoly F a ≠ 0"
    by (rule Subfield.minpoly_nonzero[OF sfF alg])
  then have card_roots_degree:
      "card {r. poly (minpoly F a) r = 0} = ext_degree F a"
    by (metis sep_minpoly card_roots_eq_degree_alg_closed ext_degree_def)
  show ?thesis using card_group_roots card_roots_degree by simp
qed

text ‹
  A finite normal separable extension is simple by the primitive-element theorem.  Normality then
  puts every conjugate of the primitive element back in the target field, so the preceding simple
  theorem computes the whole automorphism group.  The basis theorem identifies the simple degree
  with the intrinsic extension degree.
›
context
  fixes F K :: "'a :: alg_closed_field set"
  assumes finite: "finite_subfield_tower F K"
begin

interpretation T: finite_subfield_tower F K by (rule finite)

theorem finite_normal_separable_field_auto:
  assumes normal: "normal_extension K F" and sep: "separable_extension K F"
  shows "finite (field_auto K F)"
proof -
  obtain a where aK: "a ∈ K" and prim: "primitive_element F K a"
    using finite_separable_extension_is_simple[OF finite sep] by blast
  have Kdef: "K = eval_img F a" by (rule primitive_elementD[OF prim])
  have alg: "algebraic_over F a" by (rule T.finite_extension_algebraic[OF aK])
  define p where "p ≡ minpoly F a"
  define R where "R ≡ {r. poly p r = 0}"
  have pF: "p ∈ poly_over F"
    unfolding p_def by (rule T.base.minpoly_over[OF alg])
  have p0: "p ≠ 0"
    unfolding p_def by (rule T.base.minpoly_nonzero[OF alg])
  have aR: "a ∈ R"
    unfolding R_def p_def using T.base.minpoly_root[OF alg] by simp
  have finR: "finite R" unfolding R_def using p0 by (rule poly_roots_finite)
  have roots_min: "poly_root_set (minpoly F a) ⊆ K"
    by (rule normal_extensionD[OF normal T.base.minpoly_over[OF alg]
      irreducible_over_minpoly[OF T.base.Subfield_axioms alg]
      aK T.base.minpoly_root[OF alg]])
  have rootsK: "R ⊆ K"
    using roots_min unfolding R_def p_def poly_root_set_def by simp
  have Kgen: "K = generate_field (F ∪ R)"
  proof (rule subset_antisym)
    have "K = generate_field (F ∪ {a})"
      using Kdef T.base.eval_img_eq_generate_field[OF alg] by simp
    also have "... ⊆ generate_field (F ∪ R)"
      by (rule generate_field_mono) (use aR in auto)
    finally show "K ⊆ generate_field (F ∪ R)" .
    show "generate_field (F ∪ R) ⊆ K"
      by (simp add: T.base_subset T.ext.Subfield_axioms generate_field_least rootsK)
  qed
  show ?thesis
    using finite_galois_group[OF T.ext.Subfield_axioms T.base.Subfield_axioms T.base_subset pF]
    using Kgen R_def finR by blast
qed

theorem finite_normal_separable_galois_degree:
  assumes normal: "normal_extension K F" and sep: "separable_extension K F"
  shows "card (field_auto K F) = T.extension_degree"
proof -
  obtain a where aK: "a ∈ K" and prim: "primitive_element F K a"
    using finite_separable_extension_is_simple[OF finite sep] by blast
  have Kdef: "K = eval_img F a" by (rule primitive_elementD[OF prim])
  have alg: "algebraic_over F a" by (rule T.finite_extension_algebraic[OF aK])
  have irr: "irreducible_over F (minpoly F a)"
    by (rule irreducible_over_minpoly[OF T.base.Subfield_axioms alg])
  have "poly (minpoly F a) a = 0"
    by (rule T.base.minpoly_root[OF alg])
  then have roots_simple: "{r. poly (minpoly F a) r = 0} ⊆ eval_img F a"
    using Kdef T.base.minpoly_over aK alg irr normal normal_extensionD poly_root_set_def
    by blast
  have card_simple: "card (field_auto (eval_img F a) F) = ext_degree F a"
    using Kdef T.base.Subfield_axioms alg galois_simple_normal_separable_degree roots_simple sep
    by blast
  show ?thesis
    using Kdef T.primitive_element_degree card_simple prim by presburger
qed

end

end