agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
589 stars 239 forks source link

Add `Algebra.Construct.WreathProduct` and/or `Algebra.Construct.SemiDirectProduct` #2351

Open jamesmckinna opened 7 months ago

jamesmckinna commented 7 months ago

This fell originally under #2348 but I think should be factored out on its own.

Current issues:

Re: the last point. previously I wrote on #2348 as follows: (This, viz. adding wreath products, as an instance of combining 'things-acted-upon-by-things') "... is complicated by the plethora of various definitions in the literature (according to the 'thinginess' involved), and the relationship with 'semi-direct product's... so perhaps some discussion/downstream refactoring may be necessary. "

Taneb commented 7 months ago

The binary product of Setoids is in Data.Product.Relation.Binary.Pointwise.NonDependent: https://agda.github.io/agda-stdlib/master/Data.Product.Relation.Binary.Pointwise.NonDependent.html#7308. I don't know if we already have currying defined for setoids of the top of my head.

jamesmckinna commented 7 months ago

Thanks @Taneb ! I'd just about managed to find that for myself while working on #2348 / #2350 but... not the first place I might have looked for it!

JacquesCarette commented 7 months ago

A known, thorny issue: finding things in stdlib is very hard.

JacquesCarette commented 7 months ago

As I said on #2348 : it makes sense for the constructions to be in Construct but the definitions of the structure shouldn't be in the same place.

Will Wreath be a construction (only) or will it need new structures? I don't have a strong opinion on Wreath vs SemiDirect.

jamesmckinna commented 7 months ago

Well, again, all good questions! I think that as a construction, I should at least also need Algebra.Construct.Pointwise which does not at present exist, AFAICT. (And that is a construction... not a definition).

As for WreathProduct itself, I think that that is also a construction: given a monoid, a monoid action, then ... such and such setoid ... also admits a monoid structure...

JacquesCarette commented 7 months ago

Good, I think this is converging to a design: indeed WreathProduct is a construction and so Construct is a great home for it. Yes, having a pointwise product construction would also be good. Whoever needs it first can build it.

jamesmckinna commented 7 months ago

And yes: Construct.Pointwise (properly, should we say: Power and Copower?) should, in turn, be factored out as a distinct issue/PR!

UPDATED: #2381