Relative gluing

In this file we show a relative gluing lemma (see https://stacks.math.columbia.edu/tag/01LH): If {Uᵢ} is a locally directed open cover of S and we have a compatible family of Xᵢ over Uᵢ, the Xᵢ glue to a morphism f : X ⟶ S such that Xᵢ ≅ f⁻¹ Uᵢ.

theorem AlgebraicGeometry.Scheme.isLocallyDirected_of_equifibered_of_injective {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {F G : CategoryTheory.Functor J Scheme} (s : F ⟶ G) [Quiver.IsThin J] (hs : CategoryTheory.NatTrans.Equifibered s) (H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map hij).base)) [(G.comp forget).IsLocallyDirected] : (F.comp forget).IsLocallyDirected

structure AlgebraicGeometry.Scheme.Cover.RelativeGluingData {S : Scheme} (𝒰 : S.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] : Type (max (max (u + 1) u_1) u_2)

A relative gluing datum over a locally directed cover 𝒰 of S is a scheme Xᵢ for every i : 𝒰.I₀ and natural maps Xᵢ ⟶ Uᵢ such that for every i ⟶ j, the diagram

Xᵢ --> Uᵢ
|      |
v      v
Xⱼ --> Uⱼ

is a pullback square. We bundle this in the form of a functor and an equifibered natural transformation. The Xᵢ then glue to a scheme over S (see AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued).

• functor : CategoryTheory.Functor 𝒰.I₀ Scheme

  The schemes Xᵢ.

• natTrans : self.functor ⟶ functorOfLocallyDirected 𝒰

  The natural maps Xᵢ ⟶ Uᵢ.

• equifibered : CategoryTheory.NatTrans.Equifibered self.natTrans

instance AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j) : IsOpenImmersion (d.functor.map hij)

instance AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Quiver.IsThin 𝒰.I₀] : (d.functor.comp forget).IsLocallyDirected

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] : Scheme

The glued scheme of a relative gluing datum is the colimit over the Xᵢ. For the structure map, see AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase and the isomorphisms with the preimages AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase.

Equations

• d.glued = CategoryTheory.Limits.colimit d.functor

noncomputable def AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] : d.glued.OpenCover

The cover of the glued Xᵢ given by the Xᵢ.

Equations

• d.cover = AlgebraicGeometry.Scheme.IsLocallyDirected.openCover d.functor

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] (j : 𝒰.I₀) : d.cover.f j = CategoryTheory.Limits.colimit.ι d.functor j

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_X {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] (a✝ : 𝒰.I₀) : d.cover.X a✝ = d.functor.obj a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_I₀ {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] : d.cover.I₀ = 𝒰.I₀

noncomputable def AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] : d.glued ⟶ S

The structure map from the colimit of the Xᵢ to S.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.functor i) d.toBase = CategoryTheory.CategoryStruct.comp (d.natTrans.app i) (𝒰.f i)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.functor i) (CategoryTheory.CategoryStruct.comp d.toBase h) = CategoryTheory.CategoryStruct.comp (d.natTrans.app i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h)

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀) : ⇑(CategoryTheory.ConcreteCategory.hom d.toBase.base) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f i).base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι d.functor i).base)

theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase {S : Scheme} {𝒰 : S.OpenCover} [CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] [LocallyDirected 𝒰] (d : RelativeGluingData 𝒰) [Small.{u, u_1} 𝒰.I₀] [Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀) : CategoryTheory.IsPullback (d.natTrans.app i) (CategoryTheory.Limits.colimit.ι d.functor i) (𝒰.f i) d.toBase