Commit 2025-12-03 12:21 4bf4bb17

feat(AlgebraicGeometry): locally directed colimits in P.Over ⊤ S (#30140) We lift the colimit properties of Scheme to P.Over ⊤ S if IsLocalAtSource P. In particular, P.Over ⊤ S has pushouts along open immersions and (small) coproducts. We also add two instances, that make

example {U X Y : Scheme.{u}} (f : U ⟶ X) (g : U ⟶ Y)
    [IsOpenImmersion f] [IsOpenImmersion g] : HasPushout f g :=
  inferInstance

work.