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.