From c88dfc26da7a57a824c206c96651a940da8fc28f Mon Sep 17 00:00:00 2001 From: CharlesCNorton Date: Wed, 10 Jun 2026 17:17:59 -0400 Subject: [PATCH] Add semi-additive categories infrastructure Co-authored-by: Dan Christensen --- theories/Basics/Notations.v | 3 + theories/Categories/Additive/Biproducts.v | 413 ++++++++++++++++++-- theories/Categories/Additive/SemiAdditive.v | 240 ++++++++++++ theories/Categories/Additive/ZeroObjects.v | 17 +- 4 files changed, 623 insertions(+), 50 deletions(-) create mode 100644 theories/Categories/Additive/SemiAdditive.v diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v index a87231489ae..f1ae343bd39 100644 --- a/theories/Basics/Notations.v +++ b/theories/Basics/Notations.v @@ -96,6 +96,9 @@ Reserved Infix "mod" (at level 40, no associativity). Reserved Notation "p ~ 1" (at level 1, left associativity, format "p '~' '1'"). Reserved Notation "p ~ 0" (at level 1, left associativity, format "p '~' '0'"). +(** Categories *) +Reserved Infix "⊕" (at level 40, left associativity). + (** Pointed *) Reserved Infix "@*" (at level 30). Reserved Infix "@@*" (at level 30). diff --git a/theories/Categories/Additive/Biproducts.v b/theories/Categories/Additive/Biproducts.v index 94059d20daf..4ecf8e1f2a9 100644 --- a/theories/Categories/Additive/Biproducts.v +++ b/theories/Categories/Additive/Biproducts.v @@ -4,28 +4,30 @@ to additive category theory. *) -From HoTT Require Import Basics Types. -From HoTT.Categories Require Import Category Functor. +From HoTT Require Import Basics.Overture Basics.Tactics. +From HoTT.Categories Require Import Category.Core. From HoTT.Categories.Additive Require Import ZeroObjects. Local Notation fst_type := Basics.Overture.fst. Local Notation snd_type := Basics.Overture.snd. +Local Open Scope morphism_scope. + (** * Biproduct structures *) (** ** Biproduct data - + The data of a biproduct consists of an object together with injection and projection morphisms. *) Record BiproductData {C : PreCategory} (X Y : object C) := { biproduct_obj : object C; - + (* Coproduct structure: injections *) inl : morphism C X biproduct_obj; inr : morphism C Y biproduct_obj; - + (* Product structure: projections *) outl : morphism C biproduct_obj X; outr : morphism C biproduct_obj Y @@ -40,20 +42,20 @@ Arguments outl {C X Y} b : rename. Arguments outr {C X Y} b : rename. (** ** Biproduct axioms - + The axioms that make biproduct data into an actual biproduct. These ensure the projection-injection pairs behave correctly. *) -Record IsBiproduct {C : PreCategory} `{Z : ZeroObject C} {X Y : object C} +Record IsBiproduct {C : PreCategory} `{Z : ZeroObject C} {X Y : object C} (B : BiproductData X Y) := { (* Projection-injection identities *) - beta_l : (outl B o inl B = 1)%morphism; - beta_r : (outr B o inr B = 1)%morphism; - + beta_l : outl B o inl B = 1; + beta_r : outr B o inr B = 1; + (* Mixed terms are zero *) - mixed_l : (outl B o inr B)%morphism = zero_morphism Y X; - mixed_r : (outr B o inl B)%morphism = zero_morphism X Y + mixed_l : outl B o inr B = zero_morphism Y X; + mixed_r : outr B o inl B = zero_morphism X Y }. Arguments beta_l {C Z X Y B} i : rename. @@ -62,7 +64,7 @@ Arguments mixed_l {C Z X Y B} i : rename. Arguments mixed_r {C Z X Y B} i : rename. (** ** Universal property of biproducts - + The universal property states that morphisms into/out of the biproduct are uniquely determined by their components. *) @@ -70,28 +72,29 @@ Arguments mixed_r {C Z X Y B} i : rename. Record HasBiproductUniversal {C : PreCategory} {X Y : object C} (B : BiproductData X Y) := { (* Universal property as a coproduct *) - coprod_universal : forall (W : object C) + coprod_universal : forall (W : object C) (f : morphism C X W) (g : morphism C Y W), - Contr {h : morphism C B W & - ((h o inl B = f)%morphism * (h o inr B = g)%morphism)}; - + Contr {h : morphism C B W & + ((h o inl B = f) * (h o inr B = g))}; + (* Universal property as a product *) - prod_universal : forall (W : object C) + prod_universal : forall (W : object C) (f : morphism C W X) (g : morphism C W Y), - Contr {h : morphism C W B & - ((outl B o h = f)%morphism * (outr B o h = g)%morphism)} + Contr {h : morphism C W B & + ((outl B o h = f) * (outr B o h = g))} }. Arguments coprod_universal {C X Y B} u W f g : rename. Arguments prod_universal {C X Y B} u W f g : rename. (** ** Complete biproduct structure - + A biproduct is biproduct data together with the proof that it satisfies - the biproduct axioms and universal property. + the biproduct axioms and universal property. The zero object is an + explicit argument so that instances can be written [Biproduct Z X Y]. *) -Class Biproduct {C : PreCategory} `{Z : ZeroObject C} (X Y : object C) := { +Class Biproduct {C : PreCategory} (Z : ZeroObject C) (X Y : object C) := { biproduct_data : BiproductData X Y; biproduct_is : IsBiproduct biproduct_data; biproduct_universal : HasBiproductUniversal biproduct_data @@ -106,80 +109,406 @@ Arguments biproduct_universal {C Z X Y} b : rename. (** * Biproduct operations *) Section BiproductOperations. - Context {C : PreCategory} `{Z : ZeroObject C} {X Y : object C}. - Variable (B : Biproduct X Y). + Context {C : PreCategory} {Z : ZeroObject C} {X Y : object C}. + Variable (B : Biproduct Z X Y). (** ** Uniqueness from universal property *) (** The coproduct universal morphism and its properties. *) - Definition biproduct_coprod_universal (W : object C) + Definition biproduct_coprod_universal (W : object C) (f : morphism C X W) (g : morphism C Y W) - : {h : morphism C B W & ((h o inl B = f)%morphism * (h o inr B = g)%morphism)} + : {h : morphism C B W & ((h o inl B = f) * (h o inr B = g))} := @center _ (coprod_universal (biproduct_universal B) W f g). (** Extract the unique morphism from the coproduct universal property. *) - Definition biproduct_coprod_mor (W : object C) + Definition biproduct_coprod_mor (W : object C) (f : morphism C X W) (g : morphism C Y W) : morphism C B W := (biproduct_coprod_universal W f g).1. Definition biproduct_coprod_beta_l (W : object C) (f : morphism C X W) (g : morphism C Y W) - : (biproduct_coprod_mor W f g o inl B = f)%morphism + : biproduct_coprod_mor W f g o inl B = f := fst_type (biproduct_coprod_universal W f g).2. Definition biproduct_coprod_beta_r (W : object C) (f : morphism C X W) (g : morphism C Y W) - : (biproduct_coprod_mor W f g o inr B = g)%morphism + : biproduct_coprod_mor W f g o inr B = g := snd_type (biproduct_coprod_universal W f g).2. Definition biproduct_coprod_unique (W : object C) (f : morphism C X W) (g : morphism C Y W) (h : morphism C B W) - (Hl : (h o inl B = f)%morphism) - (Hr : (h o inr B = g)%morphism) + (Hl : h o inl B = f) + (Hr : h o inr B = g) : h = biproduct_coprod_mor W f g := ap pr1 (contr (h; (Hl, Hr)))^. (** The product universal morphism and its properties. *) - Definition biproduct_prod_universal (W : object C) + Definition biproduct_prod_universal (W : object C) (f : morphism C W X) (g : morphism C W Y) - : {h : morphism C W B & ((outl B o h = f)%morphism * (outr B o h = g)%morphism)} + : {h : morphism C W B & ((outl B o h = f) * (outr B o h = g))} := @center _ (prod_universal (biproduct_universal B) W f g). (** Extract the unique morphism from the product universal property. *) - Definition biproduct_prod_mor (W : object C) + Definition biproduct_prod_mor (W : object C) (f : morphism C W X) (g : morphism C W Y) : morphism C W B := (biproduct_prod_universal W f g).1. Definition biproduct_prod_beta_l (W : object C) (f : morphism C W X) (g : morphism C W Y) - : (outl B o biproduct_prod_mor W f g = f)%morphism + : outl B o biproduct_prod_mor W f g = f := fst_type (biproduct_prod_universal W f g).2. Definition biproduct_prod_beta_r (W : object C) (f : morphism C W X) (g : morphism C W Y) - : (outr B o biproduct_prod_mor W f g = g)%morphism + : outr B o biproduct_prod_mor W f g = g := snd_type (biproduct_prod_universal W f g).2. - + Definition biproduct_prod_unique (W : object C) (f : morphism C W X) (g : morphism C W Y) (h : morphism C W B) - (Hl : (outl B o h = f)%morphism) - (Hr : (outr B o h = g)%morphism) + (Hl : outl B o h = f) + (Hr : outr B o h = g) : h = biproduct_prod_mor W f g := ap pr1 (contr (h; (Hl, Hr)))^. + (** Pairing with zero on the right is the left injection composed. *) + Lemma biproduct_prod_zero_r (W : object C) (h : morphism C W X) + : biproduct_prod_mor W h (zero_morphism W Y) + = inl B o h. + Proof. + symmetry. + rapply biproduct_prod_unique. + - rewrite <- associativity. + rewrite (beta_l (biproduct_is B)). + apply left_identity. + - rewrite <- associativity. + rewrite (mixed_r (biproduct_is B)). + apply zero_morphism_left. + Qed. + + (** Pairing with zero on the left is the right injection composed. *) + Lemma biproduct_prod_zero_l (W : object C) (h : morphism C W Y) + : biproduct_prod_mor W (zero_morphism W X) h + = inr B o h. + Proof. + symmetry. + rapply biproduct_prod_unique. + - rewrite <- associativity. + rewrite (mixed_l (biproduct_is B)). + apply zero_morphism_left. + - rewrite <- associativity. + rewrite (beta_r (biproduct_is B)). + apply left_identity. + Qed. + + (** Pairing is natural in the domain. *) + Lemma biproduct_prod_mor_nat (V W : object C) + (f : morphism C W X) (g : morphism C W Y) (h : morphism C V W) + : biproduct_prod_mor W f g o h + = biproduct_prod_mor V (f o h) (g o h). + Proof. + rapply biproduct_prod_unique. + - rewrite <- associativity. + rewrite biproduct_prod_beta_l. + reflexivity. + - rewrite <- associativity. + rewrite biproduct_prod_beta_r. + reflexivity. + Qed. + + (** Copairing is natural in the codomain. *) + Lemma biproduct_coprod_mor_nat (W V : object C) + (f : morphism C X W) (g : morphism C Y W) (h : morphism C W V) + : h o biproduct_coprod_mor W f g + = biproduct_coprod_mor V (h o f) (h o g). + Proof. + rapply biproduct_coprod_unique. + - rewrite associativity. + rewrite biproduct_coprod_beta_l. + reflexivity. + - rewrite associativity. + rewrite biproduct_coprod_beta_r. + reflexivity. + Qed. + End BiproductOperations. +Arguments biproduct_prod_mor {C Z X Y} B {W} f g. + +(** * Functoriality of biproducts *) + +Section BiproductFunctoriality. + Context {C : PreCategory} {Z : ZeroObject C} {X Y X' Y' : object C} + {BXY : Biproduct Z X Y} {BX'Y' : Biproduct Z X' Y'}. + + (** The morphism between biproducts induced by morphisms of the summands. *) + Definition biproduct_sum_map + (a : morphism C X X') (b : morphism C Y Y') + : morphism C BXY BX'Y' + := biproduct_prod_mor BX'Y' (a o outl BXY) (b o outr BXY). + + (** The biproduct map composed with the left injection is the left + summand map. *) + Lemma biproduct_sum_map_inl + (a : morphism C X X') (b : morphism C Y Y') + : biproduct_sum_map a b o inl BXY + = inl BX'Y' o a. + Proof. + rhs_V apply (biproduct_prod_zero_r BX'Y'). + rapply (biproduct_prod_unique BX'Y'). + - rewrite <- associativity. + unfold biproduct_sum_map. + rewrite (biproduct_prod_beta_l BX'Y'). + rewrite associativity. + rewrite (beta_l (biproduct_is BXY)). + apply right_identity. + - rewrite <- associativity. + unfold biproduct_sum_map. + rewrite (biproduct_prod_beta_r BX'Y'). + rewrite associativity. + rewrite (mixed_r (biproduct_is BXY)). + apply zero_morphism_right. + Qed. + + (** The biproduct map composed with the right injection is the right + summand map. *) + Lemma biproduct_sum_map_inr + (a : morphism C X X') (b : morphism C Y Y') + : biproduct_sum_map a b o inr BXY + = inr BX'Y' o b. + Proof. + rhs_V apply (biproduct_prod_zero_l BX'Y'). + rapply (biproduct_prod_unique BX'Y'). + - rewrite <- associativity. + unfold biproduct_sum_map. + rewrite (biproduct_prod_beta_l BX'Y'). + rewrite associativity. + rewrite (mixed_l (biproduct_is BXY)). + apply zero_morphism_right. + - rewrite <- associativity. + unfold biproduct_sum_map. + rewrite (biproduct_prod_beta_r BX'Y'). + rewrite associativity. + rewrite (beta_r (biproduct_is BXY)). + apply right_identity. + Qed. + + (** Biproduct maps commute with pairing. *) + Lemma biproduct_sum_map_prod {W : object C} + (a : morphism C X X') (b : morphism C Y Y') + (f : morphism C W X) (g : morphism C W Y) + : biproduct_prod_mor BX'Y' (a o f) (b o g) + = biproduct_sum_map a b o biproduct_prod_mor BXY f g. + Proof. + symmetry. + rapply (biproduct_prod_unique BX'Y'). + - rewrite <- associativity. + unfold biproduct_sum_map. + rewrite (biproduct_prod_beta_l BX'Y'). + rewrite associativity. + rewrite (biproduct_prod_beta_l BXY). + reflexivity. + - rewrite <- associativity. + unfold biproduct_sum_map. + rewrite (biproduct_prod_beta_r BX'Y'). + rewrite associativity. + rewrite (biproduct_prod_beta_r BXY). + reflexivity. + Qed. + + (** Copairing is natural in the domain with respect to biproduct maps. *) + Lemma biproduct_coprod_sum_map_nat {W : object C} + (f : morphism C X' W) (g : morphism C Y' W) + (a : morphism C X X') (b : morphism C Y Y') + : biproduct_coprod_mor BX'Y' W f g o biproduct_sum_map a b + = biproduct_coprod_mor BXY W (f o a) (g o b). + Proof. + rapply (biproduct_coprod_unique BXY). + - rewrite associativity. + rewrite biproduct_sum_map_inl. + rewrite <- associativity. + rewrite biproduct_coprod_beta_l. + reflexivity. + - rewrite associativity. + rewrite biproduct_sum_map_inr. + rewrite <- associativity. + rewrite biproduct_coprod_beta_r. + reflexivity. + Qed. + +End BiproductFunctoriality. + +(** * Symmetry of biproducts *) + +Section BiproductSymmetry. + Context {C : PreCategory} {Z : ZeroObject C} {X Y : object C} + {BXY : Biproduct Z X Y} {BYX : Biproduct Z Y X}. + + (** The swap morphism exchanges the two summands of a biproduct. *) + Definition biproduct_swap + : morphism C BXY BYX + := biproduct_prod_mor BYX (outr BXY) (outl BXY). + + (** Swapping the components of a pairing. *) + Lemma biproduct_prod_swap {W : object C} + (f : morphism C W X) (g : morphism C W Y) + : biproduct_prod_mor BYX g f + = biproduct_swap o biproduct_prod_mor BXY f g. + Proof. + symmetry. + rapply (biproduct_prod_unique BYX). + - rewrite <- associativity. + unfold biproduct_swap. + rewrite (biproduct_prod_beta_l BYX). + apply (biproduct_prod_beta_r BXY). + - rewrite <- associativity. + unfold biproduct_swap. + rewrite (biproduct_prod_beta_r BYX). + apply (biproduct_prod_beta_l BXY). + Qed. + + (** Swapping after the left injection gives the right injection. *) + Lemma biproduct_swap_inl + : biproduct_swap o inl BXY = inr BYX. + Proof. + unfold biproduct_swap. + rewrite (biproduct_prod_mor_nat BYX). + rewrite (mixed_r (biproduct_is BXY)). + rewrite (beta_l (biproduct_is BXY)). + rewrite (biproduct_prod_zero_l BYX). + apply right_identity. + Qed. + + (** Swapping after the right injection gives the left injection. *) + Lemma biproduct_swap_inr + : biproduct_swap o inr BXY = inl BYX. + Proof. + unfold biproduct_swap. + rewrite (biproduct_prod_mor_nat BYX). + rewrite (beta_r (biproduct_is BXY)). + rewrite (mixed_l (biproduct_is BXY)). + rewrite (biproduct_prod_zero_r BYX). + apply right_identity. + Qed. + +End BiproductSymmetry. + +(** Swapping twice is the identity, so [BXY] and [BYX] are isomorphic: + the biproduct is commutative. *) +Lemma biproduct_swap_swap {C : PreCategory} {Z : ZeroObject C} + {X Y : object C} {BXY : Biproduct Z X Y} {BYX : Biproduct Z Y X} + : biproduct_swap (BXY:=BYX) (BYX:=BXY) o biproduct_swap = 1. +Proof. + transitivity (biproduct_prod_mor BXY (outl BXY) (outr BXY)). + - rapply (biproduct_prod_unique BXY). + + rewrite <- associativity. + unfold biproduct_swap at 1. + rewrite (biproduct_prod_beta_l BXY). + apply (biproduct_prod_beta_r BYX). + + rewrite <- associativity. + unfold biproduct_swap at 1. + rewrite (biproduct_prod_beta_r BXY). + apply (biproduct_prod_beta_l BYX). + - symmetry. + rapply (biproduct_prod_unique BXY). + + apply right_identity. + + apply right_identity. +Qed. + +(** * Self-biproducts *) + +Section SelfBiproducts. + Context {C : PreCategory} {Z : ZeroObject C}. + + (** The codiagonal of a self-biproduct. *) + Definition biproduct_codiagonal (Y : object C) + {BYY : Biproduct Z Y Y} + : morphism C BYY Y + := biproduct_coprod_mor BYY Y 1 1. + + (** The codiagonal is natural in the codomain. *) + Lemma biproduct_codiagonal_nat {Y Y' : object C} + {BYY : Biproduct Z Y Y} + (a : morphism C Y Y') + : a o biproduct_codiagonal Y + = biproduct_coprod_mor BYY Y' a a. + Proof. + unfold biproduct_codiagonal. + rewrite biproduct_coprod_mor_nat. + repeat rewrite right_identity. + reflexivity. + Qed. + + (** The codiagonal of a biproduct map is the corresponding copairing. *) + Lemma biproduct_codiagonal_factor_through_sum_map {Y Y' : object C} + {BYY : Biproduct Z Y Y} {BYY' : Biproduct Z Y' Y'} + (a b : morphism C Y Y') + : biproduct_codiagonal Y' o biproduct_sum_map a b + = biproduct_coprod_mor BYY Y' a b. + Proof. + unfold biproduct_codiagonal. + rewrite biproduct_coprod_sum_map_nat. + rewrite !left_identity. + reflexivity. + Qed. + + (** The codiagonal of a pairing with zero on the right recovers the + left map. *) + Lemma biproduct_codiagonal_prod_zero_r {X Y : object C} + {BYY : Biproduct Z Y Y} + (f : morphism C X Y) + : biproduct_codiagonal Y + o biproduct_prod_mor BYY f (zero_morphism X Y) = f. + Proof. + unfold biproduct_codiagonal. + rewrite biproduct_prod_zero_r. + rewrite <- associativity. + rewrite biproduct_coprod_beta_l. + apply left_identity. + Qed. + + (** The codiagonal of a pairing with zero on the left recovers the + right map. *) + Lemma biproduct_codiagonal_prod_zero_l {X Y : object C} + {BYY : Biproduct Z Y Y} + (f : morphism C X Y) + : biproduct_codiagonal Y + o biproduct_prod_mor BYY (zero_morphism X Y) f = f. + Proof. + unfold biproduct_codiagonal. + rewrite biproduct_prod_zero_l. + rewrite <- associativity. + rewrite biproduct_coprod_beta_r. + apply left_identity. + Qed. + + (** The codiagonal is invariant under swapping the two summands. *) + Lemma biproduct_codiagonal_swap_invariant {Y : object C} + {BYY : Biproduct Z Y Y} + : biproduct_codiagonal Y o biproduct_swap + = biproduct_codiagonal Y. + Proof. + rapply (biproduct_coprod_unique BYY Y 1 1). + - rewrite associativity. + rewrite biproduct_swap_inl. + apply biproduct_coprod_beta_r. + - rewrite associativity. + rewrite biproduct_swap_inr. + apply biproduct_coprod_beta_l. + Qed. + +End SelfBiproducts. + (** * Export hints *) -Hint Resolve +Hint Resolve biproduct_coprod_beta_l biproduct_coprod_beta_r biproduct_prod_beta_l biproduct_prod_beta_r : biproduct. -Hint Rewrite +Hint Rewrite @zero_morphism_left @zero_morphism_right : biproduct_simplify. diff --git a/theories/Categories/Additive/SemiAdditive.v b/theories/Categories/Additive/SemiAdditive.v new file mode 100644 index 00000000000..946bfba8b36 --- /dev/null +++ b/theories/Categories/Additive/SemiAdditive.v @@ -0,0 +1,240 @@ +(** * Semi-additive categories + + Categories with zero objects and biproducts, which automatically + have commutative monoid structures on hom-sets. *) + +From HoTT Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics. +From HoTT.Classes.interfaces Require Import abstract_algebra. +From HoTT.Categories Require Import Category.Core. +From HoTT.Categories.Additive Require Import ZeroObjects Biproducts. + +Local Open Scope morphism_scope. + +(** This lets us use "+" for the [SgOp] instance and "0" for the [MonUnit] + instance defined below. *) +Local Open Scope mc_add_scope. + +(** ** Definition of semi-additive category *) + +Class SemiAdditiveCategory := { + cat : PreCategory; + semiadditive_zero :: ZeroObject cat; + semiadditive_biproduct :: forall (X Y : object cat), + Biproduct semiadditive_zero X Y +}. + +Coercion cat : SemiAdditiveCategory >-> PreCategory. + +(** Notation for biproduct objects *) +Local Notation "X ⊕ Y" := (semiadditive_biproduct X Y). + +(** ** Morphism addition via biproducts + + Addition is the codiagonal composed with the pairing morphism. *) + +Section MorphismAddition. + Context {C : SemiAdditiveCategory} {X Y : object C}. + + (** Codiagonal composed with pairing. *) + #[export] Instance sgop_morphism : SgOp (morphism C X Y) + := fun f g => + biproduct_codiagonal Y o biproduct_prod_mor (Y ⊕ Y) f g. + + (** The zero morphism is the unit for addition. *) + #[export] Instance monunit_morphism : MonUnit (morphism C X Y) + := zero_morphism X Y. + +End MorphismAddition. + +(** ** Identity laws for morphism addition *) + +Section IdentityLaws. + Context {C : SemiAdditiveCategory}. + + (** Zero is a left identity for morphism addition. *) + Definition zero_left_identity {X Y : object C} (f : morphism C X Y) + : 0 + f = f + := biproduct_codiagonal_prod_zero_l f. + + (** Zero is a right identity for morphism addition. *) + Definition zero_right_identity {X Y : object C} (f : morphism C X Y) + : f + 0 = f + := biproduct_codiagonal_prod_zero_r f. + +End IdentityLaws. + +(** ** Commutativity of morphism addition *) + +Theorem morphism_addition_commutative {C : SemiAdditiveCategory} + {X Y : object C} + : Commutative (@sgop_morphism C X Y). +Proof. + intros f g. + unfold sgop_morphism. + rewrite (biproduct_prod_swap f g). + rewrite <- associativity. + rewrite biproduct_codiagonal_swap_invariant. + reflexivity. +Qed. + +(** ** Associativity of morphism addition *) + +Section Associativity. + Context {C : SemiAdditiveCategory}. + + (** Addition is natural in the domain. *) + Lemma addition_precompose {X Y W : object C} + (f g : morphism C X Y) (a : morphism C W X) + : (f + g) o a = (f o a) + (g o a). + Proof. + unfold sg_op, sgop_morphism. + rewrite associativity. + apply ap, biproduct_prod_mor_nat. + Qed. + + (** Addition is natural in the codomain. *) + Lemma addition_postcompose {X Y Y' : object C} + (f g : morphism C X Y) (a : morphism C Y Y') + : a o (f + g) = (a o f) + (a o g). + Proof. + unfold sg_op, sgop_morphism. + rewrite <- associativity. + rewrite (biproduct_codiagonal_nat a). + rewrite <- (biproduct_codiagonal_factor_through_sum_map a a). + rewrite associativity. + rewrite <- (biproduct_sum_map_prod a a f g). + reflexivity. + Qed. + + (** Sum of pairings is the pairing of the sums. *) + Lemma addition_of_pairs {X Y Y' : object C} + (f1 f2 : morphism C X Y) (g1 g2 : morphism C X Y') + : biproduct_prod_mor (Y ⊕ Y') f1 g1 + biproduct_prod_mor (Y ⊕ Y') f2 g2 + = biproduct_prod_mor (Y ⊕ Y') (f1 + f2) (g1 + g2). + Proof. + rapply biproduct_prod_unique. + - rewrite addition_postcompose. + rewrite 2 biproduct_prod_beta_l. + reflexivity. + - rewrite addition_postcompose. + rewrite 2 biproduct_prod_beta_r. + reflexivity. + Qed. + + (** Associativity follows by functoriality of pairing and codiagonal. *) + Theorem morphism_addition_associative {X Y : object C} + (f g h : morphism C X Y) + : f + (g + h) = (f + g) + h. + Proof. + lhs_V exact (ap (fun w => w + (g + h)) (zero_right_identity f)). + lhs_V exact (ap (fun p => biproduct_codiagonal Y o p) + (addition_of_pairs f 0 g h)). + lhs napply addition_postcompose. + exact (ap (fun w => (f + g) + w) (zero_left_identity h)). + Qed. + +End Associativity. + +(** ** Main theorem: morphism sets form commutative monoids *) + +#[export] Instance is_commutative_monoid_morphisms + (C : SemiAdditiveCategory) (X Y : object C) + : IsCommutativeMonoid (morphism C X Y). +Proof. + repeat split. + - exact _. + - exact morphism_addition_associative. + - exact zero_left_identity. + - exact zero_right_identity. + - exact morphism_addition_commutative. +Defined. + +(** ** Uniqueness of the enrichment + + The canonical addition is the unique family of operations on hom-sets + with units that distributes over composition. Commutativity and + associativity of [op] are not assumed; they follow from uniqueness. *) + +Section EnrichmentUniqueness. + Context {C : SemiAdditiveCategory} + (op : forall (X Y : object C), morphism C X Y -> morphism C X Y -> morphism C X Y) + (op_zero : forall (X Y : object C), morphism C X Y) + (op_zero_l : forall (X Y : object C) (f : morphism C X Y), + op X Y (op_zero X Y) f = f) + (op_zero_r : forall (X Y : object C) (f : morphism C X Y), + op X Y f (op_zero X Y) = f) + (op_postcompose : forall (X Y Z : object C) + (h : morphism C Y Z) (f g : morphism C X Y), + h o op X Y f g = op X Z (h o f) (h o g)) + (op_precompose : forall (X Y Z : object C) + (f g : morphism C Y Z) (h : morphism C X Y), + op Y Z f g o h = op X Z (f o h) (g o h)) + (op_zero_postcompose : forall (X Y Z : object C) (h : morphism C Y Z), + h o op_zero X Y = op_zero X Z). + + (** The unit of any such operation is the zero morphism. *) + Lemma op_zero_unique (X Y : object C) + : op_zero X Y = zero_morphism X Y. + Proof. + lhs_V apply (op_zero_postcompose X semiadditive_zero Y + (zero_morphism semiadditive_zero Y)). + apply morphism_through_zero_is_zero. + Qed. + + (** Any such operation decomposes the identity of a self-biproduct. *) + Lemma op_decompose_id (X : object C) + : op (X ⊕ X) (X ⊕ X) + (inl (X ⊕ X) o outl (X ⊕ X)) + (inr (X ⊕ X) o outr (X ⊕ X)) + = 1. + Proof. + set (B := X ⊕ X). + transitivity (biproduct_prod_mor B (outl B) (outr B)). + - apply (biproduct_prod_unique B). + + rewrite op_postcompose. + rewrite <- !associativity. + rewrite (beta_l (biproduct_is B)). + rewrite (mixed_l (biproduct_is B)). + rewrite left_identity. + rewrite zero_morphism_left. + rewrite <- op_zero_unique. + apply op_zero_r. + + rewrite op_postcompose. + rewrite <- !associativity. + rewrite (mixed_r (biproduct_is B)). + rewrite (beta_r (biproduct_is B)). + rewrite left_identity. + rewrite zero_morphism_left. + rewrite <- op_zero_unique. + apply op_zero_l. + - symmetry. + apply (biproduct_prod_unique B). + all: apply right_identity. + Qed. + + (** The canonical addition is the unique such operation. *) + Theorem morphism_addition_unique {X Y : object C} (f g : morphism C X Y) + : op X Y f g = f + g. + Proof. + symmetry. + unfold sg_op, sgop_morphism, biproduct_codiagonal. + rewrite <- (left_identity C _ _ + (biproduct_prod_mor (Y ⊕ Y) f g)). + rewrite <- (op_decompose_id Y). + rewrite <- associativity. + rewrite op_postcompose. + rewrite op_precompose. + apply ap011. + - rewrite !associativity. + rewrite biproduct_prod_beta_l. + rewrite <- associativity. + rewrite biproduct_coprod_beta_l. + apply left_identity. + - rewrite !associativity. + rewrite biproduct_prod_beta_r. + rewrite <- associativity. + rewrite biproduct_coprod_beta_r. + apply left_identity. + Qed. + +End EnrichmentUniqueness. diff --git a/theories/Categories/Additive/ZeroObjects.v b/theories/Categories/Additive/ZeroObjects.v index a7bc3f571cf..aa884d9623c 100644 --- a/theories/Categories/Additive/ZeroObjects.v +++ b/theories/Categories/Additive/ZeroObjects.v @@ -4,9 +4,10 @@ concepts for additive and stable category theory. *) -From HoTT Require Import Basics Types. -From HoTT.Categories Require Import Category Functor NaturalTransformation. -From HoTT.Categories Require Import InitialTerminalCategory. +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 @@ -53,7 +54,7 @@ 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)%morphism = zero_morphism X Y. + : g o f = zero_morphism X Y. Proof. unfold zero_morphism. apply ap011. @@ -67,9 +68,9 @@ Qed. 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)%morphism = zero_morphism X W. + : g o zero_morphism X Y = zero_morphism X W. Proof. - rewrite <- Category.Core.associativity. + rewrite <- associativity. apply morphism_through_zero_is_zero. Qed. @@ -77,9 +78,9 @@ Qed. 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)%morphism = zero_morphism X W. + : zero_morphism Y W o f = zero_morphism X W. Proof. - rewrite Category.Core.associativity. + rewrite associativity. apply morphism_through_zero_is_zero. Qed.