Add additive categories infrastructure#2304
Conversation
|
Thanks @CharlesCNorton ! I just pushed a commit that shows that |
| Class AdditiveCategory := { | ||
| cat : PreCategory; | ||
| add_zero :: ZeroObject cat; | ||
| add_biproduct : forall (X Y : object cat), Biproduct X Y; |
There was a problem hiding this comment.
I'm confused by this class. The three fields above are already enough to show that cat has a unique enrichment over commutative monoids. That means that eight of the remaining nine fields are redundant. You only need to assume that inverses exist.
Here's an idea: Have a file, maybe called "SemiAdditive.v", which has a class with just the above three fields. In that file, prove that in every SemiAdditive category, the hom sets are commutative monoids in a way compatible with composition. It's probably best to use IsCommutativeMonoid from Classes/interfaces/abstract_algebra.v, which should then give you access to lots of lemmas (and notations) that hold for commutative monoids. Then, in Additive.v, you add the axiom that the commutative monoid structure defined in SemiAdditive.v has inverses. Then you can in fact say that the hom sets are abelian groups, using Algebra/AbGroups/AbelianGroup.v.
There was a problem hiding this comment.
I'm confused by this class. The three fields above are already enough to show that
cathas a unique enrichment over commutative monoids. That means that eight of the remaining nine fields are redundant. You only need to assume that inverses exist.Here's an idea: Have a file, maybe called "SemiAdditive.v", which has a class with just the above three fields. In that file, prove that in every SemiAdditive category, the hom sets are commutative monoids in a way compatible with composition. It's probably best to use
IsCommutativeMonoidfrom Classes/interfaces/abstract_algebra.v, which should then give you access to lots of lemmas (and notations) that hold for commutative monoids. Then, in Additive.v, you add the axiom that the commutative monoid structure defined in SemiAdditive.v has inverses. Then you can in fact say that the hom sets are abelian groups, using Algebra/AbGroups/AbelianGroup.v.
Just checking in - working on this, but it's taking some sweat. Will put a PR in soon.
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.
CharlesCNorton
force-pushed
the
patch-7
branch
10 times, most recently
from
16d96dd to
e96c31c
Compare
|
I think this is good to go. I've been wrong in the past though.... |
- 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.
|
LGTM. Thanks! |
2 participants
Defines additive categories on top of the semi-additive structure from #2305, following the design suggested in review.
Provides:
AdditiveCategory: aSemiAdditiveCategorytogether with anInverseoperation on each hom-set and the left inverse lawIsAbGroupinstance and a bundledabgroup_hom : AbGroupfor each hom-setAdditiveFunctor: a functor whose action on each hom-set is monoid-preserving, with preservation of zero morphisms and negation derived