# Homework (VII)

### Problem 1 (Lean)

Suppose $f \maps X \to Y$ and $g \maps Y \to Z$ are functions. Prove in Lean that if the composition $g \circ f$ is injective, then $f$ is injective.

### Problem 2 (Lean)

Suppose $f \maps X \to Y$ and $g \maps Y \to Z$ are functions. Prove in Lean that if the composition $g \circ f$ is surjective, then $g$ is surjective.

### Problem 3

Give counter-examples for the converse of the statements of problems 1 and 2.

### Problem 4 (Lean)

Prove the Frobenius Reciprocity for the images and preimages of functions by filling in the `sorry`

in below. You may prove lemma(s) first and use them to fill in the `sorry`

, or alternatively, you can simply give a direct proof.