Покажите, что функция moni c (инъективная) и epi c (сюръективная) имеет обратное значение в Coq - PullRequest
Новая
       6

Покажите, что функция moni c (инъективная) и epi c (сюръективная) имеет обратное значение в Coq

4 голосов
/ 13 января 2020

A moni c и epi c - это изоморфизм , следовательно, он имеет обратный . Я хотел бы доказать это в Coq. 

  Axiom functional_extensionality: forall A B (f g : A->B),  (forall a, f a = g a) -> f = g.
  Definition compose {A B C} (f : B->C) (g: A->B) a := f (g a).
  Notation "f ∘ g" := (compose f g) (at level 40).
  Definition id {A} (a:A) := a.
  Definition monic {A B} (f:A->B) := forall C {h k:C->A}, f ∘ h = f ∘ k -> h = k.
  Definition epic  {A B} (f:A->B) := forall C {h k:B->C}, h ∘ f = k ∘ f -> h = k.
  Definition iso {A B} (f:A->B) := monic f /\ epic f.

  Goal forall {A B} (f:A->B), iso f -> exists f', f∘f' = id /\ f'∘f = id.

Доказательства, которые я нашел в Интернете ( 1 , 2 ), не дают конструкции f' (обратный). Можно ли показать это в Coq? (Для меня не очевидно, что обратное вычислимо ...)

1 Ответ

7 голосов
/ 13 января 2020

Во-первых, вопрос терминологии. В теории категорий изоморфизм - это морфизм, имеющий левую и правую инверсию, поэтому я немного изменяю ваши определения: 

Definition compose {A B C} (f : B->C) (g: A->B) a := f (g a).
Notation "f ∘ g" := (compose f g) (at level 40).
Definition id {A} (a:A) := a.
Definition monic {A B} (f:A->B) := forall C {h k:C->A}, f ∘ h = f ∘ k -> h = k.
Definition epic  {A B} (f:A->B) := forall C {h k:B->C}, h ∘ f = k ∘ f -> h = k.
Definition iso {A B} (f:A->B) :=
  exists g : B -> A, f ∘ g = id /\ g ∘ f = id.

Можно доказать этот результат, приняв несколько стандартных аксиом, а именно экстенсиональность высказываний и определенное конструктивное описание (аксиома уникального выбора): 

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.PropExtensionality.
Require Import Coq.Logic.Description.

Section MonoEpiIso.

Context (A B : Type).

Implicit Types (f : A -> B) (x : A) (y : B).

Definition surjective f := forall y, exists x, f x = y.

Lemma epic_surjective f : epic f -> surjective f.
Proof.
intros epic_f y.
assert (H : (fun y => exists x, f x = y) = (fun y => True)).
{ apply epic_f.
  apply functional_extensionality.
  intros x; apply propositional_extensionality; split.
  - intros _; exact I.
  - now intros _; exists x. }
now pattern y; rewrite H.
Qed.

Definition injective f := forall x1 x2, f x1 = f x2 -> x1 = x2.

Lemma monic_injective f : monic f -> injective f.
Proof.
intros monic_f x1 x2 e.
assert (H : f ∘ (fun a : unit => x1) = f ∘ (fun a : unit => x2)).
{ now unfold compose; simpl; rewrite e. }
assert (e' := monic_f _ _ _ H).
exact (f_equal (fun g => g tt) e').
Qed.

Lemma monic_epic_iso f : monic f /\ epic f -> iso f.
Proof.
intros [monic_f epic_f].
assert (Hf : forall y, exists! x, f x = y).
{ intros y.
  assert (sur_f := epic_surjective _ epic_f).
  destruct (sur_f y) as [x xP].
  exists x; split; trivial.
  intros x' x'P.
  now apply (monic_injective _ monic_f); rewrite xP, x'P. }
exists (fun a => proj1_sig (constructive_definite_description _ (Hf a))).
split; apply functional_extensionality; unfold compose, id.
- intros y.
  now destruct (constructive_definite_description _ (Hf y)).
- intros x.
  destruct (constructive_definite_description _ (Hf (f x))); simpl.
  now apply (monic_injective _ monic_f).
Qed.

End MonoEpiIso.

Я считаю, что невозможно доказать этот результат, по крайней мере, без какой-либо формы уникального выбора. Предположим пропозициональную и функциональную экстенсиональность. Обратите внимание, что если выполняется exists! x : A, P x, то уникальная функция 

{x | P x} -> unit

является и инъективной, и сюръективной. (Инъективность следует из части уникальности, а сюръективность следует из части существования.) Если бы эта функция имела инверсию для каждого P : A -> Type, то мы могли бы использовать эту обратную для реализации аксиомы уникального выбора. Так как эта аксиома не выполняется в Coq, не должно быть возможности построить эту обратную в основной теории c.

...