Theory Field_Extension

section ‹Simple Algebraic Extensions inside the Complex Numbers›

theory Field_Extension
  imports Complex_Field_Extension "HOL-Computational_Algebra.Field_as_Ring" "HOL-Computational_Algebra.Polynomial_Factorial"
begin

text ‹
  Towards the transitivity of the Galois group of a rational polynomial on its complex roots,
  we develop the base isomorphism ‹ℚ(α) ≅ ℚ(β)› for two roots ‹α, β› of the same
  irreducible polynomial.  We work concretely: rational polynomials are @{typ "rat poly"},
  evaluated at a complex point through the embedding @{term "of_rat :: rat ⇒ complex"}.

  The evaluation map @{term "evalQ a"} is a ring homomorphism @{typ "rat poly ⇒ complex"};
  its image is the subfield ‹ℚ(a)› and its kernel is the set of multiples of the minimal
  polynomial.  Since @{typ "rat poly"} is a principal ideal domain (a field-coefficient
  polynomial ring), the kernel characterization needs only B\\'ezout's identity.
›

subsection ‹Evaluation of a rational polynomial at a complex point›

definition evalQ :: "complex ⇒ rat poly ⇒ complex" where
  "evalQ a p = poly (map_poly of_rat p) a"

lemma map_poly_of_rat_add: "map_poly of_rat (p + q) = map_poly of_rat p + map_poly of_rat q"
  by (intro poly_eqI) (simp_all add: coeff_map_poly of_rat_add)

lemma map_poly_of_rat_mult: "map_poly of_rat (p * q) = map_poly of_rat p * map_poly of_rat q"
  by (intro poly_eqI) (simp_all add: coeff_map_poly of_rat_mult of_rat_sum coeff_mult)

lemma evalQ_add: "evalQ a (p + q) = evalQ a p + evalQ a q"
  by (simp add: evalQ_def map_poly_of_rat_add)

lemma evalQ_mult: "evalQ a (p * q) = evalQ a p * evalQ a q"
  by (simp add: evalQ_def map_poly_of_rat_mult)

lemma evalQ_0: "evalQ a 0 = 0" by (simp add: evalQ_def)

lemma evalQ_1: "evalQ a 1 = 1" by (simp add: evalQ_def map_poly_1')

lemma evalQ_diff: "evalQ a (p - q) = evalQ a p - evalQ a q"
  by (metis eq_diff_eq evalQ_add)

text ‹The constant rational polynomial evaluates to the embedded constant; in particular
  @{term evalQ} fixes the rationals.›
lemma evalQ_const: "evalQ a [:c:] = of_rat c"
  by (simp add: evalQ_def map_poly_pCons)


subsection ‹The kernel is generated by the minimal polynomial›

text ‹If @{term m} is irreducible (over ‹ℚ›) and both @{term m} and @{term r} vanish at
  @{term a}, then @{term m} divides @{term r}: by irreducibility @{term m} is coprime to any
  non-multiple, so B\\'ezout would force ‹0 = 1› under evaluation.›
lemma evalQ_kernel_dvd:
  assumes m_irr: "irreducible m" and ma: "evalQ a m = 0" and ra: "evalQ a r = 0"
  shows "m dvd r"
proof (rule ccontr)
  assume ndvd: "¬ m dvd r"
  have pm: "prime_elem m" using m_irr by (rule field_poly_irreducible_imp_prime)
  have "coprime m r" using pm ndvd by (meson coprimeI dvd_trans prime_elemD2)
  then have g1: "gcd m r = 1" by simp
  obtain u v where "u * m + v * r = gcd m r"
    using bezout_coefficients_fst_snd[of m r] by blast
  with g1 have bz: "u * m + v * r = 1" by simp
  have "evalQ a u * evalQ a m + evalQ a v * evalQ a r = evalQ a 1"
    using bz by (metis evalQ_add evalQ_mult)
  then have "(0::complex) = 1" using ma ra by (simp add: evalQ_1)
  then show False by simp
qed

text ‹Consequently two roots of the same irreducible polynomial annihilate exactly the same
  rational polynomials.›
lemma evalQ_same_kernel:
  assumes m_irr: "irreducible m" and ma: "evalQ a m = 0" and mb: "evalQ b m = 0"
    and ra: "evalQ a r = 0"
  shows "evalQ b r = 0"
proof -
  have "m dvd r" using m_irr ma ra by (rule evalQ_kernel_dvd)
  then show ?thesis using mb
    using evalQ_mult by auto
qed


subsection ‹The simple extension ‹ℚ(a)› and the base isomorphism›

text ‹The subfield ‹ℚ(a)› is the image of the evaluation map: every element is a rational
  polynomial expression in @{term a}.›
definition Qx :: "complex ⇒ complex set" where
  "Qx a = range (evalQ a)"

lemma Qx_mem_evalQ [intro]: "evalQ a p ∈ Qx a"
  by (simp add: Qx_def)

lemma Qx_self: "a ∈ Qx a"
proof -
  have "evalQ a [:0, 1:] = a" by (simp add: evalQ_def map_poly_pCons)
  then show ?thesis by (metis Qx_mem_evalQ)
qed

lemma Qx_Rats: "of_rat c ∈ Qx a"
  using evalQ_const by (metis Qx_mem_evalQ)

text ‹For two roots @{term a}, @{term b} of the same irreducible polynomial @{term m}, the map
  sending @{term "evalQ a p"} to @{term "evalQ b p"} is well defined (independent of the
  representing polynomial @{term p}), by @{thm [source] evalQ_same_kernel}.›
definition simple_iso :: "rat poly ⇒ complex ⇒ complex ⇒ complex ⇒ complex" where
  "simple_iso m a b y = evalQ b (SOME p. evalQ a p = y)"

context
  fixes m :: "rat poly" and a b :: complex
  assumes m_irr: "irreducible m" and ma: "evalQ a m = 0" and mb: "evalQ b m = 0"
begin

text ‹Well-definedness: on the image, @{term simple_iso} agrees with ‹evalQ b›.›
lemma simple_iso_evalQ: "simple_iso m a b (evalQ a p) = evalQ b p"
proof -
  let ?q = "SOME q. evalQ a q = evalQ a p"
  have "evalQ a ?q = evalQ a p" by (rule someI[of "λq. evalQ a q = evalQ a p"]) rule
  then have "evalQ a (?q - p) = 0" by (simp add: evalQ_diff)
  then have "evalQ b (?q - p) = 0" by (rule evalQ_same_kernel[OF m_irr ma mb])
  then have "evalQ b ?q = evalQ b p" by (simp add: evalQ_diff)
  then show ?thesis by (simp add: simple_iso_def)
qed

lemma simple_iso_add:
  "⟦ x ∈ Qx a; y ∈ Qx a ⟧ ⟹ simple_iso m a b (x + y) = simple_iso m a b x + simple_iso m a b y"
  by (clarsimp simp: Qx_def) (metis simple_iso_evalQ evalQ_add)

lemma simple_iso_mult:
  "⟦ x ∈ Qx a; y ∈ Qx a ⟧ ⟹ simple_iso m a b (x * y) = simple_iso m a b x * simple_iso m a b y"
  by (clarsimp simp: Qx_def) (metis simple_iso_evalQ evalQ_mult)

lemma simple_iso_1: "simple_iso m a b 1 = 1"
  using simple_iso_evalQ[of 1] by (simp add: evalQ_1)

lemma simple_iso_0: "simple_iso m a b 0 = 0"
  using simple_iso_evalQ[of 0] by (simp add: evalQ_0)

text ‹It fixes the rationals and sends @{term a} to @{term b}.›
lemma simple_iso_Rats: "simple_iso m a b (of_rat c) = of_rat c"
  using simple_iso_evalQ[of "[:c:]"] by (simp add: evalQ_const)

lemma simple_iso_gen: "simple_iso m a b a = b"
proof -
  have "evalQ a [:0, 1:] = a" "evalQ b [:0, 1:] = b" by (simp_all add: evalQ_def map_poly_pCons)
  then show ?thesis using simple_iso_evalQ[of "[:0, 1:]"] by simp
qed

text ‹It maps ‹ℚ(a)› onto ‹ℚ(b)›.›
lemma simple_iso_image: "simple_iso m a b ` Qx a = Qx b"
proof
  show "simple_iso m a b ` Qx a ⊆ Qx b"
    by (auto simp: Qx_def simple_iso_evalQ)
  show "Qx b ⊆ simple_iso m a b ` Qx a"
    by (metis Qx_def imageI image_subsetI simple_iso_evalQ)
qed

end

end