Open DanGrayson opened 3 years ago
Open question: should commutativity be a property, rather than being recorded in the type?
What does Ordered
mean here? Are there any examples of non-ordered monoids in M2? How about Free
?
I propose following the algebraic hierarchy of an existing theorem prover, say Lean, to allow for a possible interface in the future. Based on these notes, maybe we can start with something like this:
OrderedMonoid
: associative multiplication with 1OrderedGroup
: associative, commutative addition with 0 and with additive inverseOrderedRing
: OrderedMonoid
and OrderedGroup
with distributivityOrderedCRing
: OrderedRing
with commutativityOrderedDRing
: OrderedRing
with multiplicative inverse (a division ring)OrderedField
: OrderedCRing
with commutativityThese are just the ones that seem to be useful in M2. We can of course separate each to additive and multiplicative versions, with and without canceling or commutativity.
If everything is Ordered, we might as well drop the Ordered
prefix.
A larger undertaking would be to slowly implement a "trait" system (or Concepts in C++ language) as opposed to a "type" system to make it easier to mix and match the traits above.
@DanGrayson I plan on going ahead with this if there isn't anything else to add.
Each polynomial ring comes with a degrees monoid, which harbors the degrees of the monomials. I seem to recall hearing that sometimes it's useful to have degrees monoids with torson (@ggsmith @mikestillman), and degrees monoids don't have to be ordered.
I don't like the brevity of OrderedCRing and OrderedDRing, and as for OrderedRing, I think we don't have any ordered rings. Similarly for OrderedField -- why bother with that?
As for dropping the "Ordered" prefix, that would be fine, as long as "OrderedMonoid" is retained as an ancestor.
Also, what's the point of OrderedGroup in our context?
Allowing the grading group of a polynomial ring to have torsion would be useful for some toric computations.
Allowing the grading group of a polynomial ring to have torsion would be useful for some toric computations.
My goal, roughly, is to make core functionalities more toric variety friendly, and working with Picard groups with torsion is definitely on my mind.
I don't like the brevity of OrderedCRing and OrderedDRing
The short form comes from the category CRing. I couldn't find a source that refers to DRing
for division rings; we could call them SkewField
instead.
as for OrderedRing, I think we don't have any ordered rings
I intended the definition of OrderedMonoid
to match what @mikestillman and @moorewf call
a FreeMonoid
and OrderedRing
to match FreeAlgebra
. Then OrderedCRing
would be the class of commutative rings that are ubiquitous in M2.
The benefit of having OrderedCRing
inherit from OrderedRing
(rather than NCRing
inherit from a commutative-by-default Ring
) is that a lot of functions work identically regardless of commutativity.
Similarly for OrderedField -- why bother with that?
Dealing with fields in M2 is kinda strange right now. Having a proper type for fields would simplify things like isField
and toField
(and their respective bugs).
Also, what's the point of OrderedGroup in our context?
Dealing with groups is also very lacking in M2. The degreesMonoid
, for instance, is literally a group. Packages like InvariantRings and GKMVarieties have implemented a lot of useful things with group actions, and yet there's no shared type for a group or group action to support commutative algebra involving those objects.
I don't like the brevity of OrderedCRing and OrderedDRing
The short form comes from the category CRing. I couldn't find a source that refers to
DRing
for division rings; we could call themSkewField
instead.
CRing is not a good name -- it's too terse. Why change what we have?
as for OrderedRing, I think we don't have any ordered rings
I intended the definition of
OrderedMonoid
to match what @mikestillman and @moorewf call aFreeMonoid
andOrderedRing
to matchFreeAlgebra
. ThenOrderedCRing
would be the class of commutative rings that are ubiquitous in M2.
Those rings aren't ordered.
The benefit of having
OrderedCRing
inherit fromOrderedRing
(rather thanNCRing
inherit from a commutative-by-defaultRing
) is that a lot of functions work identically regardless of commutativity.
Yes, commutative rings should be a subclass of rings.
Similarly for OrderedField -- why bother with that?
Dealing with fields in M2 is kinda strange right now. Having a proper type for fields would simplify things like
isField
andtoField
(and their respective bugs).
Those fields aren't ordered.
Also, what's the point of OrderedGroup in our context?
Dealing with groups is also very lacking in M2. The
degreesMonoid
, for instance, is literally a group. Packages like InvariantRings and GKMVarieties have implemented a lot of useful things with group actions, and yet there's no shared type for a group or group action to support commutative algebra involving those objects.
Those groups aren't ordered, and they aren't ever used as the monoid of monomials for a monoid algebra. It's probably premature to invent a type for groups, with no application in mind.
What do you mean by "aren't ordered"? Can you give an example of something that is not-ordered in M2?
i1 : S = degreesMonoid{1,2,3};
i2 : T_0 < T_1
o2 = false
i3 : T_1 < T_0
o3 = true
i4 : T_1*T_2^-1 < T_0
o4 = false
i5 : T_0 < T_1*T_2^-1
o5 = true
Without an order, how can M2 even print anything?
The (mathematical) orderings of interest are all on monoids, which serve as the monoids of monomials for our polynomial rings. The polynomial rings are not ordered, especially since finite fields are never ordered rings. For example, in this ring:
i11 : F = ZZ/3
o11 = F
i15 : 0_F ? 1_F
o15 = >
o15 : Keyword
i17 : 0_F + 2_F ? 1_F + 2_F
o17 = <
o17 : Keyword
I think everywhere I mentioned Ordered
I was referring to monomial orders, but you're right that I should drop Ordered
from OrderedGroup
because the additive group isn't ordered. You mentioned there are non-ordered monoids, is there an example of that?
No, we don't have non-ordered monoids. Eventually, though, if we have monoids with torsion, they won't be ordered.
Allowing the grading group of a polynomial ring to have torsion would be useful for some toric computations.
Such a grading monoid could probably be presented as a finitely generated free monoid modulo a (finitely generated) submonoid. Is that right? ( @ggsmith )
Re: "Dealing with groups is also very lacking in M2. The degreesMonoid, for instance, is literally a group."
Yes, but being a group can be considered as a property of a monoid. Why is it that for monomial ideals, which are currently a separate type of object, you propose removing their type and re-implementing them simply as ideals with the property of being monomial, whereas here, for monoids, you wish to create a separate type for monoids that have the property of being a group? That seems inconsistent.
Such a grading monoid could probably be presented as a finitely generated free monoid modulo a (finitely generated) submonoid. Is that right? ( @ggsmith )
Yes—I believe that gradings by finitely generated abelian groups would cover all toric applications.
GeneralOrderedMonoid
should be changed toOrderedFreeCommutativeMonoid
, and then we could add a new type,OrderedFreeMonoid
to support the recent work by Mike and Frank on associative algebras. Both types would be subtypes ofOrderedMonoid
.@mikestillman