Theory Finite_Generated_Extension

section ‹Extensions generated by finitely many algebraic elements›

theory Finite_Generated_Extension
  imports Finite_Extension_Tower
begin

text ‹
  Adjoining one algebraic element to a subfield gives a finite extension --- the power basis
  ‹1, a, …, a⇧^d⇧^-⇧¹› spans it --- and finite extensions compose.  Adjoining finitely many algebraic
  elements one at a time therefore stays finite.  This is HOL-Algebra's ‹finite_extension›, and it is
  what turns a polynomial with algebraic coefficients into a polynomial over a finite extension of
  the base field, so that a dimension count can be applied to it.

  The pieces were all present: ‹power_basis_span› supplies the spanning set,
  @{thm [source] subfield_tower.finite_subfield_tower_of_finite_spanning} converts it into
  finite-dimensionality, and the chain locale composes two finite extensions.  Only the assembly was
  missing.
›

subsection ‹A subfield is a finite extension of itself›

lemma finite_subfield_tower_self:
  assumes sfK: "Subfield K"
  shows "finite_subfield_tower K K"
proof -
  interpret K: Subfield K by (rule sfK)
  interpret T: subfield_tower K K by (rule subfield_tower_refl [OF sfK])
  have span1: "K ⊆ T.vs.span {1}"
  proof
    fix x assume x: "x ∈ K"
    have "(∑y ∈ {1 :: 'a}. x * y) ∈ T.vs.span ((λy. y) ` {1})"
      by (rule T.sum_scale_in_span) (auto simp: x)
    then show "x ∈ T.vs.span {1}" by simp
  qed
  show ?thesis
    by (rule T.finite_subfield_tower_of_finite_spanning [OF _ _ span1]) auto
qed


subsection ‹A simple algebraic extension is finite›

text ‹The spanning set is the power basis, and the coefficients supplied by ‹power_basis_span› are
  fed to @{thm [source] subfield_tower.sum_scale_in_span} unchanged.›

lemma finite_subfield_tower_simple:
  assumes sfK: "Subfield K" and alg: "algebraic_over K a"
  shows "finite_subfield_tower K (eval_img K a)"
proof -
  interpret K: Subfield K by (rule sfK)
  have sfE: "Subfield (eval_img K a)" by (rule K.subfield_eval_img [OF alg])
  interpret E: Subfield "eval_img K a" by (rule sfE)
  interpret T: subfield_tower K "eval_img K a"
    by (rule subfield_tower.intro [OF sfK sfE]) (unfold_locales, use K.eval_img_base in blast)
  define d where "d = ext_degree K a"
  define B where "B = (λi. a ^ i) ` {..<d}"
  have finB: "finite B" by (simp add: B_def)
  have powE: "a ^ i ∈ eval_img K a" for i
    by (rule E.power_closed [OF K.eval_img_self])
  then have BL: "B ⊆ eval_img K a" by (auto simp: B_def)
  have "eval_img K a ⊆ T.vs.span B"
  proof
    fix y assume y: "y ∈ eval_img K a"
    obtain c where cK: "⋀i. i < d ⟹ c i ∈ K" and yc: "y = (∑i < d. c i * a ^ i)"
      using K.power_basis_span [OF alg y] by (auto simp: d_def)
    have "(∑i ∈ {..<d}. c i * a ^ i) ∈ T.vs.span ((λi. a ^ i) ` {..<d})"
      by (rule T.sum_scale_in_span) (auto simp: powE cK)
    then show "y ∈ T.vs.span B" by (simp add: yc B_def)
  qed
  then show ?thesis
    by (rule T.finite_subfield_tower_of_finite_spanning [OF finB BL])
qed


subsection ‹Finite extensions compose›

lemma finite_subfield_tower_trans:
  assumes KL: "finite_subfield_tower K L" and LM: "finite_subfield_tower L M"
  shows "finite_subfield_tower K M"
proof -
  interpret C: finite_subfield_tower_chain K L M
    by (rule finite_subfield_tower_chain.intro [OF KL LM])
  show ?thesis
  proof (rule finite_subfield_tower.intro)
    show "subfield_tower K M" by (rule C.subfield_tower_KM)
    show "finite_subfield_tower_axioms K M"
      by (rule finite_subfield_tower_axioms.intro) (use C.KMF.finite_basis in blast)
  qed
qed


subsection ‹Finitely many algebraic elements generate a finite extension›

text ‹Adjoin the elements one at a time.  Each is algebraic over the base and hence, by
  @{thm [source] algebraic_over_mono}, over every intermediate field, so the simple-extension result
  applies at each step and the composition keeps the whole tower finite.›

theorem exists_finite_subfield_tower:
  assumes sfK: "Subfield K" and finS: "finite S"
    and algS: "⋀a. a ∈ S ⟹ algebraic_over K a"
  shows "∃L. finite_subfield_tower K L ∧ K ⊆ L ∧ S ⊆ L"
  using finS algS
proof (induct S rule: finite_induct)
  case empty
  show ?case
    using finite_subfield_tower_self [OF sfK] by blast
next
  case (insert a S)
  then obtain L where L: "finite_subfield_tower K L" and KL: "K ⊆ L" and SL: "S ⊆ L"
    by auto
  interpret L: finite_subfield_tower K L by (rule L)
  have sfL: "Subfield L" by (rule L.ext.Subfield_axioms)
  have algL: "algebraic_over L a"
    by (rule algebraic_over_mono [OF insert.prems [of a] KL]) simp
  have "finite_subfield_tower L (eval_img L a)"
    by (rule finite_subfield_tower_simple [OF sfL algL])
  with L have tower: "finite_subfield_tower K (eval_img L a)"
    by (rule finite_subfield_tower_trans)
  have "L ⊆ eval_img L a" using L.ext.eval_img_base by blast
  then have "K ⊆ eval_img L a" and "insert a S ⊆ eval_img L a"
    using KL SL L.ext.eval_img_self by auto
  with tower show ?case by blast
qed


subsection ‹Coordinates over a finite extension›

text ‹A finite extension carries a finite spanning set together with a coordinate function writing
  each of its elements as an explicit combination over the base.  Stated inside the locale, where the
  two fields are parameters: a client whose base field is a described set --- an image, say --- would
  otherwise send the automatic methods hunting through that description.›

lemma (in finite_subfield_tower) exists_coordinates:
  obtains B c where "finite B" and "B ⊆ L"
    and "⋀x. x ∈ L ⟹ (∀b∈B. c x b ∈ K)"
    and "⋀x. x ∈ L ⟹ x = (∑b∈B. c x b * b)"
proof -
  obtain B where B: "vs.basis B" using finite_basis by blast
  have sp: "vs.spanning B" using B by (rule vs.basis_spanning)
  have finB: "finite B" and BL: "B ⊆ L" using sp by (auto simp: vs.spanning_def)
  have ex: "∃f. (∀b∈B. f b ∈ K) ∧ x = (∑b∈B. f b * b)" if "x ∈ L" for x
  proof -
    have "∃c ∈ B →⇩_E K. x = vs.lincomb c B"
      by (rule bspec [OF sp [unfolded vs.spanning_def, THEN conjunct2, THEN conjunct2] that])
    then obtain f where f: "f ∈ B →⇩_E K" and xf: "x = vs.lincomb f B" by blast
    have "vs.lincomb f B = (∑b∈B. f b * b)"
      by (rule vs_lincomb_eq_sum [OF finB BL]) (use f in auto)
    with xf f show ?thesis by (auto simp: PiE_iff)
  qed
  define c where "c x = (SOME f. (∀b∈B. f b ∈ K) ∧ x = (∑b∈B. f b * b))" for x
  have "(∀b∈B. c x b ∈ K) ∧ x = (∑b∈B. c x b * b)" if "x ∈ L" for x
  proof -
    have "∃f. (∀b∈B. f b ∈ K) ∧ x = (∑b∈B. f b * b)" by (rule ex [OF that])
    then show ?thesis unfolding c_def by (rule someI_ex)
  qed
  then show thesis using finB BL by (blast intro: that)
qed

end