Colimits in P.Over ⊤ S

Let P be a morphism property in the category of schemes and S be a scheme. Let D : J ⥤ P.Over ⊤ S be a diagram and 𝒰 a locally directed open cover of S (e.g., the cover of all affine opens of S). Suppose the restrictions of D to Dᵢ : J ⥤ P.Over ⊤ (𝒰.X i) have a colimit for every i, then we show that also D has a colimit under the following assumptions:

• P is local on the source.
• For i ⟶ j, the transition map 𝒰.X i ⟶ 𝒰.X j satisfies P.
• For i ⟶ j, the base change functor P.Over ⊤ (𝒰.X j) ⥤ P.Over ⊤ (𝒰.X i) preserves colimits of shape J.

This can be used to reduce existence of certain colimits in P.Over ⊤ S to the case where S is affine.

structure AlgebraicGeometry.Scheme.Cover.ColimitGluingData {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J (P.Over ⊤ S)) (𝒰 : S.OpenCover) [CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] [LocallyDirected 𝒰] : Type (max (max (u + 1) u_1) u_2)

The data required for gluing the colimits of the Dᵢ : J ⥤ P.Over ⊤ (𝒰.X i).

• cocone (i : 𝒰.I₀) : CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))

  The cocones on the Dᵢ.

• isColimit (i : 𝒰.I₀) : CategoryTheory.Limits.IsColimit (self.cocone i)

  The cocones on the Dᵢ are colimiting.

• prop_trans {i j : 𝒰.I₀} (hij : i ⟶ j) : P (Cover.trans 𝒰 hij)

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) : D.comp ((CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).comp (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯)) ⟶ D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f j))

(Implementation) Auxiliary natural transformation for construction of AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor.

Equations

• d.trans hij = D.whiskerLeft (CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) ⋯ trivial (𝒰.f j) (𝒰.f i) ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (X : J) : ((d.trans hij).app X).left = CategoryTheory.Limits.pullback.map (D.obj X).hom (𝒰.f i) (D.obj X).hom (𝒰.f j) (CategoryTheory.CategoryStruct.id (D.obj X).left) (Cover.trans 𝒰 hij) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) : CategoryTheory.Limits.Cocone (D.comp ((CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).comp (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯)))

(Implementation) Cocone for transition map for construction of AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor.

Equations

• d.transitionCocone hij = (CategoryTheory.Limits.Cocones.precompose (d.trans hij)).obj (d.cocone j)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (X : J) : (d.transitionCocone hij).ι.app X = CategoryTheory.CategoryStruct.comp ((d.trans hij).app X) ((d.cocone j).ι.app X)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) : (d.transitionCocone hij).pt = (d.cocone j).pt

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) : (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).obj (d.cocone i).pt ⟶ (d.cocone j).pt

(Implementation) Transition map for construction of AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor.

Equations

• d.transitionMap hij = (CategoryTheory.Limits.isColimitOfPreserves (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯) (d.isColimit i)).desc (d.transitionCocone hij)

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (a : J) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a)) (d.transitionMap hij) = CategoryTheory.CategoryStruct.comp ((d.trans hij).app a) ((d.cocone j).ι.app a)

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) (a : J) {Z : P.Over ⊤ (𝒰.X j)} (h : (d.cocone j).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a)) (CategoryTheory.CategoryStruct.comp (d.transitionMap hij) h) = CategoryTheory.CategoryStruct.comp ((d.trans hij).app a) (CategoryTheory.CategoryStruct.comp ((d.cocone j).ι.app a) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) (i : 𝒰.I₀) : d.transitionMap (CategoryTheory.CategoryStruct.id i) = (CategoryTheory.MorphismProperty.Over.mapId ⊤ (𝒰.X i) (Cover.trans 𝒰 (CategoryTheory.CategoryStruct.id i)) ⋯).hom.app (d.cocone i).pt

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k) : d.transitionMap (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.mapComp ⊤ ⋯ ⋯ (Cover.trans 𝒰 (CategoryTheory.CategoryStruct.comp hij hjk)) ⋯).hom.app (d.cocone i).pt) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).map (d.transitionMap hij)) (d.transitionMap hjk))

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) : CategoryTheory.Functor 𝒰.I₀ Scheme

(Implementation): Underlying functor of associated relative gluing datum.

Equations

• d.functor = { obj := fun (i : 𝒰.I₀) => (d.cocone i).pt.left, map := fun {i j : 𝒰.I₀} (hij : i ⟶ j) => (d.transitionMap hij).left, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) : d.functor.map hij = (d.transitionMap hij).left

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) (i : 𝒰.I₀) : d.functor.obj i = (d.cocone i).pt.left

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] {i j : 𝒰.I₀} (hij : i ⟶ j) : CategoryTheory.IsPullback (d.transitionMap hij).left (d.cocone i).pt.hom (d.cocone j).pt.hom (Cover.trans 𝒰 hij)

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] : RelativeGluingData 𝒰

The relative gluing datum associated to the family of the colim Dᵢ.

Equations

• d.relativeGluingData = { functor := d.functor, natTrans := { app := fun (i : 𝒰.I₀) => (d.cocone i).pt.hom, naturality := ⋯ }, equifibered := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] (i : 𝒰.I₀) : d.relativeGluingData.natTrans.app i = (d.cocone i).pt.hom

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_functor {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] : d.relativeGluingData.functor = d.functor

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] : P.Over ⊤ S

The result of gluing the colim Dᵢ.

Equations

• d.glued = CategoryTheory.MorphismProperty.Over.mk ⊤ d.relativeGluingData.toBase ⋯

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (i : 𝒰.I₀) : (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).obj d.glued ≅ (d.cocone i).pt

colim Dᵢ is the pullback of the glued object over S along the inclusion 𝒰ᵢ ⟶ S.

Equations

• d.pullbackGluedIso i = CategoryTheory.MorphismProperty.Over.isoMk ⋯.isoPullback.symm ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left (CategoryTheory.Limits.pullback.fst d.glued.hom (𝒰.f i)) = CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (i : 𝒰.I₀) {Z : Scheme} (h : d.glued.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst d.glued.hom (𝒰.f i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i) h

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left (CategoryTheory.Limits.pullback.snd d.glued.hom (𝒰.f i)) = (d.cocone i).pt.hom

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (i : 𝒰.I₀) {Z : Scheme} (h : 𝒰.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd d.glued.hom (𝒰.f i)) h) = CategoryTheory.CategoryStruct.comp (d.cocone i).pt.hom h

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] : CategoryTheory.Limits.Cocone D

The cocone glued from the colim Dᵢ.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone_pt {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] : d.gluedCocone.pt = d.glued

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (a : J) (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.obj a).hom (𝒰.f i)) (d.gluedCocone.ι.app a).left = CategoryTheory.CategoryStruct.comp ((d.cocone i).ι.app a).left (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i)

theorem AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] (a : J) (i : 𝒰.I₀) {Z : Scheme} (h : (((CategoryTheory.Functor.const J).obj d.gluedCocone.pt).obj a).left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.obj a).hom (𝒰.f i)) (CategoryTheory.CategoryStruct.comp (d.gluedCocone.ι.app a).left h) = CategoryTheory.CategoryStruct.comp ((d.cocone i).ι.app a).left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i) h)

noncomputable def AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitGluedCocone {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover} [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (d : ColimitGluingData D 𝒰) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] : CategoryTheory.Limits.IsColimit d.gluedCocone

The glued cocone is colimiting.

Equations

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

theorem AlgebraicGeometry.Scheme.Cover.hasColimit_of_locallyDirected {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {S : Scheme} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J (P.Over ⊤ S)) (𝒰 : S.OpenCover) [CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [LocallyDirected 𝒰] (H : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans 𝒰 hij)) [∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (trans 𝒰 hij))] [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasColimit (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))] [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [IsZariskiLocalAtTarget P] : CategoryTheory.Limits.HasColimit D