Readability (was : is_affine_open dot chaos)

Stream: general

[Kevin Buzzard]

In maths, "the natural map $\mathrm{Spec}(\mathcal{O}_X(U))\to X$, for $U$ an affine open subset of the scheme $X$". 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 →
    (Scheme.Spec.obj
         (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) ⟶
       X)

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]

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

[Andrew Yang]

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]

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]

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]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

That should help at leat a little bit

[Kyle Miller]

@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]

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]

That would be really sweet!