Theorems · Theorem · category theory

CategoryTheory.simple_of_isSimpleOrder_subobject

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) [IsSimpleOrder (CategoryTheory.Subobject X)],
  CategoryTheory.Simple X

If X has subobject lattice {⊥, ⊤}, then X is simple.

Defined in

Mathlib.CategoryTheory.Simple

Cited by

1 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroObjectIsSimpleOrder