Add stable category theory formalization #2288
Conversation
This formalization includes: - Pre-stable and proper stable categories with suspension (Σ) and loop (Ω) functors - Natural transformations η : 1 → Ω∘Σ and ε : Σ∘Ω → 1 with adjunction structure - Distinguished triangles and the axioms of triangulated categories (TR1, TR2) - The fundamental duality principle: opposite of stable is stable with Σ and Ω swapped - Basic cone/cofiber construction for completing morphisms to triangles - Extensive theory of semi-stable categories and triangle identities Known limitations: - No shift/translation functor [1] that shifts degrees - No cone sequences beyond basic cone construction - No proof that rotation of distinguished triangles preserves the distinguished property in all cases - No completion of morphisms to distinguished triangles beyond the basic framework - No concrete examples (stable homotopy category, derived categories, etc.) - Uses traditional Categories library instead of newer WildCat framework Technical details: - Currently compiles with JsCoq 0.10.0~beta1 and Coq 8.10+beta2 (July 2019) - Requires refactoring for compatibility with current Coq and HoTT versions - ~2500 lines covering foundations through advanced duality theorems Opening as draft PR per discussion with @Alizter for collaborative updating to latest versions.
|
@CharlesCNorton This sounds great! Hopefully it will only require some minor tweaks to build with the current versions of Coq and the library. I don't know much about the Categories sub-library, but it hasn't changed much in years. Are you planning to work on updating it to the current versions? If so, let us know if you need any tips to fix particular issues. |
|
@jdchristensen Thank you very much! Yes I am planning on an update, though I'm worried getting Coq/HoTT updated and working on Windows might actually take more time than updating the code itself! |
|
@jdchristensen @Alizter Update complete! It now compiles on Coq 8.20.1 + HoTT 8.20. Only needed to change True → Unit and I → tt in 3 places. Much easier than expected! Please give it a run at your leisure! |
|
@CharlesCNorton That's great that it was easy to do! Hopefully @Alizter or I can review this soon. BTW, the one build error is unrelated to your PR, and I've created #2290 to track it. |
There was a problem hiding this comment.
I just took a quick look at the start of this, making mostly trivial style comments.
A larger comment is that this should be broken up into many smaller files, each achieving a specific goal. The average file in the Categories library is 81 lines long, and the longest is 677 lines long, just to give you an idea of how things are generally done.
BTW, we also have work on biproducts in wild categories in #2016, but it is being reorganized a bit right now. It might be good to follow similar naming, but this task should wait until #2016 is a bit further along (maybe in about two weeks?) @ThomatoTomato
Add suspension fixed points and octahedral axiom (TR4) - Prove zero is a suspension fixed point - Formalize TR4 with cofiber universal property
|
@jdchristensen Sorry for adding more while you're reviewing! I added two sections that might be useful:
Everything still compiles! |
No worries, I haven't started any serious review. I think it'll be easier to review when broken up a bit, as then we could tackle one piece at a time. |
|
Sounds good! I'll start on that and implement the style fixes as well. |
|
BTW, can you make the first line of your commit messages more descriptive? That's all that github and git show by default in many cases. Thanks! |
CharlesCNorton
changed the title
CharlesCNorton
changed the title
|
New commit is preparation for section division before file division. Should have this completed soon. |
Various style errands - further preprocessing for file division. Finishing touches on TR4, etc.
- Break up monolithic file per reviewer feedback. - Organize into logical modules: foundation, pre-stable, triangles, opposite, stable, advanced - Preserve all functionality with proper dependency ordering - Each file now has single responsibility: ZeroObjects, Biproducts, Triangles, etc. - No semantic changes, only structural reorganization
|
@jdchristensen File split complete! I've broken up the monolith into modular files as requested. |
| structure that makes a category "additive-like". | ||
| *) | ||
|
|
||
| From HoTT Require Import Basics Types Categories. |
There was a problem hiding this comment.
I don't think you want to require all of Categories, since once that meta-file is updated to include your work, this will cause a circular import.
|
@CharlesCNorton Thanks for splitting this up. What do you think about moving some of the files that aren't strictly about "stable" things to somewhere else? E.g. maybe an "Additive" folder would make sense? (As I mentioned, I'm not very familiar with the organization of the Categories library, so you might need to follow whatever pattern is used there.) I'm pinging @JasonGross in case he has any advice about this question, but also more generally about the whole PR. Also, can you list the new files in an order that it would be sensible to review them in (with dependencies listed before files that use them)? Then we could make a task list with those files as items, and various people (maybe @JasonGross and @Alizter and me) could tackle them one at a time, and mark them as reviewed in the task list. |
|
@jdchristensen I defer entirely to your judgment on the organization. I'll provide the ordered file list with dependencies as requested. |
|
BTW, feel free to mark things as "Resolved" when you handle them. |
|
Please forgive the presentation. I will also upload:
|
minor stylistic chore for duality theory icon. non-functional change
Oh, I didn't mean that you had to go to the trouble of listing the dependencies of each file. I just wanted the files listed in an order compatible with the dependencies. Assuming that you did this, I have added them as a task list in the first comment of this PR.
Thanks for doing that, but you should remove that file from the PR. It would make more sense as an attachment to to the PR (using the "paste, drop or click to add files" button), but it doesn't make sense as a file in the PR itself. In any case, now that the files are in a task list, we don't need the Dependencies.md file at all. |
will do 👍thank you very much for your time |
refactor(ZeroObjects): Use HoTT library definitions and fix imports Changes: - Remove Categories from imports to prevent circular dependencies - Use IsInitialObject and IsTerminalObject from Category/Objects.v - Make is_initial and is_terminal fields into instances using :: - Update documentation to better describe categorical role - Use rapply tactic for cleaner proofs Not changed: - Keep existing lemmas for backwards compatibility - Temporarily defer moving lemmas to Objects.v (requires HoTT library changes) - Temporarily defer adding map_from_initial/map_to_terminal helpers (requires HoTT library changes)
- Make `unique` tactic global by removing `Local` modifier - Add `map_from_initial` and `map_to_terminal` for canonical morphisms - Add `initial_morphism_unique` and `terminal_morphism_unique` theorems - Proofs use existing `unique` tactic These additions provide cleaner access to unique morphisms from/to initial/terminal objects, as suggested in PR HoTT#2288.
|
@CharlesCNorton I like how you factored out one task into a separate PR. I think that's a good way to continue, as this PR is going to get overwhelmed by comments as we work through the files. So maybe you can finish up ZeroObjects.v in a new PR that we'll polish and merge, and then do a PR for the next file, etc. That will also give you a chance to clean up each item before I review it. |
👍will do |
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.
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.
Move transport lemmas from separate file to Core.v per PR HoTT#2298 review - @jdchristensen Changes: - Add transport_compose_morphism and transport_compose_both_inverse to Category/Core.v - Remove TransportMorphisms.v from Additive folder - Use Definition with pattern matching instead of Lemma with destruct - Drop redundant lemmas (moveL_transport_V already exists) Extracted from stable categories formalization (PR HoTT#2288). Tested with: make -f Makefile.coq
Extracting Biproducts.v from stable categories formalization (HoTT#2288). **Status: WIP - not ready for merge** Changes from original formalization: - Fixed imports (removed non-existent ZeroMorphismLemmas.v) - Made `ZeroObject` implicit throughout using `` `{Z : ZeroObject C} `` - Updated `zero_morphism` calls to use implicit Z parameter - Removed unused definitions (bi_inl, bi_inr, bi_outl, bi_outr, biproduct) - Removed unused lemma (biproduct_prod_unique) - Applied HoTT style conventions The file provides: - `BiproductData`: injection/projection morphisms - `IsBiproduct`: axioms (beta_l, beta_r, mixed_l, mixed_r) - `HasBiproductUniversal`: universal properties as product and coproduct - `Biproduct`: complete structure combining the above - Operations: biproduct_coprod_mor, biproduct_prod_mor with beta lemmas - Uniqueness lemma: biproduct_coprod_unique @jdchristensen This is work in progress, naturally - submitting early for initial feedback. I will be continuously re-reviewing for anything I missed. Thank you very much for your time
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
This formalization includes:
Known limitations:
Technical details:
Opening as draft PR per discussion with @Alizter for collaborative updating to latest versions.
Rest added by @jdchristensen : Files to review. A checkmark indicates that at least one person has reviewed it, not that the comments have been taken into account. That could be indicated by a strikethrough, or something like that.