(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.

instance AlgebraicGeometry.instHasColimitOverScheme {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (CategoryTheory.Over S)) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (CategoryTheory.Over.Hom.left (F.map f))] [(F.comp ((CategoryTheory.Over.forget S).comp Scheme.forget)).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J] : CategoryTheory.Limits.HasColimit F

instance AlgebraicGeometry.instMonoObjWalkingSpanCompOverSchemeTopMorphismPropertySpanOverForgetForgetForgetNoneWalkingPairSomeMapInitOfIsOpenImmersionLeftDiscretePUnit (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} {U X Y : P.Over ⊤ S} (f : U ⟶ X) (g : U ⟶ Y) [IsOpenImmersion f.left] [IsOpenImmersion g.left] (i : CategoryTheory.Limits.WalkingPair) : CategoryTheory.Mono (((CategoryTheory.Limits.span f g).comp ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp ((CategoryTheory.Over.forget S).comp Scheme.forget))).map (CategoryTheory.Limits.WidePushoutShape.Hom.init i))

instance AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} {U X Y : P.Over ⊤ S} (f : U ⟶ X) (g : U ⟶ Y) [IsOpenImmersion f.left] [IsOpenImmersion g.left] {i j : CategoryTheory.Limits.WalkingSpan} (t : i ⟶ j) : IsOpenImmersion ((CategoryTheory.Limits.span f g).map t).left

theorem AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S)) [(F.comp ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp ((CategoryTheory.Over.forget S).comp Scheme.forget))).IsLocallyDirected] : (((F.comp (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)).comp (CategoryTheory.Over.forget S)).comp Scheme.forget).IsLocallyDirected

theorem AlgebraicGeometry.instIsOpenImmersionMapSchemeCompOverOverTopMorphismPropertyForgetForget (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S)) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left] {i j : J} (f : i ⟶ j) : IsOpenImmersion (((F.comp (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)).comp (CategoryTheory.Over.forget S)).map f)

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instCreatesColimitOverSchemeTopMorphismPropertyOverForget (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S)) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left] [(F.comp ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp ((CategoryTheory.Over.forget S).comp Scheme.forget))).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J] : CategoryTheory.CreatesColimit F (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.instHasColimitOverSchemeTopMorphismProperty (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S)) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left] [(F.comp ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp ((CategoryTheory.Over.forget S).comp Scheme.forget))).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J] : CategoryTheory.Limits.HasColimit F

instance AlgebraicGeometry.instPreservesColimitOverSchemeTopMorphismPropertyOverForget (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S)) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left] [(F.comp ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp ((CategoryTheory.Over.forget S).comp Scheme.forget))).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J] : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)

instance AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (F : CategoryTheory.Functor J (P.Over ⊤ S)) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left] [(F.comp ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp ((CategoryTheory.Over.forget S).comp Scheme.forget))).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, u_1} J] (j : J) : IsOpenImmersion (CategoryTheory.Limits.colimit.ι F j).left

instance AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} {ι : Type u_2} [Small.{u, u_2} ι] : CategoryTheory.Limits.HasCoproductsOfShape ι (P.Over ⊤ S)

instance AlgebraicGeometry.instHasFiniteCoproductsOverSchemeTopMorphismProperty (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} : CategoryTheory.Limits.HasFiniteCoproducts (P.Over ⊤ S)

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instCreatesColimitsOfShapeOverSchemeTopMorphismPropertyOverDiscreteForgetOfSmall (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtSource P] {S : Scheme} (J : Type u_2) [Small.{u, u_2} J] : CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete {P : CategoryTheory.MorphismProperty Scheme} [IsZariskiLocalAtSource P] {ι : Type u_2} [Small.{u, u_2} ι] {C : Type u_3} [CategoryTheory.Category.{v_2, u_3} C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) C] (L : CategoryTheory.Functor C Scheme) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) L] (X : Scheme) : (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)

instance AlgebraicGeometry.instHasFiniteCoproductsCostructuredArrowOppositeCommRingCatSchemeTopMorphismPropertySpec {S : Scheme} {P : CategoryTheory.MorphismProperty Scheme} [IsZariskiLocalAtSource P] : CategoryTheory.Limits.HasFiniteCoproducts (P.CostructuredArrow ⊤ Scheme.Spec S)