## 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.

**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.

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

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,

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.