exists_simple_subobject

Mathlib.CategoryTheory.Subobject.ArtinianObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.exists_simple_subobject

Lean4

theorem exists_simple_subobject {X : C} [IsArtinianObject X] (h : ¬IsZero X) : ∃ Y : Subobject X, Simple (Y : C) :=
  by
  have : Nontrivial (Subobject X) := nontrivial_of_not_isZero h
  obtain ⟨Y, s⟩ := (IsAtomic.eq_bot_or_exists_atom_le (⊤ : Subobject X)).resolve_left top_ne_bot
  exact ⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru