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).
Show proof.
Lemma ZeroObject_equals_TerminalObject (Z : Zero) :
ZeroObject Z = TerminalObject (Zero_to_Terminal Z).
Show proof.
ZeroObject Z = InitialObject (Zero_to_Initial Z).
Show proof.
Lemma ZeroObject_equals_TerminalObject (Z : Zero) :
ZeroObject Z = TerminalObject (Zero_to_Terminal Z).
Show proof.
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).
Show proof.
Lemma ZeroArrowToUnique (Z : Zero) (c : C) (f : C⟦c, ZeroObject Z⟧) :
f = (ZeroArrowTo Z c).
Show proof.
f = (ZeroArrowFrom Z c).
Show proof.
Lemma ZeroArrowToUnique (Z : Zero) (c : C) (f : C⟦c, ZeroObject Z⟧) :
f = (ZeroArrowTo Z c).
Show proof.
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.
Show proof.
Corollary ArrowsToZero (Z : Zero) (c : C) (f g : C⟦c, ZeroObject Z⟧) :
f = g.
Show proof.
f = g.
Show proof.
eapply pathscomp0.
apply (ZeroArrowFromUnique Z c f).
apply pathsinv0.
apply (ZeroArrowFromUnique Z c g).
apply (ZeroArrowFromUnique Z c f).
apply pathsinv0.
apply (ZeroArrowFromUnique Z c g).
Corollary ArrowsToZero (Z : Zero) (c : C) (f g : C⟦c, ZeroObject Z⟧) :
f = g.
Show proof.
eapply pathscomp0.
apply (ZeroArrowToUnique Z c f).
apply pathsinv0.
apply (ZeroArrowToUnique Z c g).
apply (ZeroArrowToUnique Z c f).
apply pathsinv0.
apply (ZeroArrowToUnique Z c g).
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.
Show proof.
(g : C⟦ZeroObject Z, d⟧) : f · g = ZeroArrow Z c d.
Show proof.
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.
Show proof.
Lemma postcomp_with_ZeroArrow (Z : Zero) (a b c : C) (f : C⟦b, c⟧) :
ZeroArrow Z a b · f = ZeroArrow Z a c.
Show proof.
f · ZeroArrow Z b c = ZeroArrow Z a c.
Show proof.
Lemma postcomp_with_ZeroArrow (Z : Zero) (a b c : C) (f : C⟦b, c⟧) :
ZeroArrow Z a b · f = ZeroArrow Z a c.
Show proof.
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).
Show proof.
(f : C⟦ZeroObject Z, ZeroObject Z⟧) :
f = identity (ZeroObject Z).
Show proof.
The morphism from ZeroObject to ZeroObject is an isomorphisms.
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.
Show proof.
(I : Initial C) (T : Terminal C)
(e: iso (InitialObject I) (TerminalObject T)) : Zero.
Show 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.
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.
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))).
Show proof.
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))).
Show proof.
End def_zero.
Lemma equiv_isZero1 (c : C) :
limits.zero.isZero c -> isZero c.
Show proof.
Lemma equiv_isZero2 (c : C) :
limits.zero.isZero c <- isZero c.
Show 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).
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).
Definition equiv_Zero1 :
limits.zero.Zero C -> @Zero C.
Show proof.
Definition equiv_Zero2 :
limits.zero.Zero C <- @Zero C.
Show proof.
intros Z.
exact (limits.zero.make_Zero
(ZeroObject Z)
(equiv_isZero2
_ ((isInitial_Initial (Zero_to_Initial Z))
,,(isTerminal_Terminal (Zero_to_Terminal Z))))).
exact (limits.zero.make_Zero
(ZeroObject Z)
(equiv_isZero2
_ ((isInitial_Initial (Zero_to_Initial Z))
,,(isTerminal_Terminal (Zero_to_Terminal Z))))).
Lemma equiv_ZeroArrowTo (x : C) (Z : Zero) :
@limits.zero.ZeroArrowTo C (equiv_Zero2 Z) x = ZeroArrowTo Z x.
Show proof.
Lemma equiv_ZeroArrowFrom (x : C) (Z : Zero) :
@limits.zero.ZeroArrowFrom C (equiv_Zero2 Z) x = ZeroArrowFrom Z x.
Show proof.
Lemma equiv_ZeroArrow (x y : C) (Z : Zero) :
@limits.zero.ZeroArrow C (equiv_Zero2 Z) x y = ZeroArrow Z x y.
Show proof.
unfold limits.zero.ZeroArrow. unfold ZeroArrow.
rewrite equiv_ZeroArrowTo.
rewrite equiv_ZeroArrowFrom.
apply idpath.
rewrite equiv_ZeroArrowTo.
rewrite equiv_ZeroArrowFrom.
apply idpath.
End zero_coincides.
Following Initial and Terminal, we clear implicit arguments.