case mono_isIso_iff_nonzero
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ ∀ {Y : C} (f : Y ⟶ X) [inst : Mono f], IsIso f ↔ f ≠ 0
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ Simple X
constructor
case mono_isIso_iff_nonzero
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0
case mono_isIso_iff_nonzero
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ ∀ {Y : C} (f : Y ⟶ X) [inst : Mono f], IsIso f ↔ f ≠ 0
intros Y f hf
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f → f ≠ 0

case mono_isIso_iff_nonzero.mpr
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f
case mono_isIso_iff_nonzero
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0
constructor
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : IsIso f
⊢ f ≠ 0
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f → f ≠ 0
intro i
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
⊢ f ≠ 0
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : IsIso f
⊢ f ≠ 0
rw [Subobject.isIso_iff_mk_eq_top] at i
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ False
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
⊢ f ≠ 0
intro w
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w✝ : f = 0
w : mk f = ⊥
⊢ False
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ False
rw [← Subobject.mk_eq_bot_iff_zero] at w
no goals
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w✝ : f = 0
w : mk f = ⊥
⊢ False
exact IsSimpleOrder.bot_ne_top (w.symm.trans i)
case mono_isIso_iff_nonzero.mpr
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
⊢ IsIso f
case mono_isIso_iff_nonzero.mpr
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f
intro i
case mono_isIso_iff_nonzero.mpr.inl
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f

case mono_isIso_iff_nonzero.mpr.inr
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f
case mono_isIso_iff_nonzero.mpr
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
⊢ IsIso f
rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
case mono_isIso_iff_nonzero.mpr.inl
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h✝ : mk f = ⊥
h : f = 0
⊢ IsIso f
case mono_isIso_iff_nonzero.mpr.inl
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f
rw [Subobject.mk_eq_bot_iff_zero] at h
no goals
case mono_isIso_iff_nonzero.mpr.inl
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h✝ : mk f = ⊥
h : f = 0
⊢ IsIso f
exact False.elim (i h)
no goals
case mono_isIso_iff_nonzero.mpr.inr
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f
exact (Subobject.isIso_iff_mk_eq_top _).mpr h