Zulip Chat Archive

Stream: general

Topic: Readability (was : is_affine_open dot chaos)

Kevin Buzzard (Sep 21 2022 at 08:59):

In maths, "the natural map Spec(OX(U))X\mathrm{Spec}(\mathcal{O}_X(U))\to X, for UU an affine open subset of the scheme XX". In Lean:

is_affine_open.from_Spec :
  Π {X : Scheme} {U : topological_space.opens (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)},
    is_affine_open U 
         (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) 

As well, as the X.a.b.c.d.e we have all these ops! Can't we just have contravariant functors? I guess this is an independent issue, but I'm just thinking generally about readability. Can we do better?

Kevin Buzzard (Sep 21 2022 at 09:00):

darn it, sorry I broke the thread. Can a mod glue?

Andrew Yang (Sep 21 2022 at 09:07):

To be fair, the situation would be better if appropriate namespaces are open. It looks like
Π {X : Scheme} {U : opens X.carrier} (hU : is_affine_open U) : Scheme.Spec.obj (op $ X.presheaf.obj $ op U) ⟶ X
in the source code, and I would say that the readability of this is not that bad.

In the info view however, X.presheaf gets expanded into X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf, so this is still a problem that needs fixing.

As for the readability of the docs, I think this is a separate issue that I have no idea how to fix.

Andrew Yang (Sep 21 2022 at 09:10):

If there is the notation Γ(X, U) for X.presheaf.obj $ op U, we could potentially shorten it into
Π {X : Scheme} {U : opens X.carrier} (hU : is_affine_open U) : Spec.obj (op Γ(X, U)) ⟶ X
with open Scheme

Andrew Yang (Sep 21 2022 at 09:24):

Let me also mention some examples that are already ugly in code.
For x f : X.presheaf.obj (op U), to restrict x onto D(f) we need to write X.presheaf.map (hom_of_le $ X.basic_open_subset f : X.basic_open f ⟶ U).op x. #16088 is an attempt fixing it, but I'm not sure if it is satisfactory.

Andrew Yang (Sep 21 2022 at 09:31):

There is also discussion on giving functor a has_coe_to_fn instance here. Though I understand that there will be difficulties providing them for both objects and morphisms, I think it is perfectly reasonable to at least provide one on the object level, and I think this is also what's done in LTE examples now?

Kevin Buzzard (Sep 21 2022 at 14:48):

I've been reading algebraic geometry today and seeing how far we've gone. Apart from the notation, which makes me occasionally sad, it looks like we have a really robust foundation nowadays. Thanks to you guys! I'm trying to figure out how to sell it, that was my frustration with the notation.

Kevin Buzzard (Sep 21 2022 at 14:48):

By "sell it" I mean "teach an 8 hour course on it in November" :-)

Adam Topaz (Sep 21 2022 at 14:55):

I heard of some fancy new dot notation tricks also in Lean3 from @Kyle Miller

Adam Topaz (Sep 21 2022 at 14:56):

That should help at leat a little bit

Kyle Miller (Sep 21 2022 at 15:47):

@Kevin Buzzard Last I checked, the Lean 4 pretty printer would still display X.carrier as X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier too.

The backported Lean 4 feature that might be helpful is that if you've got a dot-notation-friendly function foo in the PresheafedSpace namespace then you can write X.foo rather than X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.foo.

Kyle Miller (Sep 21 2022 at 15:49):

I was going to at some point take a look at adding an option to the pretty printer to more aggressively reverse dot notation, so that the first thing would actually print as X.carrier.

Johan Commelin (Sep 21 2022 at 19:39):

That would be really sweet!

Last updated: Aug 03 2023 at 10:10 UTC