Witnesses of non-simplicity #
Mathlib's CategoryTheory.Simple X says that a monomorphism into X is an isomorphism exactly
when it is nonzero. This file records the contrapositive used to split a non-simple object: a
nonzero object which is not simple receives a nonzero monomorphism that is not an isomorphism,
that is, it has a nonzero proper subobject.
Main results #
TauCeti.exists_mono_ne_zero_not_isIso_of_not_simple: a nonzero object which is not simple is the target of a nonzero monomorphism which is not an isomorphism.
theorem
TauCeti.exists_mono_ne_zero_not_isIso_of_not_simple
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
(hX : ¬CategoryTheory.Limits.IsZero X)
(hs : ¬CategoryTheory.Simple X)
:
∃ (Y : C) (f : Y ⟶ X), CategoryTheory.Mono f ∧ f ≠ 0 ∧ ¬CategoryTheory.IsIso f
A nonzero object which is not simple has a nonzero proper subobject: it is the target of a nonzero monomorphism which is not an isomorphism.