Rob Lewis (Sep 18 2020 at 11:21): Rob Lewis (Sep 18 2020 at 11:21):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.
Rob Lewis (Sep 18 2020 at 11:22):I'm also interested in projects not based on mathcomp, but this seemed like the most likely place to start.
Bas Spitters (Sep 18 2020 at 11:51):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.
Enrico Tassi (Sep 18 2020 at 12:57):FTR, here is a list of published papers that build on top of math comp: https://math-comp.github.io/papers.html
Karl Palmskog (Sep 18 2020 at 13:11):@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
Rob Lewis (Sep 18 2020 at 13:46):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.
Karl Palmskog (Sep 18 2020 at 13:49):this is an obvious one: https://github.com/CoqEAL/CoqEAL/blob/master/theory/README.md
Bas Spitters (Sep 18 2020 at 13:50):@Rob Lewis we also have a formalization of universal algebra and a proof that Z is the initial ring.
Cyril Cohen (Sep 18 2020 at 15:03):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).
Cyril Cohen (Sep 18 2020 at 15:04):@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?
Rob Lewis (Sep 18 2020 at 15:33):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.
Xuanrui Qi (Sep 18 2020 at 15:52):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.
Karl Palmskog (Sep 18 2020 at 15:57):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
Pierre Roux (Sep 25 2020 at 09:57):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
Xuanrui Qi (Sep 29 2020 at 07:24):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!
Cyril Cohen (Sep 29 2020 at 12:50):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
Cyril Cohen (Sep 29 2020 at 12:51):Nevermind, you already saw that
Xuanrui Qi (Sep 29 2020 at 15:14):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).
Daniel Kirk (Oct 23 2020 at 11:46):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.
Cyril Cohen (Oct 25 2020 at 12:15):Hi @Daniel Kirk thanks for sharing, is there something specific you'd like people to look at?
Daniel Kirk (Oct 25 2020 at 14:47):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.
Cyril Cohen (Oct 25 2020 at 14:58):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.
Daniel Kirk (Oct 25 2020 at 19:57):Ah okay thanks, I think I'll have to reevaluate my approach here.
Last updated: Dec 01 2023 at 06:01 UTC