Define `LocalRing`

[jamesmckinna]

Some delicacy required over the precise axiomatisation, in order to avoid too much decidability (and with the Maximal Ideal 'Theorem'/Axiom also lurking offstage; it might be useful to avoid any discussion of maximal ideals at this stage?), so perhaps using the geometric version: Every element is either zero or else has a multiplicative inverse? UPDATED to correct statement (:-)):

Local = ∀ x → x ≈ 0# ⊎ Invertible 1# _∙_ x  ⊎ Invertible 1#  _∙_ (#1 - x)

Nagata, (1962, Wiley), "Local Rings"
nlab page

Cf. #1615 / #1718 for antecedents.

[mechvel]

The most general construct here is a Fraction Domain over a (commutative?) Ring R by a Multiplicative system S in R, where the denominators for fractions over R are taken only from S.
And a subset S is required to be closed under * (I do not recall, maybe some more requirement is set for S).
A local ring is a special case of FractionDomain over S, where S = R \ I, where I is a prime ideal.
So, the most reasonable way (for an Applied Library for algebra!) is to

1. define what is a multiplicative system, probably as the membership function agreed with ≈ and *,
2. define the ideal notion, again, via the membership function agreed with ≈ and operations.
3. define the constructs of (FractionDomai S), (LacalRing primeIdeal-I).

But I am sure that these constructs are not for Standard library for Agda.
Such an approach leads to that Standard library will include the algebra library having million pages of the source code.
Local rings, and many other subtle and advance constructs are only for Applied libraries.

As to Standard library, it is sufficient FractionField over a GCDDomain.
I have such in in my Applied library.
But i do not believe that I am able to make it standard.
Because it relies on the general notion of GCD, GCDDomain, and I failed to make standard even these ones.

[jamesmckinna]

As to a stdlib with millions of lines of code, this is exactly the state of affairs for the Lean mathlib and the Rocq MathComponents libraries as I understand it. I think we should be bold enough to imagine a (near?) future in which Agda enjoys similar expressiveness.

Resource constraints on checking such a thing are another matter, as, ahem, are constraints on developer resources... ;-)

[JacquesCarette]

Growing stdlib a lot would be nice.

We should pay close attention to who are the main Agda users who use stdlib (and ignore cubical Agda users, they are a different breed): lots and lots use it to do the meta-theory of programming languages and the like. So our biggest impact would be to support those activities as much as possible.

[jamesmckinna]

Growing stdlib a lot would be nice.

;-) one PR at a time...

We should pay close attention to who are the main Agda users who use stdlib (and ignore cubical Agda users, they are a different breed): lots and lots use it to do the meta-theory of programming languages and the like. So our biggest impact would be to support those activities as much as possible.

For sure, but if we took this idea too far, we might end up only working on the Algebra hierarchy as regards order-theoretic concepts in denotational semantics?

Part of my motivation for pressing on with general Algebra follows not only my mathematical instincts, but also the computational, eg with recent work on actions in general, and modules in the context of work on AD.

Lurking off-stage is trying to grasp how much we need to start a programme of foundations for computer algebra... but early days yet!

[JacquesCarette]

I fully include all the needs of AD in the necessary kit stdlib should have. And I'd be happy to also support the needs for symbolic computation and computer algebra.

I'm also fine with including any "standard" stuff that someone just decides to contribute. All I'm arguing for above is that if the core maintainers have spare cycles to work on community-oriented stuff, that's likely the community who would benefit best.