feat(category_theory/noetherian): nonzero artinian objects have simpl…

…e subobjects (#13972)

# Artinian and noetherian categories

An artinian category is a category in which objects do not
have infinite decreasing sequences of subobjects.

A noetherian category is a category in which objects do not
have infinite increasing sequences of subobjects.

We show that any nonzero artinian object has a simple subobject.

## Future work
The Jordan-Hölder theorem, following https://stacks.math.columbia.edu/tag/0FCK.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/noetherian.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.subobject.lattice
+import category_theory.essentially_small
+import category_theory.simple
+
+/-!
+# Artinian and noetherian categories
+
+An artinian category is a category in which objects do not
+have infinite decreasing sequences of subobjects.
+
+A noetherian category is a category in which objects do not
+have infinite increasing sequences of subobjects.
+
+We show that any nonzero artinian object has a simple subobject.
+
+## Future work
+The Jordan-Hölder theorem, following https://stacks.math.columbia.edu/tag/0FCK.
+-/
+
+namespace category_theory
+open category_theory.limits
+
+variables {C : Type*} [category C]
+
+/--
+A noetherian object is an object
+which does not have infinite increasing sequences of subobjects.
+
+See https://stacks.math.columbia.edu/tag/0FCG
+-/
+class noetherian_object (X : C) : Prop :=
+(subobject_gt_well_founded : well_founded ((>) : subobject X → subobject X → Prop))
+
+/--
+An artinian object is an object
+which does not have infinite decreasing sequences of subobjects.
+
+See https://stacks.math.columbia.edu/tag/0FCF
+-/
+class artinian_object (X : C) : Prop :=
+(subobject_lt_well_founded [] : well_founded ((<) : subobject X → subobject X → Prop))
+
+variables (C)
+
+/-- A category is noetherian if it is essentially small and all objects are noetherian. -/
+class noetherian extends essentially_small C :=
+(noetherian_object : ∀ (X : C), noetherian_object X)
+
+attribute [priority 100, instance] noetherian.noetherian_object
+
+/-- A category is artinian if it is essentially small and all objects are artinian. -/
+class artinian extends essentially_small C :=
+(artinian_object : ∀ (X : C), artinian_object X)
+
+attribute [priority 100, instance] artinian.artinian_object
+
+variables {C}
+
+open subobject
+variables [has_zero_morphisms C] [has_zero_object C]
+
+lemma exists_simple_subobject {X : C} [artinian_object X] (h : ¬ is_zero X) :
+  ∃ (Y : subobject X), simple (Y : C) :=
+begin
+  haveI : nontrivial (subobject X) := nontrivial_of_not_is_zero h,
+  haveI := is_atomic_of_order_bot_well_founded_lt (artinian_object.subobject_lt_well_founded X),
+  have := is_atomic.eq_bot_or_exists_atom_le (⊤ : subobject X),
+  obtain ⟨Y, s⟩ := (is_atomic.eq_bot_or_exists_atom_le (⊤ : subobject X)).resolve_left top_ne_bot,
+  exact ⟨Y, (subobject_simple_iff_is_atom _).mpr s.1⟩,
+end
+
+/-- Choose an arbitrary simple subobject of a non-zero artinian object. -/
+noncomputable def simple_subobject {X : C} [artinian_object X] (h : ¬ is_zero X) : C :=
+(exists_simple_subobject h).some
+
+/-- The monomorphism from the arbitrary simple subobject of a non-zero artinian object. -/
+@[derive mono]
+noncomputable def simple_subobject_arrow {X : C} [artinian_object X] (h : ¬ is_zero X) :
+  simple_subobject h ⟶ X :=
+(exists_simple_subobject h).some.arrow
+
+instance {X : C} [artinian_object X] (h : ¬ is_zero X) : simple (simple_subobject h) :=
+(exists_simple_subobject h).some_spec
+
+end category_theory

src/category_theory/simple.lean

@@ -216,10 +216,7 @@ open_locale zero_object
 open subobject
 
 instance {X : C} [simple X] : nontrivial (subobject X) :=
-⟨⟨mk (0 : 0 ⟶ X), mk (𝟙 X), λ h, begin
-  haveI := simple.of_iso (iso_of_mk_eq_mk _ _ h),
-  exact zero_not_simple C,
-end⟩⟩
+nontrivial_of_not_is_zero (simple.not_is_zero X)
 
 instance {X : C} [simple X] : is_simple_order (subobject X) :=
 { eq_bot_or_eq_top := begin
@@ -251,6 +248,12 @@ lemma simple_iff_subobject_is_simple_order (X : C) : simple X ↔ is_simple_orde
 ⟨by { introI h, apply_instance, },
  by { introI h, exact simple_of_is_simple_order_subobject X, }⟩
 
+/-- A subobject is simple iff it is an atom in the subobject lattice. -/
+lemma subobject_simple_iff_is_atom {X : C} (Y : subobject X) : simple (Y : C) ↔ is_atom Y :=
+(simple_iff_subobject_is_simple_order _).trans
+  ((order_iso.is_simple_order_iff (subobject_order_iso Y)).trans
+    set.is_simple_order_Iic_iff_is_atom)
+
 end subobject
 
 end category_theory

src/category_theory/subobject/lattice.lean

@@ -674,6 +674,35 @@ instance {B : C} : complete_lattice (subobject B) :=
 
 end complete_lattice
 
+section zero_object
+variables [has_zero_morphisms C] [has_zero_object C]
+open_locale zero_object
+
+/-- A nonzero object has nontrivial subobject lattice. -/
+lemma nontrivial_of_not_is_zero {X : C} (h : ¬ is_zero X) : nontrivial (subobject X) :=
+⟨⟨mk (0 : 0 ⟶ X), mk (𝟙 X), λ w, h (is_zero.of_iso (is_zero_zero C) (iso_of_mk_eq_mk _ _ w).symm)⟩⟩
+
+end zero_object
+
+section subobject_subobject
+
+/-- The subobject lattice of a subobject `Y` is order isomorphic to the interval `set.Iic Y`. -/
+def subobject_order_iso {X : C} (Y : subobject X) : subobject (Y : C) ≃o set.Iic Y :=
+{ to_fun := λ Z, ⟨subobject.mk (Z.arrow ≫ Y.arrow),
+    set.mem_Iic.mpr (le_of_comm ((underlying_iso _).hom ≫ Z.arrow) (by simp))⟩,
+  inv_fun := λ Z, subobject.mk (of_le _ _ Z.2),
+  left_inv := λ Z, mk_eq_of_comm _ (underlying_iso _) (by { ext, simp, }),
+  right_inv := λ Z, subtype.ext (mk_eq_of_comm _ (underlying_iso _)
+    (by { dsimp, simp [←iso.eq_inv_comp], })),
+  map_rel_iff' := λ W Z,
+    ⟨λ h, le_of_comm
+      ((underlying_iso _).inv ≫ of_le _ _ (subtype.mk_le_mk.mp h) ≫ (underlying_iso _).hom)
+      (by { ext, simp, }),
+     λ h, subtype.mk_le_mk.mpr
+       (le_of_comm ((underlying_iso _).hom ≫ of_le _ _ h ≫ (underlying_iso _).inv) (by simp))⟩, }
+
+end subobject_subobject
+
 end subobject
 
 end category_theory