Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Function_Division.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Finite_Extensions.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Finite_Extensions
  imports Embedded_Algebras Polynomials Polynomial_Divisibility

begin

section \<open>Finite Extensions\<close>

subsection \<open>Definitions\<close>

definition (in ring) transcendental :: "'a set \ 'a \ bool"
  where "transcendental K x \ inj_on (\p. eval p x) (carrier (K[X]))"

abbreviation (in ring) algebraic :: "'a set \ 'a \ bool"
  where "algebraic K x \ \ transcendental K x"

definition (in ring) Irr :: "'a set \ 'a \ 'a list"
  where "Irr K x = (THE p. p \ carrier (K[X]) \ pirreducible K p \ eval p x = \ \ lead_coeff p = \)"

inductive_set (in ring) simple_extension :: "'a set \ 'a \ 'a set"
  for K and x where
    zero [simp, intro]: "\ \ simple_extension K x" |
    lin:  "\ k1 \ simple_extension K x; k2 \ K \ \ (k1 \ x) \ k2 \ simple_extension K x"

fun (in ring) finite_extension :: "'a set \ 'a list \ 'a set"
  where "finite_extension K xs = foldr (\x K'. simple_extension K' x) xs K"

subsection \<open>Basic Properties\<close>

lemma (in ring) transcendental_consistent:
  assumes "subring K R" shows "transcendental = ring.transcendental (R \ carrier := K \)"
  unfolding transcendental_def ring.transcendental_def[OF subring_is_ring[OF assms]]
            univ_poly_consistent[OF assms] eval_consistent[OF assms] ..

lemma (in ring) algebraic_consistent:
  assumes "subring K R" shows "algebraic = ring.algebraic (R \ carrier := K \)"
  unfolding over_def transcendental_consistent[OF assms] ..

lemma (in ring) eval_transcendental:
  assumes "(transcendental over K) x" "p \ carrier (K[X])" "eval p x = \" shows "p = []"
proof -
  have "[] \ carrier (K[X])" and "eval [] x = \"
    by (auto simp add: univ_poly_def)
  thus ?thesis
    using assms unfolding over_def transcendental_def inj_on_def by auto
qed

lemma (in ring) transcendental_imp_trivial_ker:
  shows "(transcendental over K) x \ a_kernel (K[X]) R (\p. eval p x) = { [] }"
  using eval_transcendental unfolding a_kernel_def' by (auto simp add: univ_poly_def)

lemma (in ring) non_trivial_ker_imp_algebraic:
  shows "a_kernel (K[X]) R (\p. eval p x) \ { [] } \ (algebraic over K) x"
  using transcendental_imp_trivial_ker unfolding over_def by auto

lemma (in domain) trivial_ker_imp_transcendental:
  assumes "subring K R" and "x \ carrier R"
  shows "a_kernel (K[X]) R (\p. eval p x) = { [] } \ (transcendental over K) x"
  using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]]
  unfolding transcendental_def over_def by (simp add: univ_poly_zero)

lemma (in domain) algebraic_imp_non_trivial_ker:
  assumes "subring K R" and "x \ carrier R"
  shows "(algebraic over K) x \ a_kernel (K[X]) R (\p. eval p x) \ { [] }"
  using trivial_ker_imp_transcendental[OF assms] unfolding over_def by auto

lemma (in domain) algebraicE:
  assumes "subring K R" and "x \ carrier R" "(algebraic over K) x"
  obtains p where "p \ carrier (K[X])" "p \ []" "eval p x = \"
proof -
  have "[] \ a_kernel (K[X]) R (\p. eval p x)"
    unfolding a_kernel_def' univ_poly_def by auto
  then obtain p where "p \ carrier (K[X])" "p \ []" "eval p x = \"
    using algebraic_imp_non_trivial_ker[OF assms] unfolding a_kernel_def' by blast
  thus thesis using that by auto
qed

lemma (in ring) algebraicI:
  assumes "p \ carrier (K[X])" "p \ []" and "eval p x = \" shows "(algebraic over K) x"
  using assms non_trivial_ker_imp_algebraic unfolding a_kernel_def' by auto

lemma (in ring) transcendental_mono:
  assumes "K \ K'" "(transcendental over K') x" shows "(transcendental over K) x"
proof -
  have "carrier (K[X]) \ carrier (K'[X])"
    using assms(1) unfolding univ_poly_def polynomial_def by auto
  thus ?thesis
    using assms unfolding over_def transcendental_def by (metis inj_on_subset)
qed

corollary (in ring) algebraic_mono:
  assumes "K \ K'" "(algebraic over K) x" shows "(algebraic over K') x"
  using transcendental_mono[OF assms(1)] assms(2) unfolding over_def by blast

lemma (in domain) zero_is_algebraic:
  assumes "subring K R" shows "(algebraic over K) \"
  using algebraicI[OF var_closed(1)[OF assms]] unfolding var_def by auto

lemma (in domain) algebraic_self:
  assumes "subring K R" and "k \ K" shows "(algebraic over K) k"
proof (rule algebraicI[of "[ \, \ k ]"])
  show "[ \, \ k ] \ carrier (K [X])" and "[ \, \ k ] \ []"
    using subringE(2-3,5)[OF assms(1)] assms(2) unfolding univ_poly_def polynomial_def by auto
  have "k \ carrier R"
    using subringE(1)[OF assms(1)] assms(2) by auto
  thus "eval [ \, \ k ] k = \"
    by (auto, algebra)
qed

lemma (in domain) ker_diff_carrier:
  assumes "subring K R"
  shows "a_kernel (K[X]) R (\p. eval p x) \ carrier (K[X])"
proof -
  have "eval [ \ ] x \ \" and "[ \ ] \ carrier (K[X])"
    using subringE(3)[OF assms] unfolding univ_poly_def polynomial_def by auto
  thus ?thesis
    unfolding a_kernel_def' by blast
qed

subsection \<open>Minimal Polynomial\<close>

lemma (in domain) minimal_polynomial_is_unique:
  assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x"
  shows "\!p \ carrier (K[X]). pirreducible K p \ eval p x = \ \ lead_coeff p = \"
    (is "\!p. ?minimal_poly p")
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  let ?ker_gen = "\p. p \ carrier (K[X]) \ pirreducible K p \ lead_coeff p = \ \
                    a_kernel (K[X]) R (\<lambda>p. eval p x) = PIdl\<^bsub>K[X]\<^esub> p"

  obtain p where p: "?ker_gen p" and unique: "\q. ?ker_gen q \ q = p"
    using exists_unique_pirreducible_gen[OF assms(1) eval_ring_hom[OF _ assms(2)]
          algebraic_imp_non_trivial_ker[OF _ assms(2-3)]
          ker_diff_carrier] subfieldE(1)[OF assms(1)] by auto
  hence "?minimal_poly p"
    using UP.cgenideal_self p unfolding a_kernel_def' by auto
  moreover have "\q. ?minimal_poly q \ q = p"
  proof -
    fix q assume q: "?minimal_poly q"
    then have "q \ PIdl\<^bsub>K[X]\<^esub> p"
      using p unfolding a_kernel_def' by auto
    hence "p \\<^bsub>K[X]\<^esub> q"
      using cgenideal_pirreducible[OF assms(1)] p q by simp
    hence "a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> q"
      using UP.associated_iff_same_ideal q p by simp
    thus "q = p"
      using unique q by simp
  qed
  ultimately show ?thesis by blast
qed

lemma (in domain) IrrE:
  assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x"
  shows "Irr K x \ carrier (K[X])" and "pirreducible K (Irr K x)"
    and "lead_coeff (Irr K x) = \" and "eval (Irr K x) x = \"
  using theI'[OF minimal_polynomial_is_unique[OF assms]] unfolding Irr_def by auto

lemma (in domain) Irr_generates_ker:
  assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x"
  shows "a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> (Irr K x)"
proof -
  obtain q
    where q: "q \ carrier (K[X])" "pirreducible K q"
      and ker: "a_kernel (K[X]) R (\p. eval p x) = PIdl\<^bsub>K[X]\<^esub> q"
    using exists_unique_pirreducible_gen[OF assms(1) eval_ring_hom[OF _ assms(2)]
          algebraic_imp_non_trivial_ker[OF _ assms(2-3)]
          ker_diff_carrier] subfieldE(1)[OF assms(1)] by auto
  have "Irr K x \ PIdl\<^bsub>K[X]\<^esub> q"
    using IrrE(1,4)[OF assms] ker unfolding a_kernel_def' by auto
  thus ?thesis
    using cgenideal_pirreducible[OF assms(1) q(1-2) IrrE(2)[OF assms]] q(1) IrrE(1)[OF assms]
          cring.associated_iff_same_ideal[OF univ_poly_is_cring[OF subfieldE(1)[OF assms(1)]]]
    unfolding ker
    by simp
qed

lemma (in domain) Irr_minimal:
  assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x"
    and "p \ carrier (K[X])" "eval p x = \" shows "(Irr K x) pdivides p"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  have "p \ PIdl\<^bsub>K[X]\<^esub> (Irr K x)"
    using Irr_generates_ker[OF assms(1-3)] assms(4-5) unfolding a_kernel_def' by auto
  hence "(Irr K x) divides\<^bsub>K[X]\<^esub> p"
    using UP.to_contain_is_to_divide IrrE(1)[OF assms(1-3)]
    by (meson UP.cgenideal_ideal UP.cgenideal_minimal assms(4))
  thus ?thesis
    unfolding pdivides_iff_shell[OF assms(1) IrrE(1)[OF assms(1-3)] assms(4)] .
qed

lemma (in domain) rupture_of_Irr:
  assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x" shows "field (Rupt K (Irr K x))"
  using rupture_is_field_iff_pirreducible[OF assms(1)] IrrE(1-2)[OF assms] by simp

subsection \<open>Simple Extensions\<close>

lemma (in ring) simple_extension_consistent:
  assumes "subring K R" shows "ring.simple_extension (R \ carrier := K \) = simple_extension"
proof -
  interpret K: ring "R \ carrier := K \"
    using subring_is_ring[OF assms] .

  have "\K' x. K.simple_extension K' x \ simple_extension K' x"
  proof
    fix K' x a show "a \ K.simple_extension K' x \ a \ simple_extension K' x"
      by (induction rule: K.simple_extension.induct) (auto simp add: simple_extension.lin)
  qed
  moreover
  have "\K' x. simple_extension K' x \ K.simple_extension K' x"
  proof
    fix K' x a assume a: "a \ simple_extension K' x" thus "a \ K.simple_extension K' x"
      using K.simple_extension.zero K.simple_extension.lin
      by (induction rule: simple_extension.induct) (simp)+
  qed
  ultimately show ?thesis by blast
qed

lemma (in ring) mono_simple_extension:
  assumes "K \ K'" shows "simple_extension K x \ simple_extension K' x"
proof
  fix a assume "a \ simple_extension K x" thus "a \ simple_extension K' x"
  proof (induct a rule: simple_extension.induct, simp)
    case lin thus ?case using simple_extension.lin assms by blast
  qed
qed

lemma (in ring) simple_extension_incl:
  assumes "K \ carrier R" and "x \ carrier R" shows "K \ simple_extension K x"
proof
  fix k assume "k \ K" thus "k \ simple_extension K x"
    using simple_extension.lin[OF simple_extension.zero, of k K x] assms by auto
qed

lemma (in ring) simple_extension_mem:
  assumes "subring K R" and "x \ carrier R" shows "x \ simple_extension K x"
proof -
  have "\ \ simple_extension K x"
    using simple_extension_incl[OF _ assms(2)] subringE(1,3)[OF assms(1)] by auto
  thus ?thesis
    using simple_extension.lin[OF _ subringE(2)[OF assms(1)], of \<one> x] assms(2) by auto
qed

lemma (in ring) simple_extension_carrier:
  assumes "x \ carrier R" shows "simple_extension (carrier R) x = carrier R"
proof
  show "carrier R \ simple_extension (carrier R) x"
    using simple_extension_incl[OF _ assms] by auto
next
  show "simple_extension (carrier R) x \ carrier R"
  proof
    fix a assume "a \ simple_extension (carrier R) x" thus "a \ carrier R"
      by (induct a rule: simple_extension.induct) (auto simp add: assms)
  qed
qed

lemma (in ring) simple_extension_in_carrier:
  assumes "K \ carrier R" and "x \ carrier R" shows "simple_extension K x \ carrier R"
  using mono_simple_extension[OF assms(1), of x] simple_extension_carrier[OF assms(2)] by auto

lemma (in ring) simple_extension_subring_incl:
  assumes "subring K' R" and "K \ K'" "x \ K'" shows "simple_extension K x \ K'"
  using ring.simple_extension_in_carrier[OF subring_is_ring[OF assms(1)]] assms(2-3)
  unfolding simple_extension_consistent[OF assms(1)] by simp

lemma (in ring) simple_extension_as_eval_img:
  assumes "K \ carrier R" "x \ carrier R"
  shows "simple_extension K x = (\p. eval p x) ` carrier (K[X])"
proof
  show "simple_extension K x \ (\p. eval p x) ` carrier (K[X])"
  proof
    fix a assume "a \ simple_extension K x" thus "a \ (\p. eval p x) ` carrier (K[X])"
    proof (induction rule: simple_extension.induct)
      case zero
      have "polynomial K []" and "eval [] x = \"
        unfolding polynomial_def by simp+
      thus ?case
        unfolding univ_poly_carrier by force
    next
      case (lin k1 k2)
      then obtain p where p: "p \ carrier (K[X])" "polynomial K p" "eval p x = k1"
        by (auto simp add: univ_poly_carrier)
      hence "set p \ carrier R" and "k2 \ carrier R"
        using assms(1) lin(2) unfolding polynomial_def by auto
      hence "eval (normalize (p @ [ k2 ])) x = k1 \ x \ k2"
        using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto
      moreover have "set (p @ [k2]) \ K"
        using polynomial_incl[OF p(2)] \<open>k2 \<in> K\<close> by auto
      then have "local.normalize (p @ [k2]) \ carrier (K [X])"
        using normalize_gives_polynomial univ_poly_carrier by blast
      ultimately show ?case
        unfolding univ_poly_carrier by force
    qed
  qed
next
  show "(\p. eval p x) ` carrier (K[X]) \ simple_extension K x"
  proof
    fix a assume "a \ (\p. eval p x) ` carrier (K[X])"
    then obtain p where p: "set p \ K" "eval p x = a"
      using polynomial_incl unfolding univ_poly_def by auto
    thus "a \ simple_extension K x"
    proof (induct "length p" arbitrary: p a)
      case 0 thus ?case
        using simple_extension.zero by simp
    next
      case (Suc n)
      obtain p' k where p: "p = p' @ [ k ]"
        using Suc(2) by (metis list.size(3) nat.simps(3) rev_exhaust)
      hence "a = (eval p' x) \ x \ k"
        using eval_append_aux[of p' k x] Suc(3-4) assms unfolding p by auto
      moreover have "eval p' x \ simple_extension K x"
        using Suc(1-3) unfolding p by auto
      ultimately show ?case
        using simple_extension.lin Suc(3) unfolding p by auto
    qed
  qed
qed

corollary (in domain) simple_extension_is_subring:
  assumes "subring K R" "x \ carrier R" shows "subring (simple_extension K x) R"
  using ring_hom_ring.img_is_subring[OF eval_ring_hom[OF assms]
        ring.carrier_is_subring[OF univ_poly_is_ring[OF assms(1)]]]
        simple_extension_as_eval_img[OF subringE(1)[OF assms(1)] assms(2)]
  by simp

corollary (in domain) simple_extension_minimal:
  assumes "subring K R" "x \ carrier R"
  shows "simple_extension K x = \ { K'. subring K' R \ K \ K' \ x \ K' }"
  using simple_extension_is_subring[OF assms] simple_extension_mem[OF assms]
        simple_extension_incl[OF subringE(1)[OF assms(1)] assms(2)] simple_extension_subring_incl
  by blast

corollary (in domain) simple_extension_isomorphism:
  assumes "subring K R" "x \ carrier R"
  shows "(K[X]) Quot (a_kernel (K[X]) R (\p. eval p x)) \ R \ carrier := simple_extension K x \"
  using ring_hom_ring.FactRing_iso_set_aux[OF eval_ring_hom[OF assms]]
        simple_extension_as_eval_img[OF subringE(1)[OF assms(1)] assms(2)]
  unfolding is_ring_iso_def by auto

corollary (in domain) simple_extension_of_algebraic:
  assumes "subfield K R" and "x \ carrier R" "(algebraic over K) x"
  shows "Rupt K (Irr K x) \ R \ carrier := simple_extension K x \"
  using simple_extension_isomorphism[OF subfieldE(1)[OF assms(1)] assms(2)]
  unfolding Irr_generates_ker[OF assms] rupture_def by simp

corollary (in domain) simple_extension_of_transcendental:
  assumes "subring K R" and "x \ carrier R" "(transcendental over K) x"
  shows "K[X] \ R \ carrier := simple_extension K x \"
  using simple_extension_isomorphism[OF _ assms(2), of K] assms(1)
        ring_iso_trans[OF ring.FactRing_zeroideal(2)[OF univ_poly_is_ring]]
  unfolding transcendental_imp_trivial_ker[OF assms(3)] univ_poly_zero
  by auto

proposition (in domain) simple_extension_subfield_imp_algebraic:
  assumes "subring K R" "x \ carrier R"
  shows "subfield (simple_extension K x) R \ (algebraic over K) x"
proof -
  assume simple_ext: "subfield (simple_extension K x) R" show "(algebraic over K) x"
  proof (rule ccontr)
    assume "\ (algebraic over K) x" then have "(transcendental over K) x"
      unfolding over_def by simp
    then obtain h where h: "h \ ring_iso (R \ carrier := simple_extension K x \) (K[X])"
      using ring_iso_sym[OF univ_poly_is_ring simple_extension_of_transcendental] assms
      unfolding is_ring_iso_def by blast
    then interpret Hom: ring_hom_ring "R \ carrier := simple_extension K x \" "K[X]" h
      using subring_is_ring[OF simple_extension_is_subring[OF assms]]
            univ_poly_is_ring[OF assms(1)] assms h
      by (auto simp add: ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def)
    have "field (K[X])"
      using field.ring_iso_imp_img_field[OF subfield_iff(2)[OF simple_ext] h]
      unfolding Hom.hom_one Hom.hom_zero by simp
    moreover have "\ field (K[X])"
      using univ_poly_not_field[OF assms(1)] .
    ultimately show False by simp
  qed
qed

proposition (in domain) simple_extension_is_subfield:
  assumes "subfield K R" "x \ carrier R"
  shows "subfield (simple_extension K x) R \ (algebraic over K) x"
proof
  assume alg: "(algebraic over K) x"
  then obtain h where h: "h \ ring_iso (Rupt K (Irr K x)) (R \ carrier := simple_extension K x \)"
    using simple_extension_of_algebraic[OF assms] unfolding is_ring_iso_def by blast
  have rupt_field: "field (Rupt K (Irr K x))" and "ring (R \ carrier := simple_extension K x \)"
    using subring_is_ring[OF simple_extension_is_subring[OF subfieldE(1)]]
          rupture_of_Irr[OF assms alg] assms by simp+
  then interpret Hom: ring_hom_ring "Rupt K (Irr K x)" "R \ carrier := simple_extension K x \" h
    using h cring.axioms(1)[OF domain.axioms(1)[OF field.axioms(1)]]
    by (auto simp add: ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def)
  show "subfield (simple_extension K x) R"
    using field.ring_iso_imp_img_field[OF rupt_field h] subfield_iff(1)[OF _
          simple_extension_in_carrier[OF subfieldE(3)[OF assms(1)] assms(2)]]
    by simp
next
  assume simple_ext: "subfield (simple_extension K x) R" thus "(algebraic over K) x"
    using simple_extension_subfield_imp_algebraic[OF subfieldE(1)[OF assms(1)] assms(2)] by simp
qed

subsection \<open>Link between dimension of K-algebras and algebraic extensions\<close>

lemma (in domain) exp_base_independent:
  assumes "subfield K R" "x \ carrier R" "(algebraic over K) x"
  shows "independent K (exp_base x (degree (Irr K x)))"
proof -
  have "\n. n \ degree (Irr K x) \ independent K (exp_base x n)"
  proof -
    fix n show "n \ degree (Irr K x) \ independent K (exp_base x n)"
    proof (induct n, simp add: exp_base_def)
      case (Suc n)
      have "x [^] n \ Span K (exp_base x n)"
      proof (rule ccontr)
        assume "\ x [^] n \ Span K (exp_base x n)"
        then obtain a Ks
          where Ks: "a \ K - { \ }" "set Ks \ K" "length Ks = n" "combine (a # Ks) (exp_base x (Suc n)) = \"
          using Span_mem_imp_non_trivial_combine[OF assms(1) exp_base_closed[OF assms(2), of n]]
          by (auto simp add: exp_base_def)
        hence "eval (a # Ks) x = \"
          using combine_eq_eval by (auto simp add: exp_base_def)
        moreover have "(a # Ks) \ carrier (K[X]) - { [] }"
          unfolding univ_poly_def polynomial_def using Ks(1-2) by auto
        ultimately have "degree (Irr K x) \ n"
          using pdivides_imp_degree_le[OF subfieldE(1)[OF assms(1)]
                IrrE(1)[OF assms] _ _  Irr_minimal[OF assms, of "a # Ks"]] Ks(3) by auto
        from \<open>Suc n \<le> degree (Irr K x)\<close> and this show False by simp
      qed
      thus ?case
        using independent.li_Cons assms(2) Suc by (auto simp add: exp_base_def)
    qed
  qed
  thus ?thesis
    by simp
qed

lemma (in ring) Span_eq_eval_img:
  assumes "subfield K R" "x \ carrier R"
  shows "Span K (exp_base x n) = (\p. eval p x) ` { p \ carrier (K[X]). length p \ n }"
    (is "?Span = ?eval_img")
proof
  show "?Span \ ?eval_img"
  proof
    fix u assume "u \ Span K (exp_base x n)"
    then obtain Ks where Ks: "set Ks \ K" "length Ks = n" "u = combine Ks (exp_base x n)"
      using Span_eq_combine_set_length_version[OF assms(1) exp_base_closed[OF assms(2)]]
      by (auto simp add: exp_base_def)
    hence "u = eval (normalize Ks) x"
      using combine_eq_eval eval_normalize[OF _ assms(2)] subfieldE(3)[OF assms(1)] by auto
    moreover have "normalize Ks \ carrier (K[X])"
      using normalize_gives_polynomial[OF Ks(1)] unfolding univ_poly_def by auto
    moreover have "length (normalize Ks) \ n"
      using normalize_length_le[of Ks] Ks(2) by auto
    ultimately show "u \ ?eval_img" by auto
  qed
next
  show "?eval_img \ ?Span"
  proof
    fix u assume "u \ ?eval_img"
    then obtain p where p: "p \ carrier (K[X])" "length p \ n" "u = eval p x"
      by blast
    hence "combine p (exp_base x (length p)) = u"
      using combine_eq_eval by auto
    moreover have set_p: "set p \ K"
      using polynomial_incl[of K p] p(1) unfolding univ_poly_carrier by auto
    hence "set p \ carrier R"
      using subfieldE(3)[OF assms(1)] by auto
    moreover have "drop (n - length p) (exp_base x n) = exp_base x (length p)"
      using p(2) drop_exp_base by auto
    ultimately have "combine ((replicate (n - length p) \) @ p) (exp_base x n) = u"
      using combine_prepend_replicate[OF _ exp_base_closed[OF assms(2), of n]] by auto
    moreover have "set ((replicate (n - length p) \) @ p) \ K"
      using subringE(2)[OF subfieldE(1)[OF assms(1)]] set_p by auto
    ultimately show "u \ ?Span"
      using Span_eq_combine_set[OF assms(1) exp_base_closed[OF assms(2), of n]] by blast
  qed
qed

lemma (in domain) Span_exp_base:
  assumes "subfield K R" "x \ carrier R" "(algebraic over K) x"
  shows "Span K (exp_base x (degree (Irr K x))) = simple_extension K x"
  unfolding simple_extension_as_eval_img[OF subfieldE(3)[OF assms(1)] assms(2)]
            Span_eq_eval_img[OF assms(1-2)]
proof (auto)
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .
  note hom_simps = ring_hom_memE[OF eval_is_hom[OF subfieldE(1)[OF assms(1)] assms(2)]]

  fix p assume p: "p \ carrier (K[X])"
  have Irr: "Irr K x \ carrier (K[X])" "Irr K x \ []"
    using IrrE(1-2)[OF assms] unfolding ring_irreducible_def univ_poly_zero by auto
  then obtain q r
    where q: "q \ carrier (K[X])" and r: "r \ carrier (K[X])"
      and dvd: "p = Irr K x \\<^bsub>K [X]\<^esub> q \\<^bsub>K [X]\<^esub> r" "r = [] \ degree r < degree (Irr K x)"
    using subfield_long_division_theorem_shell[OF assms(1) p Irr(1)] unfolding univ_poly_zero by auto
  hence "eval p x = (eval (Irr K x) x) \ (eval q x) \ (eval r x)"
    using hom_simps(2-3) Irr(1) by simp
  hence "eval p x = eval r x"
    using hom_simps(1) q r unfolding IrrE(4)[OF assms] by simp
  moreover have "length r < length (Irr K x)"
    using dvd(2) Irr(2) by auto
  ultimately
  show "eval p x \ (\p. local.eval p x) ` { p \ carrier (K [X]). length p \ length (Irr K x) - Suc 0 }"
    using r by auto
qed

corollary (in domain) dimension_simple_extension:
  assumes "subfield K R" "x \ carrier R" "(algebraic over K) x"
  shows "dimension (degree (Irr K x)) K (simple_extension K x)"
  using dimension_independent[OF exp_base_independent[OF assms]] Span_exp_base[OF assms]
  by (simp add: exp_base_def)

lemma (in ring) finite_dimension_imp_algebraic:
  assumes "subfield K R" "subring F R" and "finite_dimension K F"
  shows "x \ F \ (algebraic over K) x"
proof -
  let ?Us = "\n. map (\i. x [^] i) (rev [0..< Suc n])"

  assume x: "x \ F" then have in_carrier: "x \ carrier R"
    using subringE[OF assms(2)] by auto
  obtain n where n: "dimension n K F"
    using assms(3) by auto
  have set_Us: "set (?Us n) \ F"
    using x subringE(3,6)[OF assms(2)] by (induct n) (auto)
  hence "set (?Us n) \ carrier R"
    using subringE(1)[OF assms(2)] by auto
  moreover have "dependent K (?Us n)"
    using independent_length_le_dimension[OF assms(1) n _ set_Us] by auto
  ultimately
  obtain Ks where Ks: "length Ks = Suc n" "combine Ks (?Us n) = \" "set Ks \ K" "set Ks \ { \ }"
    using dependent_imp_non_trivial_combine[OF assms(1), of "?Us n"] by auto
  have "set Ks \ carrier R"
    using subring_props(1)[OF assms(1)] Ks(3) by auto
  hence "eval (normalize Ks) x = \"
    using combine_eq_eval[of Ks] eval_normalize[OF _ in_carrier] Ks(1-2) by (simp add: exp_base_def)
  moreover have "normalize Ks = [] \ set Ks \ { \ }"
    by (induct Ks) (auto, meson list.discI,
                    metis all_not_in_conv list.discI list.sel(3) singletonD subset_singletonD)
  hence "normalize Ks \ []"
    using Ks(1,4) by (metis list.size(3) nat.distinct(1) set_empty subset_singleton_iff)
  moreover have "normalize Ks \ carrier (K[X])"
    using normalize_gives_polynomial[OF Ks(3)] unfolding univ_poly_def by auto
  ultimately show ?thesis
    using algebraicI by auto
qed

corollary (in domain) simple_extension_dim:
  assumes "subfield K R" "x \ carrier R" "(algebraic over K) x"
  shows "(dim over K) (simple_extension K x) = degree (Irr K x)"
  using dimI[OF assms(1) dimension_simple_extension[OF assms]] .

corollary (in domain) finite_dimension_simple_extension:
  assumes "subfield K R" "x \ carrier R"
  shows "finite_dimension K (simple_extension K x) \ (algebraic over K) x"
  using finite_dimensionI[OF dimension_simple_extension[OF assms]]
        finite_dimension_imp_algebraic[OF _ simple_extension_is_subring[OF subfieldE(1)]]
        simple_extension_mem[OF subfieldE(1)] assms
  by auto

subsection \<open>Finite Extensions\<close>

lemma (in ring) finite_extension_consistent:
  assumes "subring K R" shows "ring.finite_extension (R \ carrier := K \) = finite_extension"
proof -
  have "\K' xs. ring.finite_extension (R \ carrier := K \) K' xs = finite_extension K' xs"
  proof -
    fix K' xs show "ring.finite_extension (R \ carrier := K \) K' xs = finite_extension K' xs"
      using ring.finite_extension.simps[OF subring_is_ring[OF assms]]
            simple_extension_consistent[OF assms] by (induct xs) (auto)
  qed
  thus ?thesis by blast
qed

lemma (in ring) mono_finite_extension:
  assumes "K \ K'" shows "finite_extension K xs \ finite_extension K' xs"
  using mono_simple_extension assms by (induct xs) (auto)

lemma (in ring) finite_extension_carrier:
  assumes "set xs \ carrier R" shows "finite_extension (carrier R) xs = carrier R"
  using assms simple_extension_carrier by (induct xs) (auto)

lemma (in ring) finite_extension_in_carrier:
  assumes "K \ carrier R" and "set xs \ carrier R" shows "finite_extension K xs \ carrier R"
  using assms simple_extension_in_carrier by (induct xs) (auto)

lemma (in ring) finite_extension_subring_incl:
  assumes "subring K' R" and "K \ K'" "set xs \ K'" shows "finite_extension K xs \ K'"
  using ring.finite_extension_in_carrier[OF subring_is_ring[OF assms(1)]] assms(2-3)
  unfolding finite_extension_consistent[OF assms(1)] by simp

lemma (in ring) finite_extension_incl_aux:
  assumes "K \ carrier R" and "x \ carrier R" "set xs \ carrier R"
  shows "finite_extension K xs \ finite_extension K (x # xs)"
  using simple_extension_incl[OF finite_extension_in_carrier[OF assms(1,3)] assms(2)] by simp

lemma (in ring) finite_extension_incl:
  assumes "K \ carrier R" and "set xs \ carrier R" shows "K \ finite_extension K xs"
  using finite_extension_incl_aux[OF assms(1)] assms(2) by (induct xs) (auto)

lemma (in ring) finite_extension_as_eval_img:
  assumes "K \ carrier R" and "x \ carrier R" "set xs \ carrier R"
  shows "finite_extension K (x # xs) = (\p. eval p x) ` carrier ((finite_extension K xs) [X])"
  using simple_extension_as_eval_img[OF finite_extension_in_carrier[OF assms(1,3)] assms(2)] by simp

lemma (in domain) finite_extension_is_subring:
  assumes "subring K R" "set xs \ carrier R" shows "subring (finite_extension K xs) R"
  using assms simple_extension_is_subring by (induct xs) (auto)

corollary (in domain) finite_extension_mem:
  assumes "subring K R" "set xs \ carrier R" shows "set xs \ finite_extension K xs"
proof -
  { fix x xs assume "x \ carrier R" "set xs \ carrier R"
    hence "x \ finite_extension K (x # xs)"
      using simple_extension_mem[OF finite_extension_is_subring[OF assms(1), of xs]] by simp }
  note aux_lemma = this
  show ?thesis
    using aux_lemma finite_extension_incl_aux[OF subringE(1)[OF assms(1)]] assms(2)
    by (induct xs) (simp, smt insert_subset list.simps(15) subset_trans)
qed

corollary (in domain) finite_extension_minimal:
  assumes "subring K R" "set xs \ carrier R"
  shows "finite_extension K xs = \ { K'. subring K' R \ K \ K' \ set xs \ K' }"
  using finite_extension_is_subring[OF assms] finite_extension_mem[OF assms]
        finite_extension_incl[OF subringE(1)[OF assms(1)] assms(2)] finite_extension_subring_incl
  by blast

corollary (in domain) finite_extension_same_set:
  assumes "subring K R" "set xs \ carrier R" "set xs = set ys"
  shows "finite_extension K xs = finite_extension K ys"
  using finite_extension_minimal[OF assms(1)] assms(2-3) by auto

text \<open>The reciprocal is also true, but it is more subtle.\<close>
proposition (in domain) finite_extension_is_subfield:
  assumes "subfield K R" "set xs \ carrier R"
  shows "(\x. x \ set xs \ (algebraic over K) x) \ subfield (finite_extension K xs) R"
  using simple_extension_is_subfield algebraic_mono assms
  by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1))

proposition (in domain) finite_extension_finite_dimension:
  assumes "subfield K R" "set xs \ carrier R"
  shows "(\x. x \ set xs \ (algebraic over K) x) \ finite_dimension K (finite_extension K xs)"
    and "finite_dimension K (finite_extension K xs) \ (\x. x \ set xs \ (algebraic over K) x)"
proof -
  show "finite_dimension K (finite_extension K xs) \ (\x. x \ set xs \ (algebraic over K) x)"
    using finite_dimension_imp_algebraic[OF assms(1)
          finite_extension_is_subring[OF subfieldE(1)[OF assms(1)] assms(2)]]
          finite_extension_mem[OF subfieldE(1)[OF assms(1)] assms(2)] by auto
next
  show "(\x. x \ set xs \ (algebraic over K) x) \ finite_dimension K (finite_extension K xs)"
    using assms(2)
  proof (induct xs, simp add: finite_dimensionI[OF dimension_one[OF assms(1)]])
    case (Cons x xs)
    hence "finite_dimension K (finite_extension K xs)"
      by auto
    moreover have "(algebraic over (finite_extension K xs)) x"
      using algebraic_mono[OF finite_extension_incl[OF subfieldE(3)[OF assms(1)]]] Cons(2-3) by auto
    moreover have "subfield (finite_extension K xs) R"
      using finite_extension_is_subfield[OF assms(1)] Cons(2-3) by auto
    ultimately show ?case
      using telescopic_base_dim(1)[OF assms(1) _ _
            finite_dimensionI[OF dimension_simple_extension, of _ x]] Cons(3) by auto
  qed
qed

corollary (in domain) finite_extesion_mem_imp_algebraic:
  assumes "subfield K R" "set xs \ carrier R" and "\x. x \ set xs \ (algebraic over K) x"
  shows "y \ finite_extension K xs \ (algebraic over K) y"
  using finite_dimension_imp_algebraic[OF assms(1)
        finite_extension_is_subring[OF subfieldE(1)[OF assms(1)] assms(2)]]
        finite_extension_finite_dimension(1)[OF assms(1-2)] assms(3) by auto

corollary (in domain) simple_extesion_mem_imp_algebraic:
  assumes "subfield K R" "x \ carrier R" "(algebraic over K) x"
  shows "y \ simple_extension K x \ (algebraic over K) y"
  using finite_extesion_mem_imp_algebraic[OF assms(1), of "[ x ]"] assms(2-3) by auto

subsection \<open>Arithmetic of algebraic numbers\<close>

text \<open>We show that the set of algebraic numbers of a field
      over a subfield K is a subfield itself.\<close>

lemma (in field) subfield_of_algebraics:
  assumes "subfield K R" shows "subfield { x \ carrier R. (algebraic over K) x } R"
proof -
  let ?set_of_algebraics = "{ x \ carrier R. (algebraic over K) x }"

  show ?thesis
  proof (rule subfieldI'[OF subringI])
    show "?set_of_algebraics \ carrier R" and "\ \ ?set_of_algebraics"
      using algebraic_self[OF _ subringE(3)] subfieldE(1)[OF assms(1)] by auto
  next
    fix x y assume x: "x \ ?set_of_algebraics" and y: "y \ ?set_of_algebraics"
    have "\ x \ simple_extension K x"
      using subringE(5)[OF simple_extension_is_subring[OF subfieldE(1)]]
            simple_extension_mem[OF subfieldE(1)] assms(1) x by auto
    thus "\ x \ ?set_of_algebraics"
      using simple_extesion_mem_imp_algebraic[OF assms] x by auto

    have "x \ y \ finite_extension K [ x, y ]" and "x \ y \ finite_extension K [ x, y ]"
      using subringE(6-7)[OF finite_extension_is_subring[OF subfieldE(1)[OF assms(1)]], of "[ x, y ]"]
            finite_extension_mem[OF subfieldE(1)[OF assms(1)], of "[ x, y ]"] x y by auto
    thus "x \ y \ ?set_of_algebraics" and "x \ y \ ?set_of_algebraics"
      using finite_extesion_mem_imp_algebraic[OF assms, of "[ x, y ]"] x y by auto
  next
    fix z assume z: "z \ ?set_of_algebraics - { \ }"
    have "inv z \ simple_extension K z"
      using subfield_m_inv(1)[of "simple_extension K z"]
            simple_extension_is_subfield[OF assms, of z]
            simple_extension_mem[OF subfieldE(1)] assms(1) z by auto
    thus "inv z \ ?set_of_algebraics"
      using simple_extesion_mem_imp_algebraic[OF assms] field_Units z by auto
  qed
qed

end

¤ Dauer der Verarbeitung: 0.94 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.