feat(order/extension): extend partial order to linear order (#7142)

Adds a construction to extend a partial order to a linear order. Also fills in a missing Zorn variant.

src/analysis/convex/cone.lean

@@ -457,7 +457,7 @@ theorem exists_top (p : linear_pmap ℝ E ℝ)
   ∃ q ≥ p, q.domain = ⊤ ∧ ∀ x : q.domain, (x : E) ∈ s → 0 ≤ q x :=
 begin
   replace hp_nonneg : p ∈ { p | _ }, by { rw mem_set_of_eq, exact hp_nonneg },
-  obtain ⟨q, hqs, hpq, hq⟩ := zorn.zorn_partial_order₀ _ _ _ hp_nonneg,
+  obtain ⟨q, hqs, hpq, hq⟩ := zorn.zorn_nonempty_partial_order₀ _ _ _ hp_nonneg,
   { refine ⟨q, hpq, _, hqs⟩,
     contrapose! hq,
     rcases step s q hqs _ hq with ⟨r, hqr, hr⟩,

src/analysis/normed_space/inner_product.lean

@@ -805,7 +805,7 @@ containing it. -/
 lemma exists_maximal_orthonormal {s : set E} (hs : orthonormal 𝕜 (coe : s → E)) :
   ∃ w ⊇ s, orthonormal 𝕜 (coe : w → E) ∧ ∀ u ⊇ w, orthonormal 𝕜 (coe : u → E) → u = w :=
 begin
-  rcases zorn.zorn_subset₀ {b | orthonormal 𝕜 (coe : b → E)} _ _ hs  with ⟨b, bi, sb, h⟩,
+  rcases zorn.zorn_subset_nonempty {b | orthonormal 𝕜 (coe : b → E)} _ _ hs  with ⟨b, bi, sb, h⟩,
   { refine ⟨b, sb, bi, _⟩,
     exact λ u hus hu, h u hu hus },
   { refine λ c hc cc c0, ⟨⋃₀ c, _, _⟩,

src/linear_algebra/linear_independent.lean

@@ -1006,7 +1006,7 @@ by rw [linear_independent_fin_succ, linear_independent_unique_iff, range_unique,
 lemma exists_linear_independent (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ t) :
   ∃b⊆t, s ⊆ b ∧ t ⊆ span K b ∧ linear_independent K (λ x, x : b → V) :=
 begin
-  rcases zorn.zorn_subset₀ {b | b ⊆ t ∧ linear_independent K (λ x, x : b → V)} _ _
+  rcases zorn.zorn_subset_nonempty {b | b ⊆ t ∧ linear_independent K (λ x, x : b → V)} _ _
     ⟨hst, hs⟩ with ⟨b, ⟨bt, bi⟩, sb, h⟩,
   { refine ⟨b, bt, sb, λ x xt, _, bi⟩,
     by_contra hn,

src/order/compactly_generated.lean

@@ -361,7 +361,8 @@ theorem Iic_coatomic_of_compact_element {k : α} (h : is_compact_element k) :
   by_cases htriv : b = k,
   { left, ext, simp only [htriv, set.Iic.coe_top, subtype.coe_mk], },
   right,
-  rcases zorn.zorn_partial_order₀ (set.Iio k) _ b (lt_of_le_of_ne hbk htriv) with ⟨a, a₀, ba, h⟩,
+  rcases zorn.zorn_nonempty_partial_order₀ (set.Iio k) _ b (lt_of_le_of_ne hbk htriv)
+    with ⟨a, a₀, ba, h⟩,
   { refine ⟨⟨a, le_of_lt a₀⟩, ⟨ne_of_lt a₀, λ c hck, by_contradiction $ λ c₀, _⟩, ba⟩,
     cases h c.1 (lt_of_le_of_ne c.2 (λ con, c₀ (subtype.ext con))) hck.le,
     exact lt_irrefl _ hck, },

src/order/complete_lattice.lean

@@ -1082,6 +1082,14 @@ lemma Sup_apply {α : Type*} {β : α → Type*} [Π i, has_Sup (β i)] {s : set
   (Sup s) a = (⨆f:s, (f : Πa, β a) a) :=
 rfl
 
+lemma unary_relation_Sup_iff {α : Type*} (s : set (α → Prop)) {a : α} :
+  Sup s a ↔ ∃ (r : α → Prop), r ∈ s ∧ r a :=
+by { change (∃ _, _) ↔ _, simp [-eq_iff_iff] }
+
+lemma binary_relation_Sup_iff {α β : Type*} (s : set (α → β → Prop)) {a : α} {b : β} :
+  Sup s a b ↔ ∃ (r : α → β → Prop), r ∈ s ∧ r a b :=
+by { change (∃ _, _) ↔ _, simp [-eq_iff_iff] }
+
 lemma supr_apply {α : Type*} {β : α → Type*} {ι : Sort*} [Π i, has_Sup (β i)] {f : ι → Πa, β a}
   {a : α} :
   (⨆i, f i) a = (⨆i, f i a) :=

src/order/extension.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2021 Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta
+-/
+import data.set.lattice
+import order.zorn
+
+/-!
+# Extend a partial order to a linear order
+
+This file constructs a linear order which is an extension of the given partial order, using Zorn's
+lemma.
+-/
+
+universes u
+open set classical
+open_locale classical
+
+/--
+Any partial order can be extended to a linear order.
+-/
+theorem extend_partial_order {α : Type u} (r : α → α → Prop) [is_partial_order α r] :
+  ∃ (s : α → α → Prop) [is_linear_order α s], r ≤ s :=
+begin
+  let S := {s | is_partial_order α s},
+  have hS : ∀ c, c ⊆ S → zorn.chain (≤) c → ∀ y ∈ c, (∃ ub ∈ S, ∀ z ∈ c, z ≤ ub),
+  { rintro c hc₁ hc₂ s hs,
+    haveI := (hc₁ hs).1,
+    refine ⟨Sup c, _, λ z hz, le_Sup hz⟩,
+    refine { refl := _, trans := _, antisymm := _ }; simp_rw binary_relation_Sup_iff,
+    { intro x,
+      exact ⟨s, hs, refl x⟩ },
+    { rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩,
+      haveI : is_partial_order _ _ := hc₁ h₁s₁,
+      haveI : is_partial_order _ _ := hc₁ h₁s₂,
+      cases hc₂.total_of_refl h₁s₁ h₁s₂,
+      { exact ⟨s₂, h₁s₂, trans (h _ _ h₂s₁) h₂s₂⟩ },
+      { exact ⟨s₁, h₁s₁, trans h₂s₁ (h _ _ h₂s₂)⟩ } },
+    { rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩,
+      haveI : is_partial_order _ _ := hc₁ h₁s₁,
+      haveI : is_partial_order _ _ := hc₁ h₁s₂,
+      cases hc₂.total_of_refl h₁s₁ h₁s₂,
+      { exact antisymm (h _ _ h₂s₁) h₂s₂ },
+      { apply antisymm h₂s₁ (h _ _ h₂s₂) } } },
+  obtain ⟨s, hs₁ : is_partial_order _ _, rs, hs₂⟩ := zorn.zorn_nonempty_partial_order₀ S hS r ‹_›,
+  resetI,
+  refine ⟨s, { total := _ }, rs⟩,
+  intros x y,
+  by_contra h,
+  push_neg at h,
+  let s' := λ x' y', s x' y' ∨ s x' x ∧ s y y',
+  rw ←hs₂ s' _ (λ _ _, or.inl) at h,
+  { apply h.1 (or.inr ⟨refl _, refl _⟩) },
+  { refine
+      { refl := λ x, or.inl (refl _),
+        trans := _,
+        antisymm := _ },
+    { rintro a b c (ab | ⟨ax : s a x, yb : s y b⟩) (bc | ⟨bx : s b x, yc : s y c⟩),
+      { exact or.inl (trans ab bc), },
+      { exact or.inr ⟨trans ab bx, yc⟩ },
+      { exact or.inr ⟨ax, trans yb bc⟩ },
+      { exact or.inr ⟨ax, yc⟩ } },
+    { rintro a b (ab | ⟨ax : s a x, yb : s y b⟩) (ba | ⟨bx : s b x, ya : s y a⟩),
+      { exact antisymm ab ba },
+      { exact (h.2 (trans ya (trans ab bx))).elim },
+      { exact (h.2 (trans yb (trans ba ax))).elim },
+      { exact (h.2 (trans yb bx)).elim } } },
+end
+
+/-- A type alias for `α`, intended to extend a partial order on `α` to a linear order. -/
+def linear_extension (α : Type u) : Type u := α
+
+noncomputable instance {α : Type u} [partial_order α] : linear_order (linear_extension α) :=
+{ le := (extend_partial_order ((≤) : α → α → Prop)).some,
+  le_refl := (extend_partial_order ((≤) : α → α → Prop)).some_spec.some.1.1.1.1,
+  le_trans := (extend_partial_order ((≤) : α → α → Prop)).some_spec.some.1.1.2.1,
+  le_antisymm := (extend_partial_order ((≤) : α → α → Prop)).some_spec.some.1.2.1,
+  le_total := (extend_partial_order ((≤) : α → α → Prop)).some_spec.some.2.1,
+  decidable_le := classical.dec_rel _ }
+
+/-- The embedding of `α` into `linear_extension α` as a relation homomorphism. -/
+def to_linear_extension {α : Type u} [partial_order α] :
+  ((≤) : α → α → Prop) →r ((≤) : linear_extension α → linear_extension α → Prop) :=
+{ to_fun := λ x, x,
+  map_rel' := λ a b, (extend_partial_order ((≤) : α → α → Prop)).some_spec.some_spec _ _ }
+
+instance {α : Type u} [inhabited α] : inhabited (linear_extension α) :=
+⟨(default _ : α)⟩

src/order/zorn.lean

@@ -252,6 +252,17 @@ let ⟨m, hm⟩ := @exists_maximal_of_nonempty_chains_bounded α (≤) _ h (λ a
 ⟨m, λ a ha, le_antisymm (hm a ha) ha⟩
 
 theorem zorn_partial_order₀ {α : Type u} [partial_order α] (s : set α)
+  (ih : ∀ c ⊆ s, chain (≤) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) :
+  ∃ m ∈ s, ∀ z ∈ s, m ≤ z → z = m :=
+let ⟨⟨m, hms⟩, h⟩ := @zorn_partial_order {m // m ∈ s} _
+  (λ c hc,
+    let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (λ _ ⟨⟨x, hx⟩, _, h⟩, h ▸ hx)
+      (by { rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq;
+        refine hc _ hpc _ hqc (λ t, hpq (subtype.ext_iff.1 t)) })
+    in ⟨⟨ub, hubs⟩, λ ⟨y, hy⟩ hc, hub _ ⟨_, hc, rfl⟩⟩)
+in ⟨m, hms, λ z hzs hmz, congr_arg subtype.val (h ⟨z, hzs⟩ hmz)⟩
+
+theorem zorn_nonempty_partial_order₀ {α : Type u} [partial_order α] (s : set α)
   (ih : ∀ c ⊆ s, chain (≤) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub)
   (x : α) (hxs : x ∈ s) : ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m :=
 let ⟨⟨m, hms, hxm⟩, h⟩ := @zorn_partial_order {m // m ∈ s ∧ x ≤ m} _
@@ -268,34 +279,12 @@ let ⟨⟨m, hms, hxm⟩, h⟩ := @zorn_partial_order {m // m ∈ s ∧ x ≤ m}
 theorem zorn_subset {α : Type u} (S : set (set α))
   (h : ∀c ⊆ S, chain (⊆) c → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
   ∃ m ∈ S, ∀a ∈ S, m ⊆ a → a = m :=
-begin
-  letI : partial_order S := partial_order.lift subtype.val (λ _ _, subtype.ext_val),
-  have : ∀c:set S, @chain S (≤) c → ∃ub, ∀a∈c, a ≤ ub,
-  { intros c hc,
-    rcases h (subtype.val '' c) (image_subset_iff.2 _) _ with ⟨s, sS, hs⟩,
-    { exact ⟨⟨s, sS⟩, λ ⟨x, hx⟩ H, hs _ (mem_image_of_mem _ H)⟩ },
-    { rintro ⟨x, hx⟩ _, exact hx },
-    { rintro _ ⟨x, cx, rfl⟩ _ ⟨y, cy, rfl⟩ xy,
-      exact hc x cx y cy (mt (congr_arg _) xy) } },
-  rcases zorn_partial_order this with ⟨⟨m, mS⟩, hm⟩,
-  exact ⟨m, mS, λ a aS ha, congr_arg subtype.val (hm ⟨a, aS⟩ ha)⟩
-end
+zorn_partial_order₀ S h
 
-theorem zorn_subset₀ {α : Type u} (S : set (set α))
+theorem zorn_subset_nonempty {α : Type u} (S : set (set α))
   (H : ∀c ⊆ S, chain (⊆) c → c.nonempty → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) (x) (hx : x ∈ S) :
   ∃ m ∈ S, x ⊆ m ∧ ∀a ∈ S, m ⊆ a → a = m :=
-begin
-  let T := {s ∈ S | x ⊆ s},
-  rcases zorn_subset T _ with ⟨m, ⟨mS, mx⟩, hm⟩,
-  { exact ⟨m, mS, mx, λ a ha ha', hm a ⟨ha, subset.trans mx ha'⟩ ha'⟩ },
-  { intros c cT hc,
-    cases c.eq_empty_or_nonempty with c0 c0,
-    { rw c0, exact ⟨x, ⟨hx, subset.refl _⟩, λ _, false.elim⟩ },
-    { rcases H _ (subset.trans cT (sep_subset _ _)) hc c0 with ⟨ub, us, h⟩,
-      refine ⟨ub, ⟨us, _⟩, h⟩,
-      rcases c0 with ⟨s, hs⟩,
-      exact subset.trans (cT hs).2 (h _ hs) } }
-end
+zorn_nonempty_partial_order₀ _ (λ c cS hc y yc, H _ cS hc ⟨y, yc⟩) _ hx
 
 theorem chain.total {α : Type u} [preorder α]
   {c : set α} (H : chain (≤) c) :

src/ring_theory/ideal/operations.lean

@@ -452,7 +452,8 @@ theorem radical_eq_Inf (I : ideal R) :
   radical I = Inf { J : ideal R | I ≤ J ∧ is_prime J } :=
 le_antisymm (le_Inf $ λ J hJ, hJ.2.radical_le_iff.2 hJ.1) $
 λ r hr, classical.by_contradiction $ λ hri,
-let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_partial_order₀ {K : ideal R | r ∉ radical K}
+let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_nonempty_partial_order₀
+  {K : ideal R | r ∉ radical K}
   (λ c hc hcc y hyc, ⟨Sup c, λ ⟨n, hrnc⟩, let ⟨y, hyc, hrny⟩ :=
       (submodule.mem_Sup_of_directed ⟨y, hyc⟩ hcc.directed_on).1 hrnc in hc hyc ⟨n, hrny⟩,
     λ z, le_Sup⟩) I hri in

src/topology/subset_properties.lean

@@ -1138,7 +1138,7 @@ lemma is_irreducible.closure {s : set α} (h : is_irreducible s) :
 
 theorem exists_preirreducible (s : set α) (H : is_preirreducible s) :
   ∃ t : set α, is_preirreducible t ∧ s ⊆ t ∧ ∀ u, is_preirreducible u → t ⊆ u → u = t :=
-let ⟨m, hm, hsm, hmm⟩ := zorn.zorn_subset₀ {t : set α | is_preirreducible t}
+let ⟨m, hm, hsm, hmm⟩ := zorn.zorn_subset_nonempty {t : set α | is_preirreducible t}
   (λ c hc hcc hcn, let ⟨t, htc⟩ := hcn in
     ⟨⋃₀ c, λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩,
       let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy,