Skip to main content

La composición de funciones suprayectivas es suprayectiva

Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.

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

import Mathlib.Tactic
open Function
variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
by sorry

Demostración en lenguaje natural

Supongamos que \(f : A → B\) y \(g : B → C\) son suprayectivas. Tenemosque demostrar que \[ (∀z ∈ C)(∃x ∈ A)[g(f(x)) = z] \] Sea \(z ∈ C\). Por ser \(g\) suprayectiva, existe un \(y ∈ B\) tal que \[ g(y) = z \tag{1} \] Por ser \(f\) suprayectiva, existe un \(x ∈ A\) tal que \[ f(x) = y \tag{2} \] Por tanto, \begin{align} g(f(x)) &= g(y) &&\text{[por (2)]} \newline &= z &&\text{[por (1)]} \end{align}

Demostraciones con Lean4

import Mathlib.Tactic
open Function
variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

-- 1ª demostración
example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
by
  intro z
  -- z : γ
  -- ⊢ ∃ a, (g ∘ f) a = z
  cases' hg z with y hy
  -- y : β
  -- hy : g y = z
  cases' hf y with x hx
  -- x : α
  -- hx : f x = y
  use x
  -- ⊢ (g ∘ f) x = z
  dsimp
  -- ⊢ g (f x) = z
  rw [hx]
  -- ⊢ g y = z
  exact hy

-- 2ª demostración
example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
by
  intro z
  -- z : γ
  -- ⊢ ∃ a, (g ∘ f) a = z
  cases' hg z with y hy
  -- y : β
  -- hy : g y = z
  cases' hf y with x hx
  -- x : α
  -- hx : f x = y
  use x
  -- ⊢ (g ∘ f) x = z
  dsimp
  -- ⊢ g (f x) = z
  rw [hx, hy]

-- 3ª demostración
example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
by
  intro z
  -- z : γ
  -- ⊢ ∃ a, (g ∘ f) a = z
  cases' hg z with y hy
  -- y : β
  -- hy : g y = z
  cases' hf y with x hx
  -- x : α
  -- hx : f x = y
  exact ⟨x, by dsimp ; rw [hx, hy]⟩

-- 4ª demostración
example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
by
  intro z
  -- z : γ
  -- ⊢ ∃ a, (g ∘ f) a = z
  rcases hg z with ⟨y, hy : g y = z⟩
  rcases hf y with ⟨x, hx : f x = y⟩
  exact ⟨x, by dsimp ; rw [hx, hy]⟩

-- 5ª demostración
example
  (hg : Surjective g)
  (hf : Surjective f)
  : Surjective (g ∘ f) :=
Surjective.comp hg hf

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

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

Demostraciones interactivas

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

Referencias