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.

Author: chrisflav

Mathlib.lean

@@ -1276,6 +1276,7 @@ public import Mathlib.AlgebraicGeometry.IdealSheaf.Basic
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
 public import Mathlib.AlgebraicGeometry.Limits
+public import Mathlib.AlgebraicGeometry.LimitsOver
 public import Mathlib.AlgebraicGeometry.Modules.Presheaf
 public import Mathlib.AlgebraicGeometry.Modules.Sheaf
 public import Mathlib.AlgebraicGeometry.Modules.Tilde

Mathlib/AlgebraicGeometry/Limits.lean

@@ -516,6 +516,26 @@ instance [IsAffine X] [IsAffine Y] : IsAffine (X ⨿ Y) :=
 
 end Coproduct
 
+instance {U X Y : Scheme} (f : U ⟶ X) (g : U ⟶ Y) [IsOpenImmersion f] [IsOpenImmersion g]
+    (i : WalkingPair) : Mono ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i)) := by
+  rw [mono_iff_injective]
+  cases i
+  · simpa using f.isOpenEmbedding.injective
+  · simpa using g.isOpenEmbedding.injective
+
+instance {U X Y : Scheme} (f : U ⟶ X) (g : U ⟶ Y) [IsOpenImmersion f] [IsOpenImmersion g]
+    {i j : WalkingSpan} (t : i ⟶ j) : IsOpenImmersion ((span f g).map t) := by
+  obtain (a | (a | a)) := t
+  · simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]
+    infer_instance
+  · simpa
+  · simpa
+
+-- Test that instances on locally directed colimits fire correctly.
+example {U X Y : Scheme.{u}} (f : U ⟶ X) (g : U ⟶ Y)
+    [IsOpenImmersion f] [IsOpenImmersion g] : HasPushout f g :=
+  inferInstance
+
 instance : CartesianMonoidalCategory Scheme := .ofHasFiniteProducts
 instance : BraidedCategory Scheme := .ofCartesianMonoidalCategory
 

Mathlib/AlgebraicGeometry/LimitsOver.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.AlgebraicGeometry.Morphisms.Basic
+public import Mathlib.CategoryTheory.MorphismProperty.Comma
+
+/-!
+# (Co)limits in over categories
+
+We show that if `P` is a morphism property in `Scheme` that is local at the source, then
+colimits in `P.Over ⊤ X` for `X : Scheme` of locally directed diagrams of open immersions
+exist and agree with the colimit in `Scheme`.
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory Limits
+
+namespace AlgebraicGeometry
+
+variable (X : Scheme.{u})
+
+variable (P : MorphismProperty Scheme.{u})
+
+section Over
+
+variable {S : Scheme.{u}} {J : Type*} [Category J] (F : J ⥤ Over S)
+  [∀ {i j} (f : i ⟶ j), IsOpenImmersion (F.map f).left]
+  [(F ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected]
+  [Quiver.IsThin J] [Small.{u} J]
+
+noncomputable instance : HasColimit F :=
+  have {i j} (f : i ⟶ j) : IsOpenImmersion ((F ⋙ Over.forget S).map f) :=
+    inferInstanceAs <| IsOpenImmersion (F.map f).left
+  have : ((F ⋙ Over.forget S) ⋙ Scheme.forget).IsLocallyDirected := ‹_›
+  hasColimit_of_created _ (Over.forget S)
+
+end Over
+
+section OverProp
+
+instance {S : Scheme.{u}} {U X Y : P.Over ⊤ S} (f : U ⟶ X) (g : U ⟶ Y)
+    [IsOpenImmersion f.left] [IsOpenImmersion g.left] (i : WalkingPair) :
+    Mono ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
+      (WidePushoutShape.Hom.init i)) := by
+  rw [mono_iff_injective]
+  cases i
+  · simpa using f.left.isOpenEmbedding.injective
+  · simpa using g.left.isOpenEmbedding.injective
+
+instance {S : Scheme.{u}} {U X Y : P.Over ⊤ S} (f : U ⟶ X) (g : U ⟶ Y)
+    [IsOpenImmersion f.left] [IsOpenImmersion g.left]
+    {i j : WalkingSpan} (t : i ⟶ j) :
+      IsOpenImmersion ((span f g).map t).left := by
+  obtain (a|(a|a)) := t
+  · simp only [WidePushoutShape.hom_id, CategoryTheory.Functor.map_id]
+    infer_instance
+  · simpa
+  · simpa
+
+variable [IsZariskiLocalAtSource P] {S : Scheme.{u}} {J : Type*} [Category J] (F : J ⥤ P.Over ⊤ S)
+  [∀ {i j} (f : i ⟶ j), IsOpenImmersion (F.map f).left]
+  [(F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected]
+  [Quiver.IsThin J] [Small.{u} J]
+
+local instance :
+    (((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) ⋙
+      Scheme.forget).IsLocallyDirected :=
+  ‹_›
+
+local instance {i j} (f : i ⟶ j) :
+    IsOpenImmersion <|
+      ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S).map f :=
+  inferInstanceAs <| IsOpenImmersion (F.map f).left
+
+noncomputable instance : CreatesColimit F (MorphismProperty.Over.forget P ⊤ S) := by
+  have : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S) :=
+    hasColimit_of_created _ (Over.forget S)
+  refine createsColimitOfFullyFaithfulOfIso
+      { toComma := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
+        prop := ?_ } (Iso.refl _)
+  let e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
+      colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
+    preservesColimitIso (Over.forget S) _
+  let 𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
+    (Scheme.IsLocallyDirected.openCover _).pushforwardIso e.inv
+  rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) 𝒰]
+  intro i
+  simpa [𝒰, e] using (F.obj i).prop
+
+instance : HasColimit F := hasColimit_of_created _ (MorphismProperty.Over.forget P ⊤ S)
+
+instance : PreservesColimit F (MorphismProperty.Over.forget P ⊤ S) :=
+  -- this is only `inferInstance` with the local instances above
+  inferInstance
+
+instance (j : J) : IsOpenImmersion (colimit.ι F j).left := by
+  rw [← MorphismProperty.Over.forget_comp_forget_map]
+  let e : (colimit F).left ≅ colimit (F ⋙ _) :=
+    preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
+  rw [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _ e.hom]
+  simp only [e, CategoryTheory.ι_preservesColimitIso_hom]
+  exact inferInstanceAs <| IsOpenImmersion
+    (colimit.ι ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) j)
+
+instance {ι : Type*} [Small.{u} ι] : HasCoproductsOfShape ι (P.Over ⊤ S) where
+
+instance : HasFiniteCoproducts (P.Over ⊤ S) where
+  out := inferInstance
+
+noncomputable instance (J : Type*) [Small.{u} J] :
+    CreatesColimitsOfShape (Discrete J) (MorphismProperty.Over.forget P ⊤ S) where
+
+end OverProp
+
+end AlgebraicGeometry

Mathlib/CategoryTheory/Limits/MorphismProperty.lean

@@ -108,6 +108,25 @@ instance CostructuredArrow.closedUnderLimitsOfShape_discrete_empty [L.Faithful]
       P.costructuredArrow_iso_iff e]
     simpa using P.id_mem (L.obj Y)
 
+lemma CostructuredArrow.isClosedUnderColimitsOfShape {J : Type*} [Category J]
+    {P : MorphismProperty T} [P.RespectsIso] [PreservesColimitsOfShape J L] [HasColimitsOfShape J A]
+    (c : ∀ (D : J ⥤ T) [HasColimit D], Cocone D)
+    (hc : ∀ (D : J ⥤ T) [HasColimit D], IsColimit (c D))
+    (H : ∀ (D : J ⥤ T) [HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
+      (∀ j, P (s.app j)) → P ((hc D).desc (Cocone.mk X s))) (X : T) :
+    (P.costructuredArrowObj L (X := X)).IsClosedUnderColimitsOfShape J where
+  colimitsOfShape_le Y := by
+    intro ⟨d⟩
+    let hd : IsColimit ((CategoryTheory.CostructuredArrow.proj L X ⋙ L).mapCocone d.cocone) :=
+      isColimitOfPreserves _ d.isColimit
+    have heq : Y.hom = hd.desc { pt := X, ι := { app j := (d.diag.obj j).hom } } := by
+      refine hd.hom_ext fun j ↦ ?_
+      simp only [Functor.const_obj_obj, IsColimit.fac]
+      simp
+    rw [P.costructuredArrowObj_iff, heq, ← hd.coconePointUniqueUpToIso_hom_desc (hc _),
+      P.cancel_left_of_respectsIso]
+    exact H _ _ d.prop_diag_obj
+
 end
 
 section

Mathlib/CategoryTheory/Limits/Over.lean

@@ -5,12 +5,9 @@ Authors: Johan Commelin, Reid Barton, Bhavik Mehta
 -/
 module
 
-public import Mathlib.CategoryTheory.Comma.Over.Basic
 public import Mathlib.CategoryTheory.Limits.Comma
 public import Mathlib.CategoryTheory.Limits.ConeCategory
-public import Mathlib.CategoryTheory.Limits.Creates
-public import Mathlib.CategoryTheory.Limits.Preserves.Basic
-public import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
+public import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
 
 /-!
 # Limits and colimits in the over and under categories
@@ -51,6 +48,9 @@ instance [HasFiniteColimits C] : HasFiniteColimits (Over X) where
 instance [HasColimits C] : HasColimits (Over X) :=
   ⟨inferInstance⟩
 
+instance [HasFiniteCoproducts C] : HasFiniteCoproducts (Over X) where
+  out := inferInstance
+
 instance createsColimitsOfSize : CreatesColimitsOfSize.{w, w'} (forget X) :=
   CostructuredArrow.createsColimitsOfSize
 

Mathlib/CategoryTheory/MorphismProperty/Comma.lean

@@ -387,6 +387,10 @@ protected abbrev Over.forget : P.Over Q X ⥤ Over X :=
 instance : (Over.forget P ⊤ X).Faithful := inferInstanceAs <| (Comma.forget _ _ _ _ _).Faithful
 instance : (Over.forget P ⊤ X).Full := inferInstanceAs <| (Comma.forget _ _ _ _ _).Full
 
+/-- Occasionally useful for rewriting in the backwards direction. -/
+lemma Over.forget_comp_forget_map {A B : P.Over Q X} (f : A ⟶ B) :
+    (MorphismProperty.Over.forget P Q X ⋙ CategoryTheory.Over.forget X).map f = f.left := rfl
+
 variable {P Q X}
 
 /-- Construct a morphism in `P.Over Q X` from a morphism in `Over.X`. -/
@@ -448,6 +452,10 @@ protected abbrev Under.forget : P.Under Q X ⥤ Under X :=
 instance : (Under.forget P ⊤ X).Faithful := inferInstanceAs <| (Comma.forget _ _ _ _ _).Faithful
 instance : (Under.forget P ⊤ X).Full := inferInstanceAs <| (Comma.forget _ _ _ _ _).Full
 
+/-- Occasionally useful for rewriting in the backwards direction. -/
+lemma Under.forget_comp_forget_map {A B : P.Under Q X} (f : A ⟶ B) :
+    (MorphismProperty.Under.forget P Q X ⋙ CategoryTheory.Under.forget X).map f = f.right := rfl
+
 variable {P Q X}
 
 /-- Construct a morphism in `P.Under Q X` from a morphism in `Under.X`. -/