defeq problems in `Scheme`

Stream: mathlib4

[Kim Morrison]

I'm hoping to nerd-snipe someone into taking a look at this. :-)

There are lots of erw problems in schemes in Lean, e.g. in docs#AlgebraicGeometry.Scheme.inv_appTop. Poking around with erw?, check_compositions, and the new check_equalities in #22366 leads me to believe two things:

• docs#Opens.map_top is a bad dsimp lemma, because it very often rewrites in implicit arguments and then later blocks syntactic rewriting: can we just replace its proof by id rfl, to prevent dsimp using it? What are the consequences?
• The definition of docs#AlgebraicGeometry.Scheme.appTop is "wrong", and should be

abbrev appTop : Γ(Y, ⊤) ⟶ Γ(X, ⊤) :=
  f.app ⊤ ≫ X.presheaf.map (eqToHom (Opens.map_top _).symm).op

Can we repair the rest of the file after making this change? Does it reduce the need for erw?

[Patrick Massot]

@Kevin Buzzard it’s time to redo schemes, just like in the good old days!

[Kevin Buzzard]

I'll see if I can get some people at Xena interested in looking at this today. I feel like schemes has moved on a lot since I last looked at it :-)

[Christian Merten]

Should we more generally lint against reducible definitions that are not "type correct at reducible transparency"?

[Andrew Yang]

appTop should be appLE ⊤ ⊤ sorry (which is probably reducibly equal to your suggestion).
docs#AlgebraicGeometry.Scheme.comp_app ((f ≫ g).app U = g.app U ≫ f.app (f ⁻¹ᵁ U)) also relies on the defeq Opens.map gives, and it might be time we phase these out and switch to appLE completely.

[Kim Morrison]

Anyone interested in fixing the definition of appTop per @Andrew Yang's suggestion?

[Christian Merten]

I did a start in #22820, but have to run now. I'll have a look later today if it is not done by then :) Did you encounter any erws that you associated with appTop, @Kim Morrison?

[Christian Merten]

We might have to transition from Scheme.Hom.app to Scheme.Hom.appLE everywhere first before we get any gains from the appTop fix.

[Kim Morrison]

@Christian Merten, I think the first one I encountered was docs#AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop

[Christian Merten]

Fixing appTopalone does not seem to fix anything, another "wrong" lemma is docs#AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map which "abuses" the def-eq Γ(U, V) = Γ(X, U.ι ''ᵁ V). Almost every lemma in Mathlib.AlgebraicGeometry.Restrict uses this def-eq.

A cheap fix is

unif_hint foo (X : Scheme.{u}) (U : X.Opens) (V : U.toScheme.Opens) where
  ⊢ Γ(U, V) ≟ Γ(X, U.ι ''ᵁ V)

the proof of your example then becomes

  dsimp only [isoSpec_inv, Scheme.isoSpec]
  simp

Is this acceptable or do we need to fix every lemma in Mathlib.AlgebraicGeometry.Restrict manually? (By pre- and postcomposing with suitable Γ(U, V) = Γ(X, U.ι ''ᵁ V)-isomorphisms).