[ definition ] characteristic of a `Ring` (etc.)

[jamesmckinna]

A propos de #2704 which concerns a class of Rings which in particular have characteristic 2, the general question arises:

• where should we define this? (if they are all definable on the Raw bundle, then Algebra.Definitions.RawX would work...)
• how... ? (incl. eg. the question of how characteristic 0 conventionally fits in)
• properties (characteristic is defined to be Prime, or as a consequence of the definition?)
• etc.

We don't seem to have analogues to Algebra.Properties for definitions of things which depend (but do they?) on algebraic structure:

• Nilpotent for Groups (and perhaps even Magmas?)
• Characteristic for Rings (as an instance of the above?)
• what else?

[Taneb]

Regarding your second bullet point, the characteristic of a field is the least integer-multiple of 1 that equals 0, under the divisibility ordering - this puts 0 at the top of the order, so that a ring won't have characteristic 0 if it has any other characteristic.

[JacquesCarette]

I would think that the characteristic of a Ring is a very property-like thing that shouldn't go right in the definition. There is way too much 'kit' that comes with Ring, that seems like bloat.

It is true that we don't have a good (standard) home for such definitions. Time to design something! I'd be curious to see what agda-unimath does this.

[Taneb]

@JacquesCarette agda-unimath defines the characteristic of a ring as the kernel of the unique homomorphism from the integers into that ring: https://unimath.github.io/agda-unimath/ring-theory.characteristics-rings.html

Wikipedia says that a ring R having characteristic n is the same as this kernel being (isomorphic as an ideal to?) nZ. So I think agda-unimath's definition is more constructive/computational than the textbook definition. That said, it doesn't seem like agda-unimath actually uses this definition anywhere, so I can't tell immediately if it's a useful variation.

If we want to go down this route, I have some of the machinery in https://github.com/agda/agda-stdlib/pull/2729 (ideals, kernels of ring homomorphisms)

[JacquesCarette]

Interesting. Seems like it is better constructively. I agree that understanding if this is a better definition would require trying it out.

What I was actually curious about is agda-unimath's organization of this. And now I see: it has ring-theory and so its way of organizing things is quite different and not something we can necessarily learn from.