Library UniMath.CategoryTheory.Epis

Epis

Contents

  • Definition of Epis
  • Construction of the subcategory of Epis
  • Construction of Epis in functor categories
More proofs/definitions about epi can be found in EpiFacts

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Subcategory.Core.
Require Import UniMath.CategoryTheory.Core.Functors.

Local Open Scope cat.

Definition of Epis

Section def_epi.

  Variable C : precategory.
  Hypothesis hs : has_homsets C.

Definition and construction of isEpi.
  Definition isEpi {x y : C} (f : x --> y) : UU :=
    ∏ (z : C) (g h : y --> z), f · g = f · h -> g = h.

  Definition make_isEpi {x y : C} (f : x --> y)
             (H : ∏ (z : C) (g h : y --> z), f · g = f · h -> g = h) : isEpi f := H.

  Lemma isapropisEpi {y z : C} (f : y --> z) : isaprop (isEpi f).
  Show proof.
    apply impred_isaprop; intros t.
    apply impred_isaprop; intros g.
    apply impred_isaprop; intros h.
    apply impred_isaprop; intros H.
    apply hs.

Definition and construction of Epi.
  Definition Epi (x y : C) : UU := ∑ f : x --> y, isEpi f.
  Definition make_Epi {x y : C} (f : x --> y) (H : isEpi f) :
    Epi x y := tpair _ f H.

Gets the arrow out of Epi.
  Definition EpiArrow {x y : C} (E : Epi x y) : C⟦x, y⟧ := pr1 E.
  Coercion EpiArrow : Epi >-> precategory_morphisms.

  Definition EpiisEpi {x y : C} (E : Epi x y) : isEpi E := pr2 E.

Isomorphism to isEpi and Epi.
  Lemma is_iso_isEpi {x y : C} (f : x --> y) (H : is_z_isomorphism f) : isEpi f.
  Show proof.
    apply make_isEpi.
    intros z g h X.
    apply (pre_comp_with_z_iso_is_inj H).
    exact X.

  Lemma is_iso_Epi {x y : C} (f : x --> y) (H : is_z_isomorphism f) : Epi x y.
  Show proof.
    apply (make_Epi f (is_iso_isEpi f H)).

Identity to isEpi and Epi.
  Lemma identity_isEpi {x : C} : isEpi (identity x).
  Show proof.
    apply (is_iso_isEpi (identity x) (is_z_isomorphism_identity x)).

  Lemma identity_Epi {x : C} : Epi x x.
  Show proof.
    exact (tpair _ (identity x) (identity_isEpi)).

Composition of isEpis and Epis.
  Definition isEpi_comp {x y z : C} (f : x --> y) (g : y --> z) :
    isEpi f -> isEpi g -> isEpi (f · g).
  Show proof.
    intros X X0. unfold isEpi. intros z0 g0 h X1.
    repeat rewrite <- assoc in X1. apply X in X1. apply X0 in X1. apply X1.

  Definition Epi_comp {x y z : C} (E1 : Epi x y) (E2 : Epi y z) :
    Epi x z := tpair _ (E1 · E2) (isEpi_comp E1 E2 (pr2 E1) (pr2 E2)).

If precomposition of g with f is an epi, then g is an epi.
  Definition isEpi_precomp {x y z : C} (f : x --> y) (g : y --> z) : isEpi (f · g) -> isEpi g.
  Show proof.
    intros X. intros w φ ψ H.
    apply (maponpaths (λ g', f · g')) in H.
    repeat rewrite assoc in H.
    apply (X w _ _ H).

  Lemma isEpi_path {x y : C} (f1 f2 : x --> y) (e : f1 = f2) (isE : isEpi f1) : isEpi f2.
  Show proof.
    induction e. exact isE.

Transport of isEpi
  Lemma transport_target_isEpi {x y z : C} (f : x --> y) (E : isEpi f) (e : y = z) :
    isEpi (transportf (precategory_morphisms x) e f).
  Show proof.
    induction e. apply E.

  Lemma transport_source_isEpi {x y z : C} (f : y --> z) (E : isEpi f) (e : y = x) :
    isEpi (transportf (λ x' : ob C, precategory_morphisms x' z) e f).
  Show proof.
    induction e. apply E.

End def_epi.
Arguments isEpi [C] [x] [y] _.

Lemma precomp_with_epi_isincl {C : category} {A B : ob C} {f : A --> B} :
  isEpi f -> ∏ c, isincl (@precomp_with _ _ _ f c).
Show proof.
  intros is_epi ? ?.
  apply invproofirrelevance.
  intros z w.
  apply subtypePath; [intros ? ?; apply homset_property|].
  apply (is_epi _ (hfiberpr1 _ _ z) (hfiberpr1 _ _ w)).
  exact (hfiberpr2 _ _ z @ !hfiberpr2 _ _ w).

Construction of the subcategory consisting of all epis.

Section epis_subcategory.

  Variable C : category.

  Definition hsubtype_obs_isEpi : hsubtype C := (λ c : C, make_hProp _ isapropunit).

  Definition hsubtype_mors_isEpi : ∏ (a b : C), hsubtype (C⟦a, b⟧) :=
    (λ a b : C, (fun f : C⟦a, b⟧ => make_hProp _ (isapropisEpi C C f))).

  Definition subprecategory_of_epis : sub_precategories C.
  Show proof.
    use tpair.
    split.
    - exact hsubtype_obs_isEpi.
    - exact hsubtype_mors_isEpi.
    - cbn. unfold is_sub_precategory. cbn.
      split.
      + intros a tt. exact (identity_isEpi C).
      + apply isEpi_comp.

  Definition has_homsets_subprecategory_of_epis : has_homsets subprecategory_of_epis.
  Show proof.
    intros a b.
    apply is_set_sub_precategory_morphisms.

  Definition subprecategory_of_epis_ob (c : C) : ob (subprecategory_of_epis) := tpair _ c tt.

End epis_subcategory.

In functor categories epis can be constructed from pointwise epis

Section epis_functorcategories.

  Lemma is_nat_trans_epi_from_pointwise_epis (C D : precategory) (hs : has_homsets D)
        (F G : ob (functor_precategory C D hs)) (α : F --> G) (H : ∏ a : ob C, isEpi (pr1 α a)) :
    isEpi α.
  Show proof.
    intros G' β η H'.
    use (nat_trans_eq hs).
    intros x.
    set (H'' := nat_trans_eq_pointwise H' x). cbn in H''.
    apply (H x) in H''.
    exact H''.

End epis_functorcategories.