From 957d5dd1187ba53aa3a8b3f5d0a04525abec9cb0 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 9 Oct 2024 07:18:05 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20define=20finite=20length=20modules=20an?= =?UTF-8?q?d=20show=20equivalence=20with=20`IsNoetherian=20=E2=88=A7=20IsA?= =?UTF-8?q?rtinian`=20(#17478)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit and equivalence with the existence of a CompositionSeries. Add order-theoretic results: a simple order is finite; WellFoundedLT implies every non-top element is covered by some other element, and the dual result; WellFoundedLT + WellFoundedGT implies there exists a finite sequence from ⊥ to ⊤ with each element covering the previous one. Also generalize two proof_wanted statements about semisimple modules/rings. --- Mathlib.lean | 1 + Mathlib/Order/Atoms/Finite.lean | 9 ++-- Mathlib/Order/Cover.lean | 16 ++++++ Mathlib/Order/OrderIsoNat.lean | 17 ++++++ Mathlib/RingTheory/Artinian.lean | 2 +- Mathlib/RingTheory/FiniteLength.lean | 78 ++++++++++++++++++++++++++++ Mathlib/RingTheory/SimpleModule.lean | 2 +- 7 files changed, 120 insertions(+), 5 deletions(-) create mode 100644 Mathlib/RingTheory/FiniteLength.lean diff --git a/Mathlib.lean b/Mathlib.lean index ad184af87be01..7ba04a7c6a7f7 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3891,6 +3891,7 @@ import Mathlib.RingTheory.EssentialFiniteness import Mathlib.RingTheory.Etale.Basic import Mathlib.RingTheory.EuclideanDomain import Mathlib.RingTheory.Filtration +import Mathlib.RingTheory.FiniteLength import Mathlib.RingTheory.FinitePresentation import Mathlib.RingTheory.FiniteStability import Mathlib.RingTheory.FiniteType diff --git a/Mathlib/Order/Atoms/Finite.lean b/Mathlib/Order/Atoms/Finite.lean index c17782a493d32..93cca39127a7d 100644 --- a/Mathlib/Order/Atoms/Finite.lean +++ b/Mathlib/Order/Atoms/Finite.lean @@ -22,23 +22,26 @@ variable {α β : Type*} namespace IsSimpleOrder +variable [LE α] [BoundedOrder α] [IsSimpleOrder α] + section DecidableEq /- It is important that `IsSimpleOrder` is the last type-class argument of this instance, so that type-class inference fails quickly if it doesn't apply. -/ -instance (priority := 200) {α} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : - Fintype α := +instance (priority := 200) [DecidableEq α] : Fintype α := Fintype.ofEquiv Bool equivBool.symm end DecidableEq +instance (priority := 200) : Finite α := by classical infer_instance + end IsSimpleOrder namespace Fintype namespace IsSimpleOrder -variable [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] +variable [LE α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α] theorem univ : (Finset.univ : Finset α) = {⊤, ⊥} := by change Finset.map _ (Finset.univ : Finset Bool) = _ diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index 17ba059d015c4..cf13cbab95f7f 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -591,3 +591,19 @@ variable [Preorder α] {a b : α} simp only [wcovBy_iff_Ioo_eq, ← image_coe_Iio, bot_le, image_eq_empty, true_and, Iio_eq_empty_iff] end WithBot + +section WellFounded + +variable [Preorder α] + +lemma exists_covBy_of_wellFoundedLT [wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬ IsMax a) : + ∃ a', a ⋖ a' := by + rw [not_isMax_iff] at h + exact ⟨_, wellFounded_lt.min_mem _ h, fun a' ↦ wf.wf.not_lt_min _ h⟩ + +lemma exists_covBy_of_wellFoundedGT [wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬ IsMin a) : + ∃ a', a' ⋖ a := by + rw [not_isMin_iff] at h + exact ⟨_, wf.wf.min_mem _ h, fun a' h₁ h₂ ↦ wf.wf.not_lt_min _ h h₂ h₁⟩ + +end WellFounded diff --git a/Mathlib/Order/OrderIsoNat.lean b/Mathlib/Order/OrderIsoNat.lean index 5eddb07567f64..da0fabb452ad3 100644 --- a/Mathlib/Order/OrderIsoNat.lean +++ b/Mathlib/Order/OrderIsoNat.lean @@ -232,3 +232,20 @@ theorem WellFounded.iSup_eq_monotonicSequenceLimit [CompleteLattice α] · cases' WellFounded.monotone_chain_condition'.1 h a with n hn have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk) exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge + +theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α) [Preorder α] + [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] : + ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1) := by + choose next hnext using exists_covBy_of_wellFoundedLT (α := α) + have hα := Set.nonempty_iff_univ_nonempty.mp ‹_› + classical + let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha + refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ hα trivial, ?_⟩ + have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by + change a n ⋖ if ha : IsMax (a n) then a n else _ + rw [dif_neg hn] + exact hnext hn + have H : ∃ n, IsMax (a n) := by + by_contra! + exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded_of_decreasing_seq wfg.wf + exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ fun h' ↦ wellFounded_lt.not_lt_min _ H h' h⟩ diff --git a/Mathlib/RingTheory/Artinian.lean b/Mathlib/RingTheory/Artinian.lean index e3f2bcd132e70..9e43f7cbc62b9 100644 --- a/Mathlib/RingTheory/Artinian.lean +++ b/Mathlib/RingTheory/Artinian.lean @@ -522,7 +522,7 @@ instance [IsReduced R] : DecompositionMonoid (Polynomial R) := theorem isSemisimpleRing_of_isReduced [IsReduced R] : IsSemisimpleRing R := (equivPi R).symm.isSemisimpleRing -proof_wanted IsSemisimpleRing.isArtinianRing (R : Type*) [CommRing R] [IsSemisimpleRing R] : +proof_wanted IsSemisimpleRing.isArtinianRing (R : Type*) [Ring R] [IsSemisimpleRing R] : IsArtinianRing R end IsArtinianRing diff --git a/Mathlib/RingTheory/FiniteLength.lean b/Mathlib/RingTheory/FiniteLength.lean new file mode 100644 index 0000000000000..d0305806bd193 --- /dev/null +++ b/Mathlib/RingTheory/FiniteLength.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2024 Junyan Xu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Junyan Xu +-/ +import Mathlib.Order.Atoms.Finite +import Mathlib.RingTheory.Artinian + +/-! +# Modules of finite length + +We define modules of finite length (`IsFiniteLength`) to be finite iterated extensions of +simple modules, and show that a module is of finite length iff it is both Noetherian and Artinian, +iff it admits a composition series. +We do not make `IsFiniteLength` a class, instead we use `[IsNoetherian R M] [IsArtinian R M]`. + +## Tag + +Finite length, Composition series +-/ + +universe u + +variable (R : Type*) [Ring R] + +/-- A module of finite length is either trivial or a simple extension of a module known +to be of finite length. -/ +inductive IsFiniteLength : ∀ (M : Type u) [AddCommGroup M] [Module R M], Prop + | of_subsingleton {M} [AddCommGroup M] [Module R M] [Subsingleton M] : IsFiniteLength M + | of_simple_quotient {M} [AddCommGroup M] [Module R M] {N : Submodule R M} + [IsSimpleModule R (M ⧸ N)] : IsFiniteLength N → IsFiniteLength M + +variable {R} {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] + +theorem LinearEquiv.isFiniteLength (e : M ≃ₗ[R] N) + (h : IsFiniteLength R M) : IsFiniteLength R N := by + induction' h with M _ _ _ M _ _ S _ _ ih generalizing N + · have := e.symm.toEquiv.subsingleton; exact .of_subsingleton + · have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) := + IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm + exact .of_simple_quotient (ih <| e.submoduleMap S) + +variable (R M) in +theorem exists_compositionSeries_of_isNoetherian_isArtinian [IsNoetherian R M] [IsArtinian R M] : + ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := by + obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M) + exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩ + +theorem isFiniteLength_of_exists_compositionSeries + (h : ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤) : + IsFiniteLength R M := + Submodule.topEquiv.isFiniteLength <| by + obtain ⟨s, s_head, s_last⟩ := h + rw [← s_last] + suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _) + intro i + induction' i using Fin.induction with i ih + · change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton + let cov := s.step i + have := (covBy_iff_quot_is_simple cov.le).mp cov + have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective + _ (Submodule.injective_subtype _) + rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this + exact .of_simple_quotient (this.symm.isFiniteLength ih) + +theorem isFiniteLength_iff_isNoetherian_isArtinian : + IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M := + ⟨fun h ↦ h.rec (fun {M} _ _ _ ↦ ⟨inferInstance, inferInstance⟩) fun M _ _ {N} _ _ ⟨_, _⟩ ↦ + ⟨(isNoetherian_iff_submodule_quotient N).mpr ⟨‹_›, isNoetherian_iff'.mpr inferInstance⟩, + (isArtinian_iff_submodule_quotient N).mpr ⟨‹_›, inferInstance⟩⟩, + fun ⟨_, _⟩ ↦ isFiniteLength_of_exists_compositionSeries + (exists_compositionSeries_of_isNoetherian_isArtinian R M)⟩ + +theorem isFiniteLength_iff_exists_compositionSeries : + IsFiniteLength R M ↔ ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := + ⟨fun h ↦ have ⟨_, _⟩ := isFiniteLength_iff_isNoetherian_isArtinian.mp h + exists_compositionSeries_of_isNoetherian_isArtinian R M, + isFiniteLength_of_exists_compositionSeries⟩ diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean index 86e5d7e807588..9a27c4b72d304 100644 --- a/Mathlib/RingTheory/SimpleModule.lean +++ b/Mathlib/RingTheory/SimpleModule.lean @@ -338,7 +338,7 @@ variable (ι R) proof_wanted IsSemisimpleRing.mulOpposite [IsSemisimpleRing R] : IsSemisimpleRing Rᵐᵒᵖ -proof_wanted IsSemisimpleRing.module_end [IsSemisimpleRing R] [Module.Finite R M] : +proof_wanted IsSemisimpleRing.module_end [IsSemisimpleModule R M] [Module.Finite R M] : IsSemisimpleRing (Module.End R M) proof_wanted IsSemisimpleRing.matrix [Fintype ι] [DecidableEq ι] [IsSemisimpleRing R] :