Theory Galois_Correspondence

section ‹The Galois correspondence between intermediate fields and subgroups›

theory Galois_Correspondence
  imports Galois_Automorphism Order_Theory
begin

text ‹Let ‹F ⊆ K› be subfields of an ambient type-class field.  There are two natural operations between the
  ∗‹intermediate fields› of the extension and the ∗‹subgroups› of its Galois group
  @{term "field_auto K F"}:

    ▪ ∗‹fixing› a set of automorphisms, @{text "H ↦ K⇧H"}, the subfield of @{term K} on which every
      element of @{term H} acts as the identity;

    ▪ ∗‹the relative Galois group› of an intermediate field, @{text "E ↦ field_auto K E"}, the
      automorphisms of @{term K} fixing @{term E} pointwise.

  Both are ∗‹inclusion-reversing›: a bigger group of automorphisms fixes fewer points, and a bigger
  intermediate field admits fewer automorphisms fixing it.  So this is an ∗‹antitone› adjoint pair,
  and the way to see it as a @{locale Galois_Connection} --- which is defined for ∗‹monotone›
  adjoints --- is to order one of the two lattices by reverse inclusion.  We order the subgroups by
  ‹⊇›; then both maps become isotone and the adjunction reads
  @{text "K⇧H ⊆ E ⟷ H ⊇ field_auto K E"}.
›


subsection ‹The fixed field of a set of automorphisms›

text ‹The subfield of @{term K} fixed pointwise by every automorphism in @{term H}.  We do not
  require @{term H} to be a subgroup.›
text ‹The fixed field is a subfield by the generic closure theorem
  @{thm [source] field_auto_fixed_field_subfield}; the empty case is @{term K} itself.›
theorem fixed_field_subfield:
  assumes Ksub: "Subfield K" and H: "H ⊆ field_auto K F"
  shows "Subfield (fixed_field K H)"
  by (rule field_auto_fixed_field_subfield[OF Ksub H])

text ‹The base field lies inside every fixed field: by definition each automorphism in the Galois
  group fixes @{term F} pointwise.›
lemma base_subset_fixed_field:
  assumes H: "H ⊆ field_auto K F" and FK: "F ⊆ K"
  shows "F ⊆ fixed_field K H"
  using field_auto_base_subset_fixed_field[OF H FK] .


subsection ‹Intermediate fields and the relative Galois group›

text ‹The intermediate fields of the extension ‹F ⊆ K›: the subfields lying between the two.›
definition inter_fields :: "'a :: field set ⇒ 'a set ⇒ 'a set set"
  where "inter_fields K F ≡ {E. Subfield E ∧ F ⊆ E ∧ E ⊆ K}"

lemma inter_fields_iff:
  "E ∈ inter_fields K F ⟷ Subfield E ∧ F ⊆ E ∧ E ⊆ K"
  by (simp add: inter_fields_def)

text ‹The two ends of the extension are intermediate fields.›
lemma base_in_inter_fields:
  "⟦ Subfield F; F ⊆ K ⟧ ⟹ F ∈ inter_fields K F"
  by (simp add: inter_fields_iff)

lemma top_in_inter_fields:
  "⟦ Subfield K; F ⊆ K ⟧ ⟹ K ∈ inter_fields K F"
  by (simp add: inter_fields_iff)

text ‹Taking the relative Galois group is inclusion-reversing: a bigger intermediate field imposes
  more conditions, so fewer automorphisms survive.›
lemma field_auto_antitone: "E ⊆ E' ⟹ field_auto K E' ⊆ field_auto K E"
  by (auto simp: field_auto_def)

text ‹The relative Galois group of an intermediate field is a subgroup of the whole Galois group:
  it consists of automorphisms of @{term K}, and fixing @{term E} pointwise implies fixing the
  smaller @{term F} pointwise.›
theorem field_auto_subgroup_of_Galois_group:
  assumes Ksub: "Subfield K" and FK: "F ⊆ K" and E: "E ∈ inter_fields K F"
  shows "Subgroup (field_auto K E) (field_auto K F) (compose K) (identity K)"
proof -
  from E have Esub: "Subfield E" and FE: "F ⊆ E" and EK: "E ⊆ K"
    by (auto simp: inter_fields_iff)
  ― ‹Work inside the whole Galois group as the ambient group, so that ‹subgroupI› applies.›
  interpret W: Group "field_auto K F" "compose K" "identity K"
    using Ksub FK by (rule field_auto_group)
  ― ‹The relative group is also a subgroup of the symmetric group, which supplies inverses.›
  interpret S: Subgroup "field_auto K E" "transformations.Sym K" "compose K" "identity K"
    using Ksub EK by (rule field_auto_subgroup)
  have EF: "field_auto K E ⊆ field_auto K F" using FE by (rule field_auto_antitone)
  show ?thesis
  proof (rule W.subgroupI [OF EF])
    show "identity K ∈ field_auto K E" using Ksub EK by (rule field_auto_identity)
    show "⋀g h. ⟦ g ∈ field_auto K E; h ∈ field_auto K E ⟧ ⟹ compose K g h ∈ field_auto K E"
      using Ksub EK by (blast intro: field_auto_compose)
    ― ‹Invertibility and the inverse are computed in the symmetric group; because
      @{term "field_auto K E"} is a subgroup there, the inverse stays inside it, and the two
      ambient groups agree on inverses by @{thm [source] Subgroup.subgroup_inverse_equality}.›
    show "⋀g. g ∈ field_auto K E ⟹ W.invertible g"
      using EF by (blast intro: W.invertible)
    show "W.inverse g ∈ field_auto K E" if "g ∈ field_auto K E" for g
    proof -
      have gW: "g ∈ field_auto K F" using that EF by blast
      have inv_in: "S.sub.inverse g ∈ field_auto K E"
        using that by (simp add: S.sub.invertible_inverse_closed)
      ― ‹The symmetric-group inverse is a two-sided inverse of ‹g› in the ambient Galois group
        too, so the two notions of inverse agree.›
      have "W.inverse g = S.sub.inverse g"
      proof (rule W.inverse_equality)
        show "S.sub.inverse g ∈ field_auto K F" using inv_in EF by blast
      qed (use that gW in auto)
      then show "W.inverse g ∈ field_auto K E" using inv_in by simp
    qed
  qed
qed

text ‹The set of subgroups of the Galois group, as the second of the two lattices.›
definition galois_subgroups :: "'a :: field set ⇒ 'a set ⇒ ('a ⇒ 'a) set set"
  where "galois_subgroups K F ≡
    {H. Subgroup H (field_auto K F) (compose K) (identity K)}"

lemma galois_subgroups_iff:
  "H ∈ galois_subgroups K F ⟷ Subgroup H (field_auto K F) (compose K) (identity K)"
  by (simp add: galois_subgroups_def)

lemma galois_subgroups_subset:
  assumes "H ∈ galois_subgroups K F" shows "H ⊆ field_auto K F"
  using assms by (meson Subgroup_def Submonoid.subset galois_subgroups_iff)


subsection ‹The adjunction›

locale galois_extension =
  fixes K F :: "'a :: field set"
  assumes Ksub: "Subfield K" and Fsub: "Subfield F" and FK: "F ⊆ K"
begin

text ‹Fixing lands in the intermediate fields: the fixed field of a subgroup is a subfield lying
  between @{term F} and @{term K}.›
lemma fixed_field_in_inter_fields:
  assumes H: "H ∈ galois_subgroups K F"
  shows "fixed_field K H ∈ inter_fields K F"
proof -
  have HG: "H ⊆ field_auto K F" using H by (rule galois_subgroups_subset)
  show ?thesis
    unfolding inter_fields_iff
  proof (intro conjI)
    show "Subfield (fixed_field K H)" using Ksub HG by (rule fixed_field_subfield)
    show "F ⊆ fixed_field K H" using HG FK by (rule base_subset_fixed_field)
    show "fixed_field K H ⊆ K" by (rule fixed_field_subset)
  qed
qed

text ‹∗‹The adjunction.›  Both sides of the biconditional say the same thing --- ∗‹every›
  automorphism in @{term H} fixes ∗‹every› point of @{term E} --- so the proof is a matter of
  unfolding.  This is the antitone (or ∗‹polarity›) form of an adjunction: both maps reverse
  inclusion, and each side bounds one argument by the image of the other.

  It is worth being precise about which biconditional is formal, because the other one is a deep
  theorem.  The statement proved here bounds @{term E} ∗‹above› by a fixed field and @{term H}
  ∗‹above› by a Galois group.  The reverse reading --- @{text "fixed_field K H ⊆ E ⟷
  field_auto K E ⊆ H"} --- is ∗‹not› a formal consequence: its left-to-right direction asserts that
  every automorphism fixing @{term E} already lies in @{term H}, which is Artin's theorem and needs
  @{term H} finite.›
theorem fixed_field_galois:
  assumes E: "E ∈ inter_fields K F" and H: "H ∈ galois_subgroups K F"
  shows "E ⊆ fixed_field K H ⟷ H ⊆ field_auto K E"
proof
  assume "E ⊆ fixed_field K H"
  then have fixes_E: "⋀σ x. ⟦ σ ∈ H; x ∈ E ⟧ ⟹ σ x = x"
    by (auto dest: fixed_field_memD)
  show "H ⊆ field_auto K E"
    using fixes_E galois_subgroups_subset [OF H] 
    by (smt (cvc5, dec_internal_enum_inst_sum) field_auto_mem_iff subset_iff)
next
  assume "H ⊆ field_auto K E"
  then show "E ⊆ fixed_field K H"
    using E by (meson field_auto_base_subset_fixed_field inter_fields_iff)
qed

text ‹The two ∗‹unit› inequalities, which hold unconditionally and in both directions.  These are
  the parts of the correspondence that need no hypotheses; it is their ∗‹converses› that require
  normality and separability.›
lemma le_fixed_field_galois_group:
  assumes E: "E ∈ inter_fields K F"
  shows "E ⊆ fixed_field K (field_auto K E)"
  using E by (auto simp: inter_fields_iff fixed_field_def field_auto_def)

lemma le_galois_group_fixed_field:
  assumes H: "H ∈ galois_subgroups K F"
  shows "H ⊆ field_auto K (fixed_field K H)"
  using assms fixed_field_galois fixed_field_in_inter_fields by blast


subsection ‹The Galois connection›

text ‹Both maps reverse inclusion, so to view the pair as a @{locale Galois_Connection} --- whose
  adjoints are ∗‹isotone› --- we order the subgroup lattice by ∗‹reverse› inclusion.  Then the
  adjunction @{thm [source] fixed_field_galois} is literally the @{text galois} axiom, with
  @{term "field_auto K"} as the lower adjoint out of the intermediate fields and
  @{term "fixed_field K"} as the upper adjoint back.

  Note the direction: @{term "field_auto K"} is the ∗‹lower› adjoint here, even though it is the map
  ∗‹into› the groups, because the group side carries the reversed order.  Inclusion is a partial order
  on any set of sets, and so is its converse.›

text ‹Inclusion and reverse inclusion are partial orders on the two lattices.›
lemma partial_order_inter_fields: "Partial_Order (inter_fields K F) (⊆)"
  by unfold_locales auto

lemma partial_order_galois_subgroups: "Partial_Order (galois_subgroups K F) (λH H'. H' ⊆ H)"
  by unfold_locales auto

theorem galois_correspondence:
  "Galois_Connection
     (inter_fields K F) (⊆)
     (galois_subgroups K F) (λH H'. H' ⊆ H)
     (field_auto K) (fixed_field K)"
proof (intro partial_order_inter_fields partial_order_galois_subgroups Galois_Connection.intro)
  show "Galois_Connection_axioms
          (inter_fields K F) (⊆) (galois_subgroups K F) (λH H'. H' ⊆ H)
          (field_auto K) (fixed_field K)"
  proof
    show "field_auto K ∈ inter_fields K F → galois_subgroups K F"
      using Ksub FK field_auto_subgroup_of_Galois_group by (auto simp: galois_subgroups_iff)
    show "fixed_field K ∈ galois_subgroups K F → inter_fields K F"
      using fixed_field_in_inter_fields by auto
    fix E H assume "E ∈ inter_fields K F" and "H ∈ galois_subgroups K F"
    then show "H ⊆ field_auto K E ⟷ E ⊆ fixed_field K H"
      using fixed_field_galois by blast
  qed
qed

text ‹The consequences, specialised to the correspondence.  As in ‹Ideal_Extension› these come from a
  local @{command interpretation} of the theorem rather than a @{command sublocale} declaration.›

context
begin

interpretation GC: Galois_Connection
  "inter_fields K F" "(⊆)" "galois_subgroups K F" "λH H'. H' ⊆ H"
  "field_auto K" "fixed_field K"
  by (rule galois_correspondence)

text ‹Both maps are inclusion-reversing on their lattices --- the isotonicity of the connection,
  read back through the reversed order on subgroups.›
corollary field_auto_mono:
  "⟦ E ∈ inter_fields K F; E' ∈ inter_fields K F; E ⊆ E' ⟧
   ⟹ field_auto K E' ⊆ field_auto K E"
  using isotone_le[OF GC.lower_isotone] by simp

corollary fixed_field_mono:
  "⟦ H ∈ galois_subgroups K F; H' ∈ galois_subgroups K F; H' ⊆ H ⟧
   ⟹ fixed_field K H ⊆ fixed_field K H'"
  using isotone_le[OF GC.upper_isotone] by simp

text ‹The ∗‹semi-inverse› laws: one round trip and back is the identity.  These are the strongest
  fixed-point statements available without finiteness --- they say the closure and kernel operators
  are idempotent, ∗‹not› that either is the identity.›
corollary field_auto_fixed_field_field_auto:
  "E ∈ inter_fields K F ⟹ field_auto K (fixed_field K (field_auto K E)) = field_auto K E"
  using GC.lower_semi_inverse by simp

corollary fixed_field_field_auto_fixed_field:
  "H ∈ galois_subgroups K F ⟹ fixed_field K (field_auto K (fixed_field K H)) = fixed_field K H"
  using GC.upper_semi_inverse by simp

end

end (* galois_extension *)


text ‹❙‹Scope and downstream completion.›  This theory deliberately stops at the
  representation-independent, inclusion-reversing adjunction, packaged as a
  @{locale Galois_Connection}.  No separability, normality or finiteness hypothesis belongs in this
  layer: the unit, counit and semi-inverse laws are the reusable order-theoretic API.›

end