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

• AlgebraicGeometry.Scheme.AffineZariskiSite.instPreorder = Preorder.mk ⋯ ⋯ ⋯

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 = PartialOrder.mk ⋯

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, ⋯⟩

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

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

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

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

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

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

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.toPresheafedSpace) (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

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