Monomorphisms and epimorphisms in the category of sets.

iff.lean

import tactic.basic

/-

Lean é em _proof assistant_ (verificador de provas formais) baseado em _type
theory_ (teoria de tipos) desenvolvido por Leonardo de Moura. _Type theory_
pode ser usado como uma alternativa à _set theory_ (teoria de conjuntos) como
fundamento matemático.

Usando _type theory_, é possível formalizar alguns análogos entre _set theory_
e _category theory_ (teoria de categorias). Neste arquivo, formalizamos a
equivalência entre funções injetoras e monomorfismos e a equivalência entre
funções sobrejetivas e epimorfismos na categoria **Set**.

Já que estamos trabalhando em teoria de tipos o universo `Type` é usado como
nossa categoria **Set** e, simultaneamente, como nosso universo de conjuntos.

-/

-- `α` e `β` são usados como conjuntos _e_ objetos (quando objetos, nenhum
-- termo do tipo é referenciado). Note que a escolha de `α` e `β` é arbitrária,
-- consequentemente estamos provando o caso geral.
--
-- `f` é usado como uma função _e_ como um morfismo.
variables {α β : Type} {f : α → β}

-- Em teoria de conjuntos uma função `f` é injetora quando para todo `x` e `y`
-- `f x = f y` implica que `x = y`.
--
-- Esta definição é equivalente a afirmar que a função `f` é de "um pra um," ou
-- seja, somente uma entrada é mapeada para cada saída.
def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂

-- Em teoria de categorias um monomorfismo `f : α → β` é um morfismo que, para
-- todo objeto `γ` e par de morfismos `g₁ g₂ : γ → α`, `f ∘ g₁ = f ∘ g₂`
-- implica que `g₁ = g₂`.
--
-- Note que, diferente da definição de função injetora, a definição de
-- monomorfismo _não_ referencia nenhum termo ("elemento") do tipo é
-- referenciado.
def monomorphism (f : α → β) :=
  ∀ {γ : Type} {g₁ g₂ : γ → α}, f ∘ g₁ = f ∘ g₂ → g₁ = g₂

example : monomorphism f → injective f :=
begin
  -- `h` é a hipótese que `f` é um monomorfism.
  intro h,
  -- O estado da prova se encontra da seguinte forma:
  --
  --    α : Type
  --    β : Type
  --    f : α → β
  --    h : monomorphism f
  --    ⊢ function.injective f
  --
  -- `⊢` indica o objetivo e cada linha acida mostra uma hipótese.
  --
  -- Podemos expandir a definição de `injective` para visualizar melhor o
  -- objetivo.
  unfold injective,
  -- O novo objetivo é `⊢ ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂`, deixando claro
  -- que podemos introduzir `a₁` e `a₂` assim como a hipótese `f a₁ = f a₂`. No
  -- jargão matemático, este passo é equivalente a dizer "seja `a₁ a₂ ∈ α` e
  -- suponha que `f a₁ = f a₂`".
  intros a₁ a₂ ha,
  -- Definimos as funções constantes `g₁` e `g₂` do conjunto unitário ao
  -- conjunto `α`. O tipo `unit` é habitado por somente pelo termo `()`, ou
  -- seja, é equivalente a um conjunto unitário.
  --
  -- Na categoria **Set**, essas funções são equivalentes a dois morfismos `g₁`
  -- e `g₂` de um objeto terminal ao objeto `α`.
  let g₁ : unit → α := λ _, a₁,
  let g₂ : unit → α := λ _, a₂,
  -- Se `g₁ = g₂`, conseguimos chegar ao objetivo (`⊢ a₁ = a₂`) aplicando `()`
  -- aos dois lados da igualdade, isto é, precisamos apenas mostrar que
  -- `g₁ = g₂`.
  suffices : g₁ = g₂, from congr_fun this (),
  -- Nesse ponto, o objetivo é `⊢ g₁ = g₂`. Lembre que a hipótese `h` afirma
  -- que para todo morfismo `g₁` e `g₂`, `f ∘ g₁ = f ∘ g₂ → g₁ = g₂`. Após
  -- aplicar a hipótese, o objetivo se torna `⊢ f ∘ g₁ = f ∘ g₂`.
  apply h,
  -- Para mostrar a igualdade entre duas funções, neste caso `f ∘ g₁` e
  -- `f ∘ g₂`, basta mostrar que para todo `x`, `(f ∘ g₁) x = (f ∘ g₂) x`.
  ext ⟨⟩,
  -- Porém, como as funções `g₁` e `g₂` são constantes, `f (g₁ x) = f (g₂ x)`
  -- simplifica para `f a₁ = f a₂`, que é exatamente o que diz hipótese `ha`.
  simp [ha]
end

-- Para completar a equivalência entre funções injetoras e monomorfismos, basta
-- mostrar que uma função injetora é um monomorfismo na categoria **Set**.
example : injective f → monomorphism f :=
begin
  -- Introduz a hipótese `h : injective f`.
  intro h,
  -- Expande a definição de monomorfismo no objetivo.
  unfold monomorphism,
  -- Introduz o tipo `γ`, assim como as funções `g₁` e `g₂` e a hipótese
  -- `f ∘ g₁ = f ∘ g₂`. Após a introdução, o estado da prova se torna:
  --
  --    α : Type
  --    β : Type
  --    f : α → β
  --    h : injective f
  --    γ : Type
  --    g₁ : γ → α
  --    g₂ : γ → α
  --    hg : f ∘ g₁ = f ∘ g₂
  --    ⊢ g₁ = g₂
  --
  -- Note que não sabemos nada específico sobre as funções `g₁` e `g₂` ou sobre
  -- o tipo `γ`, ou seja, não podemos expandir suas definições como na prova
  -- anterior.
  intros γ g₁ g₂ hg,
  -- Para provar que `g₁ = g₂`, basta mostrar que para todo `x`, `g₁ x = g₂ x`.
  ext x,
  -- Aplicamos `x` aos dois lados da igualdade da hipótese `hg`.
  have hg := congr_fun hg x,
  -- Agora, a hipótese `hg` tem o tipo `f (g₁ x) = f (g₂ x)`, sendo que os
  -- termos `g₁ x` e `g₂ x` tem tipo `α`. Aplicando a definição de função
  -- injetora onde `a₁ = g₁ x` e `a₂ = g₂ x`, sabemos que `a₁ = a₂`, ou seja,
  -- `g₁ x = g₂ x`.
  exact h hg
end

/-

As provas abaixo estão brevemente comentadas.

-/

def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b

def epimorphism (f : α → β) :=
  ∀ {γ : Type} {g₁ g₂ : β → γ}, g₁ ∘ f = g₂ ∘ f → g₁ = g₂

example : epimorphism f → surjective f :=
begin
  intro h,
  unfold surjective,
  -- `classical` inclui uma hipótese com o tipo `Π (a : Prop), decidable a` ao
  -- contexto. `decidable a` é um tipo contendo uma prova de `a` ou uma prova
  -- `¬a`, ou seja, é equivalente a lei do terceiro excluído. Esta hipótese é
  -- necessária para fazermos uma prova por contradição.
  classical,
  -- O objetivo é `⊢ ∀ (b : β), ∃ (a : α), f a = b`, após `by_contra hb` a
  -- negação do objetivo será adicionada ao contexto e teremos um novo
  -- objetivo: `false`, ou seja, contradição.
  by_contra hb,
  -- `push_neg` transforma a hipótese `hb : ¬∀ (b : β), ∃ (a : α), f a = b` em
  -- `hb : ∃ (b : β), ∀ (a : α), ¬f a = b`.
  push_neg at hb,
  -- `cases` permite separar a hipótese `∃ (b : β), ∀ (a : α), ¬f a = b` em
  -- `b : β` e `hb : ∀ (a : α), ¬f a = b`.
  cases hb with b hb,
  let g₁ : β → bool := λ _, tt,
  let g₂ : β → bool := λ b', if b' = b then ff else tt,
  -- Já que `b` não está na imagem de `f`, `g₁ ∘ f = g₂ ∘ f`.
  have : g₁ ∘ f = g₂ ∘ f,
  { ext a, simp [hb a, g₁, g₂] },
  -- Porém, `g₁ ∘ f = g₂ ∘ f` implica `g₁ = g₂`, o que claramente não é o
  -- caso, concluindo a contradição.
  have := h this,
  have := congr_fun this b,
  -- `simpa` simplifica a hipótese `this` e a aplica para completar o objetivo.
  simpa [g₁, g₂, if_pos rfl] using this,
end

example : surjective f → epimorphism f :=
begin
  intro h,
  unfold surjective at h,
  intros γ g₁ g₂ hg,
  ext b,
  cases h b with a ha,
  have hg := congr_fun hg a,
  simpa [←ha]
end

Top