From 0d6edfae691ae600daf974ddbd294fc8e4ca2ebd Mon Sep 17 00:00:00 2001 From: CharlesCNorton Date: Wed, 10 Jun 2026 09:18:31 -0400 Subject: [PATCH 1/3] Rework additive categories as semi-additive plus inverses --- theories/Categories/Additive/Additive.v | 161 ++++++++++++++++++++++++ 1 file changed, 161 insertions(+) create mode 100644 theories/Categories/Additive/Additive.v diff --git a/theories/Categories/Additive/Additive.v b/theories/Categories/Additive/Additive.v new file mode 100644 index 00000000000..85612669119 --- /dev/null +++ b/theories/Categories/Additive/Additive.v @@ -0,0 +1,161 @@ +(** * 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.Classes.theory Require Import groups. +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 Biproducts 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 inverse law on the other side follows by commutativity. *) + Definition additive_inverse_r (f : morphism A X Y) + : f + (- f) = 0 + := morphism_addition_commutative f (- f) @ additive_inverse_l f. + + #[export] Instance isabgroup_morphisms : IsAbGroup (morphism A X Y). + Proof. + split. + - split. + + exact _. + + exact additive_inverse_l. + + exact additive_inverse_r. + - exact _. + Defined. + + (** The bundled abelian group of morphisms from [X] to [Y]. *) + Definition abgroup_hom : AbGroup + := Build_AbGroup' (morphism A X Y) _ _ _ _. + +End HomAbGroup. + +Arguments abgroup_hom {A} X Y. + +(** ** Negation and composition *) + +(** Additive inverses are unique. *) +Definition inverse_morphism_unique {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). +Proof. + apply inverse_morphism_unique. + lhs_V napply addition_precompose. + refine (ap (fun g => g o a) (additive_inverse_l f) @ _). + 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). +Proof. + apply inverse_morphism_unique. + lhs_V napply addition_postcompose. + refine (ap (fun g => a o g) (additive_inverse_l f) @ _). + 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) := { + add_functor :> Functor A B; + + addfunctor_monoid :: forall (X Y : object A), + IsMonoidPreserving (@morphism_of _ _ add_functor X Y); +}. + +Arguments add_functor {A B} F : rename. +Arguments addfunctor_monoid {A B} F X Y : rename. + +Section AdditiveFunctorLaws. + Context {A B : AdditiveCategory} (F : AdditiveFunctor A B) + {X Y : object A}. + + (** Additive functors preserve addition of morphisms. *) + Definition additive_functor_preserves_addition (f g : morphism A X Y) + : morphism_of F (f + g) = morphism_of F f + morphism_of F g + := preserves_sg_op f g. + + (** Additive functors preserve zero morphisms. *) + Definition additive_functor_preserves_zero_morphisms + : morphism_of F (zero_morphism X Y) = zero_morphism (F X) (F Y) + := preserves_mon_unit. + + (** Additive functors preserve negation. *) + Definition additive_functor_preserves_inverse (f : morphism A X Y) + : morphism_of F (- f) = - morphism_of F f + := preserves_inverse f. + +End AdditiveFunctorLaws. + +(** The identity functor is additive. *) +Definition id_additive_functor (A : AdditiveCategory) + : AdditiveFunctor A A. +Proof. + snapply Build_AdditiveFunctor. + - exact 1%functor. + - intros X Y. + split. + + intros f g. + reflexivity. + + reflexivity. +Defined. + +(** Additive functors compose. *) +Definition compose_additive_functors {A B C : AdditiveCategory} + (G : AdditiveFunctor B C) (F : AdditiveFunctor A B) + : AdditiveFunctor A C. +Proof. + snapply Build_AdditiveFunctor. + - exact (G o F)%functor. + - intros X Y. + split. + + intros f g. + refine (ap (fun h => morphism_of G h) (preserves_sg_op f g) @ _). + exact (preserves_sg_op _ _). + + refine (ap (fun h => morphism_of G h) preserves_mon_unit @ _). + exact preserves_mon_unit. +Defined. From 9ee5547e1ae8fad095cfd964f55e377d012bc304 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 15 Jun 2026 11:19:31 -0400 Subject: [PATCH 2/3] Additive: simplify several proofs --- theories/Categories/Additive/Additive.v | 40 ++++++------------------- 1 file changed, 9 insertions(+), 31 deletions(-) diff --git a/theories/Categories/Additive/Additive.v b/theories/Categories/Additive/Additive.v index 85612669119..30762d6f54a 100644 --- a/theories/Categories/Additive/Additive.v +++ b/theories/Categories/Additive/Additive.v @@ -39,30 +39,16 @@ Coercion additive_semiadditive : AdditiveCategory >-> SemiAdditiveCategory. (** ** Hom-sets are abelian groups *) Section HomAbGroup. - Context {A : AdditiveCategory} {X Y : object A}. - - (** The inverse law on the other side follows by commutativity. *) - Definition additive_inverse_r (f : morphism A X Y) - : f + (- f) = 0 - := morphism_addition_commutative f (- f) @ additive_inverse_l f. - - #[export] Instance isabgroup_morphisms : IsAbGroup (morphism A X Y). - Proof. - split. - - split. - + exact _. - + exact additive_inverse_l. - + exact additive_inverse_r. - - exact _. - Defined. + 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) _ _ _ _. + := Build_AbGroup' (morphism A X Y) _ _ _ additive_inverse_l. -End HomAbGroup. + #[export] Instance isabgroup_morphisms : IsAbGroup (morphism A X Y) + := @isabgroup_abgroup abgroup_hom. -Arguments abgroup_hom {A} X Y. +End HomAbGroup. (** ** Negation and composition *) @@ -79,7 +65,7 @@ Definition inverse_precompose {A : AdditiveCategory} {X Y W : object A} Proof. apply inverse_morphism_unique. lhs_V napply addition_precompose. - refine (ap (fun g => g o a) (additive_inverse_l f) @ _). + lhs napply (ap (fun g => g o a) (additive_inverse_l f)). napply zero_morphism_left. Qed. @@ -90,7 +76,7 @@ Definition inverse_postcompose {A : AdditiveCategory} {X Y W : object A} Proof. apply inverse_morphism_unique. lhs_V napply addition_postcompose. - refine (ap (fun g => a o g) (additive_inverse_l f) @ _). + lhs napply (ap (fun g => a o g) (additive_inverse_l f)). napply zero_morphism_right. Qed. @@ -138,10 +124,7 @@ Proof. snapply Build_AdditiveFunctor. - exact 1%functor. - intros X Y. - split. - + intros f g. - reflexivity. - + reflexivity. + rapply id_monoid_morphism. Defined. (** Additive functors compose. *) @@ -152,10 +135,5 @@ Proof. snapply Build_AdditiveFunctor. - exact (G o F)%functor. - intros X Y. - split. - + intros f g. - refine (ap (fun h => morphism_of G h) (preserves_sg_op f g) @ _). - exact (preserves_sg_op _ _). - + refine (ap (fun h => morphism_of G h) preserves_mon_unit @ _). - exact preserves_mon_unit. + rapply compose_monoid_morphism. Defined. From d80705f9e42cdb1fd09e73bed73b94ae7d935307 Mon Sep 17 00:00:00 2001 From: CharlesCNorton Date: Mon, 15 Jun 2026 14:46:37 -0400 Subject: [PATCH 3/3] Additive: drop unused imports and wrapper lemmas, fix field names - Remove the unused imports Categories.Additive.Biproducts and Classes.theory.groups. Nothing in the file refers to either: the monoid-morphism helpers (IsMonoidPreserving, id_monoid_morphism, compose_monoid_morphism, preserves_sg_op, ...) all come from abstract_algebra, which is already imported, and biproducts are reached transitively through SemiAdditive. - Rename inverse_morphism_unique to hom_moveL_1V, paralleling the group movement lemma grp_moveL_1V, and update its two uses. - Name the AdditiveFunctor fields consistently: the coercion is addfunctor and the monoid-preservation instance is ismonoidpreserving_addfunctor. - Remove the AdditiveFunctorLaws section; its three lemmas were direct applications of preserves_sg_op, preserves_mon_unit and preserves_inverse, which apply to an additive functor's action without a wrapper. --- theories/Categories/Additive/Additive.v | 42 ++++++------------------- 1 file changed, 10 insertions(+), 32 deletions(-) diff --git a/theories/Categories/Additive/Additive.v b/theories/Categories/Additive/Additive.v index 30762d6f54a..398f14027cf 100644 --- a/theories/Categories/Additive/Additive.v +++ b/theories/Categories/Additive/Additive.v @@ -5,10 +5,9 @@ From HoTT Require Import Basics.Overture Basics.Tactics. From HoTT.Classes.interfaces Require Import canonical_names abstract_algebra. -From HoTT.Classes.theory Require Import groups. 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 Biproducts SemiAdditive. +From HoTT.Categories.Additive Require Import ZeroObjects SemiAdditive. From HoTT.Algebra.AbGroups Require Import AbelianGroup. Local Open Scope morphism_scope. @@ -52,8 +51,8 @@ End HomAbGroup. (** ** Negation and composition *) -(** Additive inverses are unique. *) -Definition inverse_morphism_unique {A : AdditiveCategory} {X Y : object A} +(** 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. @@ -63,7 +62,7 @@ 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). Proof. - apply inverse_morphism_unique. + apply hom_moveL_1V. lhs_V napply addition_precompose. lhs napply (ap (fun g => g o a) (additive_inverse_l f)). napply zero_morphism_left. @@ -74,7 +73,7 @@ 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). Proof. - apply inverse_morphism_unique. + apply hom_moveL_1V. lhs_V napply addition_postcompose. lhs napply (ap (fun g => a o g) (additive_inverse_l f)). napply zero_morphism_right. @@ -87,35 +86,14 @@ Qed. Such functors automatically preserve zero morphisms and negation. *) Record AdditiveFunctor (A B : AdditiveCategory) := { - add_functor :> Functor A B; + addfunctor :> Functor A B; - addfunctor_monoid :: forall (X Y : object A), - IsMonoidPreserving (@morphism_of _ _ add_functor X Y); + ismonoidpreserving_addfunctor :: forall (X Y : object A), + IsMonoidPreserving (@morphism_of _ _ addfunctor X Y); }. -Arguments add_functor {A B} F : rename. -Arguments addfunctor_monoid {A B} F X Y : rename. - -Section AdditiveFunctorLaws. - Context {A B : AdditiveCategory} (F : AdditiveFunctor A B) - {X Y : object A}. - - (** Additive functors preserve addition of morphisms. *) - Definition additive_functor_preserves_addition (f g : morphism A X Y) - : morphism_of F (f + g) = morphism_of F f + morphism_of F g - := preserves_sg_op f g. - - (** Additive functors preserve zero morphisms. *) - Definition additive_functor_preserves_zero_morphisms - : morphism_of F (zero_morphism X Y) = zero_morphism (F X) (F Y) - := preserves_mon_unit. - - (** Additive functors preserve negation. *) - Definition additive_functor_preserves_inverse (f : morphism A X Y) - : morphism_of F (- f) = - morphism_of F f - := preserves_inverse f. - -End AdditiveFunctorLaws. +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)