open CategoryTheory

Stream: maths

[Antoine Chambert-Loir]

What does open CategoryTheorydo?
(Apparently, it replaces Ideal R by some ↑(ModuleCat.of R { x // x ∈ S }), and I would like to understand how that happens! I did not succeed by searching in the docs…)
More generally, is there a comprehensive list of all the open … ? (I could not even understand how what happens when you open Classical actually happens)

[Yury G. Kudryashov]

Do you have a #mwe?

[Yury G. Kudryashov]

Possibly, it adds some Coe* scoped instance.

[Antoine Chambert-Loir]

No, I don't have a #mwe… I was adding a DefinableEq (R[X])instance to mathlib, as in #5942, but that failed soon, because Lean cannot reconcile that instance with the Classical one. So I started playing with that, removing open Classical. At some point, in the theory of Euclidean rings, I added a \all (S : Ideal R), Decidable (Nontrivial S), but then that failed again in the proof of docs4#AddCommGroupCat.injective_of_divisible…

[Antoine Chambert-Loir]

Indeed, there, S : Ideal ℤ is changed to ↑(ModuleCat.of ℤ { x // x ∈ S }) and I don't understand how…

[Antoine Chambert-Loir]

(The initial goal was to make Lean minimally capable of computing Sturm sequences of polynomials with rational coefficients…)

[Antoine Chambert-Loir]

(I made a mistake in posting here, can someone can move this thread to #mathlib4 ?)

[Adam Topaz]

It seems like some coercion triggering. Probably the one from ideals to additive groups, to Z-modules.

[Yury G. Kudryashov]

IMHO, we should have types with different representations of polynomials that work better for computations.

[Yury G. Kudryashov]

And theorems saying that some operations on these types agree with those on R[X].

[Yury G. Kudryashov]

Then tactics should move input polynomials to one of those other types, compute there, then use one of those theorems to move back.

[Yury G. Kudryashov]

In fact, we may want to have a typeclass for that so that different implementations can share some code.

[Kevin Buzzard]

Antoine, remember that polynomials are noncomputable for a reason (it was hard to work with them). It would be interesting to see whether we can make them computable without too much pain but it might be easier to write a new type. One answer to your question is that Lean 4 open X is the same as lean 3 open X + open_locale X

[Antoine Chambert-Loir]

That I have understood. But docs4#MvPolynomial have a DecidableEq instance, and we need the analogue for Polynomial if we want to avoid a plain open classical ... So I tried to add it and things went wrong.
(I really find annoying that Lean can't presently compute a gcd of polynomials with rational coefficients…)

[Yury G. Kudryashov]

Do you mean DecidableEq?

[Antoine Chambert-Loir]

Yes

[Antoine Chambert-Loir]

Sorry for the typo (I fixed it up above)

[Eric Wieser]

@Antoine Chambert-Loir, I think hoping for it to compute GCDs is (at least compatively) rather silly when it can't even compute X + 1 right now

[Eric Wieser]

Having said that, I don't think your instance is unreasonable, and is probably indicative of a bad lemma somewher

[Eric Wieser]

I pushed some changes to your PR; feel free to discard them if you don't want them

[Antoine Chambert-Loir]

@Eric Wieser , thanks for the "good cop/bad cop" language, “silly” in one sentence, “not unreasonable” in the next one… But above all, thank you for these changes, they work better than the one I had started to write — but not pushed yet.