Opens of locally directed colimits of schemes

Let F : J ⥤ Scheme be a locally directed diagram of open immersions indexed by a small thin category, so that its colimit is the scheme glued from the F j along the images of the transition maps (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover). This file describes how the images of the F j in the colimit meet.

Main results

• AlgebraicGeometry.Scheme.IsLocallyDirected.preimage_opensRange_ι_le: the part of F j lying over the image of F i is contained in the image of F f, for any f : i ⟶ j.
• AlgebraicGeometry.Scheme.IsLocallyDirected.preimage_le_iSup_preimage_inf_opensRange: the preimage in F j of an open contained in the image of F i is covered by its intersections with the images of the F k mapping to both F i and F j.
• AlgebraicGeometry.Scheme.range_pushout_inl_union_range_pushout_inr: a pushout of two open immersions is covered by the images of its two pieces.
• AlgebraicGeometry.Scheme.pushoutOpenCover: the open cover by those two pieces.
• AlgebraicGeometry.Scheme.isPullback_pushout_of_isOpenImmersion: those two pieces intersect in precisely the common open along which they were glued.

References

• The Stacks Project, Section 26.14, Gluing schemes (Tag 01JA).

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.preimage_opensRange_ι_le {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] {i j : J} (f : i ⟶ j) : (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F j).base).obj (Hom.opensRange (CategoryTheory.Limits.colimit.ι F i)) ≤ Hom.opensRange (F.map f)

In the colimit of a thin locally directed diagram of open immersions, the part of F j lying over the image of F i is contained in the image of F f, for any f : i ⟶ j.

theorem AlgebraicGeometry.Scheme.IsLocallyDirected.preimage_le_iSup_preimage_inf_opensRange {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J Scheme) [∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)] [(F.comp forget).IsLocallyDirected] [Quiver.IsThin J] {i j : J} {U : (CategoryTheory.Limits.colimit F).Opens} (hU : U ≤ Hom.opensRange (CategoryTheory.Limits.colimit.ι F i)) : (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F j).base).obj U ≤ ⨆ (k : (k : J) × (k ⟶ j) × (k ⟶ i)), (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F j).base).obj (U ⊓ Hom.opensRange (CategoryTheory.Limits.colimit.ι F k.fst))

In the colimit of a thin locally directed diagram of open immersions, the opens U ⊓ ιₖ(F k), for k mapping to both i and j, cover the preimage in F j of an open U contained in the image of F i.

theorem AlgebraicGeometry.Scheme.range_pushout_inl_union_range_pushout_inr {W X Z : Scheme} (g : W ⟶ X) (h : W ⟶ Z) [IsOpenImmersion g] [IsOpenImmersion h] : Set.range ⇑(CategoryTheory.Limits.pushout.inl g h) ∪ Set.range ⇑(CategoryTheory.Limits.pushout.inr g h) = Set.univ

A pushout of open immersions is covered by its two pieces. Every point of the pushout of two open immersions X ⟵ W ⟶ Z of schemes lies in the image of X or of Z.

noncomputable def AlgebraicGeometry.Scheme.pushoutOpenCover {W X Y : Scheme} (i : W ⟶ X) (j : W ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] : (CategoryTheory.Limits.pushout i j).OpenCover

The open cover of a pushout of open immersions by its two pieces, indexed by Bool, with the left piece at false and the right piece at true.

instance AlgebraicGeometry.Scheme.instFiniteI₀PushoutOpenCover {W X Y : Scheme} (i : W ⟶ X) (j : W ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] : Finite (pushoutOpenCover i j).I₀

The two-piece pushout cover has a finite index type.

@[simp]

theorem AlgebraicGeometry.Scheme.pushoutOpenCover_f_false {W X Y : Scheme} (i : W ⟶ X) (j : W ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] : (pushoutOpenCover i j).f false = CategoryTheory.Limits.pushout.inl i j

The first chart of the pushout cover is its left inclusion.

@[simp]

theorem AlgebraicGeometry.Scheme.pushoutOpenCover_f_true {W X Y : Scheme} (i : W ⟶ X) (j : W ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] : (pushoutOpenCover i j).f true = CategoryTheory.Limits.pushout.inr i j

The second chart of the pushout cover is its right inclusion.

theorem AlgebraicGeometry.Scheme.isPullback_pushout_of_isOpenImmersion {W X Y : Scheme} (i : W ⟶ X) (j : W ⟶ Y) [IsOpenImmersion i] [IsOpenImmersion j] : CategoryTheory.IsPullback i j (CategoryTheory.Limits.pushout.inl i j) (CategoryTheory.Limits.pushout.inr i j)

The square defining the pushout of two open immersions is also cartesian: the two pieces intersect in precisely the open subscheme along which they were glued.