bijection


  • Dimitri Hendriks 2013-10-09
  • http://www.cs.vu.nl/~diem/coq/calkin-wilf/bijection.html

Set Implicit Arguments.


Section bijections.


Variables A B : Type.


Definition injective (f : A -> B) := forall x y : A, f x = f y -> x = y.


Definition surjective (f : A -> B) := forall y : B, {x : A | f x = y}.


Inductive bijective (f : A -> B) : Type :=
  is_bijective : injective f -> surjective f -> bijective f.


Definition left_inverse (f : A -> B) (f' : B -> A) :=
  forall x : A, f' (f x) = x.


Definition right_inverse (f : A -> B) (f' : B -> A) :=
  forall y : B, f (f' y) = y.


Definition inverse f f' :=
  left_inverse f f' /\ right_inverse f f'.


Lemma left_inv_inj f f' : left_inverse f f' -> injective f.

Proof.

intros H x y H0.

rewrite <- (H x).

rewrite H0.

apply H.

Qed.


Lemma right_inv_surj f f' : right_inverse f f' -> surjective f.

Proof.

intros H y.

rewrite <- (H y).

exact (exist (fun x => f x = f (f' y)) (f' y) (refl_equal (f (f' y)))).

Qed.


Lemma inv2bij f f' : inverse f f' -> bijective f.

Proof.

intros [H1 H2].

exact (is_bijective (left_inv_inj H1) (right_inv_surj H2)).

Qed.


End bijections.