Comments (1)
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
- define what is a multiplicative system, probably as the membership function agreed with ≈ and *,
- define the ideal notion, again, via the membership function agreed with ≈ and operations.
- 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.
from agda-stdlib.
Related Issues (20)
- List of wrinkles in `Data.List.Properties` HOT 7
- List of sub-optimal definitions in `Data.List.Base` HOT 25
- Add the `Setoid`al structure of a (free) `Monoid` on `List` HOT 1
- lib2.0 : `ℕᵇ `(binary) can be pure unlike `ℕ`. HOT 8
- To let or not to let HOT 3
- lemma for `map` for `⊆` as Subset
- Allow `.lagda` for library sources HOT 7
- `m+[n∸m]≡n` in the wrong section HOT 2
- Add bundled mono-/iso-{/epi-} morphisms
- Add bundles for lattice-like and module-like morphisms
- Document `variable` block indentation style HOT 5
- [DRY] what's the best way to `public`ly re-export properties/structure? HOT 5
- Use the Monoid structure of Endomorphisms to define powering HOT 1
- [DRY] More redundant `zero` fields in `Algebra.Structures`
- Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole HOT 5
- What's the 'right' notion of equality between functions? HOT 7
- [DRY] Refactor `Algebra.Solver.*Monoid` (or deprecate entirely?)
- Rename `WeaklyDecidable`? HOT 4
- Add `Algebra.Properties.IdempotentCommutativeMonoid`
- Naming of new functions `tail∘inits` and `tail∘tails` HOT 5
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda-stdlib.