Theorems · Inductive type · category theory

CategoryTheory.Mono

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop

A morphism f is a monomorphism if it can be cancelled when postcomposed: g ≫ f = h ≫ f implies g = h. [Stacks Tag 003B](https://stacks.math.columbia.edu/tag/003B)

Defined in

Mathlib.CategoryTheory.Category.Basic

Cited by

893 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 7 definitions · uses no axioms

Assumes

CategoryTheory.Category