rschwiebert / dart_data

Data for the Database of Ring theory
Creative Commons Attribution 4.0 International
5 stars 2 forks source link

Equational classes and elementary sentences #80

Open dyunov opened 2 months ago

dyunov commented 2 months ago

The following ring classes also seem to be equational/formed by elementary sentences, but are not marked yet. Note that 0, 1 and inverses of elements are described using elementary sentences that only use quantifiers and conjunction (and thus are suitable for equational classes): $a+x=x$; $\forall x$ $ax=xa=x$; $ax = xa = u \wedge \forall z$ $uz=zu=z$.

rschwiebert commented 2 months ago

GCD domain can't be equational: the product of two such rings is not a GCD domain. But maybe the "GCD" part without "domain" might be equational?

Can't remember if Jose and I checked stable range 1. I think the conditional bit of the definition given currently doesn't qualify. Are you using an alternative criterion?

dyunov commented 2 months ago

@rschwiebert Yes, "GCD ring" would be equational :-) Then GCD domain is elementary. I avoided the conditional in "stable range 1" by "solving for $b$".

JoseBrox commented 1 month ago
* [ ]  GCD domain. _Elementary._ The GCD map is encoded by ∀a,b∃c∀d,e∃f ad+be=cf. 

I'm not sure about this: this is enconding the existence of a common divisor, but it doesn't enforce its uniqueness (it doesn't really matter if we ask the ring to be a domain and we are satisfied with "elementariness").

dyunov commented 1 month ago

@JoseBrox Please excuse me, I don't understand the parenthesized part of your message, as the property in DaRT already includes "domain". Did you mean to add this as a separate entry akin to "Ore domain/ring" or "PID/ring"? This one would be slightly weaker than Bezout, right?