Affine étale site

In this file we define the small affine étale site of a scheme S. The underlying category is the category of commutative rings R equipped with an étale structure morphism Spec R ⟶ S. We show that this category is essentially small, that it is a dense subsite of the small étale site, and that it is 1-hypercover dense, which allows to show that if S : Scheme.{u}, then we can sheafify étale presheaves with values in Type u, AddCommGrpCat.{u}, etc.

Main results

• AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv: The category of sheaves on the small affine étale site is equivalent to the category of schemes on the small étale site.
• AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_smallEtaleTopology: The category of sheaves on the étale site with values in a Grothendieck abelian category is Grothendieck abelian.

def AlgebraicGeometry.Scheme.AffineEtale (S : Scheme) : Type (u + 1)

The small affine étale site: The category of affine schemes étale over S, whose objects are commutative rings R with an étale structure morphism Spec R ⟶ S.

Equations

• S.AffineEtale = CategoryTheory.MorphismProperty.CostructuredArrow @AlgebraicGeometry.Etale ⊤ AlgebraicGeometry.Scheme.Spec S

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instCategoryAffineEtale (S : Scheme) : CategoryTheory.Category.{u_1, u_1 + 1} S.AffineEtale

Equations

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

instance AlgebraicGeometry.Scheme.instHasPullbacksAffineEtale (S : Scheme) : CategoryTheory.Limits.HasPullbacks S.AffineEtale

noncomputable def AlgebraicGeometry.Scheme.AffineEtale.mk {S : Scheme} {R : CommRingCat} (f : Spec R ⟶ S) [Etale f] : S.AffineEtale

Construct an object of the small affine étale site.

Equations

• AlgebraicGeometry.Scheme.AffineEtale.mk f = CategoryTheory.MorphismProperty.CostructuredArrow.mk ⊤ f inst✝

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.mk_hom {S : Scheme} {R : CommRingCat} (f : Spec R ⟶ S) [Etale f] : (AffineEtale.mk f).hom = f

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.mk_right_as {S : Scheme} {R : CommRingCat} (f : Spec R ⟶ S) [Etale f] : (AffineEtale.mk f).right.as = PUnit.unit

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.mk_left {S : Scheme} {R : CommRingCat} (f : Spec R ⟶ S) [Etale f] : (AffineEtale.mk f).left = Opposite.op R

noncomputable def AlgebraicGeometry.Scheme.AffineEtale.Spec (S : Scheme) : CategoryTheory.Functor S.AffineEtale S.Etale

The Spec functor from the small affine étale site of S to the small étale site of S.

Equations

• AlgebraicGeometry.Scheme.AffineEtale.Spec S = CategoryTheory.MorphismProperty.CostructuredArrow.toOver (@AlgebraicGeometry.Etale) AlgebraicGeometry.Scheme.Spec S

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.Spec_map_left (S : Scheme) {X✝ Y✝ : CategoryTheory.MorphismProperty.CostructuredArrow @Etale ⊤ Scheme.Spec S} (f : X✝ ⟶ Y✝) : ((AffineEtale.Spec S).map f).left = Spec.map f.left.unop

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.Spec_obj_left (S : Scheme) (A : CategoryTheory.MorphismProperty.CostructuredArrow @Etale ⊤ Scheme.Spec S) : ((AffineEtale.Spec S).obj A).left = Spec (Opposite.unop A.left)

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.Spec_obj_hom (S : Scheme) (A : CategoryTheory.MorphismProperty.CostructuredArrow @Etale ⊤ Scheme.Spec S) : ((AffineEtale.Spec S).obj A).hom = A.hom

instance AlgebraicGeometry.Scheme.AffineEtale.instFaithfulEtaleSpec {S : Scheme} : (AffineEtale.Spec S).Faithful

instance AlgebraicGeometry.Scheme.AffineEtale.instFullEtaleSpec {S : Scheme} : (AffineEtale.Spec S).Full

instance AlgebraicGeometry.Scheme.AffineEtale.instIsCoverDenseEtaleSpecSmallEtaleTopology {S : Scheme} : (AffineEtale.Spec S).IsCoverDense S.smallEtaleTopology

noncomputable def AlgebraicGeometry.Scheme.AffineEtale.topology (S : Scheme) : CategoryTheory.GrothendieckTopology S.AffineEtale

The topology on the small affine étale site is the topology induced by Spec from the small étale site.

Equations

• AlgebraicGeometry.Scheme.AffineEtale.topology S = (AlgebraicGeometry.Scheme.AffineEtale.Spec S).inducedTopology S.smallEtaleTopology

instance AlgebraicGeometry.Scheme.AffineEtale.instIsDenseSubsiteEtaleTopologySmallEtaleTopologySpec {S : Scheme} : CategoryTheory.Functor.IsDenseSubsite (topology S) S.smallEtaleTopology (AffineEtale.Spec S)

instance AlgebraicGeometry.Scheme.AffineEtale.instIsOneHypercoverDenseEtaleSpecTopologySmallEtaleTopology {S : Scheme} : (AffineEtale.Spec S).IsOneHypercoverDense (topology S) S.smallEtaleTopology

instance AlgebraicGeometry.Scheme.AffineEtale.instEssentiallySmall {S : Scheme} : CategoryTheory.EssentiallySmall.{u, u, u + 1} S.AffineEtale

instance AlgebraicGeometry.Scheme.instHasSheafifyAffineEtaleTopology {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : CategoryTheory.HasSheafify (AffineEtale.topology S) A

instance AlgebraicGeometry.Scheme.instIsEquivalenceSheafEtaleSmallEtaleTopologyAffineEtaleTopologySheafPushforwardContinuousSpec {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A] : ((AffineEtale.Spec S).sheafPushforwardContinuous A (AffineEtale.topology S) S.smallEtaleTopology).IsEquivalence

instance AlgebraicGeometry.Scheme.instHasSheafifyEtaleSmallEtaleTopology {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : CategoryTheory.HasSheafify S.smallEtaleTopology A

instance AlgebraicGeometry.Scheme.instIsEquivalenceSheafEtaleSmallEtaleTopologyAffineEtaleTopologySheafPushforwardContinuousSpec_1 {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A] : ((AffineEtale.Spec S).sheafPushforwardContinuous A (AffineEtale.topology S) S.smallEtaleTopology).IsEquivalence

instance AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveAffineEtaleTopology {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : (AffineEtale.topology S).WEqualsLocallyBijective A

instance AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveEtaleSmallEtaleTopology {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] : S.smallEtaleTopology.WEqualsLocallyBijective A

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instAbelianSheafAffineEtaleTopology {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] : CategoryTheory.Abelian (CategoryTheory.Sheaf (AffineEtale.topology S) A)

Equations

• AlgebraicGeometry.Scheme.instAbelianSheafAffineEtaleTopology = inferInstance

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instAbelianSheafEtaleSmallEtaleTopology {S : Scheme} {A : Type u'} [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] : CategoryTheory.Abelian (CategoryTheory.Sheaf S.smallEtaleTopology A)

Equations

• AlgebraicGeometry.Scheme.instAbelianSheafEtaleSmallEtaleTopology = inferInstance

noncomputable def AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv (S : Scheme) (A : Type u') [CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A] : CategoryTheory.Sheaf (topology S) A ≌ CategoryTheory.Sheaf S.smallEtaleTopology A

The category of sheaves on the small affine étale site is equivalent to the category of sheaves on the small étale site.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv_inverse (S : Scheme) (A : Type u') [CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A] : (sheafEquiv S A).inverse = (AffineEtale.Spec S).sheafPushforwardContinuous A (topology S) S.smallEtaleTopology

instance AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_affineEtaleTopology (S : Scheme) (A : Type u') [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{u, u, u'} A] : CategoryTheory.IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (CategoryTheory.Sheaf (AffineEtale.topology S) A)

instance AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_smallEtaleTopology (S : Scheme) (A : Type u') [CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1} {CD : A → Type u} [(X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)] [CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{u, u, u'} A] : CategoryTheory.IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u} (CategoryTheory.Sheaf S.smallEtaleTopology A)