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.

@[reducible, inline]

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

The inclusion from X.AffineZariskiSite to X.Opens.

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

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

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.

@[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.

@[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

def AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec (X : Scheme) : (toOpensFunctor X).comp (X.restrictFunctor.comp (CategoryTheory.Over.forget X)) ≅ (toOpensFunctor X).comp ((CategoryTheory.Functor.rightOp X.presheaf).comp Scheme.Spec)

The forgetful functor from X.AffineZariskiSite to Scheme is isomorphic to Spec Γ(X, -).

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_hom_app (X : Scheme) (X✝ : X.AffineZariskiSite) : (restrictIsoSpec X).hom.app X✝ = ⋯.isoSpec.hom

@[simp]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec_inv_app (X : Scheme) (X✝ : X.AffineZariskiSite) : (restrictIsoSpec X).inv.app X✝ = ⋯.isoSpec.inv

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.

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.

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.

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.{v_1, 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.

@[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.

@[simp]

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

@[simp]

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

@[simp]

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

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

"Quasi-coherent 𝒪ₓ-algebras"

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

Under this condition we can construct a family of gluing data (See relativeGluingData) and glue F into a scheme over X via (relativeGluingData _).glued, Also see the relative gluing API in Mathlib/AlgebraicGeometry/RelativeGluing.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.

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.

@[simp]

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

@[simp]

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

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway {X : Scheme} {F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat} {α : (toOpensFunctor X).op.comp X.presheaf ⟶ F} : CategoryTheory.NatTrans.Coequifibered α ↔ ∀ (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), IsLocalization.Away ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))) f) ↑(F.obj (Opposite.op (U.basicOpen f)))

@[deprecated CategoryTheory.NatTrans.Coequifibered (since := "2026-02-01")]

def AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization {J : Type u_1} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_3} C] : CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)

Alias of CategoryTheory.NatTrans.Coequifibered.

def AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData {X : Scheme} {F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat} {α : (toOpensFunctor X).op.comp X.presheaf ⟶ F} (H : CategoryTheory.NatTrans.Coequifibered α) : Cover.RelativeGluingData (directedCover X)

The relative gluing data associated to a quasi-coherent 𝒪ₓ algebra.

@[deprecated "By `inferInstance`." (since := "2026-02-01")]

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

@[deprecated "By `inferInstance`." (since := "2026-02-01")]

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

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

@[deprecated AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map (since := "2026-02-01")]

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

Alias of AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map.

@[deprecated AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι (since := "2026-02-01")]

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage {X : Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat) (α : (toOpensFunctor X).op.comp X.presheaf ⟶ F) (H : CategoryTheory.NatTrans.Coequifibered α) (U : X.AffineZariskiSite) : (TopologicalSpace.Opens.map (relativeGluingData H).toBase.base).obj ↑U = Hom.opensRange ((relativeGluingData H).cover.f U)

@[deprecated CategoryTheory.NatTrans.Coequifibered.of_isIso (since := "2026-02-01")]

theorem AlgebraicGeometry.Scheme.preservesLocalization_toOpensFunctor {J : Type u_1} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.IsIso α] : CategoryTheory.NatTrans.Coequifibered α

Alias of CategoryTheory.NatTrans.Coequifibered.of_isIso.

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

X is the colimit of its affine opens.