Functions on finite domains

Main result : for functions f:A->A with finite A, f injective <-> f bijective <-> f surjective.

From Stdlib Require Import List ListDec.
Set Implicit Arguments.

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

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

Definition Bijective {A B} (f : A ->B) :=
exists g:B ->A , (forall x, g (f x) = x ) /\ (forall y, f (g y) = y ).

Finiteness is defined here via exhaustive list enumeration

Definition Full {A:Type} (l:list A) := forall a:A, In a l.
Definition Finite (A:Type) := exists (l:list A ), Full l.

In many of the following proofs, it will be convenient to have list enumerations without duplicates. As soon as we have decidability of equality (in Prop), this is equivalent to the previous notion (s. lemma Finite_dec).

Definition Listing {A:Type} (l:list A) := NoDup l /\ Full l.
Definition Finite' (A:Type) := exists (l:list A ), Listing l.

Lemma Listing_decidable_eq {A:Type} (l:list A): Listing l -> decidable_eq A.

Lemma Finite_dec {A:Type}: Finite A /\ decidable_eq A <-> Finite' A.

Lemma Finite_alt_deprecated A (d:decidable_eq A) : Finite A <-> Finite' A.
#[deprecated(since="8.17", note="Use Finite_dec instead.")]
Notation Finite_alt := Finite_alt_deprecated.

Lemma Injective_map_NoDup A B (f:A ->B) (l:list A) :
Injective f -> NoDup l -> NoDup (map f l).

Lemma Injective_map_NoDup_in A B (f:A ->B) (l:list A) :
  (forall x y, In x l -> In y l -> f x = f y -> x = y ) -> NoDup l -> NoDup (map f l).

Lemma Injective_list_carac A B (d:decidable_eq A)(f:A ->B) :
  Injective f <-> (forall l, NoDup l -> NoDup (map f l)).

Lemma Injective_carac A B (l:list A) : Listing l ->
   forall (f:A ->B), Injective f <-> NoDup (map f l).

Lemma Surjective_list_carac A B (f:A ->B):
Surjective f <-> (forall lB, exists lA , incl lB (map f lA)).

Lemma Surjective_carac A B : Finite B -> decidable_eq B ->
forall f:A ->B, Surjective f <-> (exists lA , Listing (map f lA)).

Lemma Endo_Injective_Surjective :
forall A, Finite A -> decidable_eq A ->
forall f:A ->A, Injective f <-> Surjective f.

An injective and surjective function is bijective. We need here stronger hypothesis : decidability of equality in Type.

Definition EqDec (A:Type) := forall x y:A, {x =y }+{x <>y }.

First, we show that a surjective f has an inverse function g such that f.g = id.

Lemma Finite_Empty_or_not A :
  Finite A -> (A ->False ) \/ exists a:A ,True.

Lemma Surjective_inverse :
  forall A B, Finite A -> EqDec B ->
   forall f:A ->B, Surjective f ->
    exists g:B ->A , forall x, f (g x) = x.

Same, with more knowledge on the inverse function: g.f = f.g = id

Library Stdlib.Lists.Finite

Functions on finite domains