Algebraic closure via Zorn's lemma (correct approach).

alg_closure_zorn.lean

import field_theory.is_alg_closed.basic
import logic.equiv.transfer_instance
import algebra.direct_limit

/-! Existence of algebraic closure via Zorn's lemma. We follow Zbigniew Jelonek's proof from
  https://math.stackexchange.com/a/621955/12932;
  also in GTM 167, *Field and Galois Theory* by Patrick Morandi. -/

universe u

variables (k : Type u) [field k]

open_locale polynomial

/-- A type with cardinality exceeding cardinalities of all possible algebraic extensions K of k,
  ensuring that we have enough room to fit in a proper extension of K whenever K is not
  algebraically closed. -/
@[reducible] def big : Type u := set k[X]

variable {k}
/-- A embedding from `k` into `big k`, so as to view `k` as a subset of `big k`. -/
def emb : k ↪ big k :=
{ to_fun := λ x, ({polynomial.monomial 0 x} : set k[X]),
  inj' := λ _ _ h, polynomial.monomial_injective 0 (set.singleton_injective h) }

variable (k)
/-- The type of all algebraic extensions `K/k` with underlying set a subset of `big k`;
  the `compatible` condition ensures that the [algebra k K] structure comes from
  the inclusion `k ⊆ K`.
  It is necessary to restrict the carriers to subsets of a fixed set, as this allows us to take
  the union of the carriers as the carrier of the supremum of a chain. The important thing is that
  there is a partial order ⊆ on the type of subsets, such that whenever s ⊆ t, there is a canonical
  injective function from ↥s to ↥t (`set.inclusion`), and these functions are compatible under
  composition given r ⊆ s ⊆ t. In other words, `set.inclusion` is a functor, which allows us to
  take a direct limit.
  If we allow the carrier to be any `α : Type u`, we could still define a preorder on the type
  of algebraic extensions by `α ≤ β := nonempty (α →ₐ[k] β)`, but that does not give rise to a
  canonical `α ↪ β`, and when we have a chain of algebraic extensions, we could not take the direct
  limit to get an upper bound, because the maps may not be compatible. -/
structure alg_extension :=
(carrier : set $ big k)
(field : field carrier)
(algebra : algebra k carrier)
(is_algebraic : _root_.algebra.is_algebraic k carrier)
(compatible (x : k) : (algebra_map k carrier x : big k) = emb x)

attribute [instance] alg_extension.field alg_extension.algebra

/-- Field structures are not unique on a subset, so this is not a `set_like` instance. -/
instance : has_coe_to_sort (alg_extension k) (Type u) := ⟨λ K, K.carrier⟩

def map_one_add_mul {α β} [has_one α] [has_one β] [has_add α] [has_add β] [has_mul α] [has_mul β]
  (f : α → β) : Prop := f 1 = 1 ∧ ∀ {a b}, f (a + b) = f a + f b ∧ f (a * b) = f a * f b

variables (K₁ K₂ : alg_extension k)

/-- K₁ ≤ K₂ iff the underlying set of K₁ is a subset of that of K₂ and the inclusion is a ring
  homomorphism. -/
structure incl_hom : Prop :=
(incl : K₁.carrier ⊆ K₂.carrier)
(map : map_one_add_mul $ set.inclusion incl)

/-- This should really be a partial order, but it is hard to show (and not necessary to apply
  Zorn's lemma), because the lack of extensionality lemmas for `field` and `algebra`. -/
instance : preorder (alg_extension k) :=
{ le := incl_hom k,
  le_refl := λ K, ⟨set.subset.rfl, by ext1; refl, by { rintro ⟨⟩ ⟨⟩, split; ext1; refl }⟩,
  le_trans := by { rintro _ _ _ ⟨hi₁, ho₁, ham₁⟩ ⟨hi₂, ho₂, ham₂⟩, refine ⟨hi₁.trans hi₂, _⟩,
    simp_rw [map_one_add_mul, ← set.inclusion_inclusion, ho₁, ho₂, ham₁.1, ham₂.1, ham₁.2, ham₂.2],
    exact ⟨rfl, λ _ _, ⟨rfl, rfl⟩⟩ } }

/-! Algebraic structures on `set.inclusion` and instances. -/
variables {K₁ K₂ k}

def alg_extension.ring_hom (h : K₁ ≤ K₂) : K₁ →+* K₂ :=
ring_hom.mk' ⟨set.inclusion h.incl, h.map.1, λ _ _, h.map.2.2⟩ $ λ _ _, h.map.2.1

def alg_extension.algebra_of_le (h : K₁ ≤ K₂) : algebra K₁ K₂ :=
(alg_extension.ring_hom h).to_algebra

def alg_extension.is_scalar_tower (h : K₁ ≤ K₂) :
  @is_scalar_tower k K₁ K₂ _ (alg_extension.algebra_of_le h).to_has_smul _ :=
begin
  letI := alg_extension.algebra_of_le h,
  apply is_scalar_tower.of_algebra_map_eq (λ x, _),
  ext1, erw [set.coe_inclusion h.incl, K₁.compatible, K₂.compatible],
end

def alg_extension.alg_hom (h : K₁ ≤ K₂) : K₁ →ₐ[k] K₂ :=
begin
  letI := alg_extension.algebra_of_le h,
  letI := alg_extension.is_scalar_tower h,
  apply is_scalar_tower.to_alg_hom,
end

/-- Transfer `is_algebraic` across an equivalence. -/
lemma equiv.is_algebraic {α β R} [comm_ring R] (e : α ≃ β) [ring β] [algebra R β]
  (h : algebra.is_algebraic R β) :
  begin let := e.ring, let := e.algebra R, exactI algebra.is_algebraic R α end :=
begin
  introsI _ _ x,
  convert ← is_algebraic_alg_hom_of_is_algebraic (e.alg_equiv R).symm.to_alg_hom (h _),
  apply equiv.left_inv,
end

/-- Given an embedding f from a subset s of a type α into another type β whose complement sᶜ has
  enough cardinality to fit in the whole β (in particular the complement of the image of s), we may
  extend f to a bijection between a superset of s and β. -/
lemma exists_extension {α β} {s : set α} {f : s → β} (hf : function.injective f)
  (hc : cardinal.mk β ≤ cardinal.mk ↥sᶜ) :
  ∃ (t : set α) (h : s ⊆ t) (g : t ≃ β), ∀ x, g (set.inclusion h x) = f x :=
begin
  cases hc, let c := (function.embedding.subtype (set.range f)ᶜ).trans hc,
  refine ⟨s ∪ subtype.val '' set.range c, set.subset_union_left _ _, _, λ x, _⟩,
  { apply (equiv.set.union _).trans,
    { apply (equiv.sum_congr (equiv.of_injective f hf) $ equiv.symm _).trans,
      { classical, apply equiv.set.sum_compl (set.range f) },
      exact (equiv.of_injective c c.inj').trans (equiv.set.image _ _ subtype.val_injective) },
    { apply_instance },
    { rintro _ ⟨hs, b, -, rfl⟩, cases b.2 hs } },
  cases x, simp only [equiv.trans_apply], rw equiv.set.union_apply_left, refl,
end

section
variables {K : Type u} [field K] [algebra k K] (h : algebra.is_algebraic k K)
include h

/-- The cardinality of an algebraic extension of k does not exceed that of k[X]. -/
lemma cardinal_le_polynomial : cardinal.mk K ≤ cardinal.mk k[X] :=
begin
  choose f hf using h,
  apply le_of_le_of_eq (cardinal.mk_le_mk_mul_of_mk_preimage_le f $ λ p, _),
  { rw mul_comm, apply cardinal.aleph_0_mul_mk_eq },
  refine (set.finite.lt_aleph_0 _).le,
  apply (finset.finite_to_set _ : (p.root_set K).finite).subset,
  rintro x (rfl : _ = p),
  exact (polynomial.mem_root_set (hf x).1).2 (hf x).2,
end

lemma cardinal_lt_big : cardinal.mk K < cardinal.mk (big k) :=
(cardinal_le_polynomial h).trans_lt (cardinal.mk_set.substr $ cardinal.cantor _)

end

/-- A maximal element in the preorder `alg_extension k` is an algebraic closure of k. -/
theorem is_max.is_alg_closure {K : alg_extension k} (hm : is_max K) : is_alg_closure k K :=
begin
  refine ⟨is_alg_closed.of_exists_root K _, K.is_algebraic⟩,
  by_contra, push_neg at h,
  /- Assume for contradiction that K is not algebraically closed,
    i.e. there exists p : K[X] without a root in K. -/
  obtain ⟨p, mp, ip, hp⟩ := h,
  haveI := fact.mk ip,
  have aar : algebra.is_algebraic k (adjoin_root p),
  { apply algebra.is_algebraic_trans K.is_algebraic,
    iterate 2 { swap, apply_instance },
    convert algebra.is_algebraic_of_finite _ _,
    exact (adjoin_root.power_basis ip.ne_zero).finite_dimensional },

  /- Realize `adjoin_root p` as a subset L of `big k` containing K. -/
  obtain ⟨L, hKL, g, hg⟩ := exists_extension (adjoin_root.of p).injective _, swap,
  { rw cardinal.mk_compl_of_infinite,
    apply le_of_lt,
    all_goals { apply cardinal_lt_big },
    exacts [aar, K.is_algebraic] },

  /- Put algebraic structures on L and show K ≤ L, so by maximality of K (hm), L ≤ K as well. -/
  letI : field L := g.field,
  letI : algebra k L := g.algebra k,
  have hg' : ∀ x, _ = (g.alg_equiv k).symm _ := λ x, g.eq_symm_apply.2 (hg x),
  specialize @hm ⟨L, g.field, g.algebra k, g.is_algebraic aar, λ x, _⟩ ⟨hKL, _, _⟩,
  { rw [← (g.alg_equiv k).symm.to_alg_hom.comp_algebra_map, ring_hom.comp_apply],
    erw [← hg', set.coe_inclusion, K.compatible x] },
  { rw [hg', map_one, map_one] },
  { intros, iterate 4 {rw hg'}, split; simp only [map_add, map_mul] },

  /- Now push the root of p in `adjoin_root p` across `g : L ≃ adjoin_root p` and `L ≤ K` to obtain
    a root of p in K, thereby arriving at a contradiction. -/
  apply hp (set.inclusion hm.incl $ g.symm $ adjoin_root.root p),
  apply (adjoin_root.of p).injective,
  rw [← polynomial.eval₂_hom, ← hg, set.inclusion_inclusion, set.inclusion_self, map_zero],
  rw g.apply_symm_apply,
  exact adjoin_root.eval₂_root p,
end

section chain

variables {α : Type*} [preorder α] {c : set α} [fact $ is_chain (≤) c]
/- [has_le α] [is_refl α (≤)] should also work,
  but `is_refl` lacks API, making proofs inconvenient. -/

lemma le_or_ge (K₁ K₂ : c) : K₁ ≤ K₂ ∨ K₂ ≤ K₁ :=
(fact.out $ is_chain (≤) c).total K₁.2 K₂.2

instance : is_directed c (≤) :=
⟨λ K₁ K₂, (le_or_ge K₁ K₂).elim (λ h, ⟨K₂, h, le_rfl⟩) (λ h, ⟨K₁, le_rfl, h⟩)⟩

end chain

variable (c : set $ alg_extension k)

/-- We could directly construct a field structure on the union, but there are too many fields
  (no pun intended) to fill in, so we defer to the existing direct limit API. -/

def dir_sys (K₁ K₂ : c) (h : K₁ ≤ K₂) := (alg_extension.alg_hom h).to_ring_hom

def dir_lim := ring.direct_limit _ (λ _ _ h, dir_sys c _ _ h)
/- The first placeholder is G := λ K : c, K.1.carrier -/

instance dir_sys.directed_system : directed_system _ (λ _ _ h, dir_sys c _ _ h) :=
⟨λ K x h, set.inclusion_self x,  λ _ _ _ h₁ h₂ x, set.inclusion_inclusion _ _ x⟩

noncomputable theory

/-! Instances and lemmas on the direct limit given a nonempty chain. -/

variables [nonempty c] [fact $ is_chain (≤) c]

instance : field (dir_lim c) := field.direct_limit.field _ _

instance dir_lim.algebra' (K : c) : algebra K.1 (dir_lim c) :=
ring_hom.to_algebra (ring.direct_limit.of _ (λ _ _ h, dir_sys c _ _ h) K)
/- Takes a long time (6~7s)! -/

instance : algebra k (dir_lim c) :=
((algebra_map (classical.arbitrary c).1 _).comp $ algebra_map k _).to_algebra

lemma dir_lim.commute (K₁ K₂ : c) (h : K₁ ≤ K₂) (x : K₁) :
  algebra_map K₂.1 (dir_lim c) (alg_extension.alg_hom h x) = algebra_map K₁.1 (dir_lim c) x :=
ring.direct_limit.of_f h x

instance (K : c) : is_scalar_tower k K.1 (dir_lim c) :=
is_scalar_tower.of_algebra_map_eq $ λ x, begin
  cases le_or_ge K (classical.arbitrary c);
  { erw [← dir_lim.commute _ _ _ h, alg_hom.commutes], refl },
end

def dir_lim.is_algebraic : algebra.is_algebraic k (dir_lim c) :=
λ x, begin
  obtain ⟨K, x, rfl⟩ := ring.direct_limit.exists_of x,
  convert_to is_algebraic k (algebra_map K.1 (dir_lim c) x), /- Why doesn't `change` work? -/
  exact is_algebraic_algebra_map_of_is_algebraic (K.1.is_algebraic x),
end

/-- The union of the fields in the chain. We show it is in bijection with the direct limit
  and transfer the field and algebra structure from the direct limit to the union. -/
def Union := ⋃ K : c, K.1.carrier

def dir_lim.of_Union (x : Union c) : dir_lim c :=
let h := set.mem_Union.1 x.2 in algebra_map h.some.1 _ ⟨x, h.some_spec⟩

variable {c}
lemma dir_lim.of_Union_indep {K : c} (x : K) :
  dir_lim.of_Union c (set.inclusion (set.subset_Union _ K) x) = algebra_map K.1 _ x :=
begin
  cases le_or_ge K _,
  { apply dir_lim.commute _ _ _ h },
  { cases x, exact (dir_lim.commute _ _ _ h _).symm },
end

lemma dir_lim.of_Union_indep' {x : Union c} {K : c} (hx : x.1 ∈ K.1.carrier) :
  dir_lim.of_Union c x = algebra_map K.1 _ ⟨x, hx⟩ :=
by { cases x, convert dir_lim.of_Union_indep _, refl }

lemma dir_lim.bijective : function.bijective (dir_lim.of_Union c) :=
begin
  refine ⟨λ x₁ x₂ he, _, λ x, _⟩,
  { obtain ⟨K₁, h₁⟩ := set.mem_Union.1 x₁.2,
    obtain ⟨K₂, h₂⟩ := set.mem_Union.1 x₂.2,
    have oui := @dir_lim.of_Union_indep',
    cases le_or_ge K₁ K₂,
    rw [oui (h.incl h₁), oui h₂] at he, swap,
    rw [oui (h.incl h₂), oui h₁] at he,
    all_goals { ext1, exact subtype.mk_eq_mk.1 (ring_hom.injective _ he) } },
  { obtain ⟨K, x, rfl⟩ := ring.direct_limit.exists_of x,
    split, apply dir_lim.of_Union_indep x },
end

variable (c)
def dir_lim.equiv : Union c ≃ dir_lim c := equiv.of_bijective _ dir_lim.bijective

instance : field (Union c) := (dir_lim.equiv c).field
instance : algebra k (Union c) := (dir_lim.equiv c).algebra k
instance Union.algebra' (K : c) : algebra K.1 (Union c) := (dir_lim.equiv c).algebra K

variable {c}
def Union.alg_hom (K : c) : K.1 →ₐ[k] Union c :=
((dir_lim.equiv c).alg_equiv k).symm.to_alg_hom.comp (is_scalar_tower.to_alg_hom _ _ _)

lemma Union.alg_hom_eq (K : c) : ⇑(Union.alg_hom K) = set.inclusion (set.subset_Union _ K) :=
funext $ λ x, (equiv.symm_apply_eq _).2 (dir_lim.of_Union_indep x).symm

/-- Every chain in `alg_extension k` has an upper bound. -/
theorem chain_bdd_above (c : set $ alg_extension k) [fact $ is_chain (≤) c] : bdd_above c :=
begin
  unfreezingI { obtain rfl | hne := c.eq_empty_or_nonempty },
  { let e := (equiv.of_injective _ (@emb k _).inj').symm,
    refine ⟨⟨_, e.field, e.algebra k, λ x, _, λ x, rfl⟩, _⟩,
    { convert ← is_algebraic_algebra_map (e x), apply e.left_inv },
    { rw upper_bounds_empty, trivial } },

  haveI : nonempty c := set.nonempty_coe_sort.2 hne,
  let e := dir_lim.equiv c,
  refine ⟨⟨_, e.field, e.algebra k, e.is_algebraic (dir_lim.is_algebraic c), λ x, _⟩, _⟩,
  { rw [← (Union.alg_hom $ classical.arbitrary c).commutes, Union.alg_hom_eq],
    erw alg_extension.compatible },
  /- ↓ Show the transferred k-algebra structure on the union is an upper bound for the chain c. -/
  refine λ K hK, ⟨set.subset_Union (λ K : c, K.1.carrier) ⟨K, hK⟩, _⟩,
  rw ← Union.alg_hom_eq ⟨K, hK⟩,
  exact ⟨map_one _, λ _ _, ⟨map_add _ _ _, map_mul _ _ _⟩⟩,
end

variable (k)
theorem exists_alg_closure : ∃ K : alg_extension k, is_alg_closure k K :=
let ⟨K, hK⟩ := @zorn_preorder (alg_extension k) _
  (λ c hc, by let := fact.mk hc; exactI chain_bdd_above c) in ⟨K, is_max.is_alg_closure hK⟩

/-- The algebraic closure is constructed, but it might take some work to fix definitional
  equalities of the data fields. -/
def algebraic_closure : Type u := (exists_alg_closure k).some.carrier
instance : field (algebraic_closure k) := (exists_alg_closure k).some.field
instance : algebra k (algebraic_closure k) := (exists_alg_closure k).some.algebra

theorem algebraic_closure.is_alg_closure : is_alg_closure k (algebraic_closure k) :=
(exists_alg_closure k).some_spec