(** * Zero objects in categories

    Zero objects (both initial and terminal) and zero morphisms, foundational
    concepts for additive and stable category theory.
*)

From HoTT Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics.
From HoTT.Categories Require Import Category.Core Category.Objects.

Local Open Scope morphism_scope.

(** * Zero objects
    
    A zero object in a category is an object that is both initial and terminal.
    Such objects play a fundamental role in additive and abelian categories,
    where they enable the definition of zero morphisms and kernels.
*)

Class ZeroObject (C : PreCategory) := {
  zero : object C;
  is_initial :: IsInitialObject C zero;
  is_terminal :: IsTerminalObject C zero
}.

Coercion zero : ZeroObject >-> object.

Arguments zero {C} z : rename.
Arguments is_initial {C} z : rename.
Arguments is_terminal {C} z : rename.

Instance initialobject_zeroobject {C : PreCategory} (Z : ZeroObject C)
  : InitialObject C
  := {| object_initial := zero Z; isinitial_object_initial := _ |}.

Instance terminalobject_zeroobject {C : PreCategory} (Z : ZeroObject C)
  : TerminalObject C
  := {| object_terminal := zero Z; isterminal_object_terminal := _ |}.

(** The zero morphism between any two objects is the unique morphism
    that factors through the zero object. *)

Definition zero_morphism {C : PreCategory} {Z : ZeroObject C} (X Y : object C)
  : morphism C X Y
  := morphism_from_initial Y o morphism_to_terminal X.

Arguments zero_morphism {C Z} X Y : simpl never.

(** * Basic properties of zero objects *)

(** ** Properties of zero morphisms *)

(** Any morphism that factors through a zero object is the zero morphism. *)
Lemma morphism_through_zero_is_zero {C : PreCategory} 
  {Z : ZeroObject C} {X Y : object C}
  (f : morphism C X Z)
  (g : morphism C Z Y)
  : g o f = zero_morphism X Y.
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
g o f = zero_morphism X Y
Proof.
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
g o f = zero_morphism X Y
  unfold zero_morphism.
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
g o f = morphism_from_initial Y o morphism_to_terminal X
  apply ap011.
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
g = morphism_from_initial Y
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
f = morphism_to_terminal X
  -
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
g = morphism_from_initial Y rapply initial_morphism_unique.
  -
C: PreCategory
Z: ZeroObject C
X, Y: C
f: morphism C X Z
g: morphism C Z Y
f = morphism_to_terminal X rapply terminal_morphism_unique.
Qed.

(** ** Composition properties of zero morphisms *)

(** Composition with zero morphism on the right. *)
Lemma zero_morphism_right {C : PreCategory} {Z : ZeroObject C}
  {X Y W : object C}
  (g : morphism C Y W)
  : g o zero_morphism X Y = zero_morphism X W.
C: PreCategory
Z: ZeroObject C
X, Y, W: C
g: morphism C Y W
g o zero_morphism X Y = zero_morphism X W
Proof.
C: PreCategory
Z: ZeroObject C
X, Y, W: C
g: morphism C Y W
g o zero_morphism X Y = zero_morphism X W
  rewrite <- associativity.
C: PreCategory
Z: ZeroObject C
X, Y, W: C
g: morphism C Y W
g o morphism_from_initial Y o morphism_to_terminal X = zero_morphism X W
  apply morphism_through_zero_is_zero.
Qed.

(** Composition with zero morphism on the left. *)
Lemma zero_morphism_left {C : PreCategory} {Z : ZeroObject C}
  {X Y W : object C}
  (f : morphism C X Y)
  : zero_morphism Y W o f = zero_morphism X W.
C: PreCategory
Z: ZeroObject C
X, Y, W: C
f: morphism C X Y
zero_morphism Y W o f = zero_morphism X W
Proof.
C: PreCategory
Z: ZeroObject C
X, Y, W: C
f: morphism C X Y
zero_morphism Y W o f = zero_morphism X W
  rewrite associativity.
C: PreCategory
Z: ZeroObject C
X, Y, W: C
f: morphism C X Y
morphism_from_initial W o (morphism_to_terminal Y o f) = zero_morphism X W
  apply morphism_through_zero_is_zero.
Qed.

(** ** Export hints *)

Hint Rewrite @zero_morphism_left @zero_morphism_right : zero_morphism.