Monomorphisms and Epimorphisms, Surjection and Injection.

Morphism.v

Definition injective {A B} (f : A -> B) := forall a1 a2, f a1 = f a2 -> a1 = a2.

Lemma False_injective : forall {A} (f : False -> A), injective f.
Proof. unfold injective. contradiction. Qed.

Definition monomorphism {A B} (f : A -> B) :=
  forall X (g1 g2 : X -> A) x, (forall x, f (g1 x) = f (g2 x)) -> g1 x = g2 x.

Theorem injective_monomorphism : forall {A B} (f : A -> B),
  injective f <-> monomorphism f.
Proof.
  unfold injective, monomorphism.
  split; auto.
  intros.
  specialize (H True (fun _ => a1) (fun _ => a2)). auto.
Qed.

Definition surjective {A B} (f : A -> B) := forall b, exists a, f a = b.

Definition epimorphism {A B} (f : A -> B) :=
  forall X (g1 g2 : B -> X) b, (forall a, g1 (f a) = g2 (f a)) -> g1 b = g2 b.

Theorem surjective_epimorphism : forall {A B} (f : A -> B),
  surjective f -> epimorphism f.
Proof.
  unfold surjective, epimorphism.
  intros A B f H X g1 g2 b.
  specialize (H b) as [a eq].
  intros.
  specialize (H a).
  rewrite eq in H.
  assumption.
Qed.

Definition im_dec {A} {B} (f : A -> B) :=
  exists g, forall b, g b = true <-> exists a, f a = b.

Theorem epimorphism_surjective : forall {A B} (f : A -> B),
  im_dec f -> epimorphism f -> surjective f.
Proof.
  unfold im_dec, epimorphism, surjective.
  intros A B f [g Hg] Hf b.
  destruct (g b) eqn:Heqb.
  - destruct (Hg b). auto.
  - specialize (Hf bool (fun _ => true) g b).
    simpl in Hf. rewrite Heqb in Hf.
    assert (true = false); try discriminate.
    apply Hf.
    intros.
    destruct (Hg (f a)).
    symmetry.
    eauto.
Qed.