Algebraic closure via Zorn's lemma (wrong approach, can't take direct limit without commutativity).

alg_closure_zorn.lean

import field_theory.is_alg_closed.basic

universe u

variables (k : Type u) [field k]

structure alg_extension :=
(K : Type u)
(field : field K)
(algebra : algebra k K)
(is_algebraic : _root_.algebra.is_algebraic k K)

instance : preorder (alg_extension k) :=
{ le := by { rintro ⟨K₁⟩ ⟨K₂⟩, exactI nonempty (K₁ →ₐ[k] K₂) },
  le_refl := by { rintro ⟨K⟩, exactI ⟨alg_hom.id k K⟩ },
  le_trans := by { rintro ⟨⟩ ⟨⟩ ⟨⟩ ⟨f₁⟩ ⟨f₂⟩, exactI ⟨f₂.comp f₁⟩ } }

namespace polynomial

open_locale polynomial

variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain R] [is_domain S] 

lemma map_roots_le (f : R →+* S) (p : R[X]) (h : p.map f ≠ 0) : p.roots.map f ≤ (p.map f).roots :=
begin
  rw [← roots_multiset_prod_X_sub_C (p.roots.map f), multiset.map_map],
  apply roots.le_of_dvd h,
  convert polynomial.map_dvd _ (prod_multiset_X_sub_C_dvd p),
  rw [polynomial.map_multiset_prod, multiset.map_map],
  congr, ext1, dsimp only [function.comp_app],
  rw [polynomial.map_sub, map_X, map_C],
end

lemma card_roots_le_map (f : R →+* S) (p : R[X]) (h : p.map f ≠ 0) :
  p.roots.card ≤ (p.map f).roots.card :=
by { rw ← p.roots.card_map f, exact multiset.card_le_of_le (map_roots_le f p h) }

end polynomial

lemma max_is_alg_closure {K : alg_extension k} (h : is_max K) : 
  by { letI := K.field, letI := K.algebra, exact is_alg_closure k K.K } :=
begin
  split, swap, { exact K.is_algebraic },
  apply is_alg_closed.of_exists_root,
  by_contra, push_neg at h,
  obtain ⟨p, mp, ip, hp⟩ := h,
  casesI K,
  haveI := fact.mk ip,
  have har : 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 power_basis.finite_dimensional (adjoin_root.power_basis ip.ne_zero) },
  let ah := is_scalar_tower.to_alg_hom k K_K (adjoin_root p),
  specialize @h ⟨adjoin_root p, infer_instance, infer_instance, har⟩ ⟨ah⟩,
  let q := minpoly k (adjoin_root.root p),
  let c1 := (q.map $ algebra_map k K_K).roots.card,
  let c2 := (q.map $ algebra_map k $ adjoin_root p).roots.card,
  cases h,
  have mq : q.monic := minpoly.monic (is_algebraic_iff_is_integral.1 $ har _),
  have c21 : c2 ≤ c1,
  { convert polynomial.card_roots_le_map h.to_ring_hom _ ((mq.map _).map _).ne_zero, 
    erw [polynomial.map_map, alg_hom.comp_algebra_map] },
  obtain ⟨r, hr⟩ : p ∣ q.map (algebra_map k K_K),
  { convert minpoly.dvd_map_of_is_scalar_tower k K_K (adjoin_root.root p),
    rw [adjoin_root.minpoly_root mp.ne_zero, mp.leading_coeff, inv_one, polynomial.C_1, mul_one] },
  apply c21.not_lt, -- show c1 < c2
  dsimp only [c1, c2],
  rw [← ah.comp_algebra_map, ← polynomial.map_map, hr, polynomial.map_mul],
  iterate 2 { rw [polynomial.roots_mul, multiset.card_add] },
  { apply add_lt_add_of_lt_of_le _ (polynomial.card_roots_le_map _ _ _), swap,
    { apply ((mp.of_mul_monic_left $ hr.subst $ mq.map _).map _).ne_zero, apply_instance },
    convert multiset.card_pos.2 _,
    { rw [multiset.card_eq_zero, multiset.eq_zero_iff_forall_not_mem],
      refine λ a ha, hp a ((polynomial.mem_roots ip.ne_zero).1 ha) },
    { exact λ re0, multiset.eq_zero_iff_forall_not_mem.1 re0 (adjoin_root.root p)
        ((polynomial.mem_roots $ (mp.map _).ne_zero).2 $ adjoin_root.is_root_root p) } },
  { rw ← polynomial.map_mul, exact ((hr.subst $ mq.map _).map _).ne_zero },
  { exact (hr.subst $ mq.map _).ne_zero },
end