instIsSimpleOrderSubobjectOfSimple

English

The subobject lattice of a simple X is a simple order.

Русский

Лад подобъектов X простого является простым порядком.

LaTeX

$$$ IsSimpleOrder(Subobject\ X). $$$

Lean4

instance {X : C} [Simple X] : IsSimpleOrder (Subobject X) where
  eq_bot_or_eq_top := by
    rintro ⟨⟨⟨Y : C, ⟨⟨⟩⟩, f : Y ⟶ X⟩, m : Mono f⟩⟩
    change mk f = ⊥ ∨ mk f = ⊤
    by_cases h : f = 0
    · exact Or.inl (mk_eq_bot_iff_zero.mpr h)
    · refine Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero f).mpr h))

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