feat(Algebra/GroupWithZero/Divisibility): add ad-hoc ring division #5930

Multramate · 2023-07-15T16:39:24Z

Mathlib/Algebra/GroupWithZero/Divisibility.lean

jcommelin · 2023-07-18T05:50:35Z

Mathlib/Algebra/GroupWithZero/Divisibility.lean

+Note that while this is in the `Ring` namespace for brevity, it requires the weaker assumption
+`MonoidWithZero M₀` instead of `Ring M₀`. -/
+noncomputable def divide (x y : M₀) : M₀ :=
+  if h : y ≠ 0 ∧ y ∣ x then h.right.choose else 0


Why do you require y to be non-zero? In a general ring, being non-zero isn't a very natural condition. You can still have plenty of nilpotents and/or zero-divisors.

Fair enough. In my head I'm working with only integral domains, but I just didn't want to impose this on the definition. Without this condition I wouldn't be able to prove divide_zero, which I think is something nice to have.

I mean somthing like epsX / epsX should still be well-defined, I guess?

but it'd also be nice to have zero_divide in general. I wonder if there's another design that allows this, maybe prioritising zero if it's possible

jcommelin · 2023-07-18T05:51:26Z

Mathlib/Algebra/GroupWithZero/Divisibility.lean

 import Mathlib.Algebra.Divisibility.Units

 /-!
 # Divisibility in groups with zero.

 Lemmas about divisibility in groups and monoids with zero.

+We also define `Ring.divide`, a globally defined function on any ring


Can you please elaborate on how/where you want to use this function? Would a DivInvMonoid work in your setting?

I'm looking at polynomial rings over (say) a commutative ring, which a priori don't have division/inversion but the notion of "cancelling out factors formally" still makes sense.

Shouldn't we treat division in polynomial rings the same way we treat it in Nat and Int? So we can just use the ordinary division symbol for some "truncated division" operation.

~~Yes I think we should, but I don't know how to best introduce this. Define Ring.divide as I have and then add notation?~~ I figured it out!

Isn't this what rem and quot are for? I don't remember what typeclass they are from...

There are EuclideanDomain.quotient and EuclideanDomain.remainder but my polynomial rings are not Euclidean.

Multramate · 2023-07-18T07:56:12Z

This seems to cause a whole lot of other overloading (?) issues - any ideas?

eric-wieser · 2023-07-18T15:20:25Z

Making this a div instance is a very bad idea IMO

Multramate · 2023-07-18T20:47:20Z

Yeah, I reverted it.

ericrbg

I think it's probably fine to leave more API building to when it's needed, Ring.divide (a + b) x is probably one of the obvious things but I have a feeling that's actually got stronger requirements than you'd hope.

ericrbg · 2023-08-08T21:09:55Z

Mathlib/Algebra/GroupWithZero/Divisibility.lean

+Note that while this is in the `Ring` namespace for brevity, it requires the weaker assumption
+`MonoidWithZero M₀` instead of `Ring M₀`. -/
+noncomputable def divide (x y : M₀) : M₀ :=
+  if h : y ≠ 0 ∧ y ∣ x then h.right.choose else 0


I mean somthing like epsX / epsX should still be well-defined, I guess?

Mathlib/Algebra/GroupWithZero/Divisibility.lean

ericrbg · 2023-08-08T21:51:54Z

Mathlib/Algebra/GroupWithZero/Divisibility.lean

+Note that while this is in the `Ring` namespace for brevity, it requires the weaker assumption
+`MonoidWithZero M₀` instead of `Ring M₀`. -/
+noncomputable def divide (x y : M₀) : M₀ :=
+  if h : y ≠ 0 ∧ y ∣ x then h.right.choose else 0


but it'd also be nice to have zero_divide in general. I wonder if there's another design that allows this, maybe prioritising zero if it's possible

ericrbg · 2023-08-08T22:51:58Z

Like epsilon in some ring where epsilon^2 = 0. I meant to reply to Johan's comments so maybe that's where the reply option is.

And I get that with this definition, zero_divide needs a domain - I wonder if we could tweak it so that it works everywhere

ocfnash · 2023-08-20T14:49:05Z

I'm not convinced that we should introduce such an arbitrary function for all MonoidWithZero. To be convinced I think I'd need to see:

evidence of significant benefit that this provides in some setting (e.g., your polynomial rings), and
evidence that no other solutions exist,

(and even then I might still be dubious).

I'm going to relabel this "awaiting-author" pending such evidence.

Multramate · 2023-08-20T15:12:55Z

I'm not convinced that we should introduce such an arbitrary function for all MonoidWithZero.

The only reason I'm defining it for a MonoidWithZero is to match Ring.inverse, which shares a similar name, but I really only need it for an integral domain as I mentioned above. I'm definitely open to restricting this.

evidence of significant benefit that this provides in some setting (e.g., your polynomial rings), and

I don't have my environment set up currently, but the gist of what I'm trying to do is as follows. I have a (strong odd/even) recursive function f : \N -> R[X] for a commutative ring R, such that when n is even, f n is defined to be some polynomial g (in terms of f (n / 2 - 1), etc) divided by f 2. It's impossible to extract out a factor of f 2 from g formally, and the only way I can think of is to use my current Ring.divide, and prove later that g is divisible by f 2.

evidence that no other solutions exist,

I don't know how to show this other than providing the example.

ocfnash · 2023-08-21T08:31:01Z

Your example sounds interesting but I would like to see a precise statement before it is admitted as evidence for a decision on this PR.

Can you provide such a statement (informally) or a reference with the precise details?

Multramate · 2023-08-21T11:52:27Z

Can you provide such a statement (informally) or a reference with the precise details?

I'm trying to define a characteristic two version of division polynomials, a slightly incorrect version of which can be found in Silverman's The Arithmetic of Elliptic Curves Exercise 3.7. The code would look something like: #6703

ericrbg · 2023-08-21T16:28:56Z

Ring.divide...chooseP

Here's an idea I had to use a choose Preferring (hence the name). All the theorems you proved are true (if not in more generality) and I didn't take much care to make the API nice yet, as it's just an idea. What do you think, David?

Multramate · 2023-08-21T18:21:13Z

Ring.divide...chooseP

Here's an idea I had to use a choose Preferring (hence the name). All the theorems you proved are true (if not in more generality) and I didn't take much care to make the API nice yet, as it's just an idea. What do you think, David?

I don't know enough of the design principle behind classical choice, so I can't say for sure this is a good idea, but I do not mind. I would think there's a lot of API to be developed though. It might also just be overkill, since my choice of having Ring was again just arbitrary.

kbuzzard · 2023-11-11T09:04:04Z

What the application David has in mind boils down to, is the theory of elliptic divisibility sequences https://en.wikipedia.org/wiki/Elliptic_divisibility_sequence . So the question really is whether one can formalise these without having to introduce some ad hoc ring division (and I suspect we can).

Multramate · 2023-11-20T20:39:21Z

I am closing this after discussions with Kevin (Thanks!) :)

Add Ring.divide

4ee67ce

Multramate added awaiting-review awaiting-CI labels Jul 15, 2023

Multramate changed the title ~~feat(Algebra/GroupWithZero/Divisibility): add Ring.divide~~ feat(Algebra/GroupWithZero/Divisibility): add ad-hoc ring division Jul 15, 2023

github-actions bot removed the awaiting-CI label Jul 15, 2023

Multramate added the t-algebra Algebra (groups, rings, fields, etc) label Jul 17, 2023

eric-wieser reviewed Jul 18, 2023

View reviewed changes

Mathlib/Algebra/GroupWithZero/Divisibility.lean Show resolved Hide resolved

jcommelin reviewed Jul 18, 2023

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 18, 2023

Add IsUnit.divide_eq_mul_inverse

eab1469

Multramate added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 18, 2023

Multramate force-pushed the Ring.divide branch from 34e0400 to eab1469 Compare July 18, 2023 20:47

Remove redundant assumption

50f07f5

ericrbg reviewed Aug 8, 2023

View reviewed changes

Replace NeZero with Nontrivial

7cd0323

ocfnash added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Aug 20, 2023

Multramate added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 20, 2023

ocfnash removed the awaiting-review label Aug 21, 2023

ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 21, 2023

Merge branch 'master' into Ring.divide

4dc082e

Multramate added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 21, 2023

bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24

kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:16

Multramate closed this Nov 20, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Algebra/GroupWithZero/Divisibility): add ad-hoc ring division #5930

feat(Algebra/GroupWithZero/Divisibility): add ad-hoc ring division #5930

Multramate commented Jul 15, 2023

jcommelin Jul 18, 2023

Multramate Jul 18, 2023

ericrbg Aug 8, 2023

ericrbg Aug 8, 2023

jcommelin Jul 18, 2023

Multramate Jul 18, 2023

jcommelin Jul 18, 2023

Multramate Jul 18, 2023 •

edited

Loading

eric-wieser Jul 18, 2023

Multramate Jul 18, 2023

Multramate commented Jul 18, 2023

eric-wieser commented Jul 18, 2023

Multramate commented Jul 18, 2023

ericrbg left a comment

ericrbg Aug 8, 2023

ericrbg Aug 8, 2023

ericrbg commented Aug 8, 2023

ocfnash commented Aug 20, 2023

Multramate commented Aug 20, 2023 •

edited

Loading

ocfnash commented Aug 21, 2023

Multramate commented Aug 21, 2023

ericrbg commented Aug 21, 2023

Multramate commented Aug 21, 2023 •

edited

Loading

kbuzzard commented Nov 11, 2023

Multramate commented Nov 20, 2023

feat(Algebra/GroupWithZero/Divisibility): add ad-hoc ring division #5930

feat(Algebra/GroupWithZero/Divisibility): add ad-hoc ring division #5930

Conversation

Multramate commented Jul 15, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Multramate Jul 18, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Multramate commented Jul 18, 2023

eric-wieser commented Jul 18, 2023

Multramate commented Jul 18, 2023

ericrbg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ericrbg commented Aug 8, 2023

ocfnash commented Aug 20, 2023

Multramate commented Aug 20, 2023 • edited Loading

ocfnash commented Aug 21, 2023

Multramate commented Aug 21, 2023

ericrbg commented Aug 21, 2023

Multramate commented Aug 21, 2023 • edited Loading

kbuzzard commented Nov 11, 2023

Multramate commented Nov 20, 2023

Multramate Jul 18, 2023 •

edited

Loading

Multramate commented Aug 20, 2023 •

edited

Loading

Multramate commented Aug 21, 2023 •

edited

Loading