Chosen products/coproducts

Stream: mathlib4

[Jad Ghalayini]

I was wondering if it would make sense to include chosen products/coproducts into Mathlib, since I need chosen coproducts for my work on programming language formalization. I've got a rough implementation in https://github.com/imbrem/discretion, and was thinking of adding AddMonoidalCategory, which would just wrap MonoidalCategory but with an alternative additive syntax, and having ChosenCoproducts extend it. ChosenProducts, if necessary, can extend MonoidalCategory.

My personal use for doing so would be as a stepping stone towards formalizing distributive categories and Conway iteration operators. While this could be done using coprod.desc, this has the issue of not working nicely with subcategories, where we would like the coproduct of the subcategory to agree. Eventually, this may also allow us to formalize e.g. rig categories, though I'm personally not currently interested in that.

[Markus Himmel]

Are you aware of docs#CategoryTheory.ChosenFiniteProducts and #20182?

[Adam Topaz]

I think if we go with ChosenProducts, then we should go all the way and have ChosenProductsOfShape X for some type X, ChosenProductsOfSize defined as ChosenProductsOfShape X for all X : Type u for some u, etc.

[Adam Topaz]

Then ChosenFiniteProducts could be refactored to become Forall n, ChosenProductsOfShape (Fin n), or something like that. (edit: on second thought, it's quite convenient to have chosen binary products in Type u being defeq to the type theoretic product, so maybe that last point needs more thought.)

[Joël Riou]

I think we should consider ChosenFiniteProducts as a proxy for a construction of a monoidal category structure, so we should keep the definition with binary products and the terminal object. (For the application to simplicial sets, that simplicies in a tensor product are just tuples is very convenient!)

[Adam Topaz]

Chosen finite products could have a built in binary product, terminal object, and products indexed by an arbitrary finite type. There was some discussion previously about doing something for n-fold tensor products in a monoidal category.

[Joël Riou]

We could have another class which extends ChosenFiniteProducts, but I am not sure we need to do this.
I agree that in a general monoidal category C, we should be able to consider the tensor product of a list of objects, and that there are variations on this theme in the symmetric case.

[Jad Ghalayini]

Markus Himmel said:

Are you aware of docs#CategoryTheory.ChosenFiniteProducts and #20182?

Yes, though I forgot about it at the time; what I need is ChosenFiniteCoproducts, essentially. Would a PR implementing that be welcome?

[Jad Ghalayini]

It would also be _really_ nice if we had some notation for these coproducts

[Jad Ghalayini]

I don't know if ⊕ would work since we use that for types, or + since using Add that way is slightly weird

[Jad Ghalayini]

My thoughts about AddMonoidalCategory were basically on whether the notation should be for coproducts specifically or a "coproduct flavor" symmetric monoidal structure, since the latter would allow us to work towards formalizing rig categories, which are cool (but not necessary for my work so I'm happy either way)

[Jad Ghalayini]

I do somewhat like the analogy between e.g. Monoid and AddMonoid, MonoidalCategory and AddMonoidalCategory

[Jad Ghalayini]

Most of the theorems would just be renamings, and could eventually even be handled with an AddMonoid like to_additive macro if we decide to go down that route

[Jad Ghalayini]

That said that's a lot of work and ChosenFiniteCoproducts is quite easy so I'd rather just start doing that as a PR if that seems likely to be accepted

[Jad Ghalayini]

Jad Ghalayini said:

I don't know if ⊕ would work since we use that for types, or + since using Add that way is slightly weird

Could also use something else if anyone has any suggestions. In discretion we use

• +ₒ for adding objects
• 𝟘_ C for the monoidal unit, which for the chosen coproducts case is the initial object of C
• ◁⁺ and ▷⁺ for additive whiskering
• +ₕ for adding morphisms
• α⁺ for the additive associator
• λ⁺ and ρ⁺ for the additive unitors
• σ⁺ for the additive symmetry, but this is a local convention, for Mathlib I'd want to be more consistent and e.g. use β⁺
  (for simplicity we just assume an AddMonoidalCategory is symmetric, since it is in all the cases we care about)

[Jad Ghalayini]

I've made a PR here, please let me know if it's any good: https://github.com/leanprover-community/mathlib4/pull/21603

[Sina Hazratpour 𓃵]

Joël Riou said:

We could have another class which extends ChosenFiniteProducts, but I am not sure we need to do this.
I agree that in a general monoidal category C, we should be able to consider the tensor product of a list of objects, and that there are variations on this theme in the symmetric case.

I think this is called "unbiased monoidal category" in the 2-category literature. See

• Leinster, 2004: Operads in higher-dimensional category theory, Sec 1.2: Unbiased bicategories (arxiv)

And the category of unbiased monoidal categories can be obtained as the category of strict/pseudo/lax algebras for the usual free monoid construction on the 2-category Cat.

I've recently started a formalization project which involves virtual double categories and the unbiased theme is very much there as well. But, maybe a good idea to do unbiased monoidal cats as first step?

(sorry, did not want to detract too much from the main point of this PR about ChosenFiniteCoproducts)

[Jad Ghalayini]

@Sina Hazratpour 𓃵 that's fine; I've also looked at your PR for distributive categories, and what I would really like for my thesis is for distributive categories to use chosen coproducts rather than the choice-based ones

[Jad Ghalayini]

And also of course to be based on premonoidal rather than monoidal categories

[Jad Ghalayini]

Would it make sense to make a PR which depends on both our PRs and does this?

[Sina Hazratpour 𓃵]

Interesting! For applications I had in mind and i guess consistent with the rest of mathlib i went for HasBinaryCoproducts instead of ChosenFiniteCoproducts. I think our motivations are quite different, but to give you some context i basically followed

1. Hans-Joachim Baues, Mamuka Jibladze, Andy Tonks, Cohomology of
   monoids in monoidal categories, in: Operads: Proceedings of Renaissance
   Conferences, Contemporary Mathematics 202, AMS (1997) 137-166

2. Carboni et al, Introduction to extensive and distributive categories

3. J.R.B.Cockett, Introduction to distributive categories, 1992

Note that HasBinaryCoproducts is slightly more general than ChosenFiniteCoproducts since I am not assuming the existence of an initial object, thought in its presence you can prove more. I think if you go full bimonoidal (aka rig-category), it does not make sense to assume existence of an initial object, unless you work in the less general case of semicartesian bimonoidal or some such thing.

@Joël Riou has been reviewing my PR (#20182). I'd wait to see what he has to say.

[Sina Hazratpour 𓃵]

One solution that comes to my mind: define rig-categories first, similar to distributive categories but with a second monoidal structure replacing coproducts. Then the second monoidal structure can come from ChosenFiniteCoproducts in the co-cartesian case. Then this will be consistent with ChosenFiniteCoproducts as a proxy for a construction of a the second cocartesian monoidal category structure.

[Sina Hazratpour 𓃵]

Jad Ghalayini said:

And also of course to be based on premonoidal rather than monoidal categories

i have not checked, do we have premonoidal stuff in mathlib?

[Jad Ghalayini]

@Sina Hazratpour 𓃵 I have a PR open for premonoidal stuff here: https://github.com/leanprover-community/mathlib4/pull/21488

[Jad Ghalayini]

I was thinking of doing the rig approach; the other alternative is to separate out chosen finite (co)products from choices of initial/terminal object; maybe do ChosenBinary(Co)products for just the products without the objects?

[Jad Ghalayini]

The issue is that's a lot more changes and tbf I want distributive premonoidal categories ASAP since I'm using them to formalize my thesis and currently using my own implementation, which is a bit irritating

[Jad Ghalayini]

How would you feel about ChosenBinaryCoproducts and ChosenInitialObject classes, with ChosenFiniteCoproducts just extending both of those? Then likewise for products

[Jad Ghalayini]

For the rig category stuff I proposed AddMonoidalCategory but again seems like a big change

[Sina Hazratpour 𓃵]

Wouldn't distributive premonoidal categories be more general than distributive monoidal categories? So, maybe a separate development in a premonoidal directory would be justified? Again, I am not a maintainer, so it would be better if one of the maintainers added a comment on this.

[Jad Ghalayini]

I have no idea how to get projects like this merged tbf, not really used to contributing to mathlib as I've mainly just done stuff in my own dependent libraries, but excited to get some of this work upstream (all this stuff is formalized in https://github.com/imbrem/discretion)

[Jad Ghalayini]

Sina Hazratpour 𓃵 said:

Wouldn't distributive premonoidal categories be more general than distributive monoidal categories? So, maybe a separate development in a premonoidal directory would be justified? Again, I am not a maintainer, so it would be better if one of the maintainers added a comment on this.

Well a distributive monoidal category is just a distributive premonoidal category where everything is central

[Jad Ghalayini]

For example in my PR I just changed the definition for BraidedCategory to require only premonoidal category + the braiding is central and things work just fine (the default tactic for the central field is infer_instance, and I added an instance so that for a monoidal category everything is central)

[Jad Ghalayini]

If you look in discretion distributive categories are the same way; you just have fields telling you coproducts preserve centrality and injections are central (this implies the distributor + inverse distributor are central) filled in automatically

[Jad Ghalayini]

Most of the theory goes through the same way (with perhaps a sprinkling of Central instances), and anything that doesn't can just replace the PremonoidalCategory instance with a MonoidalCategory instance

[Bhavik Mehta]

Jad Ghalayini said:

How would you feel about ChosenBinaryCoproducts and ChosenInitialObject classes, with ChosenFiniteCoproducts just extending both of those? Then likewise for products

@Markus Himmel do you have thoughts on this? I recall you feeling strongly that these shouldn't be made, but this was quite a while ago

[Yaël Dillies]

@Michał Mrugała and I are reaching a point in Toric where it would be really convenient to have a ChosenFiniteCoproduct API. We want to write Spec as a contravariant functor from R-Hopf algebras to group schemes over Spec R, whose type would tentatively be (Hopf_ (Under R))ᵒᵖ ⥤ Grp_ (Over (Spec R)).

[Andrew Yang]

I think it would be easier to use Grp_ ((Under R)^op) instead. Which also doesn’t need ChosenFiniteCoproduct

[Kevin Buzzard]

Then you're only looking at affine schemes not schemes, right?

[Adam Topaz]

Yeah I would argue that the “right” way to think about Hopf algebras is as group objects in affine schemes.

[Adam Topaz]

I assume we know that the functor from affine schemes to schemes preserves finite products, and that any functor that preserves finite products induces a functor on group objects, so that way you can also obtain a group schemes easily

[Adam Topaz]

The one thing I would change with this whole setup is to define the category of affine schemes as CommRing^op.

[Yaël Dillies]

Andrew Yang said:

I think it would be easier to use Grp_ ((Under R)^op) instead. Which also doesn’t need ChosenFiniteCoproduct

Okay sure, but then how do I solve

import Mathlib.CategoryTheory.Monoidal.Grp_

import Toric.Mathlib.CategoryTheory.ChosenFiniteProducts.Over

open AlgebraicGeometry CategoryTheory

attribute [local instance] Over.chosenFiniteProducts -- From #21399

variable {R : CommRingCat}

-- works
example : Grp_ (Over Rᵒᵖ) ⥤ Grp_ (Over <| Spec R) := sorry

-- failed to synthesize
--  ChosenFiniteProducts (Under R)ᵒᵖ
example : Grp_ (Under R)ᵒᵖ ⥤ Grp_ (Over <| Spec R) := sorry

[Yaël Dillies]

Are we going to duplicate every single ChosenFiniteProducts (Construction C) instance to ChosenFiniteProducts (Coconstruction C)ᵒᵖ?

[Yaël Dillies]

I don't really how this is better than duplicating to ChosenFiniteCoproducts (Coconstruction C)

[Andrew Yang]

I'm not sure what you need to duplicate. You would want ChosenFiniteProducts (Under R)ᵒᵖ to be formed by tensor products for the defeqs and there is nothing to generalize here.

[Andrew Yang]

But I was mainly saying that probably we don't want/need Hopf_ (or CoGrp_).