[ new ] add definitions of module-like structures

[laMudri]

This pull request introduces modules over rings. In detail, we have:

• LeftSemimodule and RightSemimodule over semirings
• Semimodule over commutative semirings
• LeftModule and RightModule over rings
• Module over commutative rings

Modules are all really R-modules. For example, the parameters of Module are the following.

Module {r ℓr} (commutativeRing : CommutativeRing r ℓr) m ℓm

As far as I understand, this best fits mathematical practice. It also means that IsModule depends on Algebra, motivating the new modules. The added modules are:

• Algebra.Module, corresponding to Algebra
• Algebra.Structures.Module, corresponding to Algebra.Structures
• Algebra.FunctionProperties.Module.Core, corresponding to Algebra.FunctionProperties.Core
• Algebra.FunctionProperties.Module.(Left|Right), corresponding to Algebra.FunctionProperties

The function properties were named based on what they look like, rather than names more meaningful for linear algebra. This produces names that are familiar from Algebra.FunctionProperties, and hopefully are beginner-friendly.

The module exports are very complicated, so there may be some bugs in them.

[MatthewDaggitt]

Looks mostly pretty good. This round of feedback is primarily concerned with the structure. I'll probably add a second round of minor formatting issues once we get everything in the right place.

[MatthewDaggitt]

I would usually say that these sort of proofs should go in Algebra.Module.Consequences, and then be imported. But of course LeftAction and RightAction aren't under Algebra.Module...

For the moment I'd put them under Algebra.FunctionProperties.LeftAction.Consequences and I'll sort them out later when I refactor Algebra as part of #876.

[MatthewDaggitt]

Hmm hierarchies don't usually have .Properties file but instead have a Properties.S for every structure S (which are usually parameterised by an S).

For example semiring⇒leftSemimodule should live in Algebra.Properties.Semiring and ring⇒rightModule should live in Algebra.Properties.Ring

[laMudri]

Do you think Algebra.Properties.LeftSemimodule &c is the way to go? Also, would this imply simplifying the names of lemmas? E.g, semiring⇒leftSemimodule becomes fromSemiring, or something like this.

[wenkokke]

This seems like putting a LOT in the module hierarchy, though: {left, right, neuter} * {semi, full}... that's a lot of modules.

[laMudri]

Yeah, this was also part of the reasoning. All of these lemmas are pretty similar, so it seems easier to keep them synchronised if they are together. Maybe we should think about how large this file is likely to get.

[MatthewDaggitt]

This seems like putting a LOT in the module hierarchy, though: {left, right, neuter} * {semi, full}... that's a lot of modules.

@wenkokke you're right, but it is the way the library is currently laid out (see Algebra.Properties). I think best to try and stay consistent.

Do you think Algebra.Properties.LeftSemimodule &c is the way to go? Also, would this imply simplifying the names of lemmas? E.g, semiring⇒leftSemimodule becomes fromSemiring, or something like this.

Yup sounds good to me.

[MatthewDaggitt]

Hmm okay, new plan! Keep this module as is, but rename it to Algebra.Module.Construct.Trivial? As you suggested earlier @laMudri, we could then ditch the semiring⇒ part of the semiring⇒leftSemimodule names?

Edit: ah, just seen that you suggested this as well. Great minds think alike 😄

[MatthewDaggitt]

I wasn't going to mention this is as the current definitions match the standard mathematical theory quite well, but having just read #898 I've realised that this should definitely be discussed.

This is the first time that we have "structures" taking in a "package" as a parameter. Is this something we want to allow? Although it matches the standard mathematical formalisation, it does introduce various problems with respect to the hierarchy.

1. As far as I can tell the issue in In CommutativeRing, Ring.semiring ≠ CommutativeSemiring.semiring #898 is caused by inheritance in the structure hierarchy not being replicated in the package hierarchy (for obvious reasons).
2. There's also the standard problem that as not all the fields from the package are exposed, it prevents you from expressing some relationships between modules. For example, you can't easily specify that two modules share all the same operations but the two underlying equality relations differ.

I'm a little worried that there might be more problems lurking out there as well. Whenever we deviate from the Structures/Packages pattern problems seem to creep in (e.g. the problems we've been having morphisms #853).

Although a little more verbose, I might be tempted to go with definitions in the style:

  record IsLeftSemimodule (+ * : Op₂ A) (0# 1# : A) (+ᴹ : Op₂ M) (*ₗ : Opₗ R M) (0ᴹ : M)  : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open L _≈_ _≈ᴹ_
    field
      +-*-isSemiring : IsSemiring + * 0# 1#
      +ᴹ-isCommutativeMonoid : IsCommutativeMonoid _≈ᴹ_ +ᴹ 0ᴹ
      *ₗ-cong : Congruent *ₗ
      *ₗ-zeroˡ : LeftZero 0# 0ᴹ *ₗ
      *ₗ-distribʳ : *ₗ DistributesOverʳ _+_ ⟶ +ᴹ
      *ₗ-identityˡ : LeftIdentity 1# *ₗ
      *ₗ-assoc : Associative _*_ *ₗ
      *ₗ-zeroʳ : RightZero 0ᴹ *ₗ
      *ₗ-distribˡ : *ₗ DistributesOverˡ +ᴹ

which would circumvent both of these problems and maintain consistency. What are people's thoughts?

[laMudri]

An odd thing is that then an R-module contains a proof that the operations of R form a ring – duplicating what is already contained in R. But still, this might be the way to go.

[laMudri]

@MatthewDaggitt Would it work to give IsLeftSemimodule a parameter of type IsSemiring, rather than Semiring?

[ajrouvoet]

@MatthewDaggitt I've been fighting with Agda to get a nice algebra hierarchy myself lately. The heavily parameterized ones are definitely the one to go for now, but are tedious to work with because you need a ton of quantification everywhere.

I wonder if Intellij's Arend gets it right, which claims to implement a neat trick where parameters and fields of records are actually one and the same thing: https://arend-lang.github.io/about/arend-features#anonymous-extensions

[jespercockx]

Sounds like the "frame type theory" by Cyril Cohen, Assia Mahboubi and Xavier Montillet (types 2019) would be useful here.

[MatthewDaggitt]

An odd thing is that then an R-module contains a proof that the operations of R form a ring – duplicating what is already contained in R. But still, this might be the way to go.

So the way I've avoided this in the Function hierarchy is not to use the Is modules internally but to simply re-list the properties. Obviously this quite a lot more effort here... Otherwise I'm not too fussed about the duplication. If you have the proof for Ring, it's easy to get IsRing out of it. It's a little inconvenient but it doesn't rule out any functionality like the current solution.

Should I introduce semiring⇒isLeftSemimodule : (R : Semiring c ℓ) → IsLeftSemimodule _≈_ R _+_ _*_ 0# 1#? Because of the requirement of a full (commutative) (semi)ring when forming Is(Left|Right|)(Semi)module, it's not quite so obvious what to do.

semiring⇒isLeftSemimodule sounds good, though I have to confess I'm not quite sure what the problem is? Is it the issue described in #898?

[MatthewDaggitt]

@ajrouvoet I've been fighting with Agda to get a nice algebra hierarchy myself lately. The heavily parameterized ones are definitely the one to go for now, but are tedious to work with because you need a ton of quantification everywhere.

Yes, it's definitely preferable to use packages when you can get away with it, but lots of quantification does seem to be required when you want dependencies between different structures.

@ajrouvoet I wonder if Intellij's Arend gets it right, which claims to implement a neat trick where parameters and fields of records are actually one and the same thing: https://arend-lang.github.io/about/arend-features#anonymous-extensions

That sounds really neat! Seems almost too neat to be honest, there must a trade-off somewhere surely? :)

@jespercockx Sounds like the "frame type theory" by Cyril Cohen, Assia Mahboubi and Xavier Montillet (types 2019) would be useful here.

I'm afraid I've temporarily fallen out of academia (working on reversing it!) and don't have journal access at the moment, so I'll have to take your word on that 👍

[jespercockx]

https://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51

[MatthewDaggitt]

@laMudri I think I'm going to bump this to v1.3 if that's okay with you? At some point I'll try and find the time to go through it and find a set of module parameters that work better.

[laMudri]

That seems fair. I think there are a few interrelated issues to work through before this can be improved and merged. I'd like to hear more from @JacquesCarette about keeping things coherent before proceeding.

[JacquesCarette]

It's definitely on my list of things to look at. I should be able to do it tomorrow or Friday.

[laMudri]

The definitions of (semi)module are now #985-compliant. An R-module is an R-R-bimodule, defined only when R is commutative. This gives the option to specify both the left scaling and the right scaling operators. There are also helper modules IsSemimoduleFromLeft and IsSemimoduleFromRight to allow specifying just one of them (it looks like I forgot to do the Module versions; will do shortly...).

[laMudri]

Oh, I forgot to add that one of the more surprising modifications to incorporate bimodules was the definitions IsPreleftSemimodule, IsPrerightSemimodule, &c. The idea is that giving both IsLeftSemimodule and IsRightSemimodule in order to prove IsBisemimodule would mean giving twice a proof of +ᴹ-isCommutativeMonoid. Instead, IsPreleftSemiring and IsPrerightSemiring omit this field, and IsLeftSemimodule and IsBisemimodule look as follows:

  record IsLeftSemimodule (+ᴹ : Op₂ M) (*ₗ : Opₗ R M) (0ᴹ : M) : Set _ where
    field
      +ᴹ-isCommutativeMonoid : IsCommutativeMonoid _≈ᴹ_ +ᴹ 0ᴹ
      isPreleftSemimodule : IsPreleftSemimodule +ᴹ *ₗ 0ᴹ

  record IsBisemimodule (+ᴹ : Op₂ M) (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M) (0ᴹ : M) : Set _ where
    field
      +ᴹ-isCommutativeMonoid : IsCommutativeMonoid _≈ᴹ_ +ᴹ 0ᴹ
      isPreleftSemimodule : IsPreleftSemimodule R-semiring +ᴹ *ₗ 0ᴹ
      isPrerightSemimodule : IsPrerightSemimodule S-semiring +ᴹ *ᵣ 0ᴹ
      *ₗ-*ᵣ-assoc : ∀ r m s → *ᵣ (*ₗ r m) s ≈ᴹ *ₗ r (*ᵣ m s)

These definitions basically abstract over duplicated code (in lieu of being able to abstract over pure rows); not much else.

[JacquesCarette]

Very nice development. It is also standard mathematical practice to have things like Module be parametric over a CommutativeRing. I think in module-theory is where the limits of listing every operator in the header of the IsFoo starts to fall apart (this isn't a criticism of this library, this is a criticism of the current Agda library methodology, but is a bit pointless since there are no good alternatives yet). What is needed are 'record definition combinators' that allow you to bundle/unbundle at will. [See the PEPM 2020 paper].

The point is that there are a whole bunch of isomorphic ways of defining the same thing in Agda, and they have different usability profiles in different contexts. So it's not like one is better than any of the others, it's that they are each relatively superior. See points 7-10 of Tom Hales' critique of Lean for many things which apply to Agda too.

Bottom line: in current Agda, I think what you've done here is the best you can do, and should be merged in. What will be needed is for someone on the core Agda team to get interested in this kind of library development and see that things have gotten unwieldly but could be fixed. (Hopefully @alhassy and @WolframKahl are paying attention too).

[MatthewDaggitt]

Hi @laMudri, apologies for taking a while to get back to this. It's definitely getting there! I've added a few more comments. Also it's missing a changelog entry but that can probably come when we've got it all nailed down.

[MatthewDaggitt]

When is the A not inferable?

[laMudri]

This module is made to be used like the old Algebra.FunctionProperties. In Algebra.Module.Structures, we do

import Algebra.FunctionProperties.LeftAction as L

and then

  record IsPreleftSemimodule (+ᴹ : Op₂ M) (*ₗ : Opₗ R M) (0ᴹ : M)
                             : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open L R _≈ᴹ_
    ...

where A is filled by R. This open fails if R is replaced by _.

Maybe Algebra.Structures does something different these days, in which case the thing here probably should be changed. But otherwise, I think it's right.

[MatthewDaggitt]

This seems like putting a LOT in the module hierarchy, though: {left, right, neuter} * {semi, full}... that's a lot of modules.

@wenkokke you're right, but it is the way the library is currently laid out (see Algebra.Properties). I think best to try and stay consistent.

Do you think Algebra.Properties.LeftSemimodule &c is the way to go? Also, would this imply simplifying the names of lemmas? E.g, semiring⇒leftSemimodule becomes fromSemiring, or something like this.

Yup sounds good to me.

[MatthewDaggitt]

Looking really good, I think we're pretty close now!

Do you do anything different for long using lists?

I think we tend to put related names on the same line but other than that not really.

[MatthewDaggitt]

Does this really work? 😮

[MatthewDaggitt]

Not sure this comment is quite right?

[MatthewDaggitt]

Hmm okay, new plan! Keep this module as is, but rename it to Algebra.Module.Construct.Trivial? As you suggested earlier @laMudri, we could then ditch the semiring⇒ part of the semiring⇒leftSemimodule names?

Edit: ah, just seen that you suggested this as well. Great minds think alike 😄

[gallais]

Note that now that we are using 2.6.1 on master, you do not need to use
\ where to pattern-match on a pair: a usual lambda abstraction will do.

[laMudri]

On my checklist:

• There is one TODO: moving a definition in Agda.Module.Construct.Biproduct into the main Algebra hierarchy. This would basically mean creating Algebra.Construct.Biproduct, and reasonably populating it.
• Tensor products are the last remaining standard construct. But they are hard, so I think they should be left for later. Perhaps I'll open an issue with a high-level description when this gets merged.

[gallais]

👍 for later. This is already a pretty big PR.

[laMudri]

For the first todo, maybe this should have its own (simple, but possibly moderately large) pull request, partially to test out the Construct structure to a wider audience.

[MatthewDaggitt]

Merged in. Thanks for everyone's contributions!