From 210657c4ea4a4a7b234392f70a3a2a83346dfa90 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Fri, 31 Mar 2023 22:20:08 +0000 Subject: [PATCH] refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'` (#15071) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The predicate `x ≤ y → y = x` is no more convenient than `¬ x < y`. For this reason, we ditch `well_founded.well_founded_iff_has_min'` and `well_founded.well_founded_iff_has_max'` in favor of `well_founded.well_founded_iff_has_min` (or in some cases, just `well_founded.has_min`. We also remove the misplaced lemma `well_founded.eq_iff_not_lt_of_le`, and we golf the theorems that used the removed theorems. The lemma `well_founded.well_founded_iff_has_min` has a misleading name when applied on `well_founded (>)`, and mildly screws over dot notation and rewriting by virtue of using `>`, but a future refactor will fix this. --- src/algebra/lie/engel.lean | 7 ++----- src/linear_algebra/free_module/pid.lean | 18 ++++++++--------- src/order/basic.lean | 3 +++ src/order/compactly_generated.lean | 22 ++++++++++----------- src/order/order_iso_nat.lean | 18 +++++------------ src/order/well_founded.lean | 20 ------------------- src/ring_theory/artinian.lean | 17 ++++++++-------- src/ring_theory/ideal/associated_prime.lean | 2 +- src/ring_theory/noetherian.lean | 18 ++++++++--------- 9 files changed, 45 insertions(+), 80 deletions(-) diff --git a/src/algebra/lie/engel.lean b/src/algebra/lie/engel.lean index fa9f351cae10e..23045db7fcb71 100644 --- a/src/algebra/lie/engel.lean +++ b/src/algebra/lie/engel.lean @@ -259,14 +259,11 @@ begin exact nontrivial_max_triv_of_is_nilpotent R K (L' ⧸ K.to_lie_submodule), }, haveI _i5 : is_noetherian R L' := is_noetherian_of_surjective L _ (linear_map.range_range_restrict (to_endomorphism R L M)), - obtain ⟨K, hK₁, hK₂⟩ := - well_founded.well_founded_iff_has_max'.mp (lie_subalgebra.well_founded_of_noetherian R L') s hs, + obtain ⟨K, hK₁, hK₂⟩ := (lie_subalgebra.well_founded_of_noetherian R L').has_min s hs, have hK₃ : K = ⊤, { by_contra contra, obtain ⟨K', hK'₁, hK'₂⟩ := this K hK₁ contra, - specialize hK₂ K' hK'₁ (le_of_lt hK'₂), - replace hK'₂ := (ne_of_lt hK'₂).symm, - contradiction, }, + exact hK₂ K' hK'₁ hK'₂, }, exact hK₃ ▸ hK₁, end diff --git a/src/linear_algebra/free_module/pid.lean b/src/linear_algebra/free_module/pid.lean index d975fcb650678..9f54c0e2859e8 100644 --- a/src/linear_algebra/free_module/pid.lean +++ b/src/linear_algebra/free_module/pid.lean @@ -59,7 +59,7 @@ variables {ι : Type*} (b : basis ι R M) open submodule.is_principal submodule lemma eq_bot_of_generator_maximal_map_eq_zero (b : basis ι R M) {N : submodule R M} - {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), N.map ϕ ≤ N.map ψ → N.map ψ = N.map ϕ) + {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), ¬ N.map ϕ < N.map ψ) [(N.map ϕ).is_principal] (hgen : generator (N.map ϕ) = (0 : R)) : N = ⊥ := begin rw submodule.eq_bot_iff, @@ -67,13 +67,13 @@ begin refine b.ext_elem (λ i, _), rw (eq_bot_iff_generator_eq_zero _).mpr hgen at hϕ, rw [linear_equiv.map_zero, finsupp.zero_apply], - exact (submodule.eq_bot_iff _).mp (hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr) bot_le) _ ⟨x, hx, rfl⟩ + exact (submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 $ hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr)) _ + ⟨x, hx, rfl⟩ end lemma eq_bot_of_generator_maximal_submodule_image_eq_zero {N O : submodule R M} (b : basis ι R O) (hNO : N ≤ O) - {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ϕ.submodule_image N ≤ ψ.submodule_image N → - ψ.submodule_image N = ϕ.submodule_image N) + {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ ϕ.submodule_image N < ψ.submodule_image N) [(ϕ.submodule_image N).is_principal] (hgen : generator (ϕ.submodule_image N) = 0) : N = ⊥ := begin @@ -82,7 +82,7 @@ begin refine congr_arg coe (show (⟨x, hNO hx⟩ : O) = 0, from b.ext_elem (λ i, _)), rw (eq_bot_iff_generator_eq_zero _).mpr hgen at hϕ, rw [linear_equiv.map_zero, finsupp.zero_apply], - refine (submodule.eq_bot_iff _).mp (hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr) bot_le) _ _, + refine (submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 $ hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr)) _ _, exact (linear_map.mem_submodule_image_of_le hNO).mpr ⟨x, hx, rfl⟩ end @@ -115,8 +115,7 @@ variables {M : Type*} [add_comm_group M] [module R M] {b : ι → M} open submodule.is_principal lemma generator_maximal_submodule_image_dvd {N O : submodule R M} (hNO : N ≤ O) - {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ϕ.submodule_image N ≤ ψ.submodule_image N → - ψ.submodule_image N = ϕ.submodule_image N) + {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ ϕ.submodule_image N < ψ.submodule_image N) [(ϕ.submodule_image N).is_principal] (y : M) (yN : y ∈ N) (ϕy_eq : ϕ ⟨y, hNO yN⟩ = generator (ϕ.submodule_image N)) (ψ : O →ₗ[R] R) : generator (ϕ.submodule_image N) ∣ ψ ⟨y, hNO yN⟩ := @@ -144,7 +143,7 @@ begin refine le_antisymm (this.trans (le_of_eq _)) (ideal.span_singleton_le_span_singleton.mpr d_dvd_left), rw span_singleton_generator, - refine hϕ ψ' (le_trans _ this), + apply (le_trans _ this).eq_of_not_gt (hϕ ψ'), rw [← span_singleton_generator (ϕ.submodule_image N)], exact ideal.span_singleton_le_span_singleton.mpr d_dvd_left, { exact subset_span (mem_insert _ _) } @@ -175,8 +174,7 @@ lemma submodule.basis_of_pid_aux [finite ι] {O : Type*} [add_comm_group O] [mod begin -- Let `ϕ` be a maximal projection of `M` onto `R`, in the sense that there is -- no `ψ` whose image of `N` is larger than `ϕ`'s image of `N`. - have : ∃ ϕ : M →ₗ[R] R, ∀ (ψ : M →ₗ[R] R), - ϕ.submodule_image N ≤ ψ.submodule_image N → ψ.submodule_image N = ϕ.submodule_image N, + have : ∃ ϕ : M →ₗ[R] R, ∀ (ψ : M →ₗ[R] R), ¬ ϕ.submodule_image N < ψ.submodule_image N, { obtain ⟨P, P_eq, P_max⟩ := set_has_maximal_iff_noetherian.mpr (infer_instance : is_noetherian R R) _ (show (set.range (λ ψ : M →ₗ[R] R, ψ.submodule_image N)).nonempty, diff --git a/src/order/basic.lean b/src/order/basic.lean index 708b8e3bdf4e2..f868ff486d619 100644 --- a/src/order/basic.lean +++ b/src/order/basic.lean @@ -227,6 +227,9 @@ le_iff_lt_or_eq.trans or.comm lemma lt_iff_le_and_ne [partial_order α] {a b : α} : a < b ↔ a ≤ b ∧ a ≠ b := ⟨λ h, ⟨le_of_lt h, ne_of_lt h⟩, λ ⟨h1, h2⟩, h1.lt_of_ne h2⟩ +lemma eq_iff_not_lt_of_le {α} [partial_order α] {x y : α} : x ≤ y → y = x ↔ ¬ x < y := +by rw [lt_iff_le_and_ne, not_and, not_not, eq_comm] + -- See Note [decidable namespace] protected lemma decidable.eq_iff_le_not_lt [partial_order α] [@decidable_rel α (≤)] {a b : α} : a = b ↔ a ≤ b ∧ ¬ a < b := diff --git a/src/order/compactly_generated.lean b/src/order/compactly_generated.lean index 6263ce4ff2347..47ee173833898 100644 --- a/src/order/compactly_generated.lean +++ b/src/order/compactly_generated.lean @@ -190,18 +190,16 @@ end lemma well_founded.is_Sup_finite_compact (h : well_founded ((>) : α → α → Prop)) : is_Sup_finite_compact α := -begin - intros s, - let p : set α := { x | ∃ (t : finset α), ↑t ⊆ s ∧ t.sup id = x }, - have hp : p.nonempty, { use [⊥, ∅], simp, }, - obtain ⟨m, ⟨t, ⟨ht₁, ht₂⟩⟩, hm⟩ := well_founded.well_founded_iff_has_max'.mp h p hp, - use t, simp only [ht₁, ht₂, true_and], apply le_antisymm, - { apply Sup_le, intros y hy, classical, - have hy' : (insert y t).sup id ∈ p, - { use insert y t, simp, rw set.insert_subset, exact ⟨hy, ht₁⟩, }, - have hm' : m ≤ (insert y t).sup id, { rw ← ht₂, exact finset.sup_mono (t.subset_insert y), }, - rw ← hm _ hy' hm', simp, }, - { rw [← ht₂, finset.sup_id_eq_Sup], exact Sup_le_Sup ht₁, }, +λ s, begin + obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := well_founded.well_founded_iff_has_min.mp h + {x | ∃ t : finset α, ↑t ⊆ s ∧ t.sup id = x} ⟨⊥, ∅, by simp⟩, + refine ⟨t, ht₁, (Sup_le (λ y hy, _)).antisymm _⟩, + { classical, + rw eq_of_le_of_not_lt (finset.sup_mono (t.subset_insert y)) + (hm _ ⟨insert y t, by simp [set.insert_subset, hy, ht₁]⟩), + simp }, + { rw finset.sup_id_eq_Sup, + exact Sup_le_Sup ht₁ }, end lemma is_Sup_finite_compact.is_sup_closed_compact (h : is_Sup_finite_compact α) : diff --git a/src/order/order_iso_nat.lean b/src/order/order_iso_nat.lean index 85145f7acda7c..b1221a36b6acf 100644 --- a/src/order/order_iso_nat.lean +++ b/src/order/order_iso_nat.lean @@ -226,17 +226,9 @@ a (monotonic_sequence_limit_index a) lemma well_founded.supr_eq_monotonic_sequence_limit [complete_lattice α] (h : well_founded ((>) : α → α → Prop)) (a : ℕ →o α) : supr a = monotonic_sequence_limit a := begin - suffices : (⨆ (m : ℕ), a m) ≤ monotonic_sequence_limit a, - { exact le_antisymm this (le_supr a _), }, - apply supr_le, - intros m, - by_cases hm : m ≤ monotonic_sequence_limit_index a, - { exact a.monotone hm, }, - { replace hm := le_of_not_le hm, - let S := { n | ∀ m, n ≤ m → a n = a m }, - have hInf : Inf S ∈ S, - { refine nat.Inf_mem _, rw well_founded.monotone_chain_condition at h, exact h a, }, - change Inf S ≤ m at hm, - change a m ≤ a (Inf S), - rw hInf m hm, }, + apply (supr_le (λ m, _)).antisymm (le_supr a _), + cases le_or_lt m (monotonic_sequence_limit_index a) with hm hm, + { exact a.monotone hm }, + { cases well_founded.monotone_chain_condition'.1 h a with n hn, + exact (nat.Inf_mem ⟨n, λ k hk, (a.mono hk).eq_of_not_lt (hn k hk)⟩ m hm.le).ge } end diff --git a/src/order/well_founded.lean b/src/order/well_founded.lean index 46f5f29ab47da..fb82de79a2a55 100644 --- a/src/order/well_founded.lean +++ b/src/order/well_founded.lean @@ -72,26 +72,6 @@ begin exact hm' y hy' hy end -lemma eq_iff_not_lt_of_le {α} [partial_order α] {x y : α} : x ≤ y → y = x ↔ ¬ x < y := -begin - split, - { intros xle nge, - cases le_not_le_of_lt nge, - rw xle left at nge, - exact lt_irrefl x nge }, - { intros ngt xle, - contrapose! ngt, - exact lt_of_le_of_ne xle (ne.symm ngt) } -end - -theorem well_founded_iff_has_max' [partial_order α] : (well_founded ((>) : α → α → Prop) ↔ - ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, m ≤ x → x = m) := -by simp only [eq_iff_not_lt_of_le, well_founded_iff_has_min] - -theorem well_founded_iff_has_min' [partial_order α] : (well_founded (has_lt.lt : α → α → Prop)) ↔ - ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, x ≤ m → x = m := -@well_founded_iff_has_max' αᵒᵈ _ - open set /-- The supremum of a bounded, well-founded order -/ protected noncomputable def sup {r : α → α → Prop} (wf : well_founded r) (s : set α) diff --git a/src/ring_theory/artinian.lean b/src/ring_theory/artinian.lean index e720b4146490f..ed598587452c9 100644 --- a/src/ring_theory/artinian.lean +++ b/src/ring_theory/artinian.lean @@ -181,12 +181,11 @@ end /-- A module is Artinian iff every nonempty set of submodules has a minimal submodule among them. -/ theorem set_has_minimal_iff_artinian : - (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M') ↔ - is_artinian R M := -by rw [is_artinian_iff_well_founded, well_founded.well_founded_iff_has_min'] + (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬ I < M') ↔ is_artinian R M := +by rw [is_artinian_iff_well_founded, well_founded.well_founded_iff_has_min] theorem is_artinian.set_has_minimal [is_artinian R M] (a : set $ submodule R M) (ha : a.nonempty) : - ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M' := + ∃ M' ∈ a, ∀ I ∈ a, ¬ I < M' := set_has_minimal_iff_artinian.mpr ‹_› a ha /-- A module is Artinian iff every decreasing chain of submodules stabilizes. -/ @@ -414,19 +413,19 @@ begin simpa only [this, top_smul, ideal.zero_eq_bot] using hJ }, by_contradiction hJ, change J ≠ ⊤ at hJ, rcases is_artinian.set_has_minimal {J' : ideal R | J < J'} ⟨⊤, hJ.lt_top⟩ - with ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → I ≤ J' → I = J'⟩, + with ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → ¬ I < J'⟩, rcases set_like.exists_of_lt hJJ' with ⟨x, hxJ', hxJ⟩, obtain rfl : J ⊔ ideal.span {x} = J', - { refine hJ' (J ⊔ ideal.span {x}) _ _, + { apply eq_of_le_of_not_lt _ (hJ' (J ⊔ ideal.span {x}) _), + { exact (sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))) }, { rw set_like.lt_iff_le_and_exists, - exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩ }, - { exact (sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))) } }, + exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩ } }, have : J ⊔ Jac • ideal.span {x} ≤ J ⊔ ideal.span {x}, from sup_le_sup_left (smul_le.2 (λ _ _ _, submodule.smul_mem _ _)) _, have : Jac * ideal.span {x} ≤ J, --Need version 4 of Nakayamas lemma on Stacks { classical, by_contradiction H, refine H (smul_sup_le_of_le_smul_of_le_jacobson_bot - (fg_span_singleton _) le_rfl (hJ' _ _ this).ge), + (fg_span_singleton _) le_rfl (this.eq_of_not_lt (hJ' _ _)).ge), exact lt_of_le_of_ne le_sup_left (λ h, H $ h.symm ▸ le_sup_right) }, have : ideal.span {x} * Jac ^ (n + 1) ≤ ⊥, calc ideal.span {x} * Jac ^ (n + 1) = ideal.span {x} * Jac * Jac ^ n : diff --git a/src/ring_theory/ideal/associated_prime.lean b/src/ring_theory/ideal/associated_prime.lean index 5ed07421fc294..c85ea9e010818 100644 --- a/src/ring_theory/ideal/associated_prime.lean +++ b/src/ring_theory/ideal/associated_prime.lean @@ -95,7 +95,7 @@ begin rw [smul_comm, hc, smul_zero] }, have H₂ : (submodule.span R {a • y}).annihilator ≠ ⊤, { rwa [ne.def, submodule.annihilator_eq_top_iff, submodule.span_singleton_eq_bot] }, - rwa [← h₃ (R ∙ a • y).annihilator ⟨l.trans H₁, H₂, _, rfl⟩ H₁, + rwa [H₁.eq_of_not_lt (h₃ (R ∙ a • y).annihilator ⟨l.trans H₁, H₂, _, rfl⟩), submodule.mem_annihilator_span_singleton, smul_comm, smul_smul] end diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean index d2110c7afeeca..a0067dc2d6d6f 100644 --- a/src/ring_theory/noetherian.lean +++ b/src/ring_theory/noetherian.lean @@ -253,20 +253,20 @@ begin { intro H, constructor, intro N, - obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ := well_founded.well_founded_iff_has_max'.mp + obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ := well_founded.has_min H { N' : α | N'.1 ≤ N } ⟨⟨⊥, submodule.fg_bot⟩, bot_le⟩, convert h₁, refine (e.antisymm _).symm, by_contra h₃, obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := set.not_subset.mp h₃, apply hx₂, - have := h₂ ⟨(R ∙ x) ⊔ N₀, _⟩ _ _, + have := eq_of_le_of_not_lt _ (h₂ ⟨(R ∙ x) ⊔ N₀, _⟩ _), { injection this with eq, - rw ← eq, + rw eq, exact (le_sup_left : (R ∙ x) ≤ (R ∙ x) ⊔ N₀) (submodule.mem_span_singleton_self _) }, { exact submodule.fg.sup ⟨{x}, by rw [finset.coe_singleton]⟩ h₁ }, - { exact sup_le ((submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e }, - { show N₀ ≤ (R ∙ x) ⊔ N₀, from le_sup_right } } + { show N₀ ≤ (R ∙ x) ⊔ N₀, from le_sup_right }, + { exact sup_le ((submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e } } end variables (R M) @@ -280,14 +280,12 @@ variables {R M} /-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them. -/ theorem set_has_maximal_iff_noetherian : - (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, M' ≤ I → I = M') ↔ - is_noetherian R M := -by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_max'] + (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬ M' < I) ↔ is_noetherian R M := +by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_min] /-- A module is Noetherian iff every increasing chain of submodules stabilizes. -/ theorem monotone_stabilizes_iff_noetherian : - (∀ (f : ℕ →o submodule R M), ∃ n, ∀ m, n ≤ m → f n = f m) - ↔ is_noetherian R M := + (∀ (f : ℕ →o submodule R M), ∃ n, ∀ m, n ≤ m → f n = f m) ↔ is_noetherian R M := by rw [is_noetherian_iff_well_founded, well_founded.monotone_chain_condition] /-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/