decidable equality on ideals

Stream: mathlib4

[Kevin Buzzard]

Searching for DecidableEq (Ideal in mathlib gives 18 hits. When I'm working with e.g. finite sums, or more generally finsets or fintypes, I expect to see the occasional Decidable hypothesis, because finsets are constructive. But I would not expect to see decidable stuff showing up in MSc level commutative algebra.

The reason this came to my attention was this instance

instance [DecidableRel ((· ≤ ·) : Ideal A → Ideal A → Prop)] : LinearOrder (Ideal A) :=
  have := decidableEqOfDecidableLE (α := Ideal A)
  have := decidableLTOfDecidableLE (α := Ideal A)
  Lattice.toLinearOrder (Ideal A)

which came up in a discussion about typeclass inference going crazy on a high SynthPendingDepth setting. The reason it goes crazy is explained here. Sebastien suggested changing the instance to be fully classical:

instance : LinearOrder (Ideal A) := by
  classical
  exact Lattice.toLinearOrder (Ideal A)

and this solves the problem. But it raises the question about whether ideals, like polynomials, should be a "fully classical" theory. Perhaps evidence that this is a good idea is the following:

import Mathlib

#synth DecidableEq (Ideal ℕ) -- fails
#synth DecidableEq (Ideal ℤ) -- fails
#synth DecidableEq (Ideal ℚ) -- fails

which indicates that up until now nobody attempted to write these instances. If we globally make = and <= on ideals decidable with a classical instance then (a) we'll be able to remove these weird decidable hypotheses in commutative algebra files (which are confusing to mathematicians) and (b) we'll be able to fix the timeout which occurs in mathlib when synthpendingdepth is set to 50 without causing diamonds. Are there any arguments against this?

[Eric Wieser]

@loogle DecidableEq (Ideal _)

[loogle]

:search: Ideal.equivFinTwo, count_le_of_ideal_ge, and 15 more

[Eric Wieser]

@loogle |- DecidableEq (Ideal _)

[loogle]

:shrug: nothing found

[Eric Wieser]

So indeed, this argument is everywhere but it is instantiated never

[Eric Wieser]

Your suggestion sounds good to me

[Eric Wieser]

Kevin Buzzard said:

should be a "fully classical" theory

I think this is the wrong way to think about this; Real isn't "fully classical", but we still create classical instances here and there. I think the more precise rule is "if a Decidable instance is never constructed computably, then construct it classically to save everyone the trouble downstream"

[David Wärn]

Indeed you can only prove DecidableEq (Ideal R) constructively if R is trivial. Otherwise, every p : Prop determines an ideal in R containing x : R if p holds or x = 0. If you can tell whether this ideal is all of R then you can decide if p is false or not false. The best you can hope for constructively is decidable equality of finitely generated ideals.

[Jz Pan]

I think if R is a CommRing not a field, then DecidableEq (Ideal R) has prerequisites that we should have DecidableEq R, the ideal in question should have DecidablePred Membership.mem, and R must satisfies very good conditions, for example, a computable Euclidean algorithm, or the ring of integers of a number field (even in this case the DecidableEq algorithm for ideals becomes very complicated, as in computational number theory).

[Edward van de Meent]

even then, i suspect it's higly likely that you need Fintype R, right?

[Jz Pan]

Edward van de Meent said:

even then, i suspect it's higly likely that you need Fintype R, right?

Oh yes, even when the ideal has DecidablePred Membership.mem, the DecidableEq (Ideal ℤ) is not possible, because although you can check if n belongs to the ideal for each n, but you cannot check if there exists a non-zero n in the ideal in finite number of steps...

[Edward van de Meent]

i think a strict requirement is a countable number of ideals?

[Jz Pan]

DecidableEq R + Fintype R + DecidablePred (· ∈ I) is the best I can come up with.

[Edward van de Meent]

it might be possible in a slightly better generality if all ideals are finitely generated, and computably so, i.e. you can compute a g:Finset R of generators, such that I = Ideal.closure g I = Ideal.span g.

[Damiano Testa]

If R is a field and membership is decidable, aren't you then also able to test for equality of ideals? The only interesting question is whether an ideal contains 1 or not.

[Edward van de Meent]

no? for integers, i imagine you'd need to check all primes in order to know what ideal you're looking at? right, field

[Edward van de Meent]

(i might need to dust off my algebra knowledge)

[Jz Pan]

I can define an ideal of ℤ whose n ∈ I is "0 ∈ I; if n is not zero, find the smallest positive integer i ≤ |n| such that there exists a zero of Riemann zeta function in the critical strip whose real part is not 1/2, if such i exists, then n ∈ I if and only if n is a multiple of i, otherwise n is not in I". This is indeed DecidablePred (but very far from implemented in Lean). But to decide whether I = 0 it's equivalent to prove or disprove Riemann hypothesis.

[Edward van de Meent]

indeed in the case of a field, every ideal is either Ideal.span 0 or Ideal.span {1}

[Damiano Testa]

You might get a little improvement for rings that only have finitely many ideals and for which you know how to test what ideal is what. For instance, a finite product of fields is probably ok, since you can test the "0-1 sequences" for membership.

[Edward van de Meent]

so indeed the question is one of finding a finite set of generators for any ideal? since then, to decide I = J, it suffices to decide gen(I) <= J and gen(J) <= I. in the case of a product, you can decompose the ideal by deciding membership of (a,0) and (0,b) (since if (a,b) is in the ideal, so is (1,0) *(a,b) etc), decide the generators of those ideals, take the cartesian product of the sets of generators, (verify they are members of the ideal,) and do the above procedure (or even do the above procedure on the respective projections? that might be more efficient).

[Eric Wieser]

DecidablePred (· ∈ I)

But in the context of DecidableEq (Ideal R), this requires that all ideals satisfy this, which amounts to requiring that all propositions are decidable via the ideal if p then \top else \bot for arbitrary p.

[Edward van de Meent]

you have that issue with any kind of DecidableEq on a non-trivial type

[Edward van de Meent]

if you're writing down if p then foo else bar, you are already either using classical or Decidable p

[Edward van de Meent]

(it's how if works)

[Eric Wieser]

Ok, let's say I write down {x | p} ∪ {0} as my carrier for an ideal then. I didn't use classical or decidable to define that, but you can't decide members, and so ∀ I : Ideal R, DecidablePred (· ∈ I) is impossible to construct for nontrivial R

[Eric Wieser]

I think your claim here reduces to "you have that issue with anything built upon Set", which is of course precisely the issue!

[Edward van de Meent]

so then ideally, you'd want to somehow express "every ideal is equal to one in which membership is decidable", and "you can decide equality for all <ideal, decidable membership> tuples"

[Eric Wieser]

every ideal is equal to one in which membership is decidable

If you can't know which one, then you don't have an algorithm available. If you can tell which one, then you could have just implemented the instance in the first place.

[Eric Wieser]

As a simple test, try proving DecidableEq (Set Bool)

[Edward van de Meent]

i guess you don't get DecidableEq but you do get DecidablePred (. \in I) -> DecidablePred (. \in J) -> Decidable (I = J)

[Jz Pan]

DecidableEq ((I : Ideal R) × DecidablePred (· ∈ I)) if R satisfies good condition, here I can't write subtype since DecidablePred contains data.