Locally directed covers

A locally directed P-cover of a scheme X is a cover 𝒰 with an ordering on the indices and compatible transition maps 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j such that every x : 𝒰ᵢ ×[X] 𝒰ⱼ comes from some 𝒰ₖ for a k ≤ i and k ≤ j.

Gluing along directed covers is easier, because the intersections 𝒰ᵢ ×[X] 𝒰ⱼ can be covered by a subcover of 𝒰. In particular, if 𝒰 is a Zariski cover, X naturally is the colimit of the 𝒰ᵢ.

Many natural covers are naturally directed, most importantly the cover of all affine opens of a scheme.

class AlgebraicGeometry.Scheme.Cover.LocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] : Type (max (max u u_1) u_2)

A directed P-cover of a scheme X is a cover 𝒰 with an ordering on the indices and compatible transition maps 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j such that every x : 𝒰ᵢ ×[X] 𝒰ⱼ comes from some 𝒰ₖ for a k ≤ i and k ≤ j.

• trans {i j : 𝒰.J} (hij : i ⟶ j) : 𝒰.obj i ⟶ 𝒰.obj j

  The transition map 𝒰ᵢ ⟶ 𝒰ⱼ for i ≤ j.

• trans_id (i : 𝒰.J) : trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.obj i)
• trans_comp {i j k : 𝒰.J} (hij : i ⟶ j) (hjk : j ⟶ k) : trans (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp (trans hij) (trans hjk)
• w {i j : 𝒰.J} (hij : i ⟶ j) : CategoryTheory.CategoryStruct.comp (trans hij) (𝒰.map j) = 𝒰.map i
• directed {i j : 𝒰.J} (x : ↥(CategoryTheory.Limits.pullback (𝒰.map i) (𝒰.map j))) : ∃ (k : 𝒰.J) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.obj k)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.lift (trans hki) (trans hkj) ⋯).base) y = x
• property_trans {i j : 𝒰.J} (hij : i ⟶ j) : P (trans hij)

def AlgebraicGeometry.Scheme.Cover.trans {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {i j : 𝒰.J} (hij : i ⟶ j) : 𝒰.obj i ⟶ 𝒰.obj j

The transition maps of a directed cover.

Equations

• 𝒰.trans hij = AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hij

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.trans_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {i j : 𝒰.J} (hij : i ⟶ j) : CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.map j) = 𝒰.map i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.trans_id {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] (i : 𝒰.J) : 𝒰.trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.obj i)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.trans_comp {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {i j k : 𝒰.J} (hij : i ⟶ j) (hjk : j ⟶ k) : 𝒰.trans (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.trans hjk)

theorem AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {i j : 𝒰.J} (x : ↥(CategoryTheory.Limits.pullback (𝒰.map i) (𝒰.map j))) : ∃ (k : 𝒰.J) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.obj k)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯).base) y = x

theorem AlgebraicGeometry.Scheme.Cover.property_trans {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {i j : 𝒰.J} (hij : i ⟶ j) : P (𝒰.trans hij)

def AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.J) : Cover P (CategoryTheory.Limits.pullback (𝒰.map i) (𝒰.map j))

If 𝒰 is a directed cover of X, this is the cover of 𝒰ᵢ ×[X] 𝒰ⱼ by {𝒰ₖ} where k ≤ i and k ≤ j.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.J) (k : (k : 𝒰.J) × (k ⟶ i) × (k ⟶ j)) : (𝒰.intersectionOfLocallyDirected i j).map k = CategoryTheory.Limits.pullback.lift (𝒰.trans k.snd.1) (𝒰.trans k.snd.2) ⋯

def AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] : CategoryTheory.Functor 𝒰.J Scheme

The canonical diagram induced by a locally directed cover.

Equations

• 𝒰.functorOfLocallyDirected = { obj := 𝒰.obj, map := fun {X_1 Y : 𝒰.J} => 𝒰.trans, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {X✝ Y✝ : 𝒰.J} (hij : X✝ ⟶ Y✝) : 𝒰.functorOfLocallyDirected.map hij = 𝒰.trans hij

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] (j : 𝒰.J) : 𝒰.functorOfLocallyDirected.obj j = 𝒰.obj j

instance AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedJCompFunctorOfLocallyDirectedForget {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] : (𝒰.functorOfLocallyDirected.comp forget).IsLocallyDirected

def AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] : CategoryTheory.Limits.Cocone 𝒰.functorOfLocallyDirected

The canonical cocone with point X on the functor induced by the locally directed cover 𝒰. If 𝒰 is an open cover, this is colimiting (see OpenCover.isColimitCoconeOfLocallyDirected).

Equations

• 𝒰.coconeOfLocallyDirected = { pt := X, ι := { app := 𝒰.map, naturality := ⋯ } }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_pt {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] : 𝒰.coconeOfLocallyDirected.pt = X

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ι_app {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] (j : 𝒰.J) : 𝒰.coconeOfLocallyDirected.ι.app j = 𝒰.map j

instance AlgebraicGeometry.Scheme.Cover.instCategoryJPullbackCover {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [P.IsStableUnderBaseChange] (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] {Y : Scheme} (f : Y ⟶ X) : CategoryTheory.Category.{u_2, u_1} (𝒰.pullbackCover f).J

Equations

• 𝒰.instCategoryJPullbackCover f = inferInstanceAs (CategoryTheory.Category.{?u.47, ?u.48} 𝒰.J)

instance AlgebraicGeometry.Scheme.Cover.locallyDirectedPullbackCover {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [P.IsStableUnderBaseChange] (𝒰 : Cover P X) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [𝒰.LocallyDirected] {Y : Scheme} (f : Y ⟶ X) : (𝒰.pullbackCover f).LocallyDirected

Equations

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

instance AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {i j : 𝒰.J} (f : i ⟶ j) : IsOpenImmersion (Cover.trans 𝒰 f)

instance AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapJFunctorOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {i j : 𝒰.J} (f : i ⟶ j) : IsOpenImmersion ((Cover.functorOfLocallyDirected 𝒰).map f)

def AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.J) → 𝒰.obj i ⟶ Y) (h : ∀ {i j : 𝒰.J} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) : X ⟶ Y

If 𝒰 is a directed open cover of X, to glue morphisms {gᵢ : 𝒰ᵢ ⟶ Y} it suffices to check compatibility with the transition maps. See OpenCover.isColimitCoconeOfLocallyDirected for this result stated in the language of colimits.

Equations

• 𝒰.glueMorphismsOfLocallyDirected g h = AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 g ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.J) → 𝒰.obj i ⟶ Y) (h : ∀ {i j : 𝒰.J} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (𝒰.map i) (𝒰.glueMorphismsOfLocallyDirected g ⋯) = g i

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.J) → 𝒰.obj i ⟶ Y) (h : ∀ {i j : 𝒰.J} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (i : 𝒰.J) {Z : Scheme} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.map i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphismsOfLocallyDirected g ⋯) h✝) = CategoryTheory.CategoryStruct.comp (g i) h✝

def AlgebraicGeometry.Scheme.OpenCover.isColimitCoconeOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] : CategoryTheory.Limits.IsColimit (Cover.coconeOfLocallyDirected 𝒰)

If 𝒰 is an open cover of X that is locally directed, X is the colimit of the components of 𝒰.

Equations

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

def AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected {S : Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.J) → 𝒰.obj i ⟶ Y.left) (h : ∀ {i j : 𝒰.J} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.J), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.map i) X.hom) : X ⟶ Y

If 𝒰 is a directed open cover of X, to glue morphisms {gᵢ : 𝒰ᵢ ⟶ Y} over S it suffices to check compatibility with the transition maps.

Equations

• 𝒰.glueMorphismsOverOfLocallyDirected g h w = CategoryTheory.Over.homMk (𝒰.glueMorphismsOfLocallyDirected g ⋯) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left {S : Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.J) → 𝒰.obj i ⟶ Y.left) (h : ∀ {i j : 𝒰.J} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.J), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.map i) X.hom) (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (𝒰.map i) (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w).left = g i

@[simp]

theorem AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc {S : Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover) [CategoryTheory.Category.{u_2, u_1} 𝒰.J] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.J) → 𝒰.obj i ⟶ Y.left) (h : ∀ {i j : 𝒰.J} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.J), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.map i) X.hom) (i : 𝒰.J) {Z : Scheme} (h✝ : Y.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.map i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w).left h✝) = CategoryTheory.CategoryStruct.comp (g i) h✝

def AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange {X : Scheme} {𝒰 : X.OpenCover} [Preorder 𝒰.J] (hle : ∀ {i j : 𝒰.J}, i ≤ j ↔ Hom.opensRange (𝒰.map i) ≤ Hom.opensRange (𝒰.map j)) (H : TopologicalSpace.Opens.IsBasis (Set.range fun (i : 𝒰.J) => Hom.opensRange (𝒰.map i))) : LocallyDirected 𝒰

If 𝒰 is an open cover such that the images of the components form a basis of the topology of X, 𝒰 is directed by the ordering of subset inclusion of the images.

Equations

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

theorem AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff {X : Scheme} {𝒰 : X.OpenCover} [Preorder 𝒰.J] (hle : ∀ {i j : 𝒰.J}, i ≤ j ↔ Hom.opensRange (𝒰.map i) ≤ Hom.opensRange (𝒰.map j)) (i j : 𝒰.J) : i ≤ j ↔ Hom.opensRange (𝒰.map i) ≤ Hom.opensRange (𝒰.map j)

theorem AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans {X : Scheme} {𝒰 : X.OpenCover} [Preorder 𝒰.J] (hle : ∀ {i j : 𝒰.J}, i ≤ j ↔ Hom.opensRange (𝒰.map i) ≤ Hom.opensRange (𝒰.map j)) (H : TopologicalSpace.Opens.IsBasis (Set.range fun (i : 𝒰.J) => Hom.opensRange (𝒰.map i))) {i j : 𝒰.J} (hij : i ≤ j) : Cover.trans 𝒰 (CategoryTheory.homOfLE hij) = IsOpenImmersion.lift (𝒰.map j) (𝒰.map i) ⋯

def AlgebraicGeometry.Scheme.directedAffineCover (X : Scheme) : X.OpenCover

The directed affine open cover of X given by all affine opens.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.directedAffineCover_obj (X : Scheme) (U : ↑X.affineOpens) : X.directedAffineCover.obj U = ↑↑U

@[simp]

theorem AlgebraicGeometry.Scheme.directedAffineCover_J (X : Scheme) : X.directedAffineCover.J = ↑X.affineOpens

@[simp]

theorem AlgebraicGeometry.Scheme.directedAffineCover_map (X : Scheme) (U : ↑X.affineOpens) : X.directedAffineCover.map U = (↑U).ι

instance AlgebraicGeometry.Scheme.instPreorderJIsOpenImmersionDirectedAffineCover {X : Scheme} : Preorder X.directedAffineCover.J

Equations

• AlgebraicGeometry.Scheme.instPreorderJIsOpenImmersionDirectedAffineCover = inferInstanceAs (Preorder ↑X.affineOpens)

instance AlgebraicGeometry.Scheme.instLocallyDirectedIsOpenImmersionDirectedAffineCover {X : Scheme} : Cover.LocallyDirected X.directedAffineCover

Equations

• AlgebraicGeometry.Scheme.instLocallyDirectedIsOpenImmersionDirectedAffineCover = AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.directedAffineCover_trans {X : Scheme} {U V : ↑X.affineOpens} (hUV : U ≤ V) : Cover.trans X.directedAffineCover (CategoryTheory.homOfLE hUV) = X.homOfLE hUV