Theory Iso_Extension_Tower

section ‹Iterating the Iso-Extension over a Finite Set of Algebraic Elements›

theory Iso_Extension_Tower
  imports Iso_Extension Complex_Field_Extension
begin

text ‹
  Starting from a homomorphism @{term f} defined on a subfield @{term K}, we extend it across a
  whole finite family of elements that are algebraic over @{term K}, reaching a homomorphism on
  the generated subfield @{term "generate_field (K ∪ A)"}.  Each extension step uses the
  single-element @{thm [source] field_hom_on.iso_extension}; the only external requirement is
  that the target field @{typ "'b"} contains a root for every non-constant polynomial, i.e. is
  ``closed enough''.  Over @{typ complex} this is the fundamental theorem of algebra.
›

text ‹The minimal polynomial is monic, so its image under @{term f} keeps the same degree.›
lemma (in field_hom_on) map_poly_minpoly_degree:
  assumes m: "is_minpoly K a m"
  shows "degree (map_poly f m) = degree m"
proof -
  have "lead_coeff m = 1" using m by (simp add: is_minpoly_def)
  then have "f (lead_coeff m) = 1" by simp
  then show ?thesis by (intro map_poly_degree_eq) simp
qed

text ‹A subfield is generated by itself.›
lemma (in Subfield) generate_field_self: "generate_field K = K"
proof
  show "generate_field K ⊆ K" using Subfield_axioms subset_refl by (rule generate_field_least)
  show "K ⊆ generate_field K" by (rule subset_generate_field)
qed

text ‹The single-element extension, packaged with the closed-target hypothesis discharging the
  existence of a root of the mapped minimal polynomial.›
lemma field_hom_on_extend_one:
  assumes f: "field_hom_on K f"
    and alg: "algebraic_over K a"
    and closed: "⋀q :: 'b :: field poly. 0 < degree q ⟹ ∃b. poly q b = 0"
  shows "∃g. field_hom_on (generate_field (K ∪ {a})) g ∧ (∀x∈K. g x = (f :: 'a :: field ⇒ 'b) x)"
proof -
  have sf: "Subfield K" using f by (rule field_hom_on.axioms(1))
  obtain m where m: "is_minpoly K a m" using Subfield.minpoly_exists[OF sf alg] by blast
  have "degree (map_poly f m) > 0"
    using m by (simp add: field_hom_on.map_poly_minpoly_degree[OF f] Subfield.minpoly_degree_pos[OF sf])
  then obtain b where b: "poly (map_poly f m) b = 0" using closed by blast
  obtain g where g: "field_hom_on (eval_img K a) g" "g a = b" "∀x∈K. g x = f x"
    using field_hom_on.iso_extension[OF f alg m b] by blast
  have "eval_img K a = generate_field (K ∪ {a})" using Subfield.eval_img_eq_generate_field[OF sf alg] .
  then show ?thesis using g by auto
qed

text ‹Iterating over a finite set: @{term f} extends to the subfield generated by @{term K}
  together with finitely many elements algebraic over @{term K}.›
theorem field_hom_on_extend_finite:
  assumes closed: "⋀q :: 'b :: field poly. 0 < degree q ⟹ ∃b. poly q b = 0"
    and "finite A"
    and "field_hom_on K (f :: 'a :: field ⇒ 'b)"
    and "⋀a. a ∈ A ⟹ algebraic_over K a"
  shows "∃g. field_hom_on (generate_field (K ∪ A)) g ∧ (∀x∈K. g x = f x)"
  using assms(2-4)
proof (induction A rule: finite_induct)
  case empty
  have sf: "Subfield K" using empty.prems(1) by (rule field_hom_on.axioms(1))
  have "generate_field (K ∪ {}) = K" by (simp add: Subfield.generate_field_self[OF sf])
  then show ?case using empty.prems(1) by auto
next
  case (insert a A)
  define L where "L = generate_field (K ∪ A)"
  obtain g1 where g1: "field_hom_on L g1" "∀x∈K. g1 x = f x"
    using insert.IH[OF insert.prems(1)] insert.prems(2) by (auto simp: L_def)
  have KsubL: "K ⊆ L"
    unfolding L_def using subset_generate_field by blast
  have algL: "algebraic_over L a"
    using insert.prems(2)[of a] KsubL by (auto intro: algebraic_over_mono)
  obtain g2 where g2: "field_hom_on (generate_field (L ∪ {a})) g2" "∀x∈L. g2 x = g1 x"
    using field_hom_on_extend_one[OF g1(1) algL closed] by blast
  have "generate_field (L ∪ {a}) = generate_field ({a} ∪ generate_field (K ∪ A))"
    unfolding L_def by (simp add: Un_commute)
  also have "… = generate_field ({a} ∪ (K ∪ A))"
    by (rule generate_field_Un_collapse2)
  also have "… = generate_field (K ∪ insert a A)"
    by (simp add: Un_commute Un_left_commute)
  finally have "generate_field (L ∪ {a}) = generate_field (K ∪ insert a A)" .
  moreover have "∀x∈K. g2 x = f x"
    using g2(2) g1(2) KsubL by auto
  ultimately show ?case using g2(1) by auto
qed


text ‹
  The generic field-extension development works over an arbitrary ambient @{typ "'a :: field"} via the @{locale Subfield} and
  @{locale field_hom_on} locales.  The complex-specific Galois theory of
  ‹Complex_Field_Extension› instead fixes @{typ complex} and packages automorphisms as the set
  @{const field_auto}. Now we connect the two.
›
text ‹The two subfield notions coincide on @{typ complex}.›
lemma complex_subfield_iff_subfield: "complex_subfield K ⟷ Subfield K"
proof
  assume "complex_subfield K"
  then interpret complex_subfield K .
  show "Subfield K"
    using complex_subfield_axioms complex_subfield_def Subfield.intro by fastforce
next
  assume "Subfield K"
  then interpret Subfield K .
  show "complex_subfield K"
    by unfold_locales (auto intro: add_closed uminus_closed mult_closed inverse_closed)
qed

text ‹A field homomorphism on @{term K} (in the generic sense) that maps @{term K} ∗‹onto›
  itself and fixes a base subfield @{term F} pointwise restricts to an element of the complex
  Galois group @{term "field_auto K F"}n.›
lemma field_hom_on_imp_field_auto:
  assumes hom: "field_hom_on K σ"
    and onto: "σ ` K = K"
    and fix_F: "⋀x. x ∈ F ⟹ σ x = x" and FK: "F ⊆ K"
  shows "restrict σ K ∈ field_auto K F"
proof -
  interpret S: field_hom_on K σ by (rule hom)
  have bij: "bij_betw (restrict σ K) K K"
    by (simp add: S.inj_on bij_betw_def onto)
  show ?thesis
    unfolding field_auto_mem_iff
  proof (intro conjI ballI)
    show "restrict σ K ∈ K →⇩E K"
      using onto by auto
    show "bij_betw (restrict σ K) K K" by (rule bij)
    show "⋀x. x ∈ F ⟹ restrict σ K x = x" using fix_F FK by auto
  qed (use S.hom_1 S.one_closed S.hom_add S.add_closed S.hom_mult S.mult_closed in auto)
qed

end