Library UniMath.CategoryTheory.categories.HSET.MonoEpiIso
Characterizations of monos, epis, and isos in HSET
Contents
- Points as global elements
- Monomorphisms are exactly injective functions MonosAreInjective_HSET
- Epimorphisms are exactly surjective functions EpisAreSurjective_HSET
- Equivalence between isomorphisms and weak equivalences
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Local Open Scope cat.
Local Definition global_element_HSET {A : hSet} (a : A) : HSET⟦unitset, A⟧ :=
invweq (weqfunfromunit A) a.
TODO: I think there is a name in UniMath for the constant function at a,
what is it?
Local Definition global_element_HSET_paths_weq {A : hSet} (x y : A) :
(x = y) ≃ (global_element_HSET x = global_element_HSET y).
Show proof.
apply weqonpaths.
Local Definition global_element_HSET_comp {A B : hSet} (f : HSET⟦A, B⟧) (x : A) :
global_element_HSET x · f = global_element_HSET (f x).
Show proof.
abstract (apply funextfun; intro z; induction z; reflexivity).
Local Definition global_element_HSET_fun_weq {A B : hSet} (f : HSET⟦A, B⟧) (x y : A) :
(f x = f y) ≃ (global_element_HSET x · f = global_element_HSET y · f).
Show proof.
abstract (do 2 rewrite global_element_HSET_comp;
apply global_element_HSET_paths_weq).
apply global_element_HSET_paths_weq).
Lemma MonosAreInjective_HSET {A B : HSET} (f: HSET ⟦ A, B ⟧) :
isMonic f ≃ isInjective f.
Show proof.
apply weqimplimpl.
- intro isM.
apply incl_injectivity; intros b.
apply invproofirrelevance; intros a1 a2.
apply subtypeEquality; [intro; apply setproperty|].
apply global_element_HSET_paths_weq.
apply isM.
apply funextsec; intro t.
abstract (induction t; exact (pr2 a1 @ ! pr2 a2)).
- intro isI.
unfold isMonic.
intros ? ? ? eq.
apply funextfun; intro.
apply (invweq (Injectivity _ isI _ _)).
apply toforallpaths in eq.
apply eq.
- apply isapropisMonic, has_homsets_HSET.
- apply isaprop_isInjective.
- intro isM.
apply incl_injectivity; intros b.
apply invproofirrelevance; intros a1 a2.
apply subtypeEquality; [intro; apply setproperty|].
apply global_element_HSET_paths_weq.
apply isM.
apply funextsec; intro t.
abstract (induction t; exact (pr2 a1 @ ! pr2 a2)).
- intro isI.
unfold isMonic.
intros ? ? ? eq.
apply funextfun; intro.
apply (invweq (Injectivity _ isI _ _)).
apply toforallpaths in eq.
apply eq.
- apply isapropisMonic, has_homsets_HSET.
- apply isaprop_isInjective.
Lemma EpisAreSurjective_HSET {A B : HSET} (f: HSET ⟦ A, B ⟧) :
isEpi f ≃ issurjective f.
Show proof.
apply weqimplimpl.
- intro epif.
apply epiissurjectiontosets; [apply setproperty|].
intros ? ? ? ?.
apply toforallpaths.
apply epif.
now apply funextfun.
- intros is_surj_f.
intros C g h H.
apply funextfun; intro.
- intro epif.
apply epiissurjectiontosets; [apply setproperty|].
intros ? ? ? ?.
apply toforallpaths.
apply epif.
now apply funextfun.
- intros is_surj_f.
intros C g h H.
apply funextfun; intro.
specialize (is_surj_f x).
apply (squash_to_prop is_surj_f); [apply setproperty|].
intro x'.
apply (squash_to_prop is_surj_f); [apply setproperty|].
intro x'.
refine (!maponpaths _ (hfiberpr2 _ _ x') @ _).
refine (_ @ maponpaths _ (hfiberpr2 _ _ x')).
apply toforallpaths in H.
apply H.
- apply isapropisEpi.
apply has_homsets_HSET.
- apply isapropissurjective.
refine (_ @ maponpaths _ (hfiberpr2 _ _ x')).
apply toforallpaths in H.
apply H.
- apply isapropisEpi.
apply has_homsets_HSET.
- apply isapropissurjective.
Equivalence between isomorphisms and weak equivalences of two hSets.
Lemma hset_iso_is_equiv (A B : ob HSET)
(f : iso A B) : isweq (pr1 f).
Show proof.
apply (isweq_iso _ (inv_from_iso f)).
- intro x.
set (T:=iso_inv_after_iso f).
set (T':=toforallpaths _ _ _ T). apply T'.
- intro x.
apply (toforallpaths _ _ _ (iso_after_iso_inv f)).
- intro x.
set (T:=iso_inv_after_iso f).
set (T':=toforallpaths _ _ _ T). apply T'.
- intro x.
apply (toforallpaths _ _ _ (iso_after_iso_inv f)).
Lemma hset_iso_equiv (A B : ob HSET) : iso A B -> (pr1 A) ≃ (pr1 B).
Show proof.
intro f.
exists (pr1 f).
apply hset_iso_is_equiv.
exists (pr1 f).
apply hset_iso_is_equiv.
Given a weak equivalence, we construct an iso.
Again mostly unwrapping and packing.
Lemma hset_equiv_is_iso (A B : hSet)
(f : (pr1 A) ≃ (pr1 B)) :
is_iso (C:=HSET) (pr1 f).
Show proof.
apply (is_iso_qinv (C:=HSET) _ (invmap f)).
split; simpl.
- apply funextfun; intro x; simpl in *.
unfold compose, identity; simpl.
apply homotinvweqweq.
- apply funextfun; intro x; simpl in *.
unfold compose, identity; simpl.
apply homotweqinvweq.
split; simpl.
- apply funextfun; intro x; simpl in *.
unfold compose, identity; simpl.
apply homotinvweqweq.
- apply funextfun; intro x; simpl in *.
unfold compose, identity; simpl.
apply homotweqinvweq.
Lemma hset_equiv_iso (A B : ob HSET) : (pr1 A) ≃ (pr1 B) -> iso A B.
Show proof.
intro f.
simpl in *.
exists (pr1 f).
apply hset_equiv_is_iso.
simpl in *.
exists (pr1 f).
apply hset_equiv_is_iso.
Both maps defined above are weak equivalences.
Lemma hset_iso_equiv_is_equiv (A B : ob HSET) : isweq (hset_iso_equiv A B).
Show proof.
apply (isweq_iso _ (hset_equiv_iso A B)).
intro; apply eq_iso.
- reflexivity.
- intro; apply subtypeEquality.
+ intro; apply isapropisweq.
+ reflexivity.
intro; apply eq_iso.
- reflexivity.
- intro; apply subtypeEquality.
+ intro; apply isapropisweq.
+ reflexivity.
Definition hset_iso_equiv_weq (A B : ob HSET) : (iso A B) ≃ ((pr1 A) ≃ (pr1 B)).
Show proof.
exists (hset_iso_equiv A B).
apply hset_iso_equiv_is_equiv.
apply hset_iso_equiv_is_equiv.
Lemma hset_equiv_iso_is_equiv (A B : ob HSET) : isweq (hset_equiv_iso A B).
Show proof.
apply (isweq_iso _ (hset_iso_equiv A B)).
{ intro f.
apply subtypeEquality.
{ intro; apply isapropisweq. }
reflexivity. }
intro; apply eq_iso.
reflexivity.
{ intro f.
apply subtypeEquality.
{ intro; apply isapropisweq. }
reflexivity. }
intro; apply eq_iso.
reflexivity.
Definition hset_equiv_weq_iso (A B : ob HSET) :
(pr1 A ≃ pr1 B) ≃ iso A B.
Show proof.
exists (hset_equiv_iso A B).
apply hset_equiv_iso_is_equiv.
apply hset_equiv_iso_is_equiv.