The small affine Zariski site

X.AffineZariskiSite is the small affine Zariski site of X, whose elements are affine open sets of X, and whose arrows are basic open sets D(f) ⟶ U for any f : Γ(X, U).

Every presieve on U is then given by a Set Γ(X, U) (presieveOfSections_surjective), and we endow X.AffineZariskiSite with grothendieckTopology X, such that s : Set Γ(X, U) is a cover if and only if Ideal.span s = ⊤ (generate_presieveOfSections_mem_grothendieckTopology).

This is a dense subsite of X.Opens (with respect to Opens.grothendieckTopology X) via the inclusion functor toOpensFunctor X, which gives an equivalence of categories of sheaves (sheafEquiv).

Note that this differs from the definition on stacks project where the arrows in the small affine Zariski site are arbitrary inclusions.

def AlgebraicGeometry.Scheme.AffineZariskiSite (X : Scheme) : Type u

X.AffineZariskiSite is the small affine Zariski site of X, whose elements are affine open sets of X, and whose arrows are basic open sets D(f) ⟶ U for any f : Γ(X, U).

Note that this differs from the definition on stacks project where the arrows in the small affine Zariski site are arbitrary inclusions.

Equations

• X.AffineZariskiSite = { U : X.Opens // AlgebraicGeometry.IsAffineOpen U }

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens {X : Scheme} (U : X.AffineZariskiSite) : X.Opens

The inclusion from X.AffineZariskiSite to X.Opens.

Equations

• U.toOpens = ↑U

instance AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder {X : Scheme} : Preorder X.AffineZariskiSite

Equations

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

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono {X : Scheme} : Monotone toOpens

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_injective {X : Scheme} : Function.Injective toOpens

instance AlgebraicGeometry.Scheme.AffineZariskiSite.instPartialOrder {X : Scheme} : PartialOrder X.AffineZariskiSite

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.instPartialOrder = { toPreorder := AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder, le_antisymm := ⋯ }

def AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen {X : Scheme} (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op U.toOpens))) : X.AffineZariskiSite

The basic open set of a section, as an element of AffineZariskiSite.

Equations

• U.basicOpen f = ⟨X.basicOpen f, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_coe {X : Scheme} (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op U.toOpens))) : ↑(U.basicOpen f) = X.basicOpen f

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_le {X : Scheme} (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op U.toOpens))) : U.basicOpen f ≤ U

def AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor (X : Scheme) : CategoryTheory.Functor X.AffineZariskiSite X.Opens

The inclusion functor from X.AffineZariskiSite to X.Opens.

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X = ⋯.functor

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor_obj (X : Scheme) (U : X.AffineZariskiSite) : (toOpensFunctor X).obj U = U.toOpens

instance AlgebraicGeometry.Scheme.AffineZariskiSite.instFaithfulOpensToOpensFunctor {X : Scheme} : (toOpensFunctor X).Faithful

instance AlgebraicGeometry.Scheme.AffineZariskiSite.instIsLocallyFullOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat {X : Scheme} : (toOpensFunctor X).IsLocallyFull (Opens.grothendieckTopology ↥X)

instance AlgebraicGeometry.Scheme.AffineZariskiSite.instIsCoverDenseOpensToOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat {X : Scheme} : (toOpensFunctor X).IsCoverDense (Opens.grothendieckTopology ↥X)

def AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology (X : Scheme) : CategoryTheory.GrothendieckTopology X.AffineZariskiSite

The Grothendieck topology on X.AffineZariskiSite induced from the topology on X.Opens. Also see mem_grothendieckTopology_iff_sectionsOfPresieve.

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X = (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).inducedTopology (Opens.grothendieckTopology ↥X)

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology {X : Scheme} {U : X.AffineZariskiSite} {S : CategoryTheory.Sieve U} : S ∈ (grothendieckTopology X) U ↔ ∀ x ∈ U.toOpens, ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens

instance AlgebraicGeometry.Scheme.AffineZariskiSite.instIsDenseSubsiteOpensCarrierCarrierCommRingCatGrothendieckTopologyGrothendieckTopologyToOpensFunctor {X : Scheme} : CategoryTheory.Functor.IsDenseSubsite (grothendieckTopology X) (Opens.grothendieckTopology ↥X) (toOpensFunctor X)

def AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections {X : Scheme} (U : X.AffineZariskiSite) (s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))) : CategoryTheory.Presieve U

The presieve associated to a set of sections. This is a surjection, see presieveOfSections_surjective.

Equations

• U.presieveOfSections s x✝ = ∃ f ∈ s, X.basicOpen f = V.toOpens

def AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve {X : Scheme} {U : X.AffineZariskiSite} (P : CategoryTheory.Presieve U) : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))

The set of sections associated to a presieve.

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve P = {f : ↑(X.presheaf.obj (Opposite.op U.toOpens)) | P (CategoryTheory.homOfLE ⋯)}

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve {X : Scheme} {U : X.AffineZariskiSite} (P : CategoryTheory.Presieve U) : U.presieveOfSections (sectionsOfPresieve P) = P

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective {X : Scheme} {U : X.AffineZariskiSite} : Function.Surjective U.presieveOfSections

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows {X : Scheme} (U : X.AffineZariskiSite) (s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))) : U.presieveOfSections s = CategoryTheory.Presieve.ofArrows (fun (i : ↑s) => U.basicOpen ↑i) fun (i : ↑s) => CategoryTheory.homOfLE ⋯

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections {X : Scheme} {U V : X.AffineZariskiSite} {s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))} {f : V ⟶ U} : (CategoryTheory.Sieve.generate (U.presieveOfSections s)).arrows f ↔ ∃ f ∈ s, ∃ (g : ↑(X.presheaf.obj (Opposite.op U.toOpens))), X.basicOpen (f * g) = V.toOpens

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology {X : Scheme} {U : X.AffineZariskiSite} {s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))} : CategoryTheory.Sieve.generate (U.presieveOfSections s) ∈ (grothendieckTopology X) U ↔ Ideal.span s = ⊤

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve {X : Scheme} {U : X.AffineZariskiSite} {S : CategoryTheory.Sieve U} : S ∈ (grothendieckTopology X) U ↔ Ideal.span (sectionsOfPresieve S.arrows) = ⊤

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.AffineZariskiSite.sheafEquiv {X : Scheme} {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [∀ (U : X.Opensᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow U (toOpensFunctor X).op) A] : CategoryTheory.Sheaf (grothendieckTopology X) A ≌ TopCat.Sheaf A ↑X.toPresheafedSpace

The category of sheaves on X.AffineZariskiSite is equivalent to the categories of sheaves over X.

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.sheafEquiv = (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).sheafInducedTopologyEquivOfIsCoverDense (Opens.grothendieckTopology ↥X) A

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover (X : Scheme) : X.OpenCover

The directed cover of a scheme indexed by X.AffineZariskiSite. Note the related Scheme.directedAffineCover, which has the same (defeq) cover but a different category instance on the indices.

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X = { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) => ↑↑U, f := fun (U : X.AffineZariskiSite) => (↑U).ι, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_f (X : Scheme) (U : X.AffineZariskiSite) : (directedCover X).f U = (↑U).ι

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_X (X : Scheme) (U : X.AffineZariskiSite) : (directedCover X).X U = ↑↑U

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_I₀ (X : Scheme) : (directedCover X).I₀ = X.AffineZariskiSite

noncomputable instance AlgebraicGeometry.Scheme.AffineZariskiSite.instLocallyDirectedIsOpenImmersionDirectedCover {X : Scheme} : Cover.LocallyDirected (directedCover X)

Equations

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

noncomputable def AlgebraicGeometry.Scheme.AffineZariskiSite.cocone (X : Scheme) : CategoryTheory.Limits.Cocone ((toOpensFunctor X).comp ((CategoryTheory.Functor.rightOp X.presheaf).comp Scheme.Spec))

X is the colimit of its affine opens. See isColimit_cocone below.

Equations

• AlgebraicGeometry.Scheme.AffineZariskiSite.cocone X = { pt := X, ι := { app := fun (U : X.AffineZariskiSite) => ⋯.fromSpec, naturality := ⋯ } }

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_ι_app (X : Scheme) (U : X.AffineZariskiSite) : (cocone X).ι.app U = ⋯.fromSpec

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt (X : Scheme) : (cocone X).pt = X

def AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization {X : Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat) (α : (toOpensFunctor X).op.comp X.presheaf ⟶ F) : Prop

A presheaf F of rings on X.AffineZariskiSite with a structural morphism α : 𝒪ₓ ⟶ F is said to PreservesLocalization if F(D(f)) = F(U)[1/f] for every open U and any section f : Γ(X, U).

Under this condition we can glue F into a scheme over X via colimit F.rightOp ⋙ Scheme.Spec, if one first have := H.isLocallyDirected; have := H.isOpenImmersion. Also see the locally directed gluing API in Mathlib/AlgebraicGeometry/Gluing.lean.

This is closely related to the notion of quasi-coherent 𝒪ₓ-algebras, and we shall link them together once the theory of quasi-coherent 𝒪ₓ-algebras are developed.

Equations

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

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isLocallyDirected {X : Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat) (α : (toOpensFunctor X).op.comp X.presheaf ⟶ F) (H : PreservesLocalization F α) : ((F.rightOp.comp Scheme.Spec).comp forget).IsLocallyDirected

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isOpenImmersion {X : Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat) (α : (toOpensFunctor X).op.comp X.presheaf ⟶ F) (H : PreservesLocalization F α) ⦃U V : X.AffineZariskiSite⦄ (f : U ⟶ V) : IsOpenImmersion ((F.rightOp.comp Scheme.Spec).map f)

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map {X : Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat) (α : (toOpensFunctor X).op.comp X.presheaf ⟶ F) (H : PreservesLocalization F α) {U : X.AffineZariskiSite} (r : ↑(X.presheaf.obj (Opposite.op ↑U))) : Hom.opensRange ((F.rightOp.comp Scheme.Spec).map (CategoryTheory.homOfLE ⋯)) = PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))) r)

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage {X : Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat) (α : (toOpensFunctor X).op.comp X.presheaf ⟶ F) (H : PreservesLocalization F α) (U : X.AffineZariskiSite) : (TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.desc (F.rightOp.comp Scheme.Spec) { pt := X, ι := CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.rightOp α) Scheme.Spec) (cocone X).ι }).base).obj ↑U = Hom.opensRange (CategoryTheory.Limits.colimit.ι (F.rightOp.comp Scheme.Spec) U)

theorem AlgebraicGeometry.Scheme.preservesLocalization_toOpensFunctor {X : Scheme} : AffineZariskiSite.PreservesLocalization ((AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf) (CategoryTheory.CategoryStruct.id ((AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf))

noncomputable def AlgebraicGeometry.Scheme.AffineZariskiSite.isColimitCocone (X : Scheme) : CategoryTheory.Limits.IsColimit (cocone X)

X is the colimit of its affine opens.

Equations

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