Fix comparison for divisors of curves (and FormalSum commutativity)

[vincentmacri]

Fixes #37966.

📝 Checklist

• The title is concise and informative.
• The description explains in detail what this PR is about.
• I have linked a relevant issue or discussion.
• I have created tests covering the changes.
• I have updated the documentation and checked the documentation preview.

[tscrim]

Thank you for submitting the PR.

First, you should not be changing the .gitignore.

Second, as far as I can tell, this is just reimplementing one part of the FormalSum comparison with a more complicated check (more transient objects and subtraction). The underlying issue is the comparison that is happening with FormalSum is not commutative, but its implementation is (effectively) commutative. In FormalSum.reduce(), it should sort the input:

try:
    self._data = [(c, x) for (x, c) in sorted(new.items()) if c]
except (TypeError, ValueError):
    self._data = [(c, x) for (x, c) in sorted(new.items(), key=str) if c]

[vincentmacri]

First, you should not be changing the .gitignore.

The change to the .gitignore was some auto-generated files I think from running ./bootstrap (I followed these instructions: https://doc.sagemath.org/html/en/installation/conda.html#using-conda-to-provide-all-dependencies-for-the-sage-library). I'll undo that though if it's out of scope (let me know if I should submit it as a separate PR).

Second, as far as I can tell, this is just reimplementing one part of the FormalSum comparison with a more complicated check (more transient objects and subtraction). The underlying issue is the comparison that is happening with FormalSum is not commutative, but its implementation is (effectively) commutative. In FormalSum.reduce(), it should sort the input:

try:
    self._data = [(c, x) for (x, c) in sorted(new.items()) if c]
except (TypeError, ValueError):
    self._data = [(c, x) for (x, c) in sorted(new.items(), key=str) if c]

I looked at FormalSum, and that comparison is element-wise. In particular, comparing the formal sums 3 + 2 > 2 + 3 gives True, and if I implemented this behaviour in FormalSum then we would have both 3 + 2 == 2 + 3 and 3 + 2 > 2 + 3, and I didn't think both of these should evaluate to True.

You're right that there is an issue where FormalSum isn't commutative. I'm not familiar enough with how FormalSum is used in Sage to know what to fix there.

Either way, I think that overriding the FormalSum implementation is needed anyway, because the divisors of a curve are a group, and shouldn't be treated exactly like formal sums. For instance, if two different curves happen to have the same point on both of them, as a group it doesn't make sense to say that those points are equal. That's what the self.parent() == other.parent() check is for in my PR. With formal sums though, these are treated as equal right now.

Here's an example of what I mean, which I think is a bug with comparison of divisors:

C = EllipticCurve([2, 1])
R = C(1, 2)

E = EllipticCurve([1, 2])
Q = E(1, 2)

R == Q # Evaluates to False, which is correct

E.divisor(Q) == C.divisor(R) # Evaluates to True, which I think is incorrect

[vincentmacri]

Some additional code showing that E.divisor(Q) == C.divisor(R) should not be True:

C = EllipticCurve([2, 1])
R = C(1, 2)

E = EllipticCurve([1, 2])
Q = E(1, 2)

Qd = E.divisor(Q)
Rd = C.divisor(R)

Qd == Rd # Evaluates to True, which as I said above I think is incorrect

Qd.support() == Rd.support() # Evaluates to False, which I think is correct but doesn't make sense if Qd == Rd is evaluating to True.

[tscrim]

Yes, the changes are out of scope. It's (very) bad practice to hide such changes in unrelated PRs. You can just remove those files yourself anyways; bootstrap is only run sparingly.

Okay, the FormalSum implementation is separate (but definitely an issue!). Running through your example I get:

sage: Rd.support()
[(1 : 2 : 1)]
sage: Qd.support()
[(1 : 2 : 1)]
sage: Rd == Qd
True
sage: Rd.support() == Qd.support()
True

The formal sum does also compare by parents. The subtlety is that there is a coercion map:

sage: Rd.parent().has_coerce_map_from(Qd.parent())
True

So the comparison is done after coercing both into a common parent (here, that is Rd.parent()). However, there should not be a coercion map. The parent FormalSums just does the "correct" thing of just comparing base rings for coercion, since that is the only input it knows about. However, the actual divisor group class should not allow coercions when there is not a coercion from the defining schemes. Hence, I think the correct fix would be to implement in sage.schemes.generic.divisor_group.DivisorGroup_generic

def _coerce_map_from_(self, other):
    return (isinstance(other, type(self))
            and self._scheme == other._scheme
            and super()._coerce_map_from_(other))

[vincentmacri]

Okay, the FormalSum implementation is separate (but definitely an issue!). Running through your example I get:

sage: Rd.support()
[(1 : 2 : 1)]
sage: Qd.support()
[(1 : 2 : 1)]
sage: Rd == Qd
True
sage: Rd.support() == Qd.support()
True

Strange, I get Rd.support() == Qd.support() is False both in 10.3 and on the develop branch...

Alternatively, I could do a larger rewrite of the Divisor_generic class using the same idea @mkoeppe suggested here: #37705 (comment)

That would involve making Divisor_generic no longer inherit from FormalSum, and instead have Divisor_generic have a FormalSum as a property. Then we could do stuff like not allow adding divisors that live in two different schemes together. I'd then have to implement __add__, __eq__, etc in Divisor_generic.

[tscrim]

No, there's no reason for the element class to not inherit from FormalSum; it is a formal sum and you would quickly find you are duplicating or redirecting everything there. Even if you did that, you would still have a problem (the proper thing is to implement _richcmp_ and allow equality via coercion). The issue is in the coercion of the parents, and it is essentially a 1 line fix as I said.

[vincentmacri]

To make sure I'm understanding before I go and implement your suggestions, you're suggesting that I make the following 3 changes?

1. Get rid of the __eq__ implementation I added in Divisor_generic in favour of the next two points.
2. Change reduce in FormalSum to give some sort of "canonical representative" by sorting the terms. This would fix the issue with comparing not respecting commutativity in Divisor_generic (and all subclasses of FormalSum for that matter)
3. Implement _coerce_map_from_ in Divisor_generic to handle correctly comparing divisors that come from different schemes.

Is that correct?

[tscrim]

Yes, that's correct. Either 2 or the richcmp should convert the data to a dict for comparisons. Although I think the normalization of the representative is better for doctors output.

[github-actions]

Documentation preview for this PR (built with commit ce4b05c; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

[vincentmacri]

Okay, I made those changes.

The build will fail because this test is failing:

sage: C = EllipticCurve([2, 1])
sage: R = C(1, 2)
sage: E = EllipticCurve([1, 2])
sage: Q = E(1, 2)
sage: Qd = E.divisor(Q)
sage: Rd = C.divisor(R)
sage: Qd == Rd
False

For some reason Qd == Rd is giving true, despite me having a test that _coerce_map_from_ gives False on those inputs.

Any ideas?

[tscrim]

The _coerce_map_from_ needs to be implemented in the parent class (DivisorGroup_generic in sage.schemes.generic.divisor_group), not the element class (Divisor_generic).

Also, I don't think it is worthwhile for FormalSum.support to change its output type. If you want to change its output, then a frozenset is best I think. There already is an implicit requirement the indices are hashable.

[vincentmacri]

Hopefully that fixes everything. I think this is a bit cleaner because now tests aren't reliant on the arbitrary string ordering I had for comparison purposes. Instead terms are in the order the you enter them in, which makes sense.

I didn't cache the results of sorting the FormalSum data, so the sorting will be computed on each FormalSum comparison. Let me know if you'd prefer I cache the results of the sorted data in __init__ (or elsewhere).

[tscrim]

I feel like not normalizing the print representation is a small step backwards. It also means that we have to sort on every comparison (instead of just when calling reduce()). Although I don't know how these are used, so I don't know which could affect speed more. Well, I understand making a minimal change. I just want to mention that the fact that some are genuinely different might be exposing bugs. That might warrant further investigation later.

[vincentmacri]

I feel like not normalizing the print representation is a small step backwards. It also means that we have to sort on every comparison (instead of just when calling reduce()). Although I don't know how these are used, so I don't know which could affect speed more. Well, I understand making a minimal change. I just want to mention that the fact that some are genuinely different might be exposing bugs. That might warrant further investigation later.

I agree and I think FormalSum in general could use some significant changes. But I think what I've done is the best way to fix #37966 without a major rewrite. I could cache the result of sorting in its own variable in __init__, but then that would increase memory usage which is maybe worse than sorting the lists, since sorting is a fairly fast operation.

[tscrim]

I wouldn't call the sorting as part of the reduce a major rewrite, but it can wait for now. Just one more little thing to do.

[vincentmacri]

The commit I just pushed updated the warning in FormalSum for setting reduce to False. With the change to sorting in richcmp, there shouldn't be issued comparing sums with different orders, just with different cancellations.

The build from yesterday failed. For test-new, the following error occurred: fatal: not a git repository: /new/.git/worktrees/worktree-image. I'm not sure what would cause this.

[tscrim]

Yea, our CI testing is currently massively broken...

[tscrim]

Okay, let's get this in.