Skip to main content

If f ∘ f is bijective, then f is bijective

Prove that if \(f ∘ f\) is bijective, then \(f\) is bijective.

To do this, complete the following Lean4 theory:

import Mathlib.Tactic
open Function

variable {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (f : X → X)
  (h : Bijective (f ∘ f))
  : Bijective f :=
by sorry

1. Proof in natural language

It follows from the following lemmas (proven in previous exercises):

  • Lemma 1: If \(g ∘ f\) is injective, then \(f\) is injective.
  • Lemma 2: If \(g ∘ f\) is surjective, then \(g\) is surjective.

Indeed, suppose that \[ f ∘ f \text {is bijective} \] then it follows that \begin{align} f ∘ f \text{ is injective } \tag{1} \newline f ∘ f \text{ is surjective} \tag{2} \end{align} From (1) and Lemma 1, it follows that \[ f \text { is injective} \tag{3} \] From (2) and Lemma 2, it follows that \[ f \text{ is surjective} \tag{4} \] From (3) and (4) it follows that \[ f \text{ is bijective} \]

2. Proofs with Lean4

import Mathlib.Tactic
open Function

variable {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

-- Proof 1
-- =======

example
  (f : X → X)
  (h : Bijective (f ∘ f))
  : Bijective f :=
by
  have h1 : Injective (f ∘ f) := Bijective.injective h
  have h2 : Surjective (f ∘ f) := Bijective.surjective h
  have h3 : Injective f := Injective.of_comp h1
  have h4 : Surjective f := Surjective.of_comp h2
  show Bijective f
  exact ⟨h3, h4⟩

-- Proof 2
-- =======

example
  (f : X → X)
  (h : Bijective (f ∘ f))
  : Bijective f :=
⟨Injective.of_comp (Bijective.injective h),
 Surjective.of_comp (Bijective.surjective h)⟩

-- Proof 3
-- =======

example
  (f : X → X)
  (h : Bijective (f ∘ f))
  : Bijective f :=
by
  constructor
  . -- ⊢ Injective f
    have h1 : Injective (f ∘ f) := Bijective.injective h
    exact Injective.of_comp h1
  . -- ⊢ Surjective f
    have h2 : Surjective (f ∘ f) := Bijective.surjective h
    exact Surjective.of_comp h2

-- Used lemmas
-- ===========

-- #check (Injective.of_comp : Injective (g ∘ f) → Injective f)
-- #check (Surjective.of_comp : Surjective (g ∘ f) → Surjective g)

You can interact with the previous proofs at Lean 4 Web.

3. Proofs with Isabelle/HOL

theory If_ff_is_biyective_then_f_is_biyective
imports Main
begin

(* Proof 1 *)
lemma
  assumes "bij (f ∘ f)"
  shows   "bij f"
proof (rule bijI)
  show "inj f"
  proof -
    have h1 : "inj (f ∘ f)"
      using assms by (simp only: bij_is_inj)
    then show "inj f"
      by (simp only: inj_on_imageI2)
  qed
next
  show "surj f"
  proof -
    have h2 : "surj (f ∘ f)"
      using assms by (simp only: bij_is_surj)
    then show "surj f"
      by auto
  qed
qed

(* Proof 2 *)
lemma
  assumes "bij (f ∘ f)"
  shows   "bij f"
proof (rule bijI)
  show "inj f"
    using assms bij_is_inj inj_on_imageI2
    by blast
next
  show "surj f"
    using assms bij_is_surj
    by fastforce
qed

(* Proof 3 *)
lemma
  assumes "bij (f ∘ f)"
  shows   "bij f"
by (metis assms
          bij_betw_comp_iff
          bij_betw_def
          bij_betw_imp_surj
          inj_on_imageI2)

end

Note: The code for the previous proofs can be found in the Calculemus repository on GitHub.