Add semi-additive categories infrastructure #2305
Conversation
Extracting SemiAdditive.v from additive categories work per PR HoTT#2304 review. **Provides:** - `SemiAdditiveCategory`: Class with just cat, zero object, and biproducts - Derives `IsCommutativeMonoid` structure on morphisms using biproducts - Addition defined as: f + g = ∇ ∘ (f ⊕ g) ∘ Δ - Proves identity laws, commutativity, associativity from biproduct axioms - Bilinearity of composition (distributivity) **Note:** The file is almost 1000 lines), especially the associativity proof. This was the only way I could get it to work - would very much appreciate help simplifying and identifying which helper lemmas can be removed. The associativity proof in particular requires many intermediate lemmas about how biproducts interact. It took me an entire week of 16 hour days to get here, but I assume there is a much more elegant method. Addresses review feedback from HoTT#2304. Next step is to update AdditiveCategories.v to build on this, adding only the inverse axiom.
|
Also apologies if there are any nits I missed - I'll give it another lookover soon. |
- Remove periods from section headers - Remove `: Type` annotations from Record/Class definitions - Use periods only for complete sentence descriptions
Convert proofs with single rapply/exact tactics to one-line format for improved readability and consistency with HoTT style.
Dead code removal - this lemma is not referenced in any proofs.
Remove explanatory comments within lemma and theorem proofs to reduce file size while preserving all section headers and documentation.
- Remove unused local definitions YY, YYYL, YYYR - Remove 5 unused lemmas: prod_of_projections_is_id, codiagonal_after_componentwise, componentwise_after_prod, biproduct_prod_compose_left, sum_of_pairs_is_pair_of_sums - Streamline associativity section to minimal required lemmas File is now 20% shorter than before.
|
Refactored. File is about 20% shorter than before at 800 lines instead of 1000. Going through it again... |
-Simplify zero-morphism projection lemmas to one-liners using zero_morphism_left (zero_through_proj_left and zero_through_proj_right). -Simplify component-zero pairing lemmas biproduct_mor_zero_left and biproduct_mor_zero_right by delegating to those one-liners via f_ap.
Restored a few mistakenly reverted "rapply" usage.
Define morphism_addition directly as ∇ ∘ ⟨f,g⟩ (codiagonal after pairing), replacing the earlier diagonal-based construction. This makes morphism_addition_simplify reflexive and shortens the zero-identity proofs by removing extra diagonal rewrites.
|
@jdchristensen In light of yesterday’s disastrous PR attempt, and out of respect for your time, I’d like to hold off on this PR for a few more weeks to ensure it’s truly shipshape. The rest of my contributions to Coq-HoTT will remain focused on the formalization. |
**Removed 4 redundant lemmas from `BiproductBasics` section:** 1. `diagonal_outl` - was just renaming `biproduct_prod_beta_l` 2. `diagonal_outr` - was just renaming `biproduct_prod_beta_r` 3. `inl_codiagonal` - was just renaming `biproduct_coprod_beta_l` 4. `inr_codiagonal` - was just renaming `biproduct_coprod_beta_r` **Updated their usages to call the original lemmas directly:** - In `compose_through_diagonal_left`: replaced `diagonal_outl` with `biproduct_prod_beta_l` - In `compose_through_diagonal_right`: replaced `diagonal_outr` with `biproduct_prod_beta_r` - In `codiagonal_zero_left`: replaced `inl_codiagonal` with `biproduct_coprod_beta_l` - In `codiagonal_zero_right`: replaced `inr_codiagonal` with `biproduct_coprod_beta_r` - In `codiagonal_postcompose_any`: replaced both `inl_codiagonal` and `inr_codiagonal` with their biproduct equivalents **Result:** Removed unnecessary wrapper lemmas and now directly use the existing biproduct infrastructure from `Biproducts.v`, making the file cleaner and avoiding redundancy.
Removed 5 redundant lemmas from BiproductHelpers section: - outr_after_inr, outl_after_inl, outr_after_inl - were just renaming beta/mixed lemmas from IsBiproduct - outl_biproduct_prod, outr_biproduct_prod - were just renaming biproduct_prod_beta_l/r Removed entire ZeroMorphismProperties section: - Deleted 4 unused lemmas that were not referenced elsewhere in the file Removed empty BiproductBasics section Removed morphism_addition_simplify: - This lemma had a trivial reflexivity proof - Replaced all uses with direct unfold morphism_addition Result: Further reduced redundancy by ~15% more lines, making proofs more direct and maintainable.
|
We're now down to about half the length of the original PR. Continuing. |
Removed 3 more unused lemmas: compose_through_diagonal_right, compose_through_diagonal_left - were not referenced anywhere outr_after_inr - was just renaming beta_r Simplified biproduct_swap: Changed from Lemma with existential and proof obligations to direct Definition Updated all references to use the simpler form
Removed 6 single-use helper lemmas by inlining their proofs: proj_inj_matched_l, proj_inj_matched_r, proj_inj_mixed_lr, proj_inj_mixed_rl codiagonal_zero_left, codiagonal_zero_right Removed empty BiproductMorphismProperties section Reorganized sections: Renamed BiproductUniqueness to BiproductCharacterization Merged BiproductHelpers into BiproductCharacterization Added clearer section headers
- Fixed indentation: 2 spaces for section contents - Limited line lengths to ~70 characters where practical - Used #[export] annotation for instances outside sections - Formatted long type signatures across multiple lines with proper indentation - Fixed comment formatting (removed periods from section titles) - Placed Proof and Defined/Qed on separate lines with indented proof scripts - Added line breaks between morphisms for readability in long definitions - Adjusted spacing in biproduct operations for consistency No functional changes - purely formatting to match library conventions.
Removed composition_left_distributive and composition_right_distributive. These were merely renamings of addition_postcompose and addition_precompose with permuted arguments.
- Deleted composition_left_distributive and composition_right_distributive which were just renamings of addition_postcompose and addition_precompose with reordered arguments. Users can use the original lemmas directly. - Deleted is_semigroup_morphisms and is_commutative_semigroup_morphisms instances. These are automatically derivable from IsCommutativeMonoid via typeclass resolution, so explicit instances are unnecessary.
- Add local notation (X ⊕ Y) for biproduct objects to replace verbose biproduct_obj (biproduct_data (semiadditive_biproduct X Y)) - Remove unnecessary simpl tactics from swap_inl and swap_inr proofs - Simplify verbose comments to be more concise and remove excessive unicode symbols
Remove outl_addition_of_pairs and outr_addition_of_pairs by inlining their proofs directly into addition_of_pairs. These helper lemmas were only used once, so inlining them reduces indirection and saves ~20 lines while keeping the proof equally clear.
Replace verbose `biproduct_obj (biproduct_data (semiadditive_biproduct X Y))` expressions with the cleaner `X ⊕ Y` notation that was already defined but applied inconsistently. Changes made in: - biproduct_morphism_unique: simplified type signature - biproduct_swap: simplified type signature and body - codiagonal_pair_inl: use notation in addition_precompose call - codiagonal_pair_inr: use notation in addition_precompose call - codiagonal_factor_through_pair: use notation in signature - addition_of_pairs: simplified type signature - morphism_addition_associative: use notation in addition_postcompose call
|
@CharlesCNorton I haven't looked at this yet and will wait until you ok it. But I'll point out a couple of things that may help. First, there's a trick for showing the a binary operation The second thing that sometimes is helpful is to study the triple product The Baer sum formalization should be particularly relevant, since it uses a lot about biproducts of abelian groups which should generalize to biproducts in any category. |
Thank you very much! |
Define sgop_morphism and monunit_morphism directly as instances rather than creating separate definitions and instance synonyms. Follows library naming pattern of sgop_*/monunit_* instead of *_sgop/*_monunit.
Use semicolon chaining, remove unnecessary set declarations, and consolidate rewrites. Reduces file by ~100 lines.
Apply tactic patterns to remaining proofs, particularly in codiagonal and addition lemmas. Focus on associativity helpers.
Streamlining more proofs for efficiency and line count savings.
- Condense codiagonal_pair_inl and codiagonal_pair_inr proofs by eliminating transitivity and ap011 in favor of direct rewrites - Simplify addition_of_pairs proof by combining branching into single rewrite statement
|
@jdchristensen Ready for review! Was having a tough time implementing the twist, and so kept a more direct proof for associativity. Please let me know what you think. Happy to make any required changes. 👍 |
| From HoTT Require Import Basics.Overture. | ||
| From HoTT.Categories Require Import Category.Core. |
There was a problem hiding this comment.
It's important to keep imports lean. This means that fewer files need to be rebuilt when changes are made, and that the builds parallelize better. (It doesn't need to be strictly the minimum. E.g. if you depend on many files in Types, you can just import Types. Or if you depend on things that depend on Types, there is no harm if depending on Types. But this basic material about Categories is fairly independent of the rest of the library, so it's worth keeping the dependencies small.)
| (biproduct_coprod_mor (semiadditive_biproduct Y Y) Y | ||
| 1%morphism 1%morphism | ||
| o biproduct_prod_mor (semiadditive_biproduct Y Y) X | ||
| f g)%morphism. |
There was a problem hiding this comment.
This is verbose. Can you come up with a better way to express these morphisms, with some arguments implicit and provided via typeclass search? This comes up a lot in the file. (A similar thing appears in the ⊕ Notation.)
|
|
||
| (** ** Biproduct characterization lemmas *) | ||
|
|
||
| Section BiproductCharacterization. |
There was a problem hiding this comment.
It seems to me that the lemmas in the section only require a single Biproduct to exist, rather than a SemiAdditiveCategory structure, so they could be proved in Biproducts.v.
| Proof. | ||
| symmetry; rapply biproduct_prod_unique; rewrite <- Category.Core.associativity; unfold biproduct_swap; | ||
| [rewrite biproduct_prod_beta_l; rapply biproduct_prod_beta_r | rewrite biproduct_prod_beta_r; rapply biproduct_prod_beta_l]. | ||
| Qed. |
There was a problem hiding this comment.
Can you rewrite all proofs so that it's possible to step through them and see what is going on? The semicolons and brackets don't actually save any characters in most cases, so I see no benefit to this style. (There are cases where such tricks are useful, e.g. if the form of the goal changes cleanly when two tactics are used together, making it more clear what is going on.)
There was a problem hiding this comment.
@jdchristensen Understood - I was prioritizing keeping the line count minimal. I'll keep things steppable from now on.
| 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 C X Y f g), <- Category.Core.associativity, codiagonal_swap_invariant; | ||
| reflexivity. | ||
| Qed. |
There was a problem hiding this comment.
Indentation issues here and elsewhere.
|
|
||
| (** ** Swap morphism for biproducts *) | ||
|
|
||
| Section BiproductSwap. |
There was a problem hiding this comment.
Again, some or all of this section probably belongs in Biproducts.v, since these results could be useful for a single biproduct object, even if you don't know you are in a semiadditive category.
| Definition biproduct_swap (A : object C) | ||
| : morphism C (A ⊕ A) (A ⊕ A) |
There was a problem hiding this comment.
Why not [A ⊕ B -> B ⊕ A]? Then you are probably close to proving that biproducts are commutative.
| Lemma biproduct_zero_right_is_inl (Y Z : object C) (h : morphism C Z Y) | ||
| : biproduct_prod_mor (semiadditive_biproduct Y Y) Z h (zero_morphism Z Y) | ||
| = (Biproducts.inl (biproduct_data (semiadditive_biproduct Y Y)) o h)%morphism. |
There was a problem hiding this comment.
This and the next lemma are ok, but I think the proof could be built out of a few more conceptual tools. In Biproducts.v, you could prove that Biproducts.inl = biproduct_prod_mor id zero (not typed precisely), which is a useful general fact. Then the third lemma in this section is a naturality result, which tells you that biproduct_prod_mor id zero o h = biproduct_prod_mor (id o h) (zero o h). Then you just use the properties of id and zero. Seems cleaner, and that result about inl is independently useful.
There was a problem hiding this comment.
Also, I think one of the Ys can be changed to a fresh object Y', giving a slightly more general result.
| Lemma biproduct_comp_general (W X Y Z : object C) | ||
| (f : morphism C W X) (g : morphism C W Y) (h : morphism C Z W) | ||
| : (biproduct_prod_mor (semiadditive_biproduct X Y) W f g o h)%morphism | ||
| = biproduct_prod_mor (semiadditive_biproduct X Y) Z (f o h) (g o h). |
There was a problem hiding this comment.
This is a naturality result, so that should be mentioned in the comment and in the name. (Also, this is a result that is just a fact about products, not biproducts. Really products (and coproducts) should have been studied on their own first, and then biproducts could make use of those results, but I think that's a refactoring for another time.)
| From HoTT Require Import Basics Types. | ||
| From HoTT.Categories Require Import Category Functor NaturalTransformation. | ||
| From HoTT.Categories Require Import InitialTerminalCategory. |
There was a problem hiding this comment.
Tons of dependencies were unnecessary here.
The examples where I've seen it used are for proving equivalences That said, the proof of associativity still looks really long, and conceptually I don't see why it should be long. I wonder if what you are missing is the associativity of the biproduct itself (for which the twist approach would help). #2016 does this for wild categories using the twist approach (but doesn't get to addition of morphisms). Not sure if it would be worth trying this. It would certainly be a lot of work, but the idea is that instead of pushing through proofs, one tries to develop the basic tools that make later proofs easy. And knowing that biproducts are associative is one of the basic facts one would expect to have. Probably not worth it here, so just take this as an aside. (This also suggests the idea of switching to wild categories. We have more about biproducts there, and they are also defined in terms of coproducts and products, so results are stated at the correct level of generality. But #2016 is still a work in progress, with @ThomatoTomato planning to reorganize things a bit.) |
|
@jdchristensen Thanks for the review. Do you think I should switch to WildCat now or stick with the current approach? I suspect I know the answer, but wanted your opinion in case there's some utility in continuing. |
I don't think there's an easy answer. If your current proofs just needed mild touch-ups, I'd lean towards just sticking with Categories, since the code has already been written and it might be quite a burden to rewrite it. But so far it seems that each file needs fairly substantial revisions, which makes me wonder if it wouldn't be that much extra work to switch to WildCat. The advantage of switching is that multiple people will be interested in using some of these results and may be able to contribute to review or even proofs. One disadvantage of switching (besides the fact that you already have code for Categories) is that dealing with the plethora of typeclasses used by WildCat can be a bit confusing. |
2 participants
Extracting SemiAdditive.v from additive categories work per PR #2304 review as part of general formalization for #2288
Provides:
SemiAdditiveCategory: Class with just cat, zero object, and biproductsIsCommutativeMonoidstructure on morphisms using biproductsNote: The file is almost 1000 lines and requires refactoring, especially the associativity proof. @jdchristensen this was the only way I could get it to work - would very much appreciate help simplifying and identifying which helper lemmas can be removed. The associativity proof in particular requires many intermediate lemmas about how biproducts interact. It took me an entire week of 16 hour days to get here, but I assume there is a much more elegant method.