Library HoTT.WildCat.PointedCat
Require Import Basics.Overture Basics.Tactics.
Require Import WildCat.Core WildCat.Opposite.
Require Import WildCat.Equiv.
Require Import WildCat.Core WildCat.Opposite.
Require Import WildCat.Equiv.
A wild category is pointed if the initial and terminal object are the same.
Class IsPointedCat (A : Type) `{Is1Cat A} := {
zero_object : A;
isinitial_zero_object :: IsInitial zero_object;
isterminal_zero_object :: IsTerminal zero_object;
}.
zero_object : A;
isinitial_zero_object :: IsInitial zero_object;
isterminal_zero_object :: IsTerminal zero_object;
}.
The zero morphism between objects a and b of a pointed category A is the unique morphism that factors through the zero object.
Definition zero_morphism {A : Type} `{IsPointedCat A} {a b : A} : a $-> b
:= (mor_initial _ b) $o (mor_terminal a _).
:= (mor_initial _ b) $o (mor_terminal a _).
The opposite category of a pointed category is also pointed.
Instance ispointedcat_op {A : Type} `{IsPointedCat A} : IsPointedCat A^op.
Proof.
snapply Build_IsPointedCat.
1: unfold op; exact zero_object.
1,2: exact _.
Defined.
Section ZeroLaws.
Context {A : Type} `{IsPointedCat A} {a b c : A}
(f : a $-> b) (g : b $-> c).
Definition cat_zero_source (h : zero_object $-> a) : h $== zero_morphism
:= mor_initial_unique' _ _ _ _.
Definition cat_zero_target (h : a $-> zero_object) : h $== zero_morphism
:= mor_terminal_unique' _ _ _ _.
Proof.
snapply Build_IsPointedCat.
1: unfold op; exact zero_object.
1,2: exact _.
Defined.
Section ZeroLaws.
Context {A : Type} `{IsPointedCat A} {a b c : A}
(f : a $-> b) (g : b $-> c).
Definition cat_zero_source (h : zero_object $-> a) : h $== zero_morphism
:= mor_initial_unique' _ _ _ _.
Definition cat_zero_target (h : a $-> zero_object) : h $== zero_morphism
:= mor_terminal_unique' _ _ _ _.
We show the last two arguments so that end points can easily be specified.
Arguments zero_morphism {_ _ _ _ _ _} _ _.
Definition cat_zero_l : zero_morphism b c $o f $== zero_morphism a c.
Proof.
refine (cat_assoc _ _ _ $@ (_ $@L _^$)).
apply mor_terminal_unique.
Defined.
Definition cat_zero_r : g $o zero_morphism a b $== zero_morphism a c.
Proof.
refine ((_ $@R _) $@ cat_assoc _ _ _)^$.
apply mor_initial_unique.
Defined.
Definition cat_zero_l : zero_morphism b c $o f $== zero_morphism a c.
Proof.
refine (cat_assoc _ _ _ $@ (_ $@L _^$)).
apply mor_terminal_unique.
Defined.
Definition cat_zero_r : g $o zero_morphism a b $== zero_morphism a c.
Proof.
refine ((_ $@R _) $@ cat_assoc _ _ _)^$.
apply mor_initial_unique.
Defined.
Any morphism which factors through an initial object is homotopic to the zero morphism.
Definition cat_zero_m_through_initial `{isinitial : !IsInitial b}
: g $o f $== zero_morphism a c.
Proof.
unfold zero_morphism.
pose (h := mor_initial b zero_object).
rhs' rapply (_ $@L mor_terminal_unique _ _ (h $o f)).
rhs_V' rapply cat_assoc.
exact (mor_initial_unique' _ _ _ _ $@R f).
Defined.
: g $o f $== zero_morphism a c.
Proof.
unfold zero_morphism.
pose (h := mor_initial b zero_object).
rhs' rapply (_ $@L mor_terminal_unique _ _ (h $o f)).
rhs_V' rapply cat_assoc.
exact (mor_initial_unique' _ _ _ _ $@R f).
Defined.
In particular, any morphism which factors through an object equivalent to the zero object is homotopic to the zero morphism.
Definition cat_zero_m_through_zero `{!HasEquivs A} (be : zero_object $<~> b)
: g $o f $== zero_morphism a c
:= cat_zero_m_through_initial (isinitial:=isinitial_cate _ _ _ be _).
End ZeroLaws.
: g $o f $== zero_morphism a c
:= cat_zero_m_through_initial (isinitial:=isinitial_cate _ _ _ be _).
End ZeroLaws.
We state the dual result outside of the section, so that the variables have been generalized.
Definition cat_zero_m_through_terminal {A : Type} `{IsPointedCat A}
{a b c : A} (f : a $-> b) (g : b $-> c) `{!IsTerminal b}
: g $o f $== zero_morphism
:= cat_zero_m_through_initial (A:=A^op) (a:=c) g f.
{a b c : A} (f : a $-> b) (g : b $-> c) `{!IsTerminal b}
: g $o f $== zero_morphism
:= cat_zero_m_through_initial (A:=A^op) (a:=c) g f.
We make the last two arguments explicit so that end points can easily be specified. We had to do this again, since the section encapsulated the previous attempt.
A functor is pointed if it preserves the zero object.
Class IsPointedFunctor {A B : Type} (F : A → B) `{Is1Functor A B F} :=
{
preservesinitial_pfunctor :: PreservesInitial F ;
preservesterminal_pfunctor :: PreservesTerminal F ;
}.
{
preservesinitial_pfunctor :: PreservesInitial F ;
preservesterminal_pfunctor :: PreservesTerminal F ;
}.
Here is an alternative constructor using preservation of the zero object. This requires more structure on the categories however.
Definition Build_IsPointedFunctor' {A B : Type} (F : A → B)
`{Is1Cat A, Is1Cat B, !Is0Functor F, !Is1Functor F}
`{!IsPointedCat A, !IsPointedCat B, !HasEquivs A, !HasEquivs B}
(p : F zero_object $<~> zero_object)
: IsPointedFunctor F.
Proof.
apply Build_IsPointedFunctor.
+ intros x inx.
rapply isinitial_cate.
symmetry.
refine (p $oE _).
rapply (emap F _).
rapply cate_isinitial.
+ intros x tex.
rapply isterminal_cate.
refine (p $oE _).
rapply (emap F _).
rapply cate_isterminal.
Defined.
`{Is1Cat A, Is1Cat B, !Is0Functor F, !Is1Functor F}
`{!IsPointedCat A, !IsPointedCat B, !HasEquivs A, !HasEquivs B}
(p : F zero_object $<~> zero_object)
: IsPointedFunctor F.
Proof.
apply Build_IsPointedFunctor.
+ intros x inx.
rapply isinitial_cate.
symmetry.
refine (p $oE _).
rapply (emap F _).
rapply cate_isinitial.
+ intros x tex.
rapply isterminal_cate.
refine (p $oE _).
rapply (emap F _).
rapply cate_isterminal.
Defined.
Pointed functors preserve the zero object up to isomorphism.
Lemma pfunctor_zero {A B : Type} (F : A → B)
`{IsPointedCat A, IsPointedCat B, !HasEquivs B,
!Is0Functor F, !Is1Functor F, !IsPointedFunctor F}
: F zero_object $<~> zero_object.
Proof.
rapply cate_isinitial.
Defined.
`{IsPointedCat A, IsPointedCat B, !HasEquivs B,
!Is0Functor F, !Is1Functor F, !IsPointedFunctor F}
: F zero_object $<~> zero_object.
Proof.
rapply cate_isinitial.
Defined.
Pointed functors preserve the zero morphism up to homotopy
Lemma fmap_zero_morphism {A B : Type} (F : A → B)
`{IsPointedCat A, IsPointedCat B,
!Is0Functor F, !Is1Functor F, !IsPointedFunctor F} {a b : A}
: fmap F (zero_morphism a b) $== zero_morphism (F a) (F b).
Proof.
lhs' rapply fmap_comp.
lhs' rapply (fmap_initial _ _ _ _ $@R _).
lhs' rapply (_ $@L fmap_terminal _ _ _ _).
rapply cat_zero_m_through_initial.
Defined.
`{IsPointedCat A, IsPointedCat B,
!Is0Functor F, !Is1Functor F, !IsPointedFunctor F} {a b : A}
: fmap F (zero_morphism a b) $== zero_morphism (F a) (F b).
Proof.
lhs' rapply fmap_comp.
lhs' rapply (fmap_initial _ _ _ _ $@R _).
lhs' rapply (_ $@L fmap_terminal _ _ _ _).
rapply cat_zero_m_through_initial.
Defined.
A pointed functor takes complexes to complexes.
Definition fmap_iscomplex {A B : Type} (F : A → B)
`{IsPointedCat A, IsPointedCat B,
!Is0Functor F, !Is1Functor F, !IsPointedFunctor F}
{x y z : A} {i : x $-> y} {f : y $-> z} (cx : f $o i $== zero_morphism x z)
: fmap F f $o fmap F i $== zero_morphism (F x) (F z)
:= (fmap_comp F i f)^$ $@ fmap2 F cx $@ fmap_zero_morphism F.
`{IsPointedCat A, IsPointedCat B,
!Is0Functor F, !Is1Functor F, !IsPointedFunctor F}
{x y z : A} {i : x $-> y} {f : y $-> z} (cx : f $o i $== zero_morphism x z)
: fmap F f $o fmap F i $== zero_morphism (F x) (F z)
:= (fmap_comp F i f)^$ $@ fmap2 F cx $@ fmap_zero_morphism F.