Add is_euclidean_type trait

[fingolfin]

The idea is that this true for ring / ring elem types that explicitly support a euclidean division with remainder, and ideally also a euclidean degree (to be defined in the interface). This is just a draft to have a point for discussion and experiments: it is missing many things, including documentation as to what is_euclidean_type(x)==true means, which promises this incurs; and of course also code needs to be adapted to use it (e.g. the residue ring or ideal constructions or whatnot that only work sensible for euclidean rings should check this.

Some possibly relevant issues:

• Implement more ring and elem properties/predicates Nemo.jl#329
• In non-euclidean ZZ[:x], calls to gcdx result in infinite loop Nemo.jl#1474
• Rings/Euclidean rings need better documentation #552
• Implement Euclidean function for Euclidean domains #36
• Implement ann(a) for Euclidean rings #35
• residue_ring of a residue_ring is very slow oscar-system/Oscar.jl#4410 (most recent motivation for this PR)

Note that this is explicitly different from the mathematical property. I'd be happy to also add a function is_euclidean_ring resp. is_euclidean(::Ring) for the mathematical property, if someone wants it, but that's a separate thing.

Anyway, with that out of the way: let's get started with the flaming and bikeshedding :-)

(Includes PR #1942 for my convenience)

[fieker]

On Fri, Dec 20, 2024 at 07:47:18AM -0800, Max Horn wrote: The idea is that this true for ring / ring elem types that explicitly support a euclidean division with remainder, and ideally also a euclidean degree (to be defined in the interface). This is just a draft to have a point for discussion and experiments: it is missing many things, including documentation as to what is_euclidean_type(x)==true means, which promises this incurs; and of course also code needs to be adapted to use it (e.g. the residue ring or ideal constructions or whatnot that only work sensible for euclidean rings should check this. Most recent motivation for this is oscar-system/Oscar.jl#4410 but there are many others. Note that this is explicitly different from the *mathematical* property. I'd be happy to also add a function `is_euclidean_ring` resp. `is_euclidean(::Ring)` for the mathematical property, if someone wants it, but that's a separate thing. Anyway, with that out of the way: let's get started with the flaming and bikeshedding :-)

Part of why we haven't proceeded with the traits was that we never fogured out what to do in the presence of more than one applicable trait... also we were waiting for some trait system to become standart in Julia

…

(Includes PR #1942 for my convenience) You can view, comment on, or merge this pull request online at: #1943 -- Commit Summary -- * Make is_exact_type and is_domain_type more convenient * Add is_euclidean_type trait -- File Changes -- M src/Fields.jl (2) M src/Poly.jl (11) M src/Rings.jl (31) -- Patch Links -- https://github.com/Nemocas/AbstractAlgebra.jl/pull/1943.patch https://github.com/Nemocas/AbstractAlgebra.jl/pull/1943.diff -- Reply to this email directly or view it on GitHub: #1943 You are receiving this because you are subscribed to this thread. Message ID: ***@***.***>

[thofma]

A few weeks ago in https://hackmd.io/EYHpciQ9ToCCYQcbmv7oGg I collected some ideas of @fieker, @joschmitt and myself on ring traits and matrix normal forms (HNF, SNF, etc). There is some overlap with this here.

Just some random comments/questions:

• We have rings where divrem is not deterministic.
• $a$ divides $b$ if and only if the remainder is zero in rem or divrem is I think too strong.
• Unique remainders is also too strong.
• There are rings, where division with remainder is a partial function, i.e., not applicable to all tuples. For example, in $R[X]$ we have a well-defined division with remainder in case the divisor is monic (or has invertible leading coefficient). Should divrem be allowed or disallowed?

From experience a "euclidean" trait is not that useful and as far as I can tell, the (real? original?) question is about collecting properties to make EuclideanResidueRing work. There is actually nothing Euclidean about it. It is just quotients modulo a principal ideal (which can be implemented for any "base" ring) and small/reduced representatives modulo principal ideals.

I think we could already solve some of these issues by doing quo(R, f) = quo(R, ideal(R, [f])) and similar for residue_ring (+ some boilerplate methods). Would already make some people happy before we agree on something here.

[codecov]

Codecov Report

Attention: Patch coverage is 14.28571% with 12 lines in your changes missing coverage. Please review.

Project coverage is 88.17%. Comparing base (9843ed5) to head (f5d43f0).
Report is 4 commits behind head on master.

Files with missing lines	Patch %	Lines
src/Rings.jl	0.00%	10 Missing ⚠️
src/Fields.jl	0.00%	1 Missing ⚠️
src/Poly.jl	66.66%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #1943      +/-   ##
==========================================
- Coverage   88.21%   88.17%   -0.04%     
==========================================
  Files         119      119              
  Lines       30385    30395      +10     
==========================================
- Hits        26803    26801       -2     
- Misses       3582     3594      +12     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[fingolfin]

Perhaps @thofma, @fieker and me can get together to make a plan and perhaps a first draft of a bunch of traits?