Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0) →
    CategoryTheory.Mono f

A morphism that only maps the zero pseudoelement to zero is a monomorphism.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian