(** * Additive categories

    Semi-additive categories in which morphism addition admits inverses,
    so that hom-sets are abelian groups and composition is bilinear. *)

From HoTT Require Import Basics.Overture Basics.Tactics.
From HoTT.Classes.interfaces Require Import canonical_names abstract_algebra.
From HoTT.Categories Require Import Category.Core Functor.Core.
From HoTT.Categories.Functor Require Import Identity Composition.Core.
From HoTT.Categories.Additive Require Import ZeroObjects SemiAdditive.
From HoTT.Algebra.AbGroups Require Import AbelianGroup.

Local Open Scope morphism_scope.

(** This lets us use "+", "-" and "0" notation for the commutative monoid
    structure on hom-sets defined in SemiAdditive.v. *)
Local Open Scope mc_add_scope.

(** ** Definition of additive category

    The commutative monoid structure on hom-sets of a semi-additive category
    is canonical, so an additive category only needs to assume that each
    morphism has an additive inverse. *)

Class AdditiveCategory := {
  additive_semiadditive :: SemiAdditiveCategory;

  additive_inverse :: forall (X Y : object additive_semiadditive),
    Inverse (morphism additive_semiadditive X Y);

  additive_inverse_l : forall {X Y : object additive_semiadditive}
    (f : morphism additive_semiadditive X Y),
    (- f) + f = 0;
}.

Coercion additive_semiadditive : AdditiveCategory >-> SemiAdditiveCategory.

(** ** Hom-sets are abelian groups *)

Section HomAbGroup.
  Context {A : AdditiveCategory} (X Y : object A).

  (** The bundled abelian group of morphisms from [X] to [Y]. *)
  Definition abgroup_hom : AbGroup
    := Build_AbGroup' (morphism A X Y) _ _ _ additive_inverse_l.

  #[export] Instance isabgroup_morphisms : IsAbGroup (morphism A X Y)
    := @isabgroup_abgroup abgroup_hom.

End HomAbGroup.

(** ** Negation and composition *)

(** A left additive inverse equals the negation. *)
Definition hom_moveL_1V {A : AdditiveCategory} {X Y : object A}
  {f g : morphism A X Y} (H : g + f = 0)
  : g = - f
  := grp_moveL_1V (G:=abgroup_hom X Y) H.

(** Negation is compatible with precomposition. *)
Definition inverse_precompose {A : AdditiveCategory} {X Y W : object A}
  (f : morphism A X Y) (a : morphism A W X)
  : (- f) o a = - (f o a).
A: AdditiveCategory
X, Y, W: A
f: morphism A X Y
a: morphism A W X
- f o a = - (f o a)
Proof.
A: AdditiveCategory
X, Y, W: A
f: morphism A X Y
a: morphism A W X
- f o a = - (f o a)
  apply hom_moveL_1V.
A: AdditiveCategory
X, Y, W: A
f: morphism A X Y
a: morphism A W X
- f o a + f o a = 0
  lhs_V napply addition_precompose.
A: AdditiveCategory
X, Y, W: A
f: morphism A X Y
a: morphism A W X
(- f + f) o a = 0
  lhs napply (ap (fun g => g o a) (additive_inverse_l f)).
A: AdditiveCategory
X, Y, W: A
f: morphism A X Y
a: morphism A W X
0 o a = 0
  napply zero_morphism_left.
Qed.

(** Negation is compatible with postcomposition. *)
Definition inverse_postcompose {A : AdditiveCategory} {X Y W : object A}
  (a : morphism A Y W) (f : morphism A X Y)
  : a o (- f) = - (a o f).
A: AdditiveCategory
X, Y, W: A
a: morphism A Y W
f: morphism A X Y
a o - f = - (a o f)
Proof.
A: AdditiveCategory
X, Y, W: A
a: morphism A Y W
f: morphism A X Y
a o - f = - (a o f)
  apply hom_moveL_1V.
A: AdditiveCategory
X, Y, W: A
a: morphism A Y W
f: morphism A X Y
a o - f + a o f = 0
  lhs_V napply addition_postcompose.
A: AdditiveCategory
X, Y, W: A
a: morphism A Y W
f: morphism A X Y
a o (- f + f) = 0
  lhs napply (ap (fun g => a o g) (additive_inverse_l f)).
A: AdditiveCategory
X, Y, W: A
a: morphism A Y W
f: morphism A X Y
a o 0 = 0
  napply zero_morphism_right.
Qed.

(** ** Additive functors

    A functor between additive categories is additive when its action on
    each hom-set is a monoid homomorphism for the canonical addition.
    Such functors automatically preserve zero morphisms and negation. *)

Record AdditiveFunctor (A B : AdditiveCategory) := {
  addfunctor :> Functor A B;

  ismonoidpreserving_addfunctor :: forall (X Y : object A),
    IsMonoidPreserving (@morphism_of _ _ addfunctor X Y);
}.

Arguments addfunctor {A B} F : rename.
Arguments ismonoidpreserving_addfunctor {A B} F X Y : rename.

(** The identity functor is additive. *)
Definition id_additive_functor (A : AdditiveCategory)
  : AdditiveFunctor A A.
A: AdditiveCategory
AdditiveFunctor A A
Proof.
A: AdditiveCategory
AdditiveFunctor A A
  snapply Build_AdditiveFunctor.
A: AdditiveCategory
Functor A A
A: AdditiveCategory
forall X Y : A, IsMonoidPreserving (morphism_of ?addfunctor (d:=Y))
  -
A: AdditiveCategory
Functor A A exact 1%functor.
  -
A: AdditiveCategory
forall X Y : A, IsMonoidPreserving (morphism_of 1 (d:=Y)) intros X Y.
A: AdditiveCategory
X, Y: A
IsMonoidPreserving (morphism_of 1 (d:=Y))
    rapply id_monoid_morphism.
Defined.

(** Additive functors compose. *)
Definition compose_additive_functors {A B C : AdditiveCategory}
  (G : AdditiveFunctor B C) (F : AdditiveFunctor A B)
  : AdditiveFunctor A C.
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
AdditiveFunctor A C
Proof.
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
AdditiveFunctor A C
  snapply Build_AdditiveFunctor.
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
Functor A C
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
forall X Y : A, IsMonoidPreserving (morphism_of ?addfunctor (d:=Y))
  -
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
Functor A C exact (G o F)%functor.
  -
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
forall X Y : A, IsMonoidPreserving (morphism_of (G o F) (d:=Y)) intros X Y.
A, B, C: AdditiveCategory
G: AdditiveFunctor B C
F: AdditiveFunctor A B
X, Y: A
IsMonoidPreserving (morphism_of (G o F) (d:=Y))
    rapply compose_monoid_morphism.
Defined.