From 19100ecba2f385ba62bf76aeecb8831c93a2444b Mon Sep 17 00:00:00 2001 From: kckennylau Date: Thu, 8 Nov 2018 18:42:11 +0000 Subject: [PATCH] chore(*): clean up uses of zorn --- analysis/metric_space.lean | 2 +- analysis/topology/topological_space.lean | 32 ++++++++++------------- linear_algebra/basic.lean | 2 +- linear_algebra/basis.lean | 2 +- logic/schroeder_bernstein.lean | 29 +++++++-------------- order/order_iso.lean | 12 --------- order/zorn.lean | 33 ++++++++++++++---------- ring_theory/ideal_operations.lean | 12 ++++----- ring_theory/ideals.lean | 23 +++++------------ 9 files changed, 59 insertions(+), 88 deletions(-) diff --git a/analysis/metric_space.lean b/analysis/metric_space.lean index 628f8a3c2ebfa..53fb967642201 100644 --- a/analysis/metric_space.lean +++ b/analysis/metric_space.lean @@ -654,7 +654,7 @@ instance complete_of_proper {α : Type u} [metric_space α] [proper_space α] : intros f hf, /-We want to show that the Cauchy filter `f` is converging. It suffices to find a closed ball (therefore compact by properness) where it is nontrivial.-/ - have A : ∃ t ∈ f.sets, ∀ x y ∈ t, dist x y < 1 := (cauchy_of_metric.1 hf).2 1 (by norm_num), + have A : ∃ t ∈ f.sets, ∀ x y ∈ t, dist x y < 1 := (cauchy_of_metric.1 hf).2 1 zero_lt_one, rcases A with ⟨t, ⟨t_fset, ht⟩⟩, rcases inhabited_of_mem_sets hf.1 t_fset with ⟨x, xt⟩, have : t ⊆ closed_ball x 1 := by intros y yt; simp [dist_comm]; apply le_of_lt (ht x y xt yt), diff --git a/analysis/topology/topological_space.lean b/analysis/topology/topological_space.lean index ac3fb34500d80..cd571605d93fc 100644 --- a/analysis/topology/topological_space.lean +++ b/analysis/topology/topological_space.lean @@ -696,24 +696,20 @@ let ⟨r, hrs, hruv⟩ := H u v hu hv ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in theorem exists_irreducible (s : set α) (H : is_irreducible s) : ∃ t : set α, is_irreducible t ∧ s ⊆ t ∧ ∀ u, is_irreducible u → t ⊆ u → u = t := -let ⟨⟨m, hsm, hm⟩, hm_max⟩ := @zorn.zorn { t | s ⊆ t ∧ is_irreducible t } (subrel (⊆) _) - (λ c hchain, classical.by_cases - (assume hc : c = ∅, ⟨⟨s, set.subset.refl s, H⟩, λ ⟨t, hsx, hx⟩, - hc.symm ▸ false.elim⟩) - (assume hc : c ≠ ∅, let ⟨⟨x, hsx, hx⟩, hxc⟩ := exists_mem_of_ne_empty hc in - ⟨⟨⋃ t ∈ c, subtype.val t, λ z hz, mem_bUnion hxc (hsx hz), λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩, - let ⟨p, hpc, hyp⟩ := mem_bUnion_iff.1 hy, - ⟨q, hqc, hzq⟩ := mem_bUnion_iff.1 hz in - or.cases_on (zorn.chain.total hchain hpc hqc) - (assume hpq : p.1 ⊆ q.1, let ⟨x, hxp, hxuv⟩ := q.2.2 u v hu hv - ⟨y, hpq hyp, hyu⟩ ⟨z, hzq, hzv⟩ in - ⟨x, mem_bUnion hqc hxp, hxuv⟩) - (assume hqp : q.1 ⊆ p, let ⟨x, hxp, hxuv⟩ := p.2.2 u v hu hv - ⟨y, hyp, hyu⟩ ⟨z, hqp hzq, hzv⟩ in - ⟨x, mem_bUnion hpc hxp, hxuv⟩)⟩, - λ ⟨p, hsp, hp⟩ hpc z hzp, mem_bUnion hpc hzp⟩)) - (λ _ _ _, set.subset.trans) in -⟨m, hm, hsm, λ u hu hmu, subset.antisymm (hm_max ⟨_, set.subset.trans hsm hmu, hu⟩ hmu) hmu⟩ +let ⟨m, hm, hsm, hmm⟩ := zorn.zorn_subset₀ { t : set α | is_irreducible t } + (λ c hc hcc hcn, let ⟨t, htc⟩ := exists_mem_of_ne_empty hcn in + ⟨⋃₀ c, λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩, + let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy, + ⟨q, hqc, hzq⟩ := mem_sUnion.1 hz in + or.cases_on (zorn.chain.total hcc hpc hqc) + (assume hpq : p ⊆ q, let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv + ⟨y, hpq hyp, hyu⟩ ⟨z, hzq, hzv⟩ in + ⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩) + (assume hqp : q ⊆ p, let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv + ⟨y, hyp, hyu⟩ ⟨z, hqp hzq, hzv⟩ in + ⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩), + λ x hxc, set.subset_sUnion_of_mem hxc⟩) s H in +⟨m, hm, hsm, λ u hu hmu, hmm _ hu hmu⟩ def irreducible_component (x : α) : set α := classical.some (exists_irreducible {x} is_irreducible_singleton) diff --git a/linear_algebra/basic.lean b/linear_algebra/basic.lean index 076061b85cfdb..79d38d5dedcf8 100644 --- a/linear_algebra/basic.lean +++ b/linear_algebra/basic.lean @@ -7,7 +7,7 @@ Basics of linear algebra. This sets up the "categorical/lattice structure" of modules, submodules, and linear maps. -/ -import algebra.pi_instances order.zorn data.set.finite data.finsupp order.order_iso +import algebra.pi_instances data.finsupp order.order_iso open function lattice diff --git a/linear_algebra/basis.lean b/linear_algebra/basis.lean index f668b2b1c05bc..5df6b723e5bb1 100644 --- a/linear_algebra/basis.lean +++ b/linear_algebra/basis.lean @@ -21,7 +21,7 @@ We define the following concepts: * `is_basis.constr s g`: constructs a `linear_map` by extending `g` from the basis `s` -/ -import linear_algebra.lc +import linear_algebra.lc order.zorn noncomputable theory open function lattice set submodule diff --git a/logic/schroeder_bernstein.lean b/logic/schroeder_bernstein.lean index 52a4f5a0c00c4..27b4b3576cd14 100644 --- a/logic/schroeder_bernstein.lean +++ b/logic/schroeder_bernstein.lean @@ -92,36 +92,27 @@ end antisymm section wo parameters {ι : Type u} {β : ι → Type v} -private def sets := {s : set (∀ i, β i) // +@[reducible] private def sets := {s : set (∀ i, β i) | ∀ (x ∈ s) (y ∈ s) i, (x : ∀ i, β i) i = y i → x = y} -private def sets.partial_order : partial_order sets := -{ le := λ s t, s.1 ⊆ t.1, - le_refl := λ s, subset.refl _, - le_trans := λ s t u, subset.trans, - le_antisymm := λ s t h₁ h₂, subtype.eq (subset.antisymm h₁ h₂) } - -local attribute [instance] sets.partial_order - theorem injective_min (I : nonempty ι) : ∃ i, nonempty (∀ j, β i ↪ β j) := -let ⟨⟨s, hs⟩, ms⟩ := show ∃s:sets, ∀a, s ≤ a → a = s, from - zorn.zorn_partial_order $ λ c hc, - ⟨⟨⋃₀ (subtype.val '' c), - λ x ⟨_, ⟨⟨s, hs⟩, sc, rfl⟩, xs⟩ y ⟨_, ⟨⟨t, ht⟩, tc, rfl⟩, yt⟩, - (hc.total sc tc).elim (λ h, ht _ (h xs) _ yt) (λ h, hs _ xs _ (h yt))⟩, - λ ⟨s, hs⟩ sc x h, ⟨s, ⟨⟨s, hs⟩, sc, rfl⟩, h⟩⟩ in +let ⟨s, hs, ms⟩ := show ∃s∈sets, ∀a∈sets, s ⊆ a → a = s, from + zorn.zorn_subset sets (λ c hc hcc, ⟨⋃₀ c, + λ x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ i hi, + (hcc.total hpc hqc).elim (λ h, hc hqc x (h hxp) y hyq i hi) (λ h, hc hpc x hxp y (h hyq) i hi), + λ _, subset_sUnion_of_mem⟩) in let ⟨i, e⟩ := show ∃ i, ∀ y, ∃ x ∈ s, (x : ∀ i, β i) i = y, from classical.by_contradiction $ λ h, have h : ∀ i, ∃ y, ∀ x ∈ s, (x : ∀ i, β i) i ≠ y, - by simpa [classical.not_forall] using h, + by simpa only [not_exists, classical.not_forall] using h, let ⟨f, hf⟩ := axiom_of_choice h in - have f ∈ (⟨s, hs⟩:sets).1, from - let s' : sets := ⟨insert f s, λ x hx y hy, begin + have f ∈ s, from + have insert f s ∈ sets := λ x hx y hy, begin cases hx; cases hy, {simp [hx, hy]}, { subst x, exact λ i e, (hf i y hy e.symm).elim }, { subst y, exact λ i e, (hf i x hx e).elim }, { exact hs x hx y hy } - end⟩ in ms s' (subset_insert f s) ▸ mem_insert _ _, + end, ms _ this (subset_insert f s) ▸ mem_insert _ _, let ⟨i⟩ := I in hf i f this rfl in let ⟨f, hf⟩ := axiom_of_choice e in ⟨i, ⟨λ j, ⟨λ a, f a j, λ a b e', diff --git a/order/order_iso.lean b/order/order_iso.lean index 025e8a80620bb..02544e436e616 100644 --- a/order/order_iso.lean +++ b/order/order_iso.lean @@ -289,18 +289,6 @@ instance (r : α → α → Prop) [is_well_order α r] (p : set α) : is_well_order p (subrel r p) := order_embedding.is_well_order (subrel.order_embedding r p) -instance [preorder α] (p : set α) : preorder p := -⟨subrel (≤) p, subrel (<) p, λ _, le_refl _, λ _ _ _, le_trans, -λ _ _, lt_iff_le_not_le⟩ - -instance [partial_order α] (p : set α) : partial_order p := -{ le_antisymm := λ _ _ hab hba, subtype.eq $ le_antisymm hab hba, - .. (infer_instance : preorder p) } - -instance [linear_order α] (p : set α) : linear_order p := -{ le_total := λ _ _, le_total _ _, - .. (infer_instance : partial_order p) } - end subrel /-- Restrict the codomain of an order embedding -/ diff --git a/order/zorn.lean b/order/zorn.lean index c4dea3fdf8bba..c9079e42fd1ec 100644 --- a/order/zorn.lean +++ b/order/zorn.lean @@ -225,19 +225,26 @@ theorem zorn_partial_order {α : Type u} [partial_order α] let ⟨m, hm⟩ := @zorn α (≤) h (assume a b c, le_trans) in ⟨m, assume a ha, le_antisymm (hm a ha) ha⟩ -theorem zorn_partial_order₀ {α : Type u} [partial_order α] - (s : set α) (x : α) (hxs : x ∈ s) - (ih : ∀ c ⊆ s, zorn.chain (≤) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) : - ∃ m ∈ s, ∀ z ∈ s, m ≤ z → z = m := -let ⟨m, hm⟩ := @zorn.zorn_partial_order s (subrel.partial_order s) - (λ c hc, classical.by_cases - (assume hce : c = ∅, hce.symm ▸ ⟨⟨x, hxs⟩, λ _, false.elim⟩) - (assume hce : c ≠ ∅, let ⟨m, hmc⟩ := set.exists_mem_of_ne_empty hce in - let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (set.image_subset_iff.2 $ λ z hz, z.2) - (by rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq; - exact hc p hpc q hqc (mt (by rintro rfl; refl) hpq)) m.1 ⟨m, hmc, rfl⟩ in - ⟨⟨ub, hubs⟩, λ a hac, hub a.1 ⟨a, hac, rfl⟩⟩)) in -⟨m.1, m.2, λ z hz hmz, congr_arg subtype.val $ hm ⟨z, hz⟩ hmz⟩ +theorem zorn_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} _ (λ c hc, classical.by_cases + (assume hce : c = ∅, hce.symm ▸ ⟨⟨x, hxs, le_refl _⟩, λ _, false.elim⟩) + (assume hce : c ≠ ∅, let ⟨m, hmc⟩ := set.exists_mem_of_ne_empty hce in + let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (image_subset_iff.2 $ λ z hzc, z.2.1) + (by rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq; + exact hc p hpc q hqc (mt (by rintro rfl; refl) hpq)) m.1 (mem_image_of_mem _ hmc) in + ⟨⟨ub, hubs, le_trans m.2.2 $ hub m.1 $ mem_image_of_mem _ hmc⟩, λ a hac, hub a.1 ⟨a, hac, rfl⟩⟩)) in +⟨m, hms, hxm, λ z hzs hmz, congr_arg subtype.val $ h ⟨z, hzs, le_trans hxm hmz⟩ hmz⟩ + +/-let ⟨m, hm⟩ := @zorn.zorn_partial_order s _ (λ c hc, classical.by_cases + (assume hce : c = ∅, hce.symm ▸ ⟨⟨x, hxs⟩, λ _, false.elim⟩) + (assume hce : c ≠ ∅, let ⟨m, hmc⟩ := set.exists_mem_of_ne_empty hce in + let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (set.image_subset_iff.2 $ λ z hz, z.2) + (by rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq; + exact hc p hpc q hqc (mt (by rintro rfl; refl) hpq)) m.1 ⟨m, hmc, rfl⟩ in + ⟨⟨ub, hubs⟩, λ a hac, hub a.1 ⟨a, hac, rfl⟩⟩)) in +⟨m.1, m.2, λ z hz hmz, congr_arg subtype.val $ hm ⟨z, hz⟩ hmz⟩-/ theorem zorn_subset {α : Type u} (S : set (set α)) (h : ∀c ⊆ S, chain (⊆) c → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) : diff --git a/ring_theory/ideal_operations.lean b/ring_theory/ideal_operations.lean index 913ef101a79a6..561bf70e90fa9 100644 --- a/ring_theory/ideal_operations.lean +++ b/ring_theory/ideal_operations.lean @@ -280,14 +280,12 @@ 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 S := { J | I ≤ J ∧ is_prime J } in -let ⟨m, ⟨him, hrm⟩, hm⟩ := zorn.zorn_partial_order₀ { K | I ≤ K ∧ r ∉ radical K } I ⟨le_refl _, hri⟩ - (λ c hc1 hc2 y hyc, ⟨Sup c, ⟨le_Sup_of_le hyc (hc1 hyc).1, λ ⟨n, hrnc⟩, - let ⟨y, hyc, hrny⟩ := submodule.mem_Sup_of_directed hrnc y hyc hc2.directed_on in - (hc1 hyc).2 ⟨n, hrny⟩⟩, λ _, le_Sup⟩) in +let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_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 hrnc y hyc hcc.directed_on in hc hyc ⟨n, hrny⟩, + λ z, le_Sup⟩) I hri in have ∀ x ∉ m, r ∈ radical (m ⊔ span {x}) := λ x hxm, classical.by_contradiction $ λ hrmx, hxm $ - have _ := hm (m ⊔ span {x}) ⟨le_trans him le_sup_left, hrmx⟩ le_sup_left, - this ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _), + hm (m ⊔ span {x}) hrmx le_sup_left ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _), have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial, λ x y hxym, classical.or_iff_not_imp_left.2 $ λ hxm, classical.by_contradiction $ λ hym, let ⟨n, hrn⟩ := this _ hxm, ⟨p, hpm, q, hq, hpqrn⟩ := submodule.mem_sup.1 hrn, ⟨c, hcxq⟩ := mem_span_singleton'.1 hq in diff --git a/ring_theory/ideals.lean b/ring_theory/ideals.lean index b7a3665af2425..9b90719067196 100644 --- a/ring_theory/ideals.lean +++ b/ring_theory/ideals.lean @@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Chris Hughes, Mario Carneiro -/ -import tactic.ring linear_algebra.basic ring_theory.associated +import linear_algebra.basic ring_theory.associated order.zorn universes u v variables {α : Type u} {β : Type v} [comm_ring α] {a b : α} @@ -133,22 +133,13 @@ instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prim theorem exists_le_maximal (I : ideal α) (hI : I ≠ ⊤) : ∃ M : ideal α, M.is_maximal ∧ I ≤ M := begin - let C : set (set α) := {s | ∃ J:ideal α, J ≠ ⊤ ∧ ↑J = s}, - rcases zorn.zorn_subset₀ C _ _ ⟨I, hI, rfl⟩ with ⟨_, ⟨M, M0, rfl⟩, IM, h⟩, + rcases zorn.zorn_partial_order₀ { J : ideal α | J ≠ ⊤ } _ I hI with ⟨M, M0, IM, h⟩, { refine ⟨M, ⟨M0, λ J hJ, by_contradiction $ λ J0, _⟩, IM⟩, - cases lt_iff_le_not_le.1 hJ with hJ₁ hJ₂, - exact hJ₂ (le_of_eq (h _ ⟨_, J0, rfl⟩ hJ₁) : _) }, - { intros S SC cC S0, - choose I hp using show ∀ x : S, ↑x ∈ C, from λ ⟨x, xs⟩, SC xs, - refine ⟨_, ⟨⨆ s:S, span s, _, rfl⟩, _⟩, - rw [ne_top_iff_one, submodule.mem_supr_of_directed - (coe_nonempty_iff_ne_empty.2 S0), not_exists], - { rintro ⟨_, xs⟩, rcases SC xs with ⟨J, J0, rfl⟩, - simp, exact J.ne_top_iff_one.1 J0 }, - { rintro ⟨i, iS⟩ ⟨j, jS⟩, - rcases cC.directed iS jS with ⟨k, kS, ik, jk⟩, - exact ⟨⟨_, kS⟩, span_mono ik, span_mono jk⟩ }, - { exact λ s ss, span_le.1 (le_supr (λ s:S, span (s:set α)) ⟨s, ss⟩) } }, + cases h J J0 (le_of_lt hJ), exact lt_irrefl _ hJ }, + { intros S SC cC I IS, + refine ⟨Sup S, λ H, _, λ _, le_Sup⟩, + rcases submodule.mem_Sup_of_directed ((eq_top_iff_one _).1 H) I IS cC.directed_on with ⟨J, JS, J0⟩, + exact SC JS ((eq_top_iff_one _).2 J0) } end end ideal