Morphism

Monomorphism

A monomorphism is a left-cancellable morphism (denoted with ). A morphism is monic iff for any and #m/def/cat

In a function is a monic iff it is injective iff it is left-invertible (i.e. split monic), but these are not equivalent in every concrete category, rather:

graph LR;
  left-invertible ==>|implies| injective ==>|implies| monic

Properties

See the dual properties.

  1. If is monic then is monic.
Proof of 1

Note implies which holds iff , proving ^P1.

#state/tidy | #lang/en | #SemBr