Library UniMath.CategoryTheory.Subcategory.Core
Sub(pre)categories
Contents :
- Subprecategories
- A sub-precategory forms a precategory (carrier_of_sub_precategory)
- (Inclusion) functor from a sub-precategory to the ambient precategory (sub_precategory_inclusion)
- Subcategories (subcategory)
- Restriction of a functor to a subcategory
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Local Open Scope cat.
Definitions
Definition is_sub_precategory {C : category}
(C' : hsubtype C)
(Cmor' : ∏ a b : C, hsubtype (a --> b)) :=
(∏ a : C, C' a -> Cmor' _ _ (identity a)) ×
(∏ (a b c : C) (f: a --> b) (g : b --> c),
Cmor' _ _ f -> Cmor' _ _ g -> Cmor' _ _ (f · g)).
Definition sub_precategories (C : category) :=
total2 (fun C' : (hsubtype (ob C)) × (∏ a b:ob C, hsubtype (a --> b)) =>
is_sub_precategory (pr1 C') (pr2 C')).
We have a coercion carrier turning every predicate P on a type A into the
total space { a : A & P a} .
For later, we define some projections with the appropriate type, also to
avoid confusion with the aforementioned coercion.
Definition sub_precategory_predicate_objects {C : category}
(C': sub_precategories C):
hsubtype (ob C) := pr1 (pr1 C').
Definition sub_ob {C : category}(C': sub_precategories C): UU :=
(sub_precategory_predicate_objects C').
Definition sub_precategory_predicate_morphisms {C : category}
(C':sub_precategories C) (a b : C) : hsubtype (a --> b) := pr2 (pr1 C') a b.
Definition sub_precategory_morphisms {C : category}(C':sub_precategories C)
(a b : C) : UU := sub_precategory_predicate_morphisms C' a b.
Projections for compatibility of the predicate with identity and
composition.
Definition sub_precategory_id (C : category) (C':sub_precategories C) :
∏ a : ob C,
sub_precategory_predicate_objects C' a ->
sub_precategory_predicate_morphisms C' _ _ (identity a) :=
dirprod_pr1 (pr2 C').
Definition sub_precategory_comp (C : category) (C':sub_precategories C) :
∏ (a b c: ob C) (f: a --> b) (g : b --> c),
sub_precategory_predicate_morphisms C' _ _ f ->
sub_precategory_predicate_morphisms C' _ _ g ->
sub_precategory_predicate_morphisms C' _ _ (f · g) :=
dirprod_pr2 (pr2 C').
An object of a subprecategory is an object of the original precategory.
Definition precategory_object_from_sub_precategory_object (C:category)
(C':sub_precategories C) (a : sub_ob C') :
ob C := pr1 a.
Coercion precategory_object_from_sub_precategory_object :
sub_ob >-> ob.
A morphism of a subprecategory is also a morphism of the original precategory.
Definition precategory_morphism_from_sub_precategory_morphism (C:category)
(C':sub_precategories C) (a b : ob C)
(f : sub_precategory_morphisms C' a b) : a --> b := pr1 f .
Coercion precategory_morphism_from_sub_precategory_morphism :
sub_precategory_morphisms >-> precategory_morphisms.
Definition sub_precategory_ob_mor (C : category)(C':sub_precategories C) :
precategory_ob_mor.
Show proof.
Definition sub_precategory_data (C : category)(C':sub_precategories C) :
precategory_data.
Show proof.
exists (sub_precategory_ob_mor C C').
split.
intro c.
exists (identity (C:=C) (pr1 c)).
apply sub_precategory_id.
apply (pr2 c).
intros a b c f g.
exists (compose (pr1 f) (pr1 g)).
apply sub_precategory_comp.
apply (pr2 f). apply (pr2 g).
split.
intro c.
exists (identity (C:=C) (pr1 c)).
apply sub_precategory_id.
apply (pr2 c).
intros a b c f g.
exists (compose (pr1 f) (pr1 g)).
apply sub_precategory_comp.
apply (pr2 f). apply (pr2 g).
A useful lemma for equality in the sub-precategory.
Lemma eq_in_sub_precategory (C : category)(C':sub_precategories C)
(a b : sub_ob C') (f g : sub_precategory_morphisms C' a b) :
pr1 f = pr1 g -> f = g.
Show proof.
Definition is_precategory_sub_precategory (C : category)(C':sub_precategories C) :
is_precategory (sub_precategory_data C C').
Show proof.
repeat split;
simpl; intros.
unfold sub_precategory_comp;
apply eq_in_sub_precategory; simpl;
apply id_left.
apply eq_in_sub_precategory. simpl.
apply id_right.
apply eq_in_sub_precategory.
cbn.
apply assoc.
apply eq_in_sub_precategory.
cbn.
apply assoc'.
simpl; intros.
unfold sub_precategory_comp;
apply eq_in_sub_precategory; simpl;
apply id_left.
apply eq_in_sub_precategory. simpl.
apply id_right.
apply eq_in_sub_precategory.
cbn.
apply assoc.
apply eq_in_sub_precategory.
cbn.
apply assoc'.
Definition carrier_of_sub_precategory (C : category)(C':sub_precategories C) :
precategory := tpair _ _ (is_precategory_sub_precategory C C').
Definition has_homsets_carrier_of_subcategory (C : category) (C' : sub_precategories C)
: has_homsets (carrier_of_sub_precategory C C').
Show proof.
intros a b.
cbn.
apply (isofhleveltotal2 2).
- apply C.
- intro f.
apply hlevelntosn.
apply propproperty.
cbn.
apply (isofhleveltotal2 2).
- apply C.
- intro f.
apply hlevelntosn.
apply propproperty.
Definition carrier_of_sub_category (C : category) (C' : sub_precategories C)
: category
:= make_category _ (has_homsets_carrier_of_subcategory C C').
Coercion carrier_of_sub_category : sub_precategories >-> category.
An object satisfying the predicate is an object of the subprecategory
Definition precategory_object_in_subcat {C : category} {C':sub_precategories C}
(a : ob C) (p : sub_precategory_predicate_objects C' a) :
ob C' := tpair _ a p.
(a : ob C) (p : sub_precategory_predicate_objects C' a) :
ob C' := tpair _ a p.
A morphism satisfying the predicate is a morphism of the subprecategory
Definition precategory_morphisms_in_subcat {C : category} {C':sub_precategories C}
{a b : ob C'}(f : pr1 a --> pr1 b)
(p : sub_precategory_predicate_morphisms C' (pr1 a) (pr1 b) (f)) :
precategory_morphisms (C:=C') a b := tpair _ f p.
{a b : ob C'}(f : pr1 a --> pr1 b)
(p : sub_precategory_predicate_morphisms C' (pr1 a) (pr1 b) (f)) :
precategory_morphisms (C:=C') a b := tpair _ f p.
A (z-)isomorphism of a subprecategory is also a (z-)isomorphism of the original precategory.
Lemma is_z_iso_from_is_z_iso_in_subcategory (C:category) (C':sub_precategories C)
(a b : C') (f : C'⟦ a , b ⟧)
(H: is_z_isomorphism f)
: is_z_isomorphism
(precategory_morphism_from_sub_precategory_morphism _ _ _ _ f).
Show proof.
(a b : C') (f : C'⟦ a , b ⟧)
(H: is_z_isomorphism f)
: is_z_isomorphism
(precategory_morphism_from_sub_precategory_morphism _ _ _ _ f).
Show proof.
induction H as (g,(gl,gr)).
induction g as (g_und,?).
use make_is_z_isomorphism.
+ exact g_und.
+ split.
- exact (maponpaths pr1 gl).
- exact (maponpaths pr1 gr).
induction g as (g_und,?).
use make_is_z_isomorphism.
+ exact g_und.
+ split.
- exact (maponpaths pr1 gl).
- exact (maponpaths pr1 gr).
Definition sub_precategory_inclusion_data (C : category) (C':sub_precategories C):
functor_data C' C.
Show proof.
Definition is_functor_sub_precategory_inclusion (C : category)
(C':sub_precategories C) :
is_functor (sub_precategory_inclusion_data C C').
Show proof.
split; simpl.
unfold functor_idax . intros. apply (idpath _ ).
unfold functor_compax . intros. apply (idpath _ ).
unfold functor_idax . intros. apply (idpath _ ).
unfold functor_compax . intros. apply (idpath _ ).
Definition sub_precategory_inclusion (C : category) (C' : sub_precategories C) :
functor C' C := tpair _ _ (is_functor_sub_precategory_inclusion C C').
Subcategories
Lemma is_set_sub_precategory_morphisms {C : category}
(C' : sub_precategories C) (a b : ob C) :
isaset (sub_precategory_morphisms C' a b).
Show proof.
Definition sub_precategory_morphisms_set {C : category}
(C':sub_precategories C) (a b : ob C) : hSet :=
tpair _ (sub_precategory_morphisms C' a b)
(is_set_sub_precategory_morphisms C' a b).
Definition subcategory (C : category) (C' : sub_precategories C) : category.
Show proof.
use make_category.
- exact (carrier_of_sub_precategory C C').
- intros ? ?.
apply is_set_sub_precategory_morphisms.
- exact (carrier_of_sub_precategory C C').
- intros ? ?.
apply is_set_sub_precategory_morphisms.
Definition restrict_functor_to_sub_precategory {C D : category}
(C' : sub_precategories C) (F : functor C D) : functor C' D.
Show proof.
use make_functor.
- use make_functor_data.
+ exact (F ∘ precategory_object_from_sub_precategory_object _ C')%functions.
+ intros ? ?.
apply (# F ∘ precategory_morphism_from_sub_precategory_morphism _ C' _ _)%functions.
- use make_dirprod.
+ intro; apply (functor_id F).
+ intros ? ? ? ? ?; apply (functor_comp F).
- use make_functor_data.
+ exact (F ∘ precategory_object_from_sub_precategory_object _ C')%functions.
+ intros ? ?.
apply (# F ∘ precategory_morphism_from_sub_precategory_morphism _ C' _ _)%functions.
- use make_dirprod.
+ intro; apply (functor_id F).
+ intros ? ? ? ? ?; apply (functor_comp F).