Library UniMath.CategoryTheory.limits.graphs.zero
Zero Objects
Zero objects are objects of precategory which are both initial objects and terminal object.Contents
- Definition of Zero
- Coincides with the direct definition
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.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.initial.
Require Import UniMath.CategoryTheory.limits.graphs.terminal.
Require Import UniMath.CategoryTheory.limits.zero.
Local Open Scope cat.
An object c is zero if it initial and terminal.
Construction of isZero for an object c from the conditions that the space
of all morphisms from c to any object d is contractible and and the space of
all morphisms from any object d to c is contractible.
Definition make_isZero (c : C) (H : (∏ (d : C), iscontr (c --> d))
× (∏ (d : C), iscontr (d --> c))) :
isZero c := make_isInitial c (dirprod_pr1 H),,make_isTerminal c (dirprod_pr2 H).
× (∏ (d : C), iscontr (d --> c))) :
isZero c := make_isInitial c (dirprod_pr1 H),,make_isTerminal c (dirprod_pr2 H).
Definition of Zero.
Definition Zero : UU := ∑ c : C, isZero c.
Definition make_Zero (c : C) (H : isZero c) : Zero := tpair _ c H.
Definition ZeroObject (Z : Zero) : C := pr1 Z.
Definition make_Zero (c : C) (H : isZero c) : Zero := tpair _ c H.
Definition ZeroObject (Z : Zero) : C := pr1 Z.
Construction of Initial and Terminal from Zero.
Definition Zero_to_Initial (Z : Zero) : Initial C :=
make_Initial (pr1 Z) (dirprod_pr1 (pr2 Z)).
Definition Zero_to_Terminal (Z : Zero) : Terminal C :=
make_Terminal (pr1 Z) (dirprod_pr2 (pr2 Z)).
make_Initial (pr1 Z) (dirprod_pr1 (pr2 Z)).
Definition Zero_to_Terminal (Z : Zero) : Terminal C :=
make_Terminal (pr1 Z) (dirprod_pr2 (pr2 Z)).
The following lemmas show that the underlying objects of Initial
and Terminal, constructed above, are equal to ZeroObject.
Lemma ZeroObject_equals_InitialObject (Z : Zero) :
ZeroObject Z = InitialObject (Zero_to_Initial Z).
Proof.
apply idpath.
Defined.
Lemma ZeroObject_equals_TerminalObject (Z : Zero) :
ZeroObject Z = TerminalObject (Zero_to_Terminal Z).
Proof.
apply idpath.
Defined.
ZeroObject Z = InitialObject (Zero_to_Initial Z).
Proof.
apply idpath.
Defined.
Lemma ZeroObject_equals_TerminalObject (Z : Zero) :
ZeroObject Z = TerminalObject (Zero_to_Terminal Z).
Proof.
apply idpath.
Defined.
We construct morphisms from ZeroObject to any other object c and from any
other object c to the ZeroObject.
Definition ZeroArrowFrom (Z : Zero) (c : C) : C⟦ZeroObject Z, c⟧ :=
InitialArrow (Zero_to_Initial Z) c.
Definition ZeroArrowTo (Z : Zero) (c : C) : C⟦c, ZeroObject Z⟧ :=
TerminalArrow (Zero_to_Terminal Z) c.
InitialArrow (Zero_to_Initial Z) c.
Definition ZeroArrowTo (Z : Zero) (c : C) : C⟦c, ZeroObject Z⟧ :=
TerminalArrow (Zero_to_Terminal Z) c.
In particular, we get a zero morphism between any objects.
Definition ZeroArrow (Z : Zero) (c d : C) : C⟦c, d⟧ :=
@compose C _ (ZeroObject Z) _ (ZeroArrowTo Z c) (ZeroArrowFrom Z d).
@compose C _ (ZeroObject Z) _ (ZeroArrowTo Z c) (ZeroArrowFrom Z d).
We show that the above morphisms from ZeroObject and to ZeroObject are
unique by using uniqueness of the morphism from InitialObject and uniqueness
of the morphism to TerminalObject.
Lemma ZeroArrowFromUnique (Z : Zero) (c : C) (f : C⟦ZeroObject Z, c⟧) :
f = (ZeroArrowFrom Z c).
Proof.
apply (InitialArrowUnique (Zero_to_Initial Z) c f).
Defined.
Lemma ZeroArrowToUnique (Z : Zero) (c : C) (f : C⟦c, ZeroObject Z⟧) :
f = (ZeroArrowTo Z c).
Proof.
apply (TerminalArrowUnique (Zero_to_Terminal Z) c f).
Defined.
f = (ZeroArrowFrom Z c).
Proof.
apply (InitialArrowUnique (Zero_to_Initial Z) c f).
Defined.
Lemma ZeroArrowToUnique (Z : Zero) (c : C) (f : C⟦c, ZeroObject Z⟧) :
f = (ZeroArrowTo Z c).
Proof.
apply (TerminalArrowUnique (Zero_to_Terminal Z) c f).
Defined.
Therefore, any two morphisms from the ZeroObject to an object c are
equal and any two morphisms from an object c to the ZeroObject are equal.
Corollary ArrowsFromZero (Z : Zero) (c : C) (f g : C⟦ZeroObject Z, c⟧) :
f = g.
Proof.
eapply pathscomp0.
apply (ZeroArrowFromUnique Z c f).
apply pathsinv0.
apply (ZeroArrowFromUnique Z c g).
Defined.
Corollary ArrowsToZero (Z : Zero) (c : C) (f g : C⟦c, ZeroObject Z⟧) :
f = g.
Proof.
eapply pathscomp0.
apply (ZeroArrowToUnique Z c f).
apply pathsinv0.
apply (ZeroArrowToUnique Z c g).
Defined.
f = g.
Proof.
eapply pathscomp0.
apply (ZeroArrowFromUnique Z c f).
apply pathsinv0.
apply (ZeroArrowFromUnique Z c g).
Defined.
Corollary ArrowsToZero (Z : Zero) (c : C) (f g : C⟦c, ZeroObject Z⟧) :
f = g.
Proof.
eapply pathscomp0.
apply (ZeroArrowToUnique Z c f).
apply pathsinv0.
apply (ZeroArrowToUnique Z c g).
Defined.
It follows that any morphism which factors through 0 is the ZeroArrow.
Corollary ZeroArrowUnique (Z : Zero) (c d : C) (f : C⟦c, ZeroObject Z⟧)
(g : C⟦ZeroObject Z, d⟧) : f · g = ZeroArrow Z c d.
Proof.
rewrite (ZeroArrowToUnique Z c f).
rewrite (ZeroArrowFromUnique Z d g).
apply idpath.
Defined.
(g : C⟦ZeroObject Z, d⟧) : f · g = ZeroArrow Z c d.
Proof.
rewrite (ZeroArrowToUnique Z c f).
rewrite (ZeroArrowFromUnique Z d g).
apply idpath.
Defined.
Compose any morphism with the ZeroArrow and you get the ZeroArrow.
Lemma precomp_with_ZeroArrow (Z : Zero) (a b c : C) (f : C⟦a, b⟧) :
f · ZeroArrow Z b c = ZeroArrow Z a c.
Proof.
unfold ZeroArrow at 1. rewrite assoc.
apply ZeroArrowUnique.
Defined.
Lemma postcomp_with_ZeroArrow (Z : Zero) (a b c : C) (f : C⟦b, c⟧) :
ZeroArrow Z a b · f = ZeroArrow Z a c.
Proof.
unfold ZeroArrow at 1. rewrite <- assoc.
apply ZeroArrowUnique.
Defined.
f · ZeroArrow Z b c = ZeroArrow Z a c.
Proof.
unfold ZeroArrow at 1. rewrite assoc.
apply ZeroArrowUnique.
Defined.
Lemma postcomp_with_ZeroArrow (Z : Zero) (a b c : C) (f : C⟦b, c⟧) :
ZeroArrow Z a b · f = ZeroArrow Z a c.
Proof.
unfold ZeroArrow at 1. rewrite <- assoc.
apply ZeroArrowUnique.
Defined.
An endomorphism of the ZeroObject is the identity morphism.
Corollary ZeroEndo_is_identity (Z : Zero)
(f : C⟦ZeroObject Z, ZeroObject Z⟧) :
f = identity (ZeroObject Z).
Proof.
apply ArrowsFromZero.
Defined.
(f : C⟦ZeroObject Z, ZeroObject Z⟧) :
f = identity (ZeroObject Z).
Proof.
apply ArrowsFromZero.
Defined.
The morphism from ZeroObject to ZeroObject is an isomorphisms.
Lemma isiso_from_Zero_to_Zero (Z Z' : Zero) :
is_iso (ZeroArrowFrom Z (ZeroObject Z')).
Proof.
apply (is_iso_qinv _ (ZeroArrowFrom Z' (ZeroObject Z))).
split; apply ArrowsFromZero.
Defined.
is_iso (ZeroArrowFrom Z (ZeroObject Z')).
Proof.
apply (is_iso_qinv _ (ZeroArrowFrom Z' (ZeroObject Z))).
split; apply ArrowsFromZero.
Defined.
Using the above lemma we can construct an isomorphisms between any two
ZeroObjects.
Definition iso_Zeros (Z Z' : Zero) : iso (ZeroObject Z) (ZeroObject Z') :=
tpair _ (ZeroArrowFrom Z (ZeroObject Z')) (isiso_from_Zero_to_Zero Z Z').
Definition hasZero := ishinh Zero.
tpair _ (ZeroArrowFrom Z (ZeroObject Z')) (isiso_from_Zero_to_Zero Z Z').
Definition hasZero := ishinh Zero.
Construct Zero from Initial and Terminal for which the underlying objects
are isomorphic.
Definition Initial_and_Terminal_to_Zero
(I : Initial C) (T : Terminal C)
(e: iso (InitialObject I) (TerminalObject T)) : Zero.
Proof.
use (make_Zero (InitialObject I)).
split.
- use (make_isInitial (InitialObject I)); intro b.
apply make_iscontr with (x := (InitialArrow I b)), InitialArrowUnique.
- use (make_isTerminal (InitialObject I)); intro a.
apply (iscontrretract (postcomp_with (inv_from_iso e))
(postcomp_with (morphism_from_iso e))).
intros y. unfold postcomp_with.
rewrite <- assoc. rewrite (iso_inv_after_iso e).
apply (remove_id_right _ _ _ y y _ (idpath _) (idpath _)).
apply (make_iscontr (TerminalArrow T a)), TerminalArrowUnique.
Defined.
(I : Initial C) (T : Terminal C)
(e: iso (InitialObject I) (TerminalObject T)) : Zero.
Proof.
use (make_Zero (InitialObject I)).
split.
- use (make_isInitial (InitialObject I)); intro b.
apply make_iscontr with (x := (InitialArrow I b)), InitialArrowUnique.
- use (make_isTerminal (InitialObject I)); intro a.
apply (iscontrretract (postcomp_with (inv_from_iso e))
(postcomp_with (morphism_from_iso e))).
intros y. unfold postcomp_with.
rewrite <- assoc. rewrite (iso_inv_after_iso e).
apply (remove_id_right _ _ _ y y _ (idpath _) (idpath _)).
apply (make_iscontr (TerminalArrow T a)), TerminalArrowUnique.
Defined.
The following lemma verifies that the ZeroObject of the Zero,
constructed from Initial and Terminal with InitialObject isomorphic to
TerminalObject, is isomorphic to the InitialObject and isomorphic to the
TerminalObject.
Lemma Initial_and_Terminal_ob_equals_Zero_ob (I : Initial C)
(T :Terminal C) (e : iso (InitialObject I) (TerminalObject T)) :
(iso (InitialObject I) (ZeroObject (Initial_and_Terminal_to_Zero I T e)))
× (iso (TerminalObject T)
(ZeroObject (Initial_and_Terminal_to_Zero I T e))).
Proof.
exact(identity_iso (InitialObject I),,iso_inv_from_iso e).
Defined.
End def_zero.
(T :Terminal C) (e : iso (InitialObject I) (TerminalObject T)) :
(iso (InitialObject I) (ZeroObject (Initial_and_Terminal_to_Zero I T e)))
× (iso (TerminalObject T)
(ZeroObject (Initial_and_Terminal_to_Zero I T e))).
Proof.
exact(identity_iso (InitialObject I),,iso_inv_from_iso e).
Defined.
End def_zero.
Lemma equiv_isZero1 (c : C) :
limits.zero.isZero c → isZero c.
Proof.
intros X.
use make_isZero.
split.
- intros d. apply ((pr1 X) d).
- intros d. apply ((pr2 X) d).
Qed.
Lemma equiv_isZero2 (c : C) :
limits.zero.isZero c <- isZero c.
Proof.
intros X.
set (XZ := make_Zero c X).
split.
- intros b.
use tpair.
apply (InitialArrow (Zero_to_Initial XZ) b).
intros t.
use (InitialArrowUnique (Zero_to_Initial XZ) b).
- intros a.
use tpair.
apply (TerminalArrow (Zero_to_Terminal XZ) a).
intros t.
use (TerminalArrowUnique (Zero_to_Terminal XZ) a).
Qed.
Definition equiv_Zero1 :
limits.zero.Zero C → @Zero C.
Proof.
intros Z.
exact (make_Zero Z (equiv_isZero1 _ (pr2 Z))).
Defined.
Definition equiv_Zero2 :
limits.zero.Zero C <- @Zero C.
Proof.
intros Z.
exact (limits.zero.make_Zero
(ZeroObject Z)
(equiv_isZero2
_ ((isInitial_Initial (Zero_to_Initial Z))
,,(isTerminal_Terminal (Zero_to_Terminal Z))))).
Defined.
Lemma equiv_ZeroArrowTo (x : C) (Z : Zero) :
@limits.zero.ZeroArrowTo C (equiv_Zero2 Z) x = ZeroArrowTo Z x.
Proof.
apply ZeroArrowToUnique.
Qed.
Lemma equiv_ZeroArrowFrom (x : C) (Z : Zero) :
@limits.zero.ZeroArrowFrom C (equiv_Zero2 Z) x = ZeroArrowFrom Z x.
Proof.
apply ZeroArrowFromUnique.
Qed.
Lemma equiv_ZeroArrow (x y : C) (Z : Zero) :
@limits.zero.ZeroArrow C (equiv_Zero2 Z) x y = ZeroArrow Z x y.
Proof.
unfold limits.zero.ZeroArrow. unfold ZeroArrow.
rewrite equiv_ZeroArrowTo.
rewrite equiv_ZeroArrowFrom.
apply idpath.
Qed.
End zero_coincides.
Following Initial and Terminal, we clear implicit arguments.