Hi all! I was wondering how much ring theory has been developed on top of mathcomp. I've seen what's in the repository, and found a few papers (eg https://arxiv.org/abs/1601.07472) that describe parts of it. Are there other projects or papers on this topic? I'm particularly interested in "general" rings, not specifically polynomials or matrices, but any references are very welcome.

I'm also interested in projects not based on mathcomp, but this seemed like the most likely place to start.

Not sure what you are looking for but we have a bit in https://math-classes.github.io/ and this library has also been ported to the HoTT library.

FTR, here is a list of *published* papers that build on top of math comp: https://math-comp.github.io/papers.html

@Rob Lewis have you looked at the Coq opam archive? For example `opam search ring coq`

with the `released`

Coq repo added gives quite a lot of results

Thanks very much, all, I'll look through these. @Bas Spitters I'm not sure exactly what I'm looking for either, hence the vague question :) mostly any developments of ring-theoretic ideas outside of the "standard" group-ring-field hierarchy.

this is an obvious one: https://github.com/CoqEAL/CoqEAL/blob/master/theory/README.md

@Rob Lewis we also have a formalization of universal algebra and a proof that Z is the initial ring.

Karl Palmskog said:

this is an obvious one: https://github.com/CoqEAL/CoqEAL/blob/master/theory/README.md

this is the companion code to the paper @Rob Lewis mentioned (with maybe a little bit more material than the strict contents of the paper).

@Rob Lewis what do you call "ring theory"? Are there specific areas of ring theory you are interested in or is it for a "survey" purpose?

What is ring theory? Anything about rings that aren't necessarily fields, I guess? :) Johan Commelin and I have been working on developing Witt vectors in Lean. Witt vectors over a base ring form a ring, there are lots of interesting ring homs, etc. I'm pretty certain this specific topic hasn't been formalized before, but I was curious about anything vaguely related.

This is also of interest to me, because of my project on doing algebraic geometry in MathComp (https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Developing.20basic.20%28modern%29.20algebraic.20geometry.20in.20mathcomp/near/210216848). For this I need a fair bit of commutative algebra, which is definitely part of ring theory.

There has been some constructive commutative algebra done in MathComp primarily by Anders Mortberg and friends, but I'm doing the classical (i.e., textbook) flavor of commutative algebra so I guess it doesn't translate directly.

apparently, "a Kleene algebra is a star semiring with idempotent addition", so this may be relevant (under heading *vaguely related*): https://github.com/damien-pous/relation-algebra

We also developed dioids (semirings with idempotent addition) : https://github.com/math-comp/dioid

We are using them with the min-plus dioid of functions to formalize analyses on traversal times of networks : https://en.wikipedia.org/wiki/Network_calculus

Here is my attempt to develop some commutative algebra in MathComp: https://github.com/xuanruiqi/commalg. Would really appreciate some feedback and advice, or even better, some collaborators. Currently struggling with maximal ideals!

Xuanrui Qi said:

Here is my attempt to develop some commutative algebra in MathComp: https://github.com/xuanruiqi/commalg. Would really appreciate some feedback and advice, or even better, some collaborators. Currently struggling with maximal ideals!

Ideals are defined here

Nevermind, you already saw that

Thanks though! Still trying to prove the basic results about max. ideals but now I have some classical results (e.g. classically every ringType is a unitRingType).

I'm working on extending the mathcomp Lmodule structure to support bases, free-modules, and finite direct sums. My library can be found at https://github.com/Modularius/CoqAlgebra (ignore everything except what's in "theories/Algebra" at the moment). My motivating aim is to formalise the connection between Algebras and Quiver Representations, but I've found myself spending a long time on formalising more general module constructions.

It's a work in progress and I'm building it in a way that is as compatible as possible with the existing mathcomp library.

Hi @Daniel Kirk thanks for sharing, is there something specific you'd like people to look at?

My pleasure, at the moment the files I'm working on and are closest to being actually functional are Modules.v, Linears.v, DirectSum.v, FreeModules.v and Dimension.v, found in "theories/Algebra". They depend on each other in that order.

In a general sense I suppose any feedback along the lines of how clear is it what I'm trying to do and whether there are any general improvements to my proofs would be very useful (I'm not very efficient with proofs). More specifically I'm looking at:

1) Making the direct sum construction more work for Zmodules. At the moment it's defined only for Lmodules over rings, I've yet to try generalising to Zmodules, I'm hoping it will be easy enough and canonical structures will make everything work for Lmodules as well as direct sums of rings etc.

2) In Dimension.v I'm struggling to prove

```
enum (ordinal_finType (n + m)) =
[seq unsplit i | i <- enum (sum_finType (ordinal_finType n) (ordinal_finType m))].
```

mainly due to my unfamiliarity with all the lemmas, but if there is a quick way anyone can think of to prove this that would be great.

For 2) noone is supposed to rely on the order of an enumeration of a a sum. The best you should be proving is `perm_eq`

of the two sequences. If you want to have an ordered enumeration, sort them.

Ah okay thanks, I think I'll have to reevaluate my approach here.

Last updated: Feb 08 2023 at 04:04 UTC