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 (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] : Type (max (max u u_1) v_1)

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 : 𝒰.I₀} (hij : i ⟶ j) : 𝒰.X i ⟶ 𝒰.X j

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

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

def AlgebraicGeometry.Scheme.Cover.trans {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j) : 𝒰.X i ⟶ 𝒰.X 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 (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j) : CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.f j) = 𝒰.f i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.trans_id {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] (i : 𝒰.I₀) : 𝒰.trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i)

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.trans_comp {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j k : 𝒰.I₀} (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 (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))) : ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯).base) y = x

theorem AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j : 𝒰.I₀} (xi : ↥(𝒰.X i)) (xj : ↥(𝒰.X j)) (h : (CategoryTheory.ConcreteCategory.hom (𝒰.f i).base) xi = (CategoryTheory.ConcreteCategory.hom (𝒰.f j).base) xj) : ∃ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (xk : ↥(𝒰.X k)), (CategoryTheory.ConcreteCategory.hom (𝒰.trans fi).base) xk = xi ∧ (CategoryTheory.ConcreteCategory.hom (𝒰.trans fj).base) xk = xj

theorem AlgebraicGeometry.Scheme.Cover.exists_of_trans_eq_trans {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {i j k : 𝒰.I₀} (fi : i ⟶ k) (fj : j ⟶ k) (xi : ↥(𝒰.X i)) (xj : ↥(𝒰.X j)) (h : (CategoryTheory.ConcreteCategory.hom (𝒰.trans fi).base) xi = (CategoryTheory.ConcreteCategory.hom (𝒰.trans fj).base) xj) : ∃ (l : 𝒰.I₀) (fli : l ⟶ i) (flj : l ⟶ j) (x : ↥(𝒰.X l)), (CategoryTheory.ConcreteCategory.hom (𝒰.trans fli).base) x = xi ∧ (CategoryTheory.ConcreteCategory.hom (𝒰.trans flj).base) x = xj

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

def AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.I₀) : Cover (precoverage P) (CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f 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_f {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.I₀) (k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)) : (𝒰.intersectionOfLocallyDirected i j).f 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 (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] : CategoryTheory.Functor 𝒰.I₀ Scheme

The canonical diagram induced by a locally directed cover.

Equations

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] (i : 𝒰.I₀) : 𝒰.functorOfLocallyDirected.obj i = 𝒰.X i

instance AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] : (𝒰.functorOfLocallyDirected.comp forget).IsLocallyDirected

def AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] : 𝒰.functorOfLocallyDirected ⟶ (CategoryTheory.Functor.const 𝒰.I₀).obj X

The structure maps to S as a natural transformation.

Equations

• 𝒰.functorOfLocallyDirectedHomBase = { app := fun (i : 𝒰.I₀) => 𝒰.f i, naturality := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase_app {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] (i : 𝒰.I₀) : 𝒰.functorOfLocallyDirectedHomBase.app i = 𝒰.f i

def AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.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, ι := 𝒰.functorOfLocallyDirectedHomBase }

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ι {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [𝒰.LocallyDirected] : 𝒰.coconeOfLocallyDirected.ι = 𝒰.functorOfLocallyDirectedHomBase

instance AlgebraicGeometry.Scheme.Cover.instCategoryI₀Pullback₁ {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [P.IsStableUnderBaseChange] (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] {Y : Scheme} (f : Y ⟶ X) : CategoryTheory.Category.{v_2, u_1} (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀

Equations

• 𝒰.instCategoryI₀Pullback₁ f = inferInstanceAs (CategoryTheory.Category.{?u.51, ?u.49} 𝒰.I₀)

instance AlgebraicGeometry.Scheme.Cover.locallyDirectedPullbackCover {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} [P.IsStableUnderBaseChange] (𝒰 : Cover (precoverage P) X) [CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [𝒰.LocallyDirected] {Y : Scheme} (f : Y ⟶ X) : LocallyDirected (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰)

Equations

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

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

instance AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {i j : 𝒰.I₀} (f : i ⟶ j) : IsOpenImmersion ((Cover.functorOfLocallyDirected 𝒰).map f)

def AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (h : ∀ {i j : 𝒰.I₀} (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.{v_1, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : Scheme} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphismsOfLocallyDirected g ⋯) = g i

@[simp]

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

def AlgebraicGeometry.Scheme.OpenCover.isColimitCoconeOfLocallyDirected {X : Scheme} (𝒰 : X.OpenCover) [CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [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.{v_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f 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.{v_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (𝒰.f 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.{v_2, u_1} 𝒰.I₀] [Cover.LocallyDirected 𝒰] {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (Cover.trans 𝒰 hij) (g j) = g i) (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom) (i : 𝒰.I₀) {Z : Scheme} (h✝ : Y.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.f 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 𝒰.I₀] (hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)) (H : TopologicalSpace.Opens.IsBasis (Set.range fun (i : 𝒰.I₀) => Hom.opensRange (𝒰.f 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 𝒰.I₀] (hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)) (i j : 𝒰.I₀) : i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)

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

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

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

Equations

• X.directedAffineCover = { I₀ := ↑X.affineOpens, X := fun (U : ↑X.affineOpens) => ↑↑U, f := fun (U : ↑X.affineOpens) => (↑U).ι, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.directedAffineCover_I₀ (X : Scheme) : X.directedAffineCover.I₀ = ↑X.affineOpens

@[simp]

theorem AlgebraicGeometry.Scheme.directedAffineCover_f (X : Scheme) (U : ↑X.affineOpens) : X.directedAffineCover.f U = (↑U).ι

@[simp]

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

instance AlgebraicGeometry.Scheme.instPreorderI₀DirectedAffineCover {X : Scheme} : Preorder X.directedAffineCover.I₀

Equations

• AlgebraicGeometry.Scheme.instPreorderI₀DirectedAffineCover = 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