Some ideas for graded and monoidal categories, and categorical algebra

[LionOfJewdah]

In PRs #534 and #535, I contributed a monoidal category coherence solver based on MacLane's free-strict-monoidal-category construction and the scalars of monoidal categories (endomorphisms of unit), which by the Eckmann-Hilton argument form a commutative monoid. I'm also working on a stack of PRs to construct the JSV trace of a compact closed category, and (as a stretch goal, via the theorem of Hajgató-Hasegawa 2013, construct the compact closed structure on traced *-Autonomous categories).

I have some more ideas for contributions. Would there be interest in these? Please let me know.

Graded Categories

As I understand it, a Graded Category is a category with a functor to a monoid as a category. In a personal project, I presented this as a category with an action on a monoid:

record GradedCategory (o h e gℓ g≈ℓ : Level) (G : Monoid gℓ g≈ℓ) : Set (lsuc (o ⊔ h ⊔ e ⊔ gℓ ⊔ g≈ℓ)) where
  private module G = Monoid G

  field
    category : Category o h e

  open Category category public

  field
    grade : ∀ {A B : Obj} → A ⇒ B → G.Carrier

    grade-id : ∀ {A : Obj} → G [ grade (id {A = A}) ≈ G.ε ]ᵐ

    grade-∘ : ∀ {A B C : Obj} {f : A ⇒ B} {g : B ⇒ C}
                     → G [ grade (g ∘ f) ≈ G [ grade g ∙ grade f ]ᵐ ]ᵐ

    grade-resp-≈ : ∀ {A B : Obj} {f g : A ⇒ B}
                 → f ≈ g → G [ grade f ≈ grade g ]ᵐ

Where I defined _[_≈_]ᵐ the obvious way. I also showed this is equivalent to a functor from category to MonoidAsCategory _ G, and defined a GradedFunctor between G-graded categories as a functor that commutes with the grading. This is the same as saying the 2-category of G-graded categories is the coslice category Cat / MonoidAsCategory(G), and for any category C and any monoid M you can form the cofree M-graded category as the product category C × MonoidAsCategory(M). Any functor F : C → M is a grading on C, and this is the same by πʳ as id {C} ※ F : C → C × MonoidAsCategory(M). (Of course, this extends to groups, and to discrete categories; I often use groupoids and categories constructed co-freely as S some set and G some group or monoid, with s t : S, s ⇒ t = G.)

Commutative Monoid ⇌ Monoidal Category Adjunction

Just as a monoid is a category on one object, a commutative monoid can be viewed as a monoidal category on one object, the unit. In fact, we already have one direction of this from #535 and the Eckmann-Hilton argument -- the endomorphism monoid of the unit of any monoidal category is a commutative monoid. The same Eckmann-Hilton argument can be applied in reverse, constructing a base category for a commutative monoid M as MC = MonoidAsCategory M, then defining a monoidal structure on MC with trivial tensor on the object and trivial unitors and associators and defining ⊗₁ = ∘. In of itself, this (provisionally named) CommMonoidAsMonoidalCat.agda would be a short file. But more interesting is the adjunction that arises between the category of commutative monoids (which I thought was CM-Category in Categories.Category.CMonoidEnriched but actually something else) and Monoidals with Monoidal functors. (I think Lax monoidal functors suffice but haven't actually proven this yet. Strong ones definitely do.) Any Monoidal Category determines the commutative monoid of its scalars, and any commutative monoid can be presented as a monoidal category on a single object. Strong monoidal functors preserve the unit up to coherent isomorphism, hence preserve scalar action in the delooping MC of M.

Algebraic adjunctions

I've also constructed adjunctions for (commutative/not assumed commutative) Semirings ⇌ Rings, Monoids ⇌ Groups, and the commutative versions of these things to the general versions. It basically works out that, if there are additive idempotents in a semiring, its ringification is trivial, else you adjoin negatives, etc. Also the center of monoids, groups, rings; and even the group of units on a ring or monoid and the free ring (or R-algebra) on a monoid. I know this repo doesn't have as much heavy non-categorical algebra, even from the categorical perspective, but I could contribute some of this if desired.

Other

I've mentioned before, my favorite is the category of matrices over a (commutative) (semi-) ring, equivalent to the category of finitely-generated free (bi)(semi)modules on that (C)(S)Ring. I would have to contribute the matrix algebra here or to stdlib. The bimodule or even Hadamard (C)(S)Ring is just Algebra.Construct.Pointwise, Fin n → Fin m → R. For matrix multiplication define e.g.

δ : ∀ {n} → Fin n → Fin n → Carrier
δ zero    zero    = 1#
δ zero    (suc _) = 0#
δ (suc _) zero    = 0#
δ (suc i) (suc j) = δ i j

Iₘ : ∀ {n} → Mat n n
Iₘ = mkMat δ

mulSummand : ∀ {n k m : ℕ} → Mat n k → Mat k m → Fin n → Fin m → Fin k → Carrier
mulSummand A B i j = (entry A i -⟨ _*_ ⟩- flip (entry B) j) ˢ id

innerProd : ∀ {n k m : ℕ} → Mat n k → Mat k m → Fin n → Fin m → Carrier
innerProd A B i j = finSum (mulSummand A B i j)

_·ₘ_ : ∀ {n k m : ℕ} → Mat n k → Mat k m → Mat n m
A ·ₘ B = mkMat (innerProd A B)

and you get the (semi)ring structure for SqMat n = Mat n n almost for free. Then (especially with a non-trivial conjugation involution) on R, you get a dagger-compact-closed rig category of matrices which (when R is commutative) is self-enriched, and for any (semi-)ring homomorphism R → S you get a strong monoidal functor MatCat R → MatCat S entrywise, natural and integer MatCat initiality among (semi-)ring matrix categories, the general linear groupoid as the core of MatCat R, the determinant (for commutative rings) as a natural transformation of (groups or monoids) of Mat n R → R or GL(n, R) → R×. Among other things, permutation matrices are possible over any semiring (in fact, they are the associators and rig distributors.)

[JacquesCarette]

I would recommend starting with IsGradedCategory as the unbundled version (i.e. C on the outside) before bundling. Might want to bundle the monoid too. But you might want to consider locally graded category as even more general. Which, in fact, @TOTBWF has partly done already but would likely appreciate someone else "pushing it over the line".

The addition of the various instances of adjunctions also seems like a good idea (but split in to many PRs).

Matrix algebra should go to stdlib, and preferably first. A solid discussion of what is a good representation of Matrix needs to happen first. The Fin-based one has serious pros and cons! I'm quite sure you'll at least be told that quite a lot of these things generalized to I-indexed items (for an arbitrary indexing set I, which sometimes will need decidable equality, other times a linear order, etc). Then picking I = Fin n will give you many of what you lay out. [I'm doing that myself, after @jamesmckinna pushed me to, for some Algebra work!]