Add zero objects infrastructure for stable categories #2293
Conversation
Per @jdchristensen's suggestion in HoTT#2288, this PR extracts just ZeroObjects.v for focused review and merging. This provides the foundational infrastructure for zero objects and zero morphisms needed for stable category theory. Changes from original PR based on review feedback: - Uses `IsInitialObject`/`IsTerminalObject` with `::` for instances - Uses new `map_from_initial`/`map_to_terminal` helpers from recently merged PR HoTT#2291 - Follows HoTT style conventions (`rapply`, single-line tactics with `1:`, etc.) - Removed lemmas that now belong in Objects.v - Fixed all import and style issues Some lemmas are retained for backwards compatibility.
|
It looks like you didn't test this before creating the PR? It wouldn't build with any version of Coq the CI uses. I fixed that in the first new commit. In the second commit, I made many of the changes that I had suggested in #2288. I thought you would have addressed those before creating this PR? |
|
We also need to discuss the location of the file before considering merging this. There's a good argument for having it beside Category/Objects.v, since it is very closely related. In fact, if the four results are removed it becomes short enough that it could just be added to that file. A third option is to put it in a folder Additive, for things about Additive categories. (I think it's likely we're going to want a folder like that for some of the other files.) |
I'm really sorry about this! There was a mixup on my end - I've only been working with GitHub for about two years and clearly made an error with which version got pushed. I sincerely apologize for the extra work this created for you, especially after you'd already taken the time to provide detailed feedback. Thank you for fixing the build issues and implementing those simplifications. |
Sounds good👍Happy to go with whichever location you think works best for the structure. We have Biproducts.v, AdditiveCategories.v coming up, and so Additive makes the most sense imo, but Objects.v fine too. Thank you again. |
|
Let's start the Additive folder and put it there. Thanks for explaining about the git mix-up; it's easy for things like that to happen. |
Following reviewer feedback, remove four unnecessary lemmas: - zero_to_zero_is_id - terminal_zero_to_zero_is_id - terminal_comp_is_zero - zero_morphism_from_zero These special cases can be replaced by the more general lemmas (initial_morphism_unique, terminal_morphism_unique, etc.) at their usage sites.
Following reviewer suggestion to organize non-stable-specific files separately in new Additive folder. ZeroObjects are foundational for additive categories and not specific to stable categories.
jdchristensen
left a comment
jdchristensen
left a comment
There was a problem hiding this comment.
(Sorry to keep adding new suggestions, but I think it'll be beneficial to get this as slick as possible, to streamline future uses of it.)
|
Let me know if there's anything that still needs to be handled. I'll probably merge tomorrow. |
LGTM! Thank you! |
|
I made a couple of minor changes, and will merge when the CI is done. @CharlesCNorton , feel free to create the next PR, taking into account the things we learned while polishing this one. |
Extract transport lemmas from stable categories formalization (PR HoTT#2288). Changes from original formalization: - Rename file from ZeroMorphismLemmas.v to TransportMorphisms.v to better reflect content - Remove ~150 lines of unused/redundant lemmas, keeping only the 4 transport lemmas actually used - Remove zero-specific sections that weren't actually zero-specific - Place in Categories/Additive/ folder alongside ZeroObjects.v The retained lemmas are: - transport_compose_morphism - transport_compose_both_inverse - transport_inverse_eq - morphism_eq_transport_inverse These lemmas handle how morphisms behave under transport along equality proofs and are essential for proving preservation properties of functors in AdditiveCategories.v and beyond. I verified these are the only lemmas from the original file actually used in the formalization. The file has been tested to compile successfully using: ``` make -f Makefile.coq theories/Categories/Additive/TransportMorphisms.vo ``` Follows lessons learned and style conventions established in PR HoTT#2293 review. @jdchristensen Please let me know if you see any issues or have suggestions for improvement. Sincere apologies if I've overlooked anything from your previous feedback.
Following patterns from ZeroObject, make Biproduct a Class to enable automatic inference. Add coercion from BiproductData to object which allows writing just (biproduct_data B) instead of the verbose (biproduct_obj (biproduct_data B)) throughout. Changes: - Change Record Biproduct to Class Biproduct for typeclass inference - Add Coercion biproduct_obj : BiproductData >-> object - Simplify all morphism type expressions using the new coercion - Style: use 1: instead of braces in biproduct_coprod_unique proof This brings the file in line with the patterns established in PR HoTT#2293.
Extracting AdditiveCategories.v from stable categories formalization (HoTT#2288). **Provides:** - `AdditiveCategory`: Categories with zero objects, biproducts, and abelian group structure on hom-sets - Helper functions for accessing biproduct components - Universal property operations with uniqueness (both product and coproduct) - `AdditiveFunctor`: Preserves zero objects, biproducts, and morphism addition - Main theorem: `additive_functor_preserves_zero_morphisms` - Identity and composition of additive functors **Changes from original:** - Fixed imports (removed non-existent ZeroMorphismLemmas.v) - Changed to `Class` with implicit `ZeroObject` instance - Added complete abelian group structure on hom-sets: - `add_morphism` operation with commutativity, associativity - Zero morphism as identity, existence of inverses - Bilinearity of composition (distributivity) - Removed 8 unused wrapper lemmas (e.g., `add_beta_l`, `add_mixed_r`) - Added `add_prod_unique` for product/coproduct duality - Updated transport lemma names to match Core.v - Applied HoTT style conventions Depends on: HoTT#2293 (ZeroObjects), HoTT#2300 (Biproducts) @jdchristensen The main new addition (no pun intended) is the abelian group structure on hom-sets, which makes this a proper additive category (not just a category with zero objects and biproducts). Also I have probably overlooked a few things. Will be looking over again, but wanted to get the PR submitted.
2 participants
Per @jdchristensen's suggestion in #2288, this PR extracts just ZeroObjects.v for focused review and merging.
This provides the foundational infrastructure for zero objects and zero morphisms needed for stable category theory.
Changes from original PR based on review feedback:
IsInitialObject/IsTerminalObjectwith::for instancesmap_from_initial/map_to_terminalhelpers from recently merged PR Add canonical morphism helpers to Objects.v #2291rapply, single-line tactics with1:, etc.)Some lemmas are retained for backwards compatibility.