ag in ml4

Stream: mathlib4

[Johan Commelin]

I think we need to do some debugging to make algebraic geometry in mathlib4 work (at least as smooth) as in mathlib3.

feat: port AlgebraicGeometry.Spec !4#4599

is porting the prime spectrum. Unfortunately several proofs are becoming longer for annoying reasons. A similar thing happened for ringed spaces in

https://github.com/leanprover-community/mathlib4/pull/4499/files/264ce3ee71096ffceffeb9c72429fc1536588227..60ec18cffc14d5c5a1608cb38ce1c3f5adc579ee

I fear that this isn't scaling.

[Jujian Zhang]

So as an experiment, I changed ConcreteCategory's way of coercing function to FunLike, it definitely makes rewriting comp_apply easier without making other proof much longer (mostly add comp_apply, id_apply to some simp call).

[Jujian Zhang]

dsimp still behaves very differently from its Lean3 counterpart which results in several long proofs. Less change are now used, most change are necessary for mostly because ↑f can either come from (forget _).map or FunLike.coe. Changing ConcreteCategory.hasCoeToFun to FunLike can solve this part.

[Jujian Zhang]

I have also fixed all change in RingedSpace.lean and some (but not all) explicit typing using this approach. The explicit typing was partly due to germ_res_apply generated by elementwise is wrong, after manually adding a correct germ_res_apply, some explicit typing can be avoided.

[Scott Morrison]

Which branch is this on?

[Jujian Zhang]

port/AlgebraicGeometry.Spec

[Jujian Zhang]

https://github.com/leanprover-community/mathlib4/pull/4599

[Jujian Zhang]

AlgebraicGeometry.Spec.sheafedSpaceMap_comp in Spec.lean is a good example where dsimp is not very good compared to Lean3

[Jujian Zhang]

Arguably, FunLike is better suited for ConcreteCategory because it uses the fact that the forgetful functor is faithful

[Yury G. Kudryashov]

BTW, if you use FunLike for coercion to function, then different ways to coerce (e.g., a generic construction vs existing instance for a bundled hom) are hidden behind defeq instances

[Johan Commelin]

We made some progress on AG in ml4, but current PRs still have quite a lot of porting notes. After some discussion with @Scott Morrison I suggest that we stack several porting PRs on top of each other. That will give us a bigger picture to consider whether the current (smallish) issues blow up to bigger problems, or whether the small tweaks stay small.

So... porters of algebraic geometry, unite!

[Scott Morrison]

In particular, I think the hope is that we may be able to get to "the end" of algebraic geometry in mathlib3, and then decide that even though we are not entirely happy with the individual ported files, in aggregate we can merge them all and decide what to do on the mathlib4 side.

The porting notes Johan is talking about are largely of the form "simp/rw doesn't work, now we need erw". I think we can hope that being more careful about definitional equality (and dsimp'ing) in the implicit arguments will resolve some of these. But I suspect achieving this is more of a refactoring project than a porting project, and it will be best to just getting everything over onto the mathlib4 side, so we can start that process. There's no point attempting to refactor on the mathlib3 side, because the behaviour of simp/rw have diverged so far (particularly in the presence of badly-dsimped implicit arguments) that we wouldn't learn anything about fixing things on the mathlib4 side by doing so.

[Scott Morrison]

For reference, this is what remains to be done in AG: https://tqft.net/mathlib4/latest/algebraic_geometry.morphisms.quasi_separated.pdf

[Johan Commelin]

The other option would be that we just merge them as is... and make refactor PRs if follow-up porting PRs get stuck

[Johan Commelin]

@Joël Riou @Jujian Zhang what do you think?

[Jujian Zhang]

Scott Morrison said:

In particular, I think the hope is that we may be able to get to "the end" of algebraic geometry in mathlib3, and then decide that even though we are not entirely happy with the individual ported files, in aggregate we can merge them all and decide what to do on the mathlib4 side.

The porting notes Johan is talking about are largely of the form "simp/rw doesn't work, now we need erw". I think we can hope that being more careful about definitional equality (and dsimp'ing) in the implicit arguments will resolve some of these. But I suspect achieving this is more of a refactoring project than a porting project, and it will be best to just getting everything over onto the mathlib4 side, so we can start that process. There's no point attempting to refactor on the mathlib3 side, because the behaviour of simp/rw have diverged so far (particularly in the presence of badly-dsimped implicit arguments) that we wouldn't learn anything about fixing things on the mathlib4 side by doing so.

by "aggregate", does it mean open one PR to include all dependencies including and up to QuasiSeparated.lean

[Johan Commelin]

I think we would have one PR per file. But once we see that everything works reasonably well in Lean 4, we just merge all of them on the same day.

[Jujian Zhang]

Ah, that makes sense

[Jujian Zhang]

I am currently working on PresheafedSpace.Gluing. Can maintains still comment or label the individual PRs as "pseudo-ready-to-merge" or something like that so that porters confidently know that they can continue onto next file

[Johan Commelin]

The other option is that we actually just merge the PR. But with the asterisk (*) that there's a small chance that we might need to do some refactoring if things get out of hand in a future file.

[Jujian Zhang]

I guess if we just merge the PR and rework them on the go, there is the advantage of being able to get cache. Compared to aggregate them all together, say for some reason we need to change a deep file, then it takes long to recompile. Not sure if this makes sense

[Johan Commelin]

Since the total amount of files involved is rather small (roughly 10) I'm starting to lean towards just merging and moving forward

[Johan Commelin]

Ok, let's give this a shot

[Johan Commelin]

algebraic_geometry.gluing #5446

has one annoying error left.