Theory Galois_Automorphism

section ‹Generic field automorphisms and fixed fields›

theory Galois_Automorphism
  imports Group_Theory Subfield
begin

text ‹
  This theory supplies the representation-independent core of the Galois development.  A field
  automorphism is a bijective endomorphism of the ambient type whose field laws hold on a subfield
  @{term K} and which fixes a base subset @{term F}.  The definition therefore works for every
  type-class field; the complex-specific locale and conjugation lemmas remain in the
  complex-field extension theory.
›

subsection ‹Automorphisms are additive, multiplicative and fix the fixed field›

definition field_auto ::
    "'a :: field set ⇒ 'a set ⇒ ('a ⇒ 'a) set" where
  "field_auto K F =
    {σ. σ ∈ K →⇩E K ∧ bij_betw σ K K
       ∧ (∀x ∈ K. ∀y ∈ K. σ (x + y) = σ x + σ y)
       ∧ (∀x ∈ K. ∀y ∈ K. σ (x * y) = σ x * σ y)
       ∧ σ 1 = 1
       ∧ (∀x ∈ F. σ x = x)}"

lemma field_auto_mem_iff:
  "σ ∈ field_auto K F ⟷
     σ ∈ K →⇩E K ∧ bij_betw σ K K
     ∧ (∀x ∈ K. ∀y ∈ K. σ (x + y) = σ x + σ y)
     ∧ (∀x ∈ K. ∀y ∈ K. σ (x * y) = σ x * σ y)
     ∧ σ 1 = 1
     ∧ (∀x ∈ F. σ x = x)"
  by (simp add: field_auto_def)

lemma field_auto_zero:
  assumes Ksub: "Subfield K" and s: "σ ∈ field_auto K F"
  shows "σ 0 = 0"
  using Ksub s by (metis Subfield.zero_closed add_cancel_right_right field_auto_mem_iff)

lemma field_auto_one:
  "σ ∈ field_auto K F ⟹ σ 1 = 1"
  by (simp add: field_auto_def)

lemma field_auto_closed:
  assumes "σ ∈ field_auto K F" and "x ∈ K"
  shows "σ x ∈ K"
  using assms bij_betwE by (fastforce simp: field_auto_def)

lemma field_auto_add:
  assumes s: "σ ∈ field_auto K F" and x: "x ∈ K" and y: "y ∈ K"
  shows "σ (x + y) = σ x + σ y"
  using s x y by (auto simp: field_auto_def)

lemma field_auto_mult:
  assumes s: "σ ∈ field_auto K F" and x: "x ∈ K" and y: "y ∈ K"
  shows "σ (x * y) = σ x * σ y"
  using s x y by (auto simp: field_auto_def)

lemma field_auto_uminus:
  assumes "Subfield K" "σ ∈ field_auto K F" and x: "x ∈ K"
  shows "σ (-x) = -σ x"
  using assms Subfield.uminus_closed add_eq_0_iff2 field_auto_add field_auto_zero x
  by fastforce

text ‹Additivity extends to finite sums, by induction on the index set.›
lemma field_auto_sum:
  assumes K: "Subfield K" and s: "σ ∈ field_auto K F"
    and x: "⋀j. j ∈ J ⟹ x j ∈ K"
  shows "σ (∑j ∈ J. x j) = (∑j ∈ J. σ (x j))"
  using assms field_auto_zero
  by (induction J rule: infinite_finite_induct) (auto simp add: Subfield.sum_closed field_auto_add)

lemma field_auto_as_hom:
  assumes Ksub: "Subfield K" and s: "σ ∈ field_auto K F"
  shows "field_hom_on K σ"
proof -
  interpret KS: Subfield K by (rule Ksub)
  show ?thesis
  proof 
    show "σ 0 = 0"
      using Ksub field_auto_zero s by blast
    show "σ 1 = 1"
      using Ksub field_auto_one s by blast
  qed (use s in ‹auto simp: field_auto_def›)
qed

lemma field_auto_inverse_on:
  assumes Ksub: "Subfield K" and s: "σ ∈ field_auto K F" and x: "x ∈ K"
  shows "σ (inverse x) = inverse (σ x)"
  using field_auto_as_hom[OF Ksub s] x by (rule field_hom_on.hom_inverse_all)

lemma field_auto_subset_Sym:
  "field_auto K F ⊆ transformations.Sym K"
  by (auto simp: field_auto_def transformations.Units_bijective)

lemma identity_apply: "x ∈ S ⟹ identity S x = x"
  by (simp add: restrict_apply')

lemma field_auto_identity:
  assumes Ksub: "Subfield K" and FK: "F ⊆ K"
  shows "identity K ∈ field_auto K F"
proof -
  interpret KS: Subfield K by (rule Ksub)
  show ?thesis
    unfolding field_auto_mem_iff
  proof (intro conjI ballI)
    show "identity K ∈ K →⇩E K"
      by (auto simp: identity_apply PiE_iff)
    show "bij_betw (identity K) K K"
      by (simp add: bij_betw_def inj_on_def identity_apply)
    show "⋀x. x ∈ F ⟹ identity K x = x"
      using FK by (auto simp: identity_apply)
  qed (auto simp: identity_apply KS.one_closed KS.add_closed KS.mult_closed)
qed

lemma field_auto_compose:
  assumes Ksub: "Subfield K" and FK: "F ⊆ K"
    and s: "σ ∈ field_auto K F" and t: "τ ∈ field_auto K F"
  shows "compose K σ τ ∈ field_auto K F"
proof -
  interpret KS: Subfield K by (rule Ksub)
  from s have sbij: "bij_betw σ K K"
    and sext: "σ ∈ K →⇩E K"
    and sadd: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x + y) = σ x + σ y"
    and smul: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x * y) = σ x * σ y"
    and sone: "σ 1 = 1" and sfix: "⋀x. x ∈ F ⟹ σ x = x"
    by (auto simp: field_auto_def)
  from t have tbij: "bij_betw τ K K"
    and text2: "τ ∈ K →⇩E K"
    and tadd: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ τ (x + y) = τ x + τ y"
    and tmul: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ τ (x * y) = τ x * τ y"
    and tone: "τ 1 = 1" and tfix: "⋀x. x ∈ F ⟹ τ x = x"
    by (auto simp: field_auto_def)
  have tinK: "⋀x. x ∈ K ⟹ τ x ∈ K" using tbij bij_betwE by blast
  let ?c = "compose K σ τ"
  show ?thesis
    unfolding field_auto_mem_iff
  proof (intro conjI ballI)
    show "?c ∈ K →⇩E K" using sext text2 by (simp add: compose_def PiE_iff)
    show "bij_betw ?c K K" using sbij tbij by (simp add: bij_betw_compose)
    show "?c 1 = 1" using KS.one_closed by (simp add: compose_eq tone sone)
    show "⋀x y. x ∈ K ⟹ y ∈ K ⟹ ?c (x + y) = ?c x + ?c y"
      by (simp add: compose_eq KS.add_closed tinK tadd sadd)
    show "⋀x y. x ∈ K ⟹ y ∈ K ⟹ ?c (x * y) = ?c x * ?c y"
      by (simp add: compose_eq KS.mult_closed tinK tmul smul)
    show "⋀x. x ∈ F ⟹ ?c x = x"
      using FK sfix tfix by (metis compose_eq in_mono)
  qed
qed

lemma field_auto_inverse:
  assumes Ksub: "Subfield K" and s: "σ ∈ field_auto K F" and FK: "F ⊆ K"
  shows "restrict (inv_into K σ) K ∈ field_auto K F"
proof -
  interpret KS: Subfield K by (rule Ksub)
  have bij: "bij_betw σ K K"
    and addh: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x + y) = σ x + σ y"
    and mulh: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x * y) = σ x * σ y"
    and one: "σ 1 = 1" and fixed: "⋀x. x ∈ F ⟹ σ x = x"
    using s by (auto simp: field_auto_def)
  define t where "t ≡ restrict (inv_into K σ) K"
  have tin: "⋀y. y ∈ K ⟹ t y ∈ K"
    using bij by (simp add: t_def inv_into_into bij_betw_def)
  have st: "⋀y. y ∈ K ⟹ σ (t y) = y"
    using bij by (simp add: t_def f_inv_into_f bij_betw_def)
  have ts: "⋀x. x ∈ K ⟹ t (σ x) = x"
    using bij by (simp add: t_def bij_betwE inv_into_f_f bij_betw_def)
  show ?thesis
    unfolding field_auto_mem_iff
  proof (intro conjI strip)
    show "bij_betw (restrict (inv_into K σ) K) K K"
      by (simp add: bij bij_betw_inv_into)
    show "restrict (inv_into K σ) K ∈ K →⇩E K"
      by (simp add: bij bij_betw_imp_funcset bij_betw_inv_into)
    show "⋀x y. x ∈ K ⟹ y ∈ K ⟹
           restrict (inv_into K σ) K (x + y) = restrict (inv_into K σ) K x + restrict (inv_into K σ) K y"
      using KS.add_closed addh st t_def tin ts by metis
    show "⋀x y. x ∈ K ⟹ y ∈ K ⟹
           restrict (inv_into K σ) K (x * y) = restrict (inv_into K σ) K x * restrict (inv_into K σ) K y"
      using KS.mult_closed mulh st t_def tin ts by metis
    show "restrict (inv_into K σ) K 1 = 1"
      using one t_def ts by fastforce
    show "⋀x. x ∈ F ⟹ restrict (inv_into K σ) K x = x"
      using FK fixed t_def ts by (metis subsetD)
  qed
qed

context
  fixes K F :: "'a :: field set"
  assumes Ksub: "Subfield K" and FK: "F ⊆ K"
begin

interpretation T: transformations K .

lemma field_auto_restrict_inv_in_Sym:
  assumes "a ∈ T.Sym"
  shows "restrict (inv_into K a) K ∈ T.Sym"
proof -
  have "bij_betw a K K" using assms by (rule T.Units_bij_betwI)
  then show ?thesis
    by (simp add: bij_betw_imp_funcset bij_betw_inv_into)
qed

lemma field_auto_Sym_inverse_eq_inv_into:
  assumes "a ∈ T.Sym"
  shows "T.symmetric.inverse a = restrict (inv_into K a) K"
proof (intro T.symmetric.inverse_equality field_auto_restrict_inv_in_Sym assms)
  show "compose K a (restrict (inv_into K a) K) = identity K"
    by (simp add: assms bij_betw_imp_surj_on compose_id_inv_into)
  show "compose K (restrict (inv_into K a) K) a = identity K"
    by (simp add: assms compose_inv_into_id)
qed

theorem field_auto_subgroup:
  "Subgroup (field_auto K F) (transformations.Sym K) (compose K) (identity K)"
proof (intro T.symmetric.subgroupI field_auto_subset_Sym)
  show "identity K ∈ field_auto K F" using Ksub FK by (rule field_auto_identity)
next
  fix a b assume "a ∈ field_auto K F" "b ∈ field_auto K F"
  then show "compose K a b ∈ field_auto K F"
    using Ksub FK by (blast intro: field_auto_compose)
next
  fix a assume a: "a ∈ field_auto K F"
  then have aSym: "a ∈ T.Sym" using field_auto_subset_Sym by blast
  then show "T.symmetric.inverse a ∈ field_auto K F"
    by (simp add: FK Ksub field_auto_Sym_inverse_eq_inv_into a field_auto_inverse)
next
  fix g assume "g ∈ field_auto K F"
  then have "g ∈ T.Sym" using field_auto_subset_Sym by blast
  then show "T.symmetric.invertible g" by (simp add: T.mem_UnitsD)
qed

corollary field_auto_group:
  "Group (field_auto K F) (compose K) (identity K)"
  by (rule subgroup_imp_Group[OF field_auto_subgroup])

end

definition fixed_field ::
    "'a :: field set ⇒ ('a ⇒ 'a) set ⇒ 'a set" where
  "fixed_field K H ≡ {x ∈ K. ∀σ ∈ H. σ x = x}"

lemma fixed_field_subset: "fixed_field K H ⊆ K"
  by (auto simp: fixed_field_def)

lemma fixed_field_memI:
  "⟦ x ∈ K; ⋀σ. σ ∈ H ⟹ σ x = x ⟧ ⟹ x ∈ fixed_field K H"
  by (simp add: fixed_field_def)

lemma fixed_field_memD:
  "x ∈ fixed_field K H ⟹ x ∈ K ∧ (∀σ ∈ H. σ x = x)"
  by (simp add: fixed_field_def)

lemma fixed_field_antitone:
  "H ⊆ H' ⟹ fixed_field K H' ⊆ fixed_field K H"
  by (auto simp: fixed_field_def)

lemma fixed_field_empty: "fixed_field K {} = K"
  by (auto simp: fixed_field_def)

lemma field_auto_fixed_set_subfield:
  assumes Ksub: "Subfield K" and s: "σ ∈ field_auto K F"
  shows "Subfield {x ∈ K. σ x = x}" (is "Subfield ?KK")
proof -
  interpret KS: Subfield K by (rule Ksub)
  have add: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x + y) = σ x + σ y"
    and mul: "⋀x y. x ∈ K ⟹ y ∈ K ⟹ σ (x * y) = σ x * σ y"
    and one: "σ 1 = 1"
    using s by (auto simp: field_auto_def)
  have zero: "σ 0 = 0"
    by (rule field_auto_zero[OF Ksub s])
  show ?thesis
  proof
    show "0 ∈ ?KK" using KS.zero_closed zero by simp
    show "1 ∈ ?KK" using KS.one_closed one by simp
  next
    fix x assume x: "x ∈ ?KK"
    show "-x ∈ ?KK" "inverse x ∈ ?KK"
      using x Ksub field_auto_uminus field_auto_inverse_on s by fastforce+
    fix y assume y: "y ∈ ?KK"
    show "x + y ∈ ?KK" "x * y ∈ ?KK"
      using x y by (auto simp: add mul)
  qed
qed

lemma field_auto_fixed_field_subfield:
  assumes Ksub: "Subfield K" and H: "H ⊆ field_auto K F"
  shows "Subfield (fixed_field K H)"
proof -
  interpret KS: Subfield K by (rule Ksub)
  show ?thesis
  proof
    show "0 ∈ fixed_field K H"
      using H KS.zero_closed Ksub by (meson field_auto_zero fixed_field_memI subsetD)
    show "1 ∈ fixed_field K H"
      using H KS.one_closed by (metis field_auto_mem_iff fixed_field_memI subsetD)
  next
    fix x y assume x: "x ∈ fixed_field K H" and y: "y ∈ fixed_field K H"
    have xK: "x ∈ K" using fixed_field_memD[OF x] by blast
    have yK: "y ∈ K" using fixed_field_memD[OF y] by blast
    show "x + y ∈ fixed_field K H"
    proof (rule fixed_field_memI)
      show "x + y ∈ K" by (rule KS.add_closed[OF xK yK])
      fix σ assume s: "σ ∈ H"
      then have add: "σ (x + y) = σ x + σ y"
        using H field_auto_add xK yK by blast
      show "σ (x + y) = x + y"
        using add s x y by (metis fixed_field_memD)
    qed
    show "x * y ∈ fixed_field K H"
    proof (rule fixed_field_memI)
      show "x * y ∈ K" by (rule KS.mult_closed[OF xK yK])
      fix σ assume s: "σ ∈ H"
      then have mul: "σ (x * y) = σ x * σ y"
        using H field_auto_mult xK yK by blast
      then show "σ (x * y) = x * y"
        using s x y by (metis fixed_field_memD)
    qed
  next
    fix x assume x: "x ∈ fixed_field K H"
    have xK: "x ∈ K" using fixed_field_memD[OF x] by blast
    show "-x ∈ fixed_field K H"
    proof (rule fixed_field_memI)
      show "-x ∈ K" by (rule KS.uminus_closed[OF xK])
      fix σ assume s: "σ ∈ H"
      show "σ (-x) = -x"
        using H Ksub field_auto_uminus fixed_field_memD s x by fastforce
    qed
    show "inverse x ∈ fixed_field K H"
    proof (rule fixed_field_memI)
      show "inverse x ∈ K" by (rule KS.inverse_closed[OF xK])
      fix σ assume s: "σ ∈ H"
      show "σ (inverse x) = inverse x"
        using H Ksub field_auto_inverse_on fixed_field_memD s x by fastforce
    qed
  qed
qed

lemma field_auto_base_subset_fixed_field:
  assumes H: "H ⊆ field_auto K F" and FK: "F ⊆ K"
  shows "F ⊆ fixed_field K H"
  using assms by (auto simp: fixed_field_def field_auto_def)

lemma field_auto_faithful:
  assumes gen: "K = generate_field (F ∪ X)"
    and s: "σ ∈ field_auto K F"
    and fixX: "⋀x. x ∈ X ⟹ σ x = x"
    and "x ∈ K"
  shows "σ x = x"
proof -
  have Ksub: "Subfield K" unfolding gen by (rule subfield_generate_field)
  have fixed_subfield: "Subfield {x ∈ K. σ x = x}"
    using Ksub s by (rule field_auto_fixed_set_subfield)
  have fixF: "⋀x. x ∈ F ⟹ σ x = x"
    using s by (auto simp: field_auto_def)
  have FXsub: "F ∪ X ⊆ {x ∈ K. σ x = x}"
    using gen subset_generate_field fixF fixX by blast
  have "generate_field (F ∪ X) ⊆ {x ∈ K. σ x = x}"
    using fixed_subfield FXsub by (rule generate_field_least)
  with gen ‹x ∈ K› show ?thesis by auto
qed

end