La composición de funciones biyectivas es biyectiva

José A. Alonso

21-06-2024

Demostrar con Lean4 que la composición de dos funciones biyectivas es una función biyectiva.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
open Function

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

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by sorry

1. Demostración en lenguaje natural

Sean \(f: X → Y\) y \(g: Y → Z\). En ejercicios anteriores hemos demostrados los siguientes lemas:

Lema 1: Si \(f\) y \(g\) son inyectiva, entonces también lo es \(g ∘ f\).
Lema 2: Si \(f\) y \(g\) son suprayectiva, entonces también lo es \(g ∘ f\).

Supongamos que \(f\) y \(g\) son biyectivas. Entonces, son inyectivas y suprayectivas. Luego, por los lemas 1 y 2, \(g ∘ f\) es inyectiva y suprayectiva. Por tanto, \(g ∘ f\) es biyectiva.

2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

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

-- 1ª demostración
-- ===============

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by
  cases' Hf with Hfi Hfs
  -- Hfi : Injective f
  -- Hfs : Surjective f
  cases' Hg with Hgi Hgs
  -- Hgi : Injective g
  -- Hgs : Surjective g
  constructor
  . -- ⊢ Injective (g ∘ f)
    apply Injective.comp
    . -- ⊢ Injective g
      exact Hgi
    . -- ⊢ Injective f
      exact Hfi
  . apply Surjective.comp
    . -- ⊢ Surjective g
      exact Hgs
    . -- ⊢ Surjective f
      exact Hfs

-- 2ª demostración
-- ===============

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by
  cases' Hf with Hfi Hfs
  -- Hfi : Injective f
  -- Hfs : Surjective f
  cases' Hg with Hgi Hgs
  -- Hgi : Injective g
  -- Hgs : Surjective g
  constructor
  . -- ⊢ Injective (g ∘ f)
    exact Injective.comp Hgi Hfi
  . -- ⊢ Surjective (g ∘ f)
    exact Surjective.comp Hgs Hfs

-- 3ª demostración
-- ===============

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by
  cases' Hf with Hfi Hfs
  -- Hfi : Injective f
  -- Hfs : Surjective f
  cases' Hg with Hgi Hgs
  -- Hgi : Injective g
  -- Hgs : Surjective g
  exact ⟨Injective.comp Hgi Hfi,
         Surjective.comp Hgs Hfs⟩

-- 4ª demostración
-- ===============

example :
  Bijective f → Bijective g → Bijective (g ∘ f) :=
by
  rintro ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩
  -- Hfi : Injective f
  -- Hfs : Surjective f
  -- Hgi : Injective g
  -- Hgs : Surjective g
  exact ⟨Injective.comp Hgi Hfi,
         Surjective.comp Hgs Hfs⟩

-- 5ª demostración
-- ===============

example :
  Bijective f → Bijective g → Bijective (g ∘ f) :=
fun ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩ ↦ ⟨Injective.comp Hgi Hfi,
                             Surjective.comp Hgs Hfs⟩

-- 6ª demostración
-- ===============

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
Bijective.comp Hg Hf

-- Lemas usados
-- ============

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

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory La_composicion_de_funciones_biyectivas_es_biyectiva
imports Main
begin

(* 1ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
proof (rule bijI)
  show "inj (g ∘ f)"
  proof (rule inj_compose)
    show "inj g"
      using ‹bij g› by (rule bij_is_inj)
  next
    show "inj f"
      using ‹bij f› by (rule bij_is_inj)
  qed
next
  show "surj (g ∘ f)"
  proof (rule comp_surj)
    show "surj f"
      using ‹bij f› by (rule bij_is_surj)
  next
    show "surj g"
      using ‹bij g› by (rule bij_is_surj)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
proof (rule bijI)
  show "inj (g ∘ f)"
  proof (rule inj_compose)
    show "inj g"
      by (rule bij_is_inj [OF ‹bij g›])
  next
    show "inj f"
      by (rule bij_is_inj [OF ‹bij f›])
  qed
next
  show "surj (g ∘ f)"
  proof (rule comp_surj)
    show "surj f"
      by (rule bij_is_surj [OF ‹bij f›])
  next
    show "surj g"
      by (rule bij_is_surj [OF ‹bij g›])
  qed
qed

(* 3ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
proof (rule bijI)
  show "inj (g ∘ f)"
    by (rule inj_compose [OF bij_is_inj [OF ‹bij g›]
                             bij_is_inj [OF ‹bij f›]])
next
  show "surj (g ∘ f)"
    by (rule comp_surj [OF bij_is_surj [OF ‹bij f›]
                           bij_is_surj [OF ‹bij g›]])
qed

(* 4ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
by (rule bijI [OF inj_compose [OF bij_is_inj  [OF ‹bij g›]
                                  bij_is_inj  [OF ‹bij f›]]
                  comp_surj   [OF bij_is_surj [OF ‹bij f›]
                                  bij_is_surj [OF ‹bij g›]]])

(* 5ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
using assms
by (rule bij_comp)

(* Nota: Auto solve indica la demostración anterior. *)

end