Link Search Menu Expand Document

Important properties of functions

Here are two import properties a function can have.

Definition. We say a function $f: A \to B$ is injective if for all $a_1,a_2$ with $a_1 \neq a_2$ we have $f(a_1) \neq f(a_2)$. So formally, a function is injective if it satisfies \(\forall a_1, a_2, a_1 \neq a_2 \to f(a_1) \neq f(a_2)\)

Example. The function \(f : \mathbb{Z} \to \mathbb{Z} \\ n \mapsto n + 1\) is injective. For, if $f(n_1) = f(n_2)$, we have $n_1 + 1 = n_2 + 1$. Adding $-1$ to both sides, gives $n_1 = n_2$.

In checking injectivity of the previous example, we encountered the contrapositive $f(a_1) = f(a_2) \to a_1 = a_2$ which is also often taken as the definition of injectivity.

Here is a definition of injectivity and a proof of this example in Lean the natural numbers.

def Injective (f : α  β) : Prop :=  a a₂⦄, f a = f a  a = a 

def f (n : Nat) : Nat := n + 1

example : Injective f := by 
  -- assume we have two natural numbers and their images are equal 
  intro (n : Nat) (n : Nat) (h : f n = f n)
  -- in the library defining the natural numbers we find the useful 
  -- fact that if n + k = m + k we know can conclude n = m. This 
  -- exactly what we want
  exact Nat.add_right_cancel h 

Example. The function \(g : \mathbb{Z} \to \mathbb{Z} \\ n \mapsto n^2 - 3n + 2\) is not injective since $g(1) = g(2) = 0$.

We can show that $g$ is also not injective in the natural numbers in Lean.

example : ¬ Injective g := by
  -- we assume that g is actually and try to reach an absurdity
  intro (n : Injective g) 
  -- we use rfl to compute and check equality 
  have : g 1 = g 2 := by rfl 
  -- applying the 
  have : 1 = 2 := n this  
  -- someone has already told Lean that n < n + 1 for all n 
  have o : 1 < 2 := Nat.lt_succ_self 1
  -- and they have also told Lean that n < m → ¬ (n = m) 
  exact Nat.ne_of_lt o this 

Injectivity can be viewed as saying $f: A \to B$ injects a copy of $A$ into $B$.

Definition. A function $f: A \to B$ is surjective if, for any $b$ in $B$, there is some $a$ with $f(a) = b$. Formally, \(\forall b, \exists a, f(a) = b\)

Returning to our two examples above, we see $n \mapsto n+1$ is also surjective. Given $m \in \mathbb{Z}$, since $f(m-1) = m$, we have an element mapping to $m$. Thus, $f$ is surjective. If we change the domain and codomain to $\mathbb{N}$, $n \mapsto n + 1$ is no longer surjective

def Surjective (f : α  β) : Prop :=  b,  a, f a = b 

example : ¬ Surjective f := by 
  intro (h : Surjective f)
  have m,g :  n, n + 1 = 0 := h 0 
  -- we use that 0 is never equal to n + 1 for n : Nat
  exact Nat.succ_ne_zero m g  

The function $n \mapsto n^2$ is not surjective since there is no integer that solves $n^2 = -1$.

Often one wants to understand the totality of $b$’s for which there is some $a$ such that $f(a) = b$. This is called the range (or image) of $f$. Note the range and codomain are distinct in general. Indeed, \(f : \mathbb{Z} \to \mathbb{Z} \\ n \mapsto n + 1\) is surjective to the range equals the codomain. But each integer is also a real number so the function \(f : \mathbb{Z} \to \mathbb{R} \\ n \mapsto n + 1\) is also well-defined. Even though, as is common, we used the same notation for the two functions, they are not equal as function because they have two different codomains.

We can think of a surjective function $f: A \to B$ as way of covering $B$ with $A$ using the rule $f$.

We can combine the two notions in a single one.

Definition. A function $f: A \to B$ is bijective if it is both injective and surjective. In Lean,

def Bijective (f : α  β) : Prop :=  Injective f  Surjective f 

Our first example, $n \mapsto n+1$, is bijective.

Bijectivity can be rephrased as \(\forall b, \exists ! a, f(a) = b\) For any $b$, there is exactly one value $a$ satisfying $f(a) = b$.

Injectivity, surjectivity, and bijectivity are preserved under composition in the following sense.

Theorem. Let $f : A \to B$ and $g : B \to C$ be functions.

  • Suppose $f$ and $g$ are injective, Then $g \circ f$ is also injective.
  • Suppose $f$ and $g$ are surjective. Then $g \circ f$ is also surjective.
  • Suppose $f$ and $g$ are bijective. Then $g \circ f$ is also bijective.
Proof. (Expand to view)

Assume that $f$ and $g$ are injective. If $g(f(a_1)) = g(f(a_2))$, then since $g$ is injective we know that $f(a_1) = f(a_2)$. But since $f$ is injective, we have $a_1 = a_2$. Thus, $g \circ f$ is injective. Assume that $f$ and $g$ are surjective. Then for a $c$ there is some $b$ with $g(b) = c$ since $g$ is sujective. There is also some $a$ with $f(a) = b$ since $f$ is surjective. Thus, we have $a$ with $g(f(a)) = c$ and $g \circ f$ is surjective. Finally if both $f$ and $g$ are bijections, then, by definition, they are both injective and surjective. We have just shown that $g \circ f$ is then injective and surjective or is a bijection.

We can also detect injectivity or surjectivity using a composition.

Theorem. Let $f : A \to B$ and $g : B \to C$ be functions.

  • If $g \circ f$ is injective, then $f$ is injective.
  • If $g \circ f$ is surjective, then $g$ is surjective.

Let’s give a proof of this in Lean.

theorem comp_inj (f : α  β) (g : β  γ) (h : Injective (g  f)) : Injective f := by 
  -- assume we have two values with equal image 
  intro (a : α) (a : α) (h :  f a = f a)
  -- apply g to equal arguments yields equal outputs 
  have : g (f a) = g (f a) := congrArg g h 
  exact h this 

theorem comp_surj (f : α  β) (g : β  γ) (h : Surjective (g  f)) : Surjective g := by 
  -- take some and try to solve g b = c for some b 
  intro (c : γ) 
  -- take the a satisfying g (f a) = c and the proof of equality
  have a,h :  a, g (f a) = c := h c 
  -- the b we want is f a and the same proof of equality works
  exact f a, h