Showing pushouts of open embedding in schemes are pullbacks

Stream: maths

[Dhyan Aranha]

I'm currently trying to formalize the following result:

lemma isPullback_of_isPushout_of_isOpenImmersion {U X Y T : Scheme.{u}} (f : U ⟶ X) (g : U ⟶ Y)
    (inl : X ⟶ T) (inr : Y ⟶ T) (h : IsPushout f g inl inr)
    [IsOpenImmersion f] [IsOpenImmersion g] :
    IsPullback f g inl inr := by sorry

Roughly speaking the idea is to use the universal property of open immersions to construct an arrow to show the diagram is a pullback. This reduces to a set-theoretic question and my proof has only one sorry remaining which is:

have range_inter : Set.range inl.base ∩ Set.range inr.base ⊆ Set.range
         (f ≫ inl).base := by sorry

I know how to prove an analogue of this result for TopCat because I can use the fact that after applying the forgetful functor I still have a pushout diagram in types. For these kind of gluing pushouts in schemes, the underlying diagram of topological space/types is a pushout in top/type, but how do I show this in Lean? (I see there is some probably relevant stuff in glue data, but I am hesitant/incompetent to use it.)

Any thoughts/help would be great :)

[Notification Bot]

This topic was moved here from #maths > Showing pushouts of open embedding i schemes are pullbacks by Dhyan Aranha.

[Edward van de Meent]

@Christian Merten didn't we prove something like this at Loki some time ago?

[Edward van de Meent]

or no, i think that was something like "open embeddings are preserved under pullback"

[Edward van de Meent]

(i'm not sure, not quite my field)

[Christian Merten]

Does this help?

import Mathlib

universe u
open CategoryTheory Limits AlgebraicGeometry

instance {X Y Z : Scheme.{u}} (f : Z ⟶ X) (g : Z ⟶ Y) [IsOpenImmersion f]
    [IsOpenImmersion g] :
    PreservesColimit (span f g) (Scheme.forgetToTop) := by
  change PreservesColimit _ (Scheme.forgetToLocallyRingedSpace ⋙
    LocallyRingedSpace.forgetToSheafedSpace ⋙ _)
  infer_instance

[Christian Merten]

(We should have the more general version of this for locally directed diagrams, which has exactly the same proof)

[Dhyan Aranha]

@Christian Merten
This exactly what I needed, thanks! [edited: figured out what I needed to do!]

[Dhyan Aranha]

@Christian Merten Sorry for this annoyance! I bumped mathlib today and now a lot of my instances have broken. In particular the one you suggested:

import Mathlib

open Polynomial AlgebraicGeometry CategoryTheory CategoryTheory.Limits Scheme TopCat Topology
open LocallyRingedSpace.IsOpenImmersion

instance {X Y Z : Scheme} (f : Z ⟶ X) (g : Z ⟶  Y) [IsOpenImmersion f] [IsOpenImmersion g] :
    PreservesColimit (span f g) (Scheme.forgetToTop) := by
  change PreservesColimit _ (Scheme.forgetToLocallyRingedSpace ⋙
    LocallyRingedSpace.forgetToSheafedSpace ⋙ _)
  infer_instance

breaks now.

[Christian Merten]

Can you try putting set_option backward.isDefEq.respectTransparency false in above the instance? There has been a Lean version bump yesterday which changed the behaviour of a def-eq check. It is still being discussed what to do about this.

[Dhyan Aranha]

it works! Thanks!