Theory Galois_Simple_Degree

section ‹Field-side inverse and degree formulas for simple normal extensions›

theory Galois_Simple_Degree
  imports Galois_Fixed_Field Algebraic_Transitivity Galois_Degree
begin

subsection ‹Algebraicity of generated splitting fields›

text ‹The generic algebraicity closure for generated fields lives in
  ‹Algebraic_Transitivity›.  This complex-specific wrapper applies it to the
  root set of a splitting-field presentation.›

text ‹Complex splitting fields are algebraic over their base.  Their generators are the root
set of the defining nonzero polynomial, and the preceding closure result applies to that set
directly (in fact, it does not need the root set's finiteness).
›
lemma splitting_field_algebraic_extension:
  fixes F K :: "complex set" and q :: "complex poly"
  assumes split: "splitting_field F q K" and sfF: "complex_subfield F"
  shows "algebraic_extension K F"
proof (rule algebraic_extensionI)
  fix x assume xK: "x ∈ K"
  have sfF': "Subfield F"
    using sfF by (simp add: complex_subfield_iff_subfield)
  have algR: "⋀r. r ∈ poly_root_set q ⟹ algebraic_over F r"
    by (rule splitting_field_root_algebraic[OF split])
  have algK: "⋀x. x ∈ generate_field (F ∪ poly_root_set q) ⟹ algebraic_over F x"
    by (rule generated_algebraic[OF sfF' algR])
  have Kdef: "K = generate_field (F ∪ poly_root_set q)"
    using splitting_fieldD[OF split] gen_subfield_eq_generate_field by simp
  show "algebraic_over F x"
    using algK xK by (simp add: Kdef)
qed

theorem splitting_field_normal_separable:
  fixes F K :: "complex set" and q :: "complex poly"
  assumes split: "splitting_field F q K" and sfF: "complex_subfield F"
  shows "normal_extension K F ∧ separable_extension K F"
proof (intro conjI)
  show "normal_extension K F"
    by (rule splitting_field_normal[OF split sfF])
  show "separable_extension K F"
    by (rule complex_extension_separable[OF sfF])
qed

text ‹With the finite-generation bridge in place, the closure theorem no longer needs an
explicit algebraicity premise for an intermediate field of a complex splitting field.
›
theorem fixed_field_eq_of_complex_splitting_field:
  fixes F E K :: "complex set" and q :: "complex poly"
  assumes split: "splitting_field F q K"
    and sfF: "complex_subfield F"
    and E: "E ∈ inter_fields K F"
  shows "fixed_field K (field_auto K E) = E"
proof -
  have FE: "F ⊆ E"
    using E by (simp add: inter_fields_iff)
  have algKF: "algebraic_extension K F"
    by (rule splitting_field_algebraic_extension[OF split sfF])
  have algKE: "algebraic_extension K E"
  proof (rule algebraic_extensionI)
    fix x assume xK: "x ∈ K"
    have algx: "algebraic_over F x"
      by (rule algebraic_extensionD[OF algKF xK])
    show "algebraic_over E x"
      by (rule algebraic_over_mono[OF algx FE])
  qed
  show ?thesis
    by (rule fixed_field_eq_of_splitting_field[OF split E algKE])
qed

text ‹
  The simple normal case is the degree-bearing part of the field-side correspondence.  The
  existing Galois-degree theorem counts the automorphisms; this theory connects its hypotheses to
  the splitting-field presentation used by the fixed-field closure theorem.
›

lemma splitting_field_finite_galois_group:
  fixes F K :: "complex set" and q :: "complex poly"
  assumes split: "splitting_field F q K" and sfF: "complex_subfield F"
  shows "finite (field_auto K F)"
proof -
  have sfF': "Subfield F"
    using sfF by (simp add: complex_subfield_iff_subfield)
  have sfK': "Subfield K"
    using splitting_field_subfield[OF split]
    by (simp add: complex_subfield_iff_subfield)
  have FK: "F ⊆ K"
    by (rule splitting_field_base_subset[OF split])
  have qF: "q ∈ poly_over F"
    using split by (auto simp: splitting_fieldD)
  have pnz: "q ≠ 0"
    using split by (auto simp: splitting_fieldD)
  have Xdef: "poly_root_set q = {r. poly q r = 0}"
    by (simp add: poly_root_set_def)
  have XK: "poly_root_set q ⊆ K"
    by (rule splitting_field_roots_subset[OF split])
  have finX: "finite (poly_root_set q)"
    by (rule finite_poly_root_set[OF pnz])
  have Kgen: "K = gen_subfield (F ∪ poly_root_set q)"
    using split by (auto simp: splitting_fieldD gen_subfield_eq_generate_field)
  show "finite (field_auto K F)"
    by (rule finite_field_auto[OF sfK' sfF' FK qF Xdef XK finX Kgen])
qed

lemma simple_normal_splitting_field:
  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 "splitting_field F (minpoly F a) (eval_img F a)"
proof -
  define R where "R = {r. poly (minpoly F a) r = 0}"
  have sfE: "Subfield (eval_img F a)"
    by (rule Subfield.subfield_eval_img[OF sfF alg])
  have FE: "F ⊆ eval_img F a"
    using Subfield.eval_img_base[OF sfF] by blast
  have pF: "minpoly F a ∈ poly_over F"
    by (rule Subfield.minpoly_over[OF sfF alg])
  have pnz: "minpoly F a ≠ 0"
    by (rule Subfield.minpoly_nonzero[OF sfF alg])
  have mroot: "poly (minpoly F a) a = 0"
    by (rule Subfield.minpoly_root[OF sfF alg])
  have aR: "a ∈ R"
    using mroot by (simp add: R_def)
  have RE: "R ⊆ eval_img F a"
    using normal by (simp add: R_def)
  have Egen: "eval_img F a = generate_field (F ∪ R)"
  proof (rule antisym)
    have "F ∪ {a} ⊆ F ∪ R" using aR by blast
    then have "generate_field (F ∪ {a}) ⊆ generate_field (F ∪ R)"
      by (rule generate_field_mono)
    then show "eval_img F a ⊆ generate_field (F ∪ R)"
      using Subfield.eval_img_eq_generate_field[OF sfF alg] by simp
    show "generate_field (F ∪ R) ⊆ eval_img F a"
      using FE RE by (intro generate_field_least[OF sfE]) auto
  qed
  show ?thesis
    unfolding splitting_field_def
    using pF pnz Egen gen_subfield_eq_generate_field
    by (simp add: R_def poly_root_set_def)
qed

text ‹For a simple normal complex extension, the field-side inverse law and the exact order
formula can be consumed together.  The subgroup-side inverse law is deliberately not reproved
here; it is the separate Artin theorem.
›
theorem simple_normal_field_inverse_and_degree:
  fixes F :: "complex set" and a :: complex
  assumes sfF: "complex_subfield F" and alg: "algebraic_over F a"
    and normal: "{r. poly (minpoly F a) r = 0} ⊆ eval_img F a"
  shows "fixed_field (eval_img F a) (field_auto (eval_img F a) F) = F ∧
    card (field_auto (eval_img F a) F) = ext_degree F a"
proof -
  have sfF': "Subfield F"
    using sfF by (simp add: complex_subfield_iff_subfield)
  have split: "splitting_field F (minpoly F a) (eval_img F a)"
    by (rule simple_normal_splitting_field[OF sfF' alg normal])
  have FE: "F ⊆ eval_img F a"
    using Subfield.eval_img_base[OF sfF'] by blast
  have Eint: "F ∈ inter_fields (eval_img F a) F"
    by (rule base_in_inter_fields[OF sfF' FE])
  have fixed:
    "fixed_field (eval_img F a) (field_auto (eval_img F a) F) = F"
    by (rule fixed_field_eq_of_complex_splitting_field[OF split sfF Eint])
  have degree:
    "card (field_auto (eval_img F a) F) = ext_degree F a"
    by (rule galois_simple_normal_degree[OF sfF' alg normal])
  show ?thesis using fixed degree by blast
qed

end