66.19 Points of the small étale… to 66.33 Morphisms towards schemes

Section66.19 Points of the small étale site #

Section 66.19 of the Stacks Project, Tag 04JU. 14 tags here are carried by 46 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0486, a definition

Tag 0486 in the Stacks Project.

AlgebraicGeometry.Space.geometricPointOfSpecHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPointOfSpecHom.lean, line 57. The attribute's comment: “part (1): a geometric point of a representable algebraic space”.

For an object U of the big fppf site over S, an algebraically closed field Ω whose spectrum the site contains, a morphism tb : Spec Ω ⟶ S and a morphism of schemes σ : Spec Ω ⟶ U over tb, the geometric point of yoneda.obj U whose field is Ω, whose structure morphism to S is tb and whose section is σ.

def geometricPointOfSpecHom (U : BigFppfOver B S hS) {Ω : Type u} [Field Ω] [IsAlgClosed Ω]
    (hΩ : B.Contains (Spec (.of Ω))) (tb : Spec (.of Ω) ⟶ S)
    (σ : Spec (.of Ω) ⟶ (BigFppfOver.toScheme B S hS).obj U)
    (hσ : σ ≫ B.inclusion.map U.hom = tb) :
    GeometricPoint B S hS (yoneda.obj U)

AlgebraicGeometry.Space.GeometricPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/GeometricPoints.lean, line 75. The attribute's comment: “part (1): geometric point”.

A morphism from the spectrum of an algebraically closed field to a presheaf over a scheme. For an algebraic space this is a geometric point.

abbrev GeometricPoint (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Type (u + 1)

AlgebraicGeometry.Space.GeometricPoint.image, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/GeometricPoints.lean, line 81. The attribute's comment: “part (2): image point”.

The point of the algebraic space represented by a geometric point.

abbrev GeometricPoint.image {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (p : GeometricPoint B S hS F) :
    points B S hS F

AlgebraicGeometry.Space.GeometricPoint.LiesOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/GeometricPoints.lean, line 87. The attribute's comment: “part (2): lying over a point”.

A geometric point lies over its image point in the underlying point set.

abbrev GeometricPoint.LiesOver {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (p : GeometricPoint B S hS F)
    (x : points B S hS F) : Prop

Tag 04JV, a definition

Tag 04JV in the Stacks Project.

AlgebraicGeometry.Space.EtaleNeighborhood, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/GeometricPoints.lean, line 94. The attribute's comment: “part (1): étale neighborhoods”. References: SGA 4½ Arcata (2.3.1), “étale neighbourhood”.

An étale neighbourhood of a geometric point of an algebraic space, with a chosen lift from the same field spectrum as the given geometric point.

structure EtaleNeighborhood (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hF : IsAlgebraicSpace B S hS F)
    (x : GeometricPoint B S hS F)

AlgebraicGeometry.Space.EtaleNeighborhood.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/GeometricPoints.lean, line 120. The attribute's comment: “part (2): morphisms of étale neighborhoods”.

A map of étale neighbourhoods over the fixed algebraic space which carries the chosen lift to the chosen lift.

structure Hom (U V : EtaleNeighborhood B S hS F hF x)

Tag 04JW, a lemma

Tag 04JW in the Stacks Project.

AlgebraicGeometry.Space.EtaleNeighborhood.exists_common_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleNeighborhood.lean, line 182. The attribute's comment: “common_refinement”.

Two étale neighbourhoods of a geometric point have a common refinement.

theorem exists_common_refinement (U V : EtaleNeighborhood B S hS F hF x) :
    ∃ W : EtaleNeighborhood B S hS F hF x, Nonempty ((W ⟶ U) × (W ⟶ V))

AlgebraicGeometry.Space.EtaleNeighborhood.exists_equalizing_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleNeighborhood.lean, line 227. The attribute's comment: “equalizing_refinement”.

Two parallel morphisms of étale neighbourhoods of a geometric point are equalized by a further étale neighbourhood.

theorem exists_equalizing_refinement {U V : EtaleNeighborhood B S hS F hF x} (h₁ h₂ : U ⟶ V) :
    ∃ (W : EtaleNeighborhood B S hS F hF x) (h : W ⟶ U), h ≫ h₁ = h ≫ h₂

AlgebraicGeometry.Space.EtaleNeighborhood.exists_smallEtaleNeighborhood_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleNeighborhood.lean, line 318. The attribute's comment: “scheme_refinement, in the small étale site”.

Every étale neighbourhood of a geometric point is refined by one coming from the small étale site, i.e. by one in the image of AlgebraicGeometry.Space.EtaleNeighborhood.ofSmallEtale.

theorem exists_smallEtaleNeighborhood_refinement (U : EtaleNeighborhood B S hS F hF x) :
    ∃ V : SmallEtaleNeighborhood x, Nonempty ((ofSmallEtale hF x).obj V ⟶ U)

AlgebraicGeometry.Space.exists_scheme_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/GeometricPoints.lean, line 167. The attribute's comment: “scheme_refinement”.

Every étale neighbourhood of a geometric point admits a refinement by a scheme.

theorem exists_scheme_refinement (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F)
    (x : GeometricPoint B S hS F)
    (U : EtaleNeighborhood B S hS F hF x) :
    ∃ (U' : EtaleNeighborhood B S hS F hF x),
      ∃ (_f : U' ⟶ U), U'.space.IsRepresentable

Tag 05VN, a lemma

Tag 05VN in the Stacks Project.

AlgebraicGeometry.Space.exists_geometricPoint_lift_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPointEtaleLift.lean, line 171.

A geometric point lifts along an étale morphism of algebraic spaces to any specified point of the source above its image, without extending its field.

theorem exists_geometricPoint_lift_of_isEtale
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {U X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hU : IsAlgebraicSpace B S hS U)
    (hX : IsAlgebraicSpace B S hS X)
    (φ : U ⟶ X) (hφ : IsEtale B S hS φ)
    (xbar : GeometricPoint B S hS X)
    (u : points B S hS U)
    (hu : pointsMap B S hS U φ u = xbar.image) :
    ∃ ubar : GeometricPoint B S hS U,
      ubar.LiesOver u ∧
        FieldValuedPoint.map B S hS U φ ubar.val = xbar.val

Tag 04JX, a lemma

Tag 04JX in the Stacks Project.

AlgebraicGeometry.Space.exists_lift_to_etaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleNeighborhood.lean, line 429.

A covering of an étale neighbourhood U of a geometric point x of an algebraic space X, taken in the spaces-étale site of X, has a member to which x lifts; that member, with the lift, is again an étale neighbourhood of x, and the covering arrow is a morphism of étale neighbourhoods.

theorem exists_lift_to_etaleCovering (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS) (x : GeometricPoint B S hS X.1)
    (U : EtaleNeighborhood B S hS X.1 X.2 x)
    (E : PreZeroHypercover.{u + 1} (etaleSiteObjectOfNeighborhood B S hS X x U))
    (hE : SpacesEtale.IsCovering B S hS X
      ⟨etaleSiteObjectOfNeighborhood B S hS X x U, E⟩) :
    ∃ i : E.I₀,
      ∃ uiBar : ((SpacesEtale.toSpaces B S hS X).obj (E.X i)).1.obj
        (Opposite.op x.val.siteObject),
      ∃ huiBar : (((SpacesEtale.inclusion B S hS X).obj (E.X i)).hom.hom).app
          (Opposite.op x.val.siteObject) uiBar = x.val.value,
      ∃ φ : etaleNeighborhoodOfSitePoint B S hS X x (E.X i) uiBar huiBar ⟶ U,
        EtaleNeighborhood.Hom.hom φ =
          ((SpacesEtale.toSpaces B S hS X).map (E.f i)).hom

Tag 04JY, a definition

Tag 04JY in the Stacks Project.

AlgebraicGeometry.Space.yonedaIdentityNeighborhood, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingFieldSpace.lean, line 84. The attribute's comment: “the identity chart of a representable algebraic space”.

A representable algebraic space is its own pointed étale chart. The identity of yoneda.obj X is an étale chart, and it is a small étale neighbourhood of every geometric point of yoneda.obj X: the section defining the point is itself the required lift.

abbrev yonedaIdentityNeighborhood (X : BigFppfOver B S hS)
    (w : GeometricPoint B S hS (yoneda.obj X)) : SmallEtaleNeighborhood w

AlgebraicGeometry.Space.stalk, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPoints.lean, line 164. The attribute's comment: “category-valued stalk”.

The stalk of a presheaf on the small étale site at a geometric point, formed as the colimit of its sections over the small étale neighbourhoods of that point.

noncomputable abbrev stalk {C : Type w} [Category.{v} C] (x : GeometricPoint B S hS F)
    (P : (SmallEtale B S hS F)ᵒᵖ ⥤ C)
    [HasColimit (SmallEtaleNeighborhood.sections (x := x) P)] : C

AlgebraicGeometry.Space.stalkFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPoints.lean, line 171. The attribute's comment: “stalk functor”.

The stalk at a geometric point, as a functor of the presheaf.

noncomputable def stalkFunctor (C : Type w) [Category.{v} C] (x : GeometricPoint B S hS F)
    [HasColimitsOfShape (SmallEtaleNeighborhood x)ᵒᵖ C] :
    ((SmallEtale B S hS F)ᵒᵖ ⥤ C) ⥤ C

AlgebraicGeometry.Space.stalkSet, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPoints.lean, line 201. The attribute's comment: “set-valued stalk”.

The set-valued stalk at a geometric point, formed as the quotient colimit CategoryTheory.Functor.ColimitType, with no smallness assumption on the neighbourhood category.

abbrev stalkSet (x : GeometricPoint B S hS F) (P : (SmallEtale B S hS F)ᵒᵖ ⥤ Type w) :
    Type _

AlgebraicGeometry.Space.stalkSetFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPoints.lean, line 230. The attribute's comment: “set-valued stalk functor”.

The set-valued stalk at a geometric point, as a functor of the presheaf.

def stalkSetFunctor (x : GeometricPoint B S hS F) :
    ((SmallEtale B S hS F)ᵒᵖ ⥤ Type w) ⥤ Type (max (u + 1) w)

Tag 04JZ, an equation

Tag 04JZ in the Stacks Project.

AlgebraicGeometry.Space.stalkSpacesEtaleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleStalk.lean, line 185.

Stacks 04JZ. The small-site stalk at a geometric point is the colimit of sections over all étale algebraic-space neighbourhoods of that point, naturally in the presheaf on the spaces-étale site.

noncomputable def stalkSpacesEtaleIso :
    ((Functor.whiskeringLeft (SmallEtale B S hS X.1)ᵒᵖ (SpacesEtale B S hS X)ᵒᵖ
        (Type w)).obj (comparisonFunctor B S hS X).op ⋙ stalkSetFunctor x) ≅
      spacesStalkSetFunctor x

Tag 04K0, a lemma

Tag 04K0 in the Stacks Project.

AlgebraicGeometry.Space.etaleSitePoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSitePoint.lean, line 286. The attribute's comment: “the point of the site”.

The point of the small étale site of an algebraic space determined by a geometric point of it: its fibre functor is the functor of lifts of the geometric point into the étale scheme charts.

noncomputable def etaleSitePoint (x : GeometricPoint B S hS F)
    (hF : IsAlgebraicSpace B S hS F) : (SmallEtale.topology B S hS F).Point.{u}

AlgebraicGeometry.Space.etaleSitePoint_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSitePoint.lean, line 296. The attribute's comment: “the fibre functor”.

The fibre functor of the point of the small étale site determined by a geometric point is the geometric fibre functor.

theorem etaleSitePoint_fiber (x : GeometricPoint B S hS F)
    (hF : IsAlgebraicSpace B S hS F) :
    (etaleSitePoint B S hS F x hF).fiber = geometricFiber B S hS F x

AlgebraicGeometry.Space.etaleSitePointStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSitePoint.lean, line 330. The attribute's comment: “the stalk comparison”.

The stalk at the point of the small étale site determined by a geometric point is isomorphic to the geometric stalk, naturally in the presheaf.

noncomputable def etaleSitePointStalkIso (x : GeometricPoint B S hS F)
    (hF : IsAlgebraicSpace B S hS F) :
    (etaleSitePoint B S hS F x hF).presheafFiber (A := Type (u + 1)) ≅
      stalkSetFunctor x

Tag 04K1, a lemma

Tag 04K1 in the Stacks Project.

AlgebraicGeometry.Space.presheafAbelianStalk_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 897. The attribute's comment: “part (1): finite limits”.

Stacks 04K1, part (1). The geometric stalk of a presheaf of abelian groups on the small étale site is left exact.

theorem presheafAbelianStalk_preservesFiniteLimits (x : GeometricPoint B S hS X) :
    PreservesFiniteLimits (stalkFunctor AddCommGrpCat.{max (u + 1) w} x)

AlgebraicGeometry.Space.presheafAbelianStalk_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 910. The attribute's comment: “part (1): finite colimits”.

Stacks 04K1, part (1). The geometric stalk of a presheaf of abelian groups on the small étale site is right exact.

theorem presheafAbelianStalk_preservesFiniteColimits (x : GeometricPoint B S hS X) :
    PreservesFiniteColimits (stalkFunctor AddCommGrpCat.{max (u + 1) w} x)

AlgebraicGeometry.Space.stalkSetMap_toSheafify_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 926. The attribute's comment: “part (2): sheafification comparison”.

Stacks 04K1, part (2). Sheafification does not change the geometric stalk of a presheaf of sets: the comparison induced by the unit of sheafification is an isomorphism.

theorem stalkSetMap_toSheafify_isIso (x : GeometricPoint B S hS X)
    (P : (SmallEtale B S hS X)ᵒᵖ ⥤ Type (max (u + 1) w)) :
    IsIso ((stalkSetFunctor x).map
      ((SmallEtale.topology B S hS X).toSheafify P))

AlgebraicGeometry.Space.sheafAbelianStalk_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 959. The attribute's comment: “part (3): finite limits”.

Stacks 04K1, part (3). The geometric stalk of a sheaf of abelian groups on the small étale site is left exact.

theorem sheafAbelianStalk_preservesFiniteLimits (x : GeometricPoint B S hS X) :
    PreservesFiniteLimits
      (sheafToPresheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{max (u + 1) w} ⋙
        stalkFunctor AddCommGrpCat.{max (u + 1) w} x)

AlgebraicGeometry.Space.sheafAbelianStalk_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 975. The attribute's comment: “part (3): finite colimits”.

Stacks 04K1, part (3). The geometric stalk of a sheaf of abelian groups on the small étale site is right exact.

theorem sheafAbelianStalk_preservesFiniteColimits (x : GeometricPoint B S hS X) :
    PreservesFiniteColimits
      (sheafToPresheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{max (u + 1) w} ⋙
        stalkFunctor AddCommGrpCat.{max (u + 1) w} x)

AlgebraicGeometry.Space.presheafSetStalk_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 997. The attribute's comment: “part (4): presheaf sets, finite limits”.

Stacks 04K1, part (4). The geometric stalk of a presheaf of sets on the small étale site preserves finite limits.

theorem presheafSetStalk_preservesFiniteLimits (x : GeometricPoint B S hS X) :
    PreservesFiniteLimits
      (stalkSetFunctor x : ((SmallEtale B S hS X)ᵒᵖ ⥤ Type w) ⥤ Type (max (u + 1) w))

AlgebraicGeometry.Space.presheafSetStalk_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 1010. The attribute's comment: “part (4): presheaf sets, finite colimits”.

Stacks 04K1, part (4). The geometric stalk of a presheaf of sets on the small étale site preserves finite colimits.

theorem presheafSetStalk_preservesFiniteColimits (x : GeometricPoint B S hS X) :
    PreservesFiniteColimits
      (stalkSetFunctor x : ((SmallEtale B S hS X)ᵒᵖ ⥤ Type w) ⥤ Type (max (u + 1) w))

AlgebraicGeometry.Space.presheafSetStalk_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 1023. The attribute's comment: “part (4): presheaf sets, colimits”.

Stacks 04K1, part (4). The geometric stalk of a presheaf of sets on the small étale site commutes with arbitrary colimits of presheaves.

theorem presheafSetStalk_preservesColimits (x : GeometricPoint B S hS X) :
    PreservesColimitsOfSize.{w, w}
      (stalkSetFunctor x : ((SmallEtale B S hS X)ᵒᵖ ⥤ Type w) ⥤ Type (max (u + 1) w))

AlgebraicGeometry.Space.sheafSetStalk_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 1042. The attribute's comment: “part (4): sheaves of sets, finite limits”.

Stacks 04K1, part (4). The geometric stalk of a sheaf of sets on the small étale site preserves finite limits.

theorem sheafSetStalk_preservesFiniteLimits (x : GeometricPoint B S hS X) :
    PreservesFiniteLimits
      (sheafToPresheaf (SmallEtale.topology B S hS X) (Type w) ⋙ stalkSetFunctor x)

AlgebraicGeometry.Space.sheafSetStalk_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 1051. The attribute's comment: “part (4): sheaves of sets, finite colimits”.

Stacks 04K1, part (4). The geometric stalk of a sheaf of sets on the small étale site preserves finite colimits.

theorem sheafSetStalk_preservesFiniteColimits (x : GeometricPoint B S hS X) :
    PreservesFiniteColimits
      (sheafToPresheaf (SmallEtale.topology B S hS X) (Type (max (u + 1) w)) ⋙
        stalkSetFunctor x)

AlgebraicGeometry.Space.sheafSetStalk_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 1068. The attribute's comment: “part (4): sheaves of sets, colimits”. References: SGA 4 VIII (3.5), “3.5 a)”.

Stacks 04K1, part (4). The geometric stalk of a sheaf of sets on the small étale site commutes with arbitrary colimits of sheaves.

theorem sheafSetStalk_preservesColimits (x : GeometricPoint B S hS X) :
    PreservesColimitsOfSize.{max (u + 1) w, max (u + 1) w}
      (sheafToPresheaf (SmallEtale.topology B S hS X) (Type (max (u + 1) w)) ⋙
        stalkSetFunctor x)

Tag 04K2, a lemma

Tag 04K2 in the Stacks Project.

AlgebraicGeometry.Space.abelianPullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImage.lean, line 73. The attribute's comment: “abelian_pullback_exact”.

Stacks 04K2. Pullback of sheaves of abelian groups along a morphism of algebraic spaces is exact on the small étale sites.

theorem abelianPullback_exact :
    exactFunctor
      (Sheaf (SmallEtale.topology B S hS Y.1) AddCommGrpCat.{u + 1})
      (Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1})
      (abelianPullback B S hS f)

AlgebraicGeometry.Space.smallEtalePullbackRepresentableNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImage.lean, line 88. The attribute's comment: “representable_pullback”.

Stacks 04K2. The inverse image of the small étale sheaf represented by an algebraic space V étale over Y is the sheaf represented by the cartesian base change X ×_Y V, naturally in V.

An algebraic space étale over Y need not be a scheme, so the sheaf it represents on the small étale site is its sheafified Yoneda presheaf on the spaces-étale site, restricted along the comparison functor of Stacks 03G1.

noncomputable def smallEtalePullbackRepresentableNatIso :
    (yoneda ⋙ presheafToSheaf (SpacesEtale.topology B S hS Y) (Type (u + 1)) ⋙
      (comparisonFunctor B S hS Y).sheafPushforwardContinuous (Type (u + 1))
        (SmallEtale.topology B S hS Y.1) (SpacesEtale.topology B S hS Y) ⋙
      (smallToposMorphism B S hS f).inverseImage) ≅
    ((spacesBaseChange B S hS f).functor ⋙ yoneda ⋙
      presheafToSheaf (SpacesEtale.topology B S hS X) (Type (u + 1)) ⋙
      (comparisonFunctor B S hS X).sheafPushforwardContinuous (Type (u + 1))
        (SmallEtale.topology B S hS X.1) (SpacesEtale.topology B S hS X))

AlgebraicGeometry.Space.smallEtaleInverseImage_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImage.lean, line 168. The attribute's comment: “sheaf_pullback_exact”.

Stacks 04K2. Pullback of sheaves of sets along a morphism of algebraic spaces is exact on the small étale sites.

theorem smallEtaleInverseImage_exact :
    exactFunctor _ _ (smallToposMorphism B S hS f).inverseImage

AlgebraicGeometry.Space.smallEtaleInverseImageFiberIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImageFiberType.lean, line 120. The attribute's comment: “part (4), for sheaves of sets at the universe of the structure rings”.

The fibre at a geometric point x of X of the inverse image along the canonical morphism of small étale topoi of Stacks 03G8 of a sheaf of sets on the small étale site of Y is the fibre of that sheaf at the image point f ∘ x, naturally in the sheaf.

It is the right-adjoint transpose of AlgebraicGeometry.Space.smallEtaleSkyscraperIso.

def smallEtaleInverseImageFiberIso :
    (etaleSitePoint B S hS Y.1 (geometricPointMap f.hom x) Y.2).sheafFiber (A := Type u) ≅
      (smallEtaleRingedToposHom B S hS f).toToposHom.inverseImage ⋙
        (etaleSitePoint B S hS X.1 x X.2).sheafFiber (A := Type u)

AlgebraicGeometry.Space.smallEtaleInverseImageStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImageStalk.lean, line 193. The attribute's comment: “stalk_pullback”.

Stacks 04K2, part (4). For a morphism f : X ⟶ Y of algebraic spaces over S and a geometric point x of X, the stalk at x of the small étale inverse image of a sheaf on Y is the stalk of that sheaf at the image geometric point f ∘ x, naturally in the sheaf.

def smallEtaleInverseImageStalkIso (f : X ⟶ Y) (x : GeometricPoint B S hS X.1) :
    (smallToposMorphism B S hS f).inverseImage ⋙
        sheafToPresheaf (SmallEtale.topology B S hS X.1) (Type (u + 1)) ⋙ stalkSetFunctor x ≅
      sheafToPresheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)) ⋙
        stalkSetFunctor (geometricPointMap f.hom x)

AlgebraicGeometry.Space.smallEtaleAbelianInverseImageStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImageStalkAbelian.lean, line 256. The attribute's comment: “stalk_pullback, abelian sheaves”.

Stacks 04K2, part (4), for abelian sheaves. For a morphism f : X ⟶ Y of algebraic spaces over S with representable underlying morphism and a geometric point x of X, the stalk at x of the inverse image of an abelian sheaf on the small étale site of Y is the stalk of that sheaf at the image geometric point f ∘ x, naturally in the sheaf.

def smallEtaleAbelianInverseImageStalkIso (x : GeometricPoint B S hS X.1) :
    letI := isContinuous_smallBaseChange B S hS f hf
    (smallBaseChange B S hS f hf).sheafPullback AddCommGrpCat.{u + 1}
          (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1) ⋙
        sheafToPresheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u + 1} ⋙
          stalkFunctor AddCommGrpCat.{u + 1} x ≅
      sheafToPresheaf (SmallEtale.topology B S hS Y.1) AddCommGrpCat.{u + 1} ⋙
        stalkFunctor AddCommGrpCat.{u + 1} (geometricPointMap f.hom x)

AlgebraicGeometry.Space.preservesFiniteLimits_smallEtaleAbelianInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInverseImageStalkAbelian.lean, line 359. The attribute's comment: “part (1): finite limits”.

Stacks 04K2, part (1). The inverse image of abelian sheaves along a morphism of algebraic spaces with representable underlying morphism is left exact.

Base change of scheme charts is not representably flat, for want of a terminal object on the small étale site; left exactness is instead inherited from base change of étale algebraic spaces through the equivalences of Stacks 03G1.

theorem preservesFiniteLimits_smallEtaleAbelianInverseImage :
    letI := isContinuous_smallBaseChange B S hS f hf
    PreservesFiniteLimits ((smallBaseChange B S hS f hf).sheafPullback AddCommGrpCat.{u + 1}
      (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1))

Tag 04K3, a remark

Tag 04K3 in the Stacks Project.

AlgebraicGeometry.Space.globalSections_isEquivalence_of_geometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkAsPullback.lean, line 199. The attribute's comment: “equivalence by global sections”. References: SGA 4½ Arcata (2.4.4), “sep. closed field, G=1”.

Global sections is an equivalence from sheaves of sets on the small étale site of the algebraic space represented by the field spectrum of a geometric point onto sets.

theorem globalSections_isEquivalence_of_geometricPoint (x : GeometricPoint B S hS F) :
    (Sheaf.Γ (SmallEtale.topology B S hS (yoneda.obj x.val.siteObject))
      (Type (u + 1))).IsEquivalence

AlgebraicGeometry.Space.smallEtaleStalkIsoPullbackGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkAsPullback.lean, line 241. The attribute's comment: “the stalk as global sections of the pullback”.

The stalk functor at a geometric point x of an algebraic space X is the inverse image along x — viewed as a morphism of algebraic spaces from the space represented by its field spectrum, hence as a morphism of small étale topoi — followed by global sections on the source.

def smallEtaleStalkIsoPullbackGlobalSections (x : GeometricPoint B S hS X.obj) :
    sheafToPresheaf (SmallEtale.topology B S hS X.obj) (Type (u + 1)) ⋙ stalkSetFunctor x ≅
      (smallToposMorphism B S hS
            (ObjectProperty.homMk (fieldMorphism B S hS X.obj x.val) :
              (⟨yoneda.obj x.val.siteObject,
                  isAlgebraicSpace_yoneda B S hS x.val.siteObject⟩ :
                AlgebraicSpaces B S hS) ⟶ X)).inverseImage ⋙
        Sheaf.Γ (SmallEtale.topology B S hS (yoneda.obj x.val.siteObject))
          (Type (u + 1))

Tag 04K4, a remark

Tag 04K4 in the Stacks Project.

AlgebraicGeometry.Space.stalkFunctor_iso_of_liesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StalkIndependenceOfGeometricPoint.lean, line 483.

Stacks 04K4. The stalk functors on the small étale site at two geometric points lying over the same point of the algebraic space are isomorphic, naturally in the presheaf. The isomorphism is not canonical: the two points are compared through a common dominating geometric point.

theorem stalkFunctor_iso_of_liesOver (hF : IsAlgebraicSpace B S hS F) (C : Type w)
    [Category.{v} C] {x : points B S hS F} (p q : GeometricPoint B S hS F)
    [HasColimitsOfShape (SmallEtaleNeighborhood p)ᵒᵖ C]
    [HasColimitsOfShape (SmallEtaleNeighborhood q)ᵒᵖ C]
    (hp : p.LiesOver x) (hq : q.LiesOver x) :
    Nonempty (stalkFunctor C p ≅ stalkFunctor C q)

Tag 04K5, a theorem

Tag 04K5 in the Stacks Project.

AlgebraicGeometry.Space.injective_iff_stalkSetMap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 502. The attribute's comment: “injectivity”. References: SGA 4 VIII (3.6), “injectivity clause”.

Stacks 04K5. A map of sheaves of sets on the small étale site of an algebraic space is injective on sections over every étale chart exactly when it is injective on every geometric stalk.

theorem injective_iff_stalkSetMap_injective
    {F G : Sheaf (SmallEtale.topology B S hS X) (Type w)} (a : F ⟶ G) :
    (∀ U : SmallEtale B S hS X, Function.Injective (a.hom.app (Opposite.op U))) ↔
      ∀ x : GeometricPoint B S hS X, Function.Injective (stalkSetMap x a.hom)

AlgebraicGeometry.Space.surjective_iff_stalkSetMap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 541. The attribute's comment: “surjectivity”. References: SGA 4 VIII (3.6), “surjectivity clause”.

Stacks 04K5. A map of sheaves of sets on the small étale site of an algebraic space is locally surjective exactly when it is surjective on every geometric stalk.

theorem surjective_iff_stalkSetMap_surjective
    {F G : Sheaf (SmallEtale.topology B S hS X) (Type w)} (a : F ⟶ G) :
    Sheaf.IsLocallySurjective a ↔
      ∀ x : GeometricPoint B S hS X, Function.Surjective (stalkSetMap x a.hom)

AlgebraicGeometry.Space.exact_iff_stalk_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStalkExactness.lean, line 689. The attribute's comment: “exactness”.

Stacks 04K5. A short complex of sheaves of abelian groups on the small étale site of an algebraic space is exact exactly when its sequence of geometric stalks is exact at every geometric point.

theorem exact_iff_stalk_exact
    (T : ShortComplex (Sheaf (SmallEtale.topology B S hS X)
      AddCommGrpCat.{max (u + 1) w})) :
    T.Exact ↔ ∀ x : GeometricPoint B S hS X,
      let Φ := sheafToPresheaf (SmallEtale.topology B S hS X)
        AddCommGrpCat.{max (u + 1) w} ⋙ stalkFunctor AddCommGrpCat.{max (u + 1) w} x
      ∀ b : Φ.obj T.X₂,
        ((Φ.map T.g).hom b = 0 ↔ ∃ a : Φ.obj T.X₁, (Φ.map T.f).hom a = b)

Tag 04K6, a lemma

Tag 04K6 in the Stacks Project.

AlgebraicGeometry.Space.exists_geometricPoint_stalkFunctor_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsOfSmallEtaleTopos.lean, line 559. References: SGA 4 VIII (7.9), “essential surjectivity”.

Stacks 04K6. Every point of the small étale topos of an algebraic space is represented, at the level of stalk functors, by a geometric point of the space.

theorem exists_geometricPoint_stalkFunctor_iso (hF : IsAlgebraicSpace B S hS F)
    (p : PointOfTopos.{u + 1} (SmallEtale.topology B S hS F)) :
    ∃ x : GeometricPoint B S hS F,
      Nonempty (p.inverseImage ≅
        sheafToPresheaf (SmallEtale.topology B S hS F) (Type (u + 1)) ⋙
          stalkSetFunctor x)

Sources

LeanAlgebraicGeometry.Space.geometricPointOfSpecHom · AlgebraicGeometry.Space.GeometricPoint · AlgebraicGeometry.Space.GeometricPoint.image · AlgebraicGeometry.Space.GeometricPoint.LiesOver · AlgebraicGeometry.Space.EtaleNeighborhood · AlgebraicGeometry.Space.EtaleNeighborhood.Hom · AlgebraicGeometry.Space.EtaleNeighborhood.exists_common_refinement · AlgebraicGeometry.Space.EtaleNeighborhood.exists_equalizing_refinement

Section66.20 Supports of abelian sheaves #

Section 66.20 of the Stacks Project, Tag 04K7. 5 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04K8, a lemma

Tag 04K8 in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_openSubspace_of_subterminalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleSubterminalSheaf.lean, line 245.

Stacks 04K8. Every subsheaf of the terminal sheaf on the spaces-étale site of an algebraic space is the sheaf of a unique open subspace.

theorem existsUnique_openSubspace_of_subterminalSheaf
    (F : Subfunctor (spacesEtaleTerminalSheaf B S hS X))
    (hF : Presheaf.IsSheaf (SpacesEtale.topology B S hS X) F.toFunctor) :
    ∃! W : {W : Subfunctor X.1 // IsOpenSubspace B S hS W},
      F = openSubspaceSheaf B S hS X W

Tag 04K9, a lemma

Tag 04K9 in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.largestOpenZeroSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleZeroLocus.lean, line 271. The attribute's comment: “part (1): the open subspace”.

Stacks 04K9, part (1). The largest open subspace of the algebraic space underlying an object U of the spaces-étale site of X on which a section of an abelian sheaf over U vanishes: the open subspace whose point set is the zero images of the section.

noncomputable def largestOpenZeroSubspace
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{v})
    (U : SpacesEtale B S hS X) (σ : F.obj.obj (op U)) :
    {W : Subfunctor (underlying B S hS X U).1 // IsOpenSubspace B S hS W}

AlgebraicGeometry.Space.SpacesEtale.largestOpenZeroSubspace_restrict_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleZeroLocus.lean, line 295. The attribute's comment: “part (2): the pullback criterion”.

Stacks 04K9, part (2). A section restricts to zero on an object of the spaces-étale site over U exactly when the image of the points of that object lies in the largest open zero subspace.

theorem largestOpenZeroSubspace_restrict_iff
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{v})
    (U : SpacesEtale B S hS X) (σ : F.obj.obj (op U))
    (V : SpacesEtale B S hS X) (f : V ⟶ U) :
    F.obj.map f.op σ = 0 ↔
      ImageInOpen B S hS X
        (openPoints B S hS X U (largestOpenZeroSubspace B S hS X F U σ)) f

AlgebraicGeometry.Space.SpacesEtale.restrict_largestOpenZeroSubspace_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleZeroLocus.lean, line 308. The attribute's comment: “part (1): the section vanishes on the open subspace”.

Stacks 04K9, part (1). A section vanishes on its largest open zero subspace.

theorem restrict_largestOpenZeroSubspace_eq_zero
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{v})
    (U : SpacesEtale B S hS X) (σ : F.obj.obj (op U)) :
    F.obj.map (openSubspaceInclusion B S hS X U
      (largestOpenZeroSubspace B S hS X F U σ)).op σ = 0

AlgebraicGeometry.Space.SpacesEtale.largestOpenZeroSubspace_maximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleZeroLocus.lean, line 320. The attribute's comment: “part (1): maximality”.

Stacks 04K9, part (1). Every open subspace on which a section vanishes is contained in its largest open zero subspace.

theorem largestOpenZeroSubspace_maximal
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{v})
    (U : SpacesEtale B S hS X) (σ : F.obj.obj (op U))
    (W : {W : Subfunctor (underlying B S hS X U).1 // IsOpenSubspace B S hS W})
    (hW : F.obj.map (openSubspaceInclusion B S hS X U W).op σ = 0) :
    W.1 ≤ (largestOpenZeroSubspace B S hS X F U σ).1

AlgebraicGeometry.Space.SpacesEtale.germ_eq_zero_iff_mem_largestOpenZeroSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleZeroLocus.lean, line 358. The attribute's comment: “part (3): the geometric-point criterion”. References: SGA 2 XIV (1.8.2.1), “abelian, geom. point”.

Stacks 04K9, part (3). The germ of a section at a geometric point of the algebraic space underlying an object U of the spaces-étale site of X vanishes in the spaces-étale stalk at the image of that point in X exactly when the point lies in the largest open zero subspace of the section.

The colimit defining the stalk is filtered, so the germ vanishes exactly when the section already vanishes on some étale neighbourhood refining U; one direction is then the restriction criterion applied to such a refinement, and the other is the restriction criterion applied to the largest open zero subspace itself, which the field-valued point factors through by Tag 03IE.

theorem germ_eq_zero_iff_mem_largestOpenZeroSubspace
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{v})
    (U : SpacesEtale B S hS X) (σ : F.obj.obj (op U))
    (p : GeometricPoint B S hS (underlying B S hS X U).1) :
    (spacesNeighborhoodSections (imageGeometricPoint B S hS X U p)
        (F.obj ⋙ forget AddCommGrpCat.{v})).ιColimitType
      (op (neighborhoodOfGeometricPoint B S hS X U p)) σ =
    (spacesNeighborhoodSections (imageGeometricPoint B S hS X U p)
        (F.obj ⋙ forget AddCommGrpCat.{v})).ιColimitType
      (op (neighborhoodOfGeometricPoint B S hS X U p)) (0 : F.obj.obj (op U)) ↔
      p.image ∈ openPoints B S hS X U (largestOpenZeroSubspace B S hS X F U σ)

AlgebraicGeometry.Space.SpacesEtale.exists_largestOpenZeroSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleZeroLocus.lean, line 448. References: SGA 2 XIV (1.8.2.1), “abelian, spaces”.

Stacks 04K9. A section σ of an abelian sheaf on the spaces-étale site of an algebraic space X, over an object U of that site, has an open subspace W of the algebraic space underlying U such that: σ vanishes on W and W contains every open subspace on which σ vanishes; σ restricts to zero on an object of the site over U exactly when the image of its points lies in W; and the germ of σ at a geometric point of U vanishes in the spaces-étale stalk at its image in X exactly when that point lies in W.

theorem exists_largestOpenZeroSubspace
    (F : Sheaf (topology B S hS X) AddCommGrpCat.{v})
    (U : SpacesEtale B S hS X) (σ : F.obj.obj (op U)) :
    ∃ W : {W : Subfunctor (underlying B S hS X U).1 // IsOpenSubspace B S hS W},
      F.obj.map (openSubspaceInclusion B S hS X U W).op σ = 0 ∧
      (∀ W' : {W : Subfunctor (underlying B S hS X U).1 // IsOpenSubspace B S hS W},
        F.obj.map (openSubspaceInclusion B S hS X U W').op σ = 0 → W'.1 ≤ W.1) ∧
      (∀ (V : SpacesEtale B S hS X) (f : V ⟶ U),
        F.obj.map f.op σ = 0 ↔ ImageInOpen B S hS X (openPoints B S hS X U W) f) ∧
      (∀ p : GeometricPoint B S hS (underlying B S hS X U).1,
        (spacesNeighborhoodSections (imageGeometricPoint B S hS X U p)
            (F.obj ⋙ forget AddCommGrpCat.{v})).ιColimitType
          (op (neighborhoodOfGeometricPoint B S hS X U p)) σ =
        (spacesNeighborhoodSections (imageGeometricPoint B S hS X U p)
            (F.obj ⋙ forget AddCommGrpCat.{v})).ιColimitType
          (op (neighborhoodOfGeometricPoint B S hS X U p)) (0 : F.obj.obj (op U)) ↔
          p.image ∈ openPoints B S hS X U W)

Tag 04KA, a definition

Tag 04KA in the Stacks Project.

AlgebraicGeometry.Space.supportOfSection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupport.lean, line 418. The attribute's comment: “support of a section”. References: SGA 4 VIII (6.6), “support of a section”.

The support of a section of an abelian sheaf on the small étale site of an algebraic space over an étale chart: the complement of the largest open on which the section restricts to zero.

abbrev supportOfSection (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v})
    (U : SmallEtale B S hS X) (σ : F.obj.obj (op U)) :
    Set (points B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U)))

AlgebraicGeometry.Space.supportOfSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupport.lean, line 626. The attribute's comment: “support of a sheaf”. References: SGA 4 VIII (6.6), “support of a sheaf”.

The support of an abelian sheaf on the small étale site of an algebraic space: the set of points at which the stalk at some geometric point lying over that point is nonzero, that is, at which the set-valued stalk is not a subsingleton.

def supportOfSheaf (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}) :
    Set (points B S hS X)

Tag 04KB, a lemma

Tag 04KB in the Stacks Project.

AlgebraicGeometry.Space.isClosed_supportOfSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupport.lean, line 436. The attribute's comment: “closed_section_support”.

The support of a section is closed.

theorem isClosed_supportOfSection
    (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v})
    (U : SmallEtale B S hS X) (σ : F.obj.obj (op U)) :
    IsClosed (supportOfSection B S hS X F U σ)

AlgebraicGeometry.Space.supportOfSection_add_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupport.lean, line 494. The attribute's comment: “support_sum”.

The support of a sum is contained in the union of the supports.

theorem supportOfSection_add_subset
    (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v})
    (U : SmallEtale B S hS X) (σ τ : F.obj.obj (op U)) :
    supportOfSection B S hS X F U (σ + τ) ⊆
      supportOfSection B S hS X F U σ ∪ supportOfSection B S hS X F U τ

AlgebraicGeometry.Space.supportOfSection_map_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupport.lean, line 521. The attribute's comment: “support_image_section”.

A morphism of abelian sheaves cannot enlarge the support of a section: the support of the image of σ under φ is contained in the support of σ.

theorem supportOfSection_map_subset
    {F G : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}} (φ : F ⟶ G)
    (U : SmallEtale B S hS X) (σ : F.obj.obj (op U)) :
    supportOfSection B S hS X G U (φ.hom.app (op U) σ) ⊆
      supportOfSection B S hS X F U σ

AlgebraicGeometry.Space.supportOfSheaf_subset_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupport.lean, line 644. The attribute's comment: “support_injection”.

The support of an abelian subsheaf is contained in the support of the ambient sheaf: a monomorphism f : F ⟶ G of abelian sheaves on the small étale site cannot enlarge the support of its source.

theorem supportOfSheaf_subset_of_mono (hX : IsAlgebraicSpace B S hS X)
    {F G : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}} (f : F ⟶ G) [Mono f] :
    supportOfSheaf B S hS X F ⊆ supportOfSheaf B S hS X G

AlgebraicGeometry.Space.supportOfSheaf_subset_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupportProperties.lean, line 161. The attribute's comment: “part (6): support along an injection”.

Stacks 04KB, part (6). If a map of abelian sheaves on the small étale site of an algebraic space is injective on sections over every étale chart, then the support of its source is contained in the support of its target.

Such a map is injective on every geometric stalk by Stacks 04K5, and an injection into a subsingleton has subsingleton source.

The hypothesis is the sectionwise one, which is what a splitting of sheaves supplies. AlgebraicGeometry.Space.supportOfSheaf_subset_of_mono draws the same conclusion from a Mono instance in the sheaf category; neither hypothesis is the other, the passage between them being full faithfulness of CategoryTheory.sheafToPresheaf together with CategoryTheory.NatTrans.mono_iff_mono_app, so both forms are stated.

theorem supportOfSheaf_subset_of_injective (hX : IsAlgebraicSpace B S hS X)
    {F G : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}} (φ : F ⟶ G)
    (hφ : ∀ U : SmallEtale B S hS X, Function.Injective (φ.hom.app (op U))) :
    supportOfSheaf B S hS X F ⊆ supportOfSheaf B S hS X G

AlgebraicGeometry.Space.supportOfSheaf_eq_iUnion_image_supportOfSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupportSections.lean, line 257. The attribute's comment: “sheaf_support_sections”.

Stacks 04KB, part (4). The support of an abelian sheaf on the small étale site of an algebraic space is the union, over all étale charts and all sections on them, of the images of the supports of those sections.

A point of the support carries a geometric point with a nonzero stalk, hence a neighbourhood and a section whose germ there is nonzero, and that section has the point of the chart in its support. Conversely a point in the support of a section is the image of a geometric point of the chart, whose germ there is then nonzero.

theorem supportOfSheaf_eq_iUnion_image_supportOfSection
    (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}) :
    supportOfSheaf B S hS X F =
      ⋃ U : SmallEtale B S hS X, ⋃ σ : F.obj.obj (op U),
        pointsMap B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U)) U.obj.hom ''
          supportOfSection B S hS X F U σ

AlgebraicGeometry.Space.supportOfSheaf_eq_iUnion_image_supportOfSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupportSections.lean, line 257. The attribute's comment: “part (4): the support of a sheaf is the union of the section supports”.

Stacks 04KB, part (4). The support of an abelian sheaf on the small étale site of an algebraic space is the union, over all étale charts and all sections on them, of the images of the supports of those sections.

A point of the support carries a geometric point with a nonzero stalk, hence a neighbourhood and a section whose germ there is nonzero, and that section has the point of the chart in its support. Conversely a point in the support of a section is the image of a geometric point of the chart, whose germ there is then nonzero.

theorem supportOfSheaf_eq_iUnion_image_supportOfSection
    (F : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}) :
    supportOfSheaf B S hS X F =
      ⋃ U : SmallEtale B S hS X, ⋃ σ : F.obj.obj (op U),
        pointsMap B S hS (yoneda.obj ((SmallEtale.toOver B S hS X).obj U)) U.obj.hom ''
          supportOfSection B S hS X F U σ

AlgebraicGeometry.Space.supportOfSheaf_subset_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupportSections.lean, line 300. The attribute's comment: “part (5): support along a surjection”.

Stacks 04KB. A surjection of abelian sheaves on the small étale site of an algebraic space does not enlarge the support: the support of the target is contained in the support of the source.

A surjection of sheaves is surjective on every geometric stalk by Stacks 04K5, so a point at which the stalk of the source is a subsingleton is one at which the stalk of the target is one too.

theorem supportOfSheaf_subset_of_isLocallySurjective
    {F G : Sheaf (SmallEtale.topology B S hS X) AddCommGrpCat.{v}} (a : F ⟶ G)
    [Sheaf.IsLocallySurjective a] :
    supportOfSheaf B S hS X G ⊆ supportOfSheaf B S hS X F

Tag 04KC, a lemma

Tag 04KC in the Stacks Project.

AlgebraicGeometry.Space.isClosed_supportOfSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafSupportProperties.lean, line 303.

Stacks 04KC. The support of a sheaf of rings on the small étale site of an algebraic space is closed.

The support is the set of points of the space at which the stalk of the underlying abelian sheaf at some geometric point is nonzero; for a sheaf of rings that is the set of points at which the ring of germs is not the zero ring, since a ring vanishes exactly when its unit does. Its complement is exhibited as the image of the maximal open zero locus of the unit section of a surjective étale atlas, which is open because an étale chart is open on points by clause (3) of Stacks 03BX.

theorem isClosed_supportOfSheaf (hX : IsAlgebraicSpace B S hS X) :
    IsClosed (supportOfSheaf B S hS X (toAddCommGrp B S hS X R))

Sources

Section66.21 The structure sheaf of an algebraic space #

Section 66.21 of the Stacks Project, Tag 04KD. 4 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03G6, a lemma

Tag 03G6 in the Stacks Project.

AlgebraicGeometry.Space.structurePresheaf_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StructureSheaf.lean, line 317.

Stacks 03G6. Global regular functions form a sheaf of commutative rings on the small étale site of an algebraic space.

Stated with 03G6's own hypotheses, in their original binder order, so that dependent results apply it positionally; the hypothesis is discarded, and structurePresheaf_isSheaf' is the general statement.

theorem structurePresheaf_isSheaf (_hF : IsAlgebraicSpace B S hS F) :
    Presheaf.IsSheaf (SmallEtale.topology B S hS F) (structurePresheaf B S hS F)

Tag 03G7, a definition

Tag 03G7 in the Stacks Project.

AlgebraicGeometry.Space.structureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StructureSheaf.lean, line 332. The attribute's comment: “the structure sheaf of an algebraic space”.

The structure sheaf of commutative rings on the small étale site of the algebraic space F.

Stated with 03G6's own hypotheses, in their original binder order, so that a ringed site built on it applies this positionally; structureSheaf' is the general form, and the two are equal by rfl.

def structureSheaf (_hF : IsAlgebraicSpace B S hS F) :
    Sheaf (SmallEtale.topology B S hS F) CommRingCat.{u}

Tag 03G8, a lemma

Tag 03G8 in the Stacks Project.

AlgebraicGeometry.Space.pushforwardAlgebraIdAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BoundedDirectImageAlgebraFactorization.lean, line 254. The attribute's comment: “the identity clause at the level of algebras: (𝟙_Y)_* 𝒪_Y is 𝒪_Y”.

The direct image of 𝒪_Y along the identity of Y is 𝒪_Y, as an 𝒪_Y-algebra, with no anti-equivalence and no hypothesis.

AlgebraicGeometry.Space.pushforwardAlgebra of a morphism is its structure map read as an algebra structure, so this is the identity clause of Stacks 03G8 — the structure map of an identity is an isomorphism, AlgebraicGeometry.Space.isIso_fSharp_id — read through AlgebraicGeometry.Space.AlgebraSheaf.ofHomIso: the inverse of that structure map carries it to the identity of 𝒪_Y, which is the structure map of AlgebraicGeometry.Space.unitAlgebra.

This is the isomorphism that AlgebraicGeometry.Space.pushforwardAlgebraIdIso of StacksFrontier.AlgebraicGeometry.Spaces.DirectImageAlgebraFactorization obtains from an assumed anti-equivalence and that StacksFrontier.AlgebraicGeometry.Spaces.RelativeSpecDirectImage carries as the hypothesis hid.

def pushforwardAlgebraIdAlgebraIso (Y : AlgebraicSpaces B S hS) :
    pushforwardAlgebra B S hS (Over.mk (𝟙 Y)) ≅ unitAlgebra B S hS Y

AlgebraicGeometry.Space.isIso_fSharp_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraMorphism.lean, line 584. The attribute's comment: “the identity clause: the structure map of an identity is an isomorphism”.

The identity clause of Stacks 03G8: the structure map of the morphism of small étale ringed topoi of 𝟙 : A ⟶ A is an isomorphism 𝒪_A ≅ (𝟙_A)_* 𝒪_A.

On underlying sheaves of sets this is AlgebraicGeometry.Space.structureSharpSet_id, which identifies the structure map of an identity with the canonical comparison AlgebraicGeometry.Space.smallEtaleDirectImageIdIso of the direct image along an identity with the identity functor; forgetting the ring operations reflects isomorphisms, so the CommRingCat-valued structure map is invertible too. AlgebraicGeometry.Space.isIso_structureSharp_id is the same statement for the RingCat-valued AlgebraicGeometry.Space.structureSharp, which is not the map that AlgebraicGeometry.Space.pushforwardAlgebra is built from.

theorem isIso_fSharp_id (A : AlgebraicSpaces B S hS) :
    IsIso (smallEtaleRingedToposHom B S hS (𝟙 A)).fSharp

AlgebraicGeometry.Space.smallEtaleRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHom.lean, line 281. The attribute's comment: “canonical morphism of ringed topoi”.

The morphism of small étale ringed topoi induced by a morphism of algebraic spaces.

noncomputable def smallEtaleRingedToposHom (f : X ⟶ Y) :
    RingedToposHom (smallEtaleRingedTopos B S hS X) (smallEtaleRingedTopos B S hS Y)

AlgebraicGeometry.Space.smallEtaleRingedToposHom_pushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHom.lean, line 288. The attribute's comment: “underlying geometric morphism”.

The underlying geometric morphism of smallEtaleRingedToposHom.

noncomputable def smallEtaleRingedToposHom_pushforward (f : X ⟶ Y) :
    ((comparisonFunctor B S hS X).sheafPushforwardContinuous (Type u)
          (SmallEtale.topology B S hS X.1) (SpacesEtale.topology B S hS X)) ⋙
        (smallEtaleRingedToposHom B S hS f).toToposHom.pushforward ≅
      ((spacesBaseChange B S hS f).functor.sheafPushforwardContinuous (Type u)
          (SpacesEtale.topology B S hS Y) (SpacesEtale.topology B S hS X)) ⋙
        (comparisonFunctor B S hS Y).sheafPushforwardContinuous (Type u)
          (SmallEtale.topology B S hS Y.1) (SpacesEtale.topology B S hS Y)

AlgebraicGeometry.Space.smallEtaleRingedToposHom_representable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHom.lean, line 347. The attribute's comment: “agreement with scheme-chart base change”.

Stacks 03G8. For a representable morphism of algebraic spaces the geometric direct image of smallEtaleRingedToposHom is base change of étale scheme charts.

noncomputable def smallEtaleRingedToposHom_representable (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f hf).toIsContinuous
    (smallEtaleRingedToposHom B S hS f).toToposHom.pushforward ≅
      (smallBaseChange B S hS f hf).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1)

AlgebraicGeometry.Space.structureSharp_comp_chartProjectionSharpDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSchemeStructureSharp.lean, line 352. The attribute's comment: “part (2): the structure map is pullback along the cartesian projection”.

Stacks 03G8, part (2), for a representable morphism of algebraic spaces. The structure map f♯ : 𝒪_Y ⟶ f_*𝒪_X of Stacks 03G8, followed by the identification AlgebraicGeometry.Space.chartProjectionSharpDirectImage of the sections of f_*𝒪_X over an étale chart V of Y with the regular functions on the scheme X ×_Y V, is pullback of regular functions along the cartesian projection X ×_Y V ⟶ V — which is the structure map of the morphism of small étale ringed sites of Stacks 070R, part (2).

theorem structureSharp_comp_chartProjectionSharpDirectImage (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    letI := isContinuous_smallBaseChange B S hS f hf
    structureSharp B S hS f ≫ chartProjectionSharpDirectImage B S hS f hf =
      cartesianProjectionSharp B S hS f hf

AlgebraicGeometry.Space.fSharp_comp_chartProjectionSharpDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSchemeStructureSharp.lean, line 401. The attribute's comment: “part (2): the same for the structure map of the morphism of ringed topoi”.

Stacks 03G8, part (2), for a representable morphism of algebraic spaces, on the morphism of ringed topoi. The structure map f♯ of the morphism of small étale ringed topoi of Stacks 03G8, read on sheaves of not necessarily commutative rings and followed by the identification of the sections of f_*𝒪_X over an étale chart V of Y with the regular functions on X ×_Y V, is pullback of regular functions along the cartesian projection X ×_Y V ⟶ V.

theorem fSharp_comp_chartProjectionSharpDirectImage (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    letI := isContinuous_smallBaseChange B S hS f hf
    (sheafCompose (SmallEtale.topology B S hS Y.1)
            (forget₂ CommRingCat.{u} RingCat.{u})).map
          (smallEtaleRingedToposHom B S hS f).fSharp ≫
        chartProjectionSharpDirectImage B S hS f hf =
      cartesianProjectionSharp B S hS f hf

AlgebraicGeometry.Space.cartesianProjectionSharpCommRing_eq_changeOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSchemeStructureSharp.lean, line 440. The attribute's comment: “part (2): for a morphism of schemes this is the Stacks 070R structure map”.

Stacks 03G8, part (2). For a morphism of schemes, f♯ of the space construction is the structure-sheaf homomorphism of Stacks 070R: the small étale site of the representable algebraic space yoneda.obj T is a site of schemes over T through AlgebraicGeometry.Space.schemeChartToOver, and over that presentation the map AlgebraicGeometry.Space.cartesianProjectionSharpCommRing — which AlgebraicGeometry.Space.structureSharp_comp_chartProjectionSharpDirectImage identifies with f♯ — is AlgebraicGeometry.ChangeOfSites.structureSharp, the structure-sheaf homomorphism of a change-of-topologies morphism of sites, formed with the cartesian projections.

theorem cartesianProjectionSharpCommRing_eq_changeOfSites :
    letI := isContinuous_smallBaseChange B S hS (representedSpaceMap B S hS g) hg
    cartesianProjectionSharpCommRing B S hS (representedSpaceMap B S hS g) hg =
      AlgebraicGeometry.ChangeOfSites.structureSharp
        (SmallEtale.topology B S hS (yoneda.obj T))
        (SmallEtale.topology B S hS (yoneda.obj T'))
        (schemeChartToOver B S hS T) (schemeChartToOver B S hS T')
        (smallBaseChange B S hS (representedSpaceMap B S hS g) hg)
        (cartesianProjection B S hS (representedSpaceMap B S hS g) hg)
        (schemeChart_structure_isSheaf B S hS T)
        (schemeChart_structure_isSheaf B S hS T')

AlgebraicGeometry.Space.structureSharp_representedSpaceMap_eq_changeOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSchemeStructureSharp.lean, line 464. The attribute's comment: “part (2): for a morphism of schemes, f♯ is the structure map of Stacks 070R”.

Stacks 03G8, part (2). For a morphism of schemes g : T' ⟶ T over S the structure map f♯ : 𝒪_Y ⟶ f_*𝒪_X of Stacks 03G8, followed by the canonical identification AlgebraicGeometry.Space.chartProjectionSharpDirectImage of the sections of f_*𝒪_{T'} over an étale chart V of T with the regular functions on the scheme T' ×_T V, is the structure map of Stacks 070R: the map AlgebraicGeometry.ChangeOfSites.structureSharp of the change-of-topologies morphism of sites given by base change of étale charts, formed with the cartesian projections T' ×_T V ⟶ V.

The identification is an isomorphism, by AlgebraicGeometry.Space.isIso_chartProjectionSharpDirectImage, so this is an equality of the two structure maps and not merely a factorization.

theorem structureSharp_representedSpaceMap_eq_changeOfSites :
    letI := isContinuous_smallBaseChange B S hS (representedSpaceMap B S hS g)
      (relativelyRepresentable_yoneda_map B S hS g)
    (sheafCompose (SmallEtale.topology B S hS (yoneda.obj T))
          (forget₂ CommRingCat.{u} RingCat.{u})).map
        (AlgebraicGeometry.ChangeOfSites.structureSharp
          (SmallEtale.topology B S hS (yoneda.obj T))
          (SmallEtale.topology B S hS (yoneda.obj T'))
          (schemeChartToOver B S hS T) (schemeChartToOver B S hS T')
          (smallBaseChange B S hS (representedSpaceMap B S hS g)
            (relativelyRepresentable_yoneda_map B S hS g))
          (cartesianProjection B S hS (representedSpaceMap B S hS g)
            (relativelyRepresentable_yoneda_map B S hS g))
          (schemeChart_structure_isSheaf B S hS T)
          (schemeChart_structure_isSheaf B S hS T')) =
      structureSharp B S hS (representedSpaceMap B S hS g) ≫
        chartProjectionSharpDirectImage B S hS (representedSpaceMap B S hS g)
          (relativelyRepresentable_yoneda_map B S hS g)

AlgebraicGeometry.Space.smallEtaleRingedToposHom_comp_fSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStructureMapComp.lean, line 561. The attribute's comment: “compatibility with composition”.

The structure map of the composite morphism of small étale ringed topoi, followed by the comparison of the direct images of sheaves of commutative rings, is the structure map of the composite morphism of algebraic spaces.

theorem smallEtaleRingedToposHom_comp_fSharp (f : X ⟶ Y) (g : Y ⟶ Z) :
    ((smallEtaleRingedToposHom B S hS g).comp
        (smallEtaleRingedToposHom B S hS f)).fSharp ≫
        (smallEtaleRingedToposHom_compRingIso B S hS f g).hom.app
          (smallEtaleRingedTopos B S hS X).O =
      (smallEtaleRingedToposHom B S hS (f ≫ g)).fSharp

AlgebraicGeometry.Space.exists_compRingIso_isCartesianComposition_comp_fSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleStructureMapComp.lean, line 595. The attribute's comment: “existence of the cartesian ring comparison”.

There is an isomorphism between the direct images of sheaves of commutative rings of the composite of morphisms of ringed topoi and of the composite morphism of algebraic spaces which is induced by cartesian composition and carries the structure map of the composite to the structure map of the composite morphism.

theorem exists_compRingIso_isCartesianComposition_comp_fSharp (f : X ⟶ Y) (g : Y ⟶ Z) :
    ∃ i : pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
        ((smallEtaleRingedToposHom B S hS g).comp
          (smallEtaleRingedToposHom B S hS f)).toToposHom ≅
      pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
        (smallEtaleRingedToposHom B S hS (f ≫ g)).toToposHom,
      IsCartesianComposition B S hS f g i ∧
        ((smallEtaleRingedToposHom B S hS g).comp
            (smallEtaleRingedToposHom B S hS f)).fSharp ≫
            i.hom.app (smallEtaleRingedTopos B S hS X).O =
          (smallEtaleRingedToposHom B S hS (f ≫ g)).fSharp

AlgebraicGeometry.Space.structureProjectionOfHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StructureProjectionComposition.lean, line 146. The attribute's comment: “compatibility with composition at the level of modules”.

[Stacks Project, Tag 03G8], compatibility with composition, at the level of modules. For f : X ⟶ Y and g : Y ⟶ Z the canonical morphism 𝒪_Z ⟶ (f ≫ g)_*𝒪_X of 𝒪_Z-modules is the canonical morphism 𝒪_Z ⟶ g_*𝒪_Y of g, followed by the direct image along g of the canonical morphism 𝒪_Y ⟶ f_*𝒪_X of f, followed by the composition comparison g_*(f_*𝒪_X) ⟶ (f ≫ g)_*𝒪_X of direct images of [Stacks Project, Tag 03LU].

The proof is the transposed one: by AlgebraicGeometry.Space.structureProjectionOfHom_eq_homEquiv_structureModulePullbackMap each of the three canonical morphisms is a transpose along the adjunction of [Stacks Project, Tag 03D7], the composition law for the comparison of inverse images is AlgebraicGeometry.Space.structureModulePullbackMap_comp, and transposing the resulting composite is AlgebraicGeometry.Space.homEquiv_modulePullbackCompIso_inv_app_comp followed by the two naturalities of CategoryTheory.Adjunction.homEquiv.

theorem structureProjectionOfHom_comp (f : X ⟶ Y) (g : Y ⟶ Z) :
    structureProjectionOfHom B S hS (f ≫ g) =
      structureProjectionOfHom B S hS g ≫
        (modulePushforward B S hS g).map (structureProjectionOfHom B S hS f) ≫
        (modulePushforwardCompIso B S hS f g).hom.app
          (SheafOfModules.unit (structureRingSheaf B S hS X))

AlgebraicGeometry.Space.isIso_structureProjectionOfHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StructureProjectionComposition.lean, line 261. The attribute's comment: “the canonical morphism of modules of an isomorphism is an isomorphism”.

The canonical morphism 𝒪_Y ⟶ e_*𝒪_X of modules of an isomorphism e of algebraic spaces is invertible.

Its underlying morphism of sheaves of sets is the structure map e.hom♯ (AlgebraicGeometry.Space.moduleSheafFunctor_map_structureProjectionOfHom), which is invertible by AlgebraicGeometry.Space.isIso_structureSharpSet, and the underlying-sheaf functor reflects isomorphisms.

theorem isIso_structureProjectionOfHom (e : X ≅ Y) :
    IsIso (structureProjectionOfHom B S hS e.hom)

Declarations registered for the tag:

AlgebraicGeometry.schemeSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHom.lean, line 712 (StacksFrontier): “schemes regarded as algebraic spaces”.

Tag 0BGS, a lemma

Tag 0BGS in the Stacks Project.

AlgebraicGeometry.Space.isReduced_globalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedGlobalFunctions.lean, line 172. The attribute's comment: “global_sections_reduced”.

Stacks 0BGS. The ring of global regular functions of a reduced algebraic space is reduced. Restriction to a reduced surjective étale chart embeds it into the ring of global regular functions of a reduced scheme.

theorem isReduced_globalFunctions (hF : IsAlgebraicSpace B S hS F)
    (hred : HasEtaleLocalProperty B S hS F
      (fun X : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced X)) :
    _root_.IsReduced (globalFunctions B S hS F)

AlgebraicGeometry.Space.eq_zero_of_forall_zeroLocus_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedGlobalFunctions.lean, line 188. The attribute's comment: “zero_of_full_vanishing_locus”.

Stacks 0BGS. A global regular function on a reduced algebraic space whose vanishing locus is all of F — its zero locus on every étale chart is the whole chart — is zero. It vanishes on a reduced surjective étale chart, hence is zero there by AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot, and restriction to that chart is injective.

theorem eq_zero_of_forall_zeroLocus_eq_univ (hF : IsAlgebraicSpace B S hS F)
    (hred : HasEtaleLocalProperty B S hS F
      (fun X : Scheme.{u} => _root_.AlgebraicGeometry.IsReduced X))
    (f : globalFunctions B S hS F)
    (hf : ∀ U : SmallEtale B S hS F,
      ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS F).obj U)).zeroLocus
        {f.val (op U)} = Set.univ) :
    f = 0

AlgebraicGeometry.Space.isReduced_iff_forall_localRing_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedLocalRings.lean, line 120. The attribute's comment: “reduced_iff_local_rings_reduced”.

Stacks 0BGS. An algebraic space is reduced exactly when all of its local rings are reduced. Reducedness of the space is the étale-local scheme property of Stacks 03E6 — a reduced surjective étale scheme chart — and reducedness of its local ring at a point is the chart condition of AlgebraicGeometry.Space.HasLocalRingPropertyAtPoint.

theorem isReduced_iff_forall_localRing_isReduced (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsReduced X) ↔
      ∀ x : points B S hS F,
        HasLocalRingPropertyAtPoint B S hS F hF x
          (fun (R : Type u) => fun [CommRing R] => _root_.IsReduced R)
          isReduced_localization_etale_invariant

Sources

LeanAlgebraicGeometry.Space.structurePresheaf_isSheaf · AlgebraicGeometry.Space.structureSheaf · AlgebraicGeometry.Space.pushforwardAlgebraIdAlgebraIso · AlgebraicGeometry.Space.isIso_fSharp_id · AlgebraicGeometry.Space.smallEtaleRingedToposHom · AlgebraicGeometry.Space.smallEtaleRingedToposHom_pushforward · AlgebraicGeometry.Space.smallEtaleRingedToposHom_representable · AlgebraicGeometry.Space.structureSharp_comp_chartProjectionSharpDirectImage

Section66.22 Stalks of the structure sheaf #

Section 66.22 of the Stacks Project, Tag 04KE. 6 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04KF, a lemma

Tag 04KF in the Stacks Project.

AlgebraicGeometry.Space.isHenselization_chartLocalRingToEtaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/EtaleLocalRingChartHenselization.lean, line 166. The attribute's comment: “the étale local ring is a strict henselization of a neighborhood stalk along the canonical map of Stacks 05VP”. References: SGA 4½ Arcata (2.3.1), “partial, special case”.

Stacks 04KF, with the structure map named. The étale local ring of an algebraic space at a geometric point x̄ is a strict henselization of the local ring 𝒪_{U, u} of a scheme chart at the point under the chosen lift, along the canonical map of Stacks 05VP AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing, with the separable closure of the residue field of 𝒪_{U, u} inside the residue field of the geometric point as the residue extension.

This is the form AlgebraicGeometry.Space.exists_algebra_isHenselization_etaleLocalRing_chart is proved from: there the algebra structure is produced existentially and an arbitrary chosen separable closure is matched to this one by uniqueness of separable closures, which is all the residue extension is used for. Naming the structure map is what lets a statement about 𝒪_{U, u} → 𝒪_{X, x̄} — flatness, locality, lengths, orders of vanishing — be read off the henselization.

theorem isHenselization_chartLocalRingToEtaleLocalRing {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) :
    @IsHenselization ↥(chartLocalRing B S hS X V) _ _
      (separableClosure (ResidueField ↥(chartLocalRing B S hS X V))
        (chartGeometricPoint V).residueField) _ _
      (etaleLocalRing B S hS X x : Type (u + 1)) _
      (isLocalRing_etaleLocalRing B S hS X hX x)
      (chartLocalRingToEtaleLocalRing B S hS X hX V).toAlgebra

AlgebraicGeometry.Space.exists_algebra_isHenselization_etaleLocalRing_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/EtaleLocalRingChartHenselization.lean, line 187. The attribute's comment: “the étale local ring is a strict henselization of a neighborhood stalk”. References: SGA 4½ Arcata (2.3.1), “special case”.

Stacks 04KF. The étale local ring of an algebraic space at a geometric point is a strict henselization of the local ring of a scheme chart at the point under the chosen lift, for every chosen separable algebraic closure of the residue field of that local ring. The algebra structure is the canonical map of Stacks 05VP.

theorem exists_algebra_isHenselization_etaleLocalRing_chart {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (p : chartScheme V.chart)
    (hp : chartPoint B S hS X V = p)
    (κsep : Type u) [Field κsep]
    [Algebra (ResidueField ((chartScheme V.chart).presheaf.stalk p : Type u)) κsep]
    [IsSepClosure (ResidueField ((chartScheme V.chart).presheaf.stalk p : Type u)) κsep] :
    letI : IsLocalRing (etaleLocalRing B S hS X x : Type (u + 1)) :=
      isLocalRing_etaleLocalRing B S hS X hX x
    ∃ alg : Algebra ((chartScheme V.chart).presheaf.stalk p : Type u)
        (etaleLocalRing B S hS X x : Type (u + 1)),
      @IsHenselization ((chartScheme V.chart).presheaf.stalk p : Type u) _ _ κsep _ _
        (etaleLocalRing B S hS X x : Type (u + 1)) _
        (isLocalRing_etaleLocalRing B S hS X hX x) alg

AlgebraicGeometry.Space.exists_algebra_isHenselization_etaleLocalRing_elementary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/EtaleLocalRingChartHenselization.lean, line 261. The attribute's comment: “the étale local ring is a strict henselization of an elementary neighborhood stalk”.

Stacks 04KF. The étale local ring of an algebraic space at a geometric point x̄ is a strict henselization of the local ring of an elementary étale neighborhood of the point below x̄, at its distinguished point, for every chosen separable algebraic closure of the residue field of that local ring.

theorem exists_algebra_isHenselization_etaleLocalRing_elementary (hxbar : xbar.LiesOver x)
    (κsep : Type u) [Field κsep]
    [instAlg : Algebra (ResidueField (U.scheme.left.1.presheaf.stalk U.point : Type u)) κsep]
    [instSep : IsSepClosure (ResidueField (U.scheme.left.1.presheaf.stalk U.point : Type u))
      κsep] :
    letI : IsLocalRing (etaleLocalRing B S hS X xbar : Type (u + 1)) :=
      isLocalRing_etaleLocalRing B S hS X hX xbar
    ∃ alg : Algebra (U.scheme.left.1.presheaf.stalk U.point : Type u)
        (etaleLocalRing B S hS X xbar : Type (u + 1)),
      @IsHenselization (U.scheme.left.1.presheaf.stalk U.point : Type u) _ _ κsep _ _
        (etaleLocalRing B S hS X xbar : Type (u + 1)) _
        (isLocalRing_etaleLocalRing B S hS X hX xbar) alg

AlgebraicGeometry.Space.etaleLocalRingEquivChart, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingChart.lean, line 603. The attribute's comment: “identification of the two étale stalks”.

The stalk of the structure sheaf of an algebraic space is canonically the étale local ring of a scheme étale neighborhood. The comparison sends ordinary chart germs and all common pointed étale-refinement germs to their scheme-side germs.

noncomputable def etaleLocalRingEquivChart
    (hF : IsAlgebraicSpace B S hS F)
    (V : SmallEtaleNeighborhood x)
    (E : BigEtaleSite.{u}) (hV : E.Contains (neighborhoodChartScheme V)) :
    { e : etaleLocalRing B S hS F x ≃+*
        _root_.AlgebraicGeometry.etaleLocalRing E (neighborhoodChartScheme V) hV
          (chartGeometricPoint V) //
      (∀ a : Γ(neighborhoodChartScheme V, ⊤),
        e (etaleLocalRingGerm B S hS F x (Opposite.op V) a) =
          structureSheafStalkFromLocalRing E (neighborhoodChartScheme V) hV
            (chartGeometricPoint V)
            ((neighborhoodChartScheme V).presheaf.germ ⊤
              ((chartGeometricPoint V).hom
                (closedPoint (chartGeometricPoint V).residueField)) trivial a)) ∧
      (∀ (W : SmallEtaleNeighborhood x) (f : W ⟶ V)
          (U : (geometricPointFiber E (neighborhoodChartScheme V) hV
            (chartGeometricPoint V)).Elementsᵒᵖ)
          (a : Γ(neighborhoodChartScheme W, ⊤))
          (hs : neighborhoodChartScheme W =
            (_root_.AlgebraicGeometry.SmallEtale.toScheme E
              (neighborhoodChartScheme V) hV).obj U.unop.1)
          (_hp : HEq (chartGeometricPoint W).hom U.unop.2.1)
          (_hf : HEq (neighborhoodChartMap f)
            (E.inclusion.map U.unop.1.obj.hom)),
        e (etaleLocalRingGerm B S hS F x (Opposite.op W) a) =
          (colimit.ι
            ((CategoryOfElements.π
              (geometricPointFiber E (neighborhoodChartScheme V) hV
                (chartGeometricPoint V))).op ⋙
              (_root_.AlgebraicGeometry.SmallEtale.structureSheaf E
                (neighborhoodChartScheme V) hV).obj)
            U).hom (show Γ((_root_.AlgebraicGeometry.SmallEtale.toScheme E
              (neighborhoodChartScheme V) hV).obj U.unop.1, ⊤) from hs ▸ a)) }

AlgebraicGeometry.Space.strictHenselizationEquivEtaleLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingChart.lean, line 641. The attribute's comment: “strict-henselization identification”.

The étale local ring of the algebraic space is the strict henselization of the local ring of a scheme étale neighborhood at the selected point.

noncomputable def strictHenselizationEquivEtaleLocalRing
    (hF : IsAlgebraicSpace B S hS F)
    (V : SmallEtaleNeighborhood x)
    (E : BigEtaleSite.{u}) (hV : E.Contains (neighborhoodChartScheme V))
    (T : IsLocalRing.HenselizationTower
      ((neighborhoodChartScheme V).presheaf.stalk
        ((chartGeometricPoint V).hom
          (closedPoint (chartGeometricPoint V).residueField)))
      (separableClosure (ResidueField
        ((neighborhoodChartScheme V).presheaf.stalk
          ((chartGeometricPoint V).hom
            (closedPoint (chartGeometricPoint V).residueField))))
        (chartGeometricPoint V).residueField)) :
    T.strictHenselization ≃+* etaleLocalRing B S hS F x

AlgebraicGeometry.Space.strictHenselizationEquivEtaleLocalRing_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingChart.lean, line 662. The attribute's comment: “compatibility with chart germs”.

The strict-henselization comparison sends the ordinary germ of a chart section to its germ in the algebraic-space structure sheaf.

theorem strictHenselizationEquivEtaleLocalRing_germ
    (hF : IsAlgebraicSpace B S hS F)
    (V : SmallEtaleNeighborhood x)
    (E : BigEtaleSite.{u}) (hV : E.Contains (neighborhoodChartScheme V))
    (T : IsLocalRing.HenselizationTower
      ((neighborhoodChartScheme V).presheaf.stalk
        ((chartGeometricPoint V).hom
          (closedPoint (chartGeometricPoint V).residueField)))
      (separableClosure (ResidueField
        ((neighborhoodChartScheme V).presheaf.stalk
          ((chartGeometricPoint V).hom
            (closedPoint (chartGeometricPoint V).residueField))))
        (chartGeometricPoint V).residueField))
    (a : Γ(neighborhoodChartScheme V, ⊤)) :
    (strictHenselizationEquivEtaleLocalRing hF V E hV T)
      (algebraMap _ T.strictHenselization
        ((neighborhoodChartScheme V).presheaf.germ ⊤
          ((chartGeometricPoint V).hom
            (closedPoint (chartGeometricPoint V).residueField)) trivial a)) =
      etaleLocalRingGerm B S hS F x (Opposite.op V) a

AlgebraicGeometry.Space.etaleLocalRingChartIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingEtaleInvariance.lean, line 305. The attribute's comment: “O_{X, xbar} = O_{U, ubar}”.

Stacks 04KF, first equality. Let X be an algebraic space over S, let x̄ be a geometric point of X and let (U, ū) be an étale neighbourhood of x̄ with U a scheme. Then the étale local ring of U at ū is the étale local ring of X at x̄.

Only the first of the two equalities of Stacks 04KF is proved here. The second, 𝒪_{U, ū} = 𝒪_{U, u}^{sh}, is Étale Cohomology, Lemma 04HX, which is not in the library.

noncomputable def etaleLocalRingChartIso {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (x : GeometricPoint B S hS F)
    (N : SmallEtaleNeighborhood x) :
    etaleLocalRing B S hS (yoneda.obj ((SmallEtale.toOver B S hS F).obj N.chart))
        (chartPresheafGeometricPoint B S hS x N) ≅ etaleLocalRing B S hS F x

Tag 04KG, a definition

Tag 04KG in the Stacks Project.

AlgebraicGeometry.Space.etaleLocalRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPoints.lean, line 387. The attribute's comment: “étale local ring”.

The étale local ring of an algebraic space at a geometric point: the stalk of the structure sheaf on the small étale site, i.e. the ring of germs at that point of regular functions on étale neighbourhoods.

noncomputable abbrev etaleLocalRing (x : GeometricPoint B S hS F) : CommRingCat.{u + 1}

AlgebraicGeometry.Space.strictHenselization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricPoints.lean, line 402. The attribute's comment: “strict henselization”. References: SGA 4½ Arcata (5.1.1).

The strict henselization of an algebraic space at a geometric point is the spectrum of its étale local ring.

noncomputable abbrev strictHenselization (x : GeometricPoint B S hS F) : Scheme.{u + 1}

Tag 04KH, a lemma

Tag 04KH in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleRingedSite_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleLocallyRinged.lean, line 135.

Stacks Project, Tag 04KH. The small étale site of an algebraic space, endowed with its structure sheaf, is a locally ringed site.

theorem smallEtaleRingedSite_isLocallyRinged (hF : IsAlgebraicSpace B S hS F) :
    RingedSite.IsLocallyRinged (smallEtaleRingedSite B S hS F hF)

Tag 04N9, a lemma

Tag 04N9 in the Stacks Project.

AlgebraicGeometry.Space.localRingDimension_eq_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocalRingGeometricStalk.lean, line 167.

Stacks 04N9. For a point x of an algebraic space and d in ℕ∞, the dimension of the local ring of the space at x is d exactly when the stalk at some geometric point above x has Krull dimension d, and exactly when the stalk at every geometric point above x does.

theorem localRingDimension_eq_tfae (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) (d : ℕ∞) :
    List.TFAE
      [localRingDimension B S hS x = d,
        ∃ xbar : GeometricPoint B S hS F, xbar.LiesOver x ∧
          ringKrullDim (etaleLocalRing B S hS F xbar) = (d : WithBot ℕ∞),
        ∀ xbar : GeometricPoint B S hS F, xbar.LiesOver x →
          ringKrullDim (etaleLocalRing B S hS F xbar) = (d : WithBot ℕ∞)]

Tag 0A4H, a lemma

Tag 0A4H in the Stacks Project.

AlgebraicGeometry.Space.dimensionAtPoint_eq_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionEtaleInvariance.lean, line 54. The attribute's comment: “dimension_at_point”.

Stacks 0A4H. An étale morphism of algebraic spaces preserves the dimension at a point.

theorem dimensionAtPoint_eq_of_isEtale (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsEtale B S hS f)
    (x : points B S hS X) :
    dimensionAtPoint B S hS X hX x =
      dimensionAtPoint B S hS Y hY (pointsMap B S hS X f x)

AlgebraicGeometry.Space.localRingDimension_pointsMap_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionEtaleInvariance.lean, line 68. The attribute's comment: “dimension_local_ring”.

Stacks 0A4H. An étale morphism of algebraic spaces preserves the dimension of the local ring at a point.

theorem localRingDimension_pointsMap_of_etale (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsEtale B S hS f)
    (x : points B S hS X) :
    localRingDimension B S hS (pointsMap B S hS X f x) = localRingDimension B S hS x

AlgebraicGeometry.Space.dimension_eq_of_isEtale_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionEtaleInvariance.lean, line 81. The attribute's comment: “dimension_surjective”.

Stacks 0A4H. A surjective étale morphism of algebraic spaces preserves the dimension.

theorem dimension_eq_of_isEtale_of_isSurjective (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsEtale B S hS f)
    (hfs : IsSurjective B S hS f) :
    dimension B S hS X hX = dimension B S hS Y hY

Tag 0E01, a lemma

Tag 0E01 in the Stacks Project.

AlgebraicGeometry.Space.isReduced_localRing_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocalRingGeometricStalk.lean, line 192.

Stacks 0E01. For a point x of an algebraic space, the local ring of the space at x is reduced exactly when the stalk at some geometric point above x is reduced, and exactly when the stalk at every geometric point above x is reduced.

theorem isReduced_localRing_tfae (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    List.TFAE
      [HasLocalRingPropertyAtPoint B S hS F hF x
          (fun (R : Type u) ↦ fun [CommRing R] ↦ _root_.IsReduced R)
          isReduced_localization_etale_invariant,
        ∃ xbar : GeometricPoint B S hS F, xbar.LiesOver x ∧
          _root_.IsReduced (etaleLocalRing B S hS F xbar),
        ∀ xbar : GeometricPoint B S hS F, xbar.LiesOver x →
          _root_.IsReduced (etaleLocalRing B S hS F xbar)]

Sources

Section66.23 Local irreducibility #

Section 66.23 of the Stacks Project, Tag 06DJ. 4 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06DK, a lemma

Tag 06DK in the Stacks Project.

AlgebraicGeometry.Space.uniqueBranch_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnibranchCriteria.lean, line 480.

Stacks 06DK. For a point x of an algebraic space F the five branch criteria are equivalent: a unique minimal prime in the local rings of the étale charts above x, a unique irreducible component of those charts through those points, unibranchness and geometric unibranchness of those local rings, and a unique minimal prime in the étale local ring at every geometric point above x.

theorem uniqueBranch_tfae (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    List.TFAE [HasUniqueMinimalPrimeOnEtaleCharts B S hS F x,
      HasUniqueIrreducibleComponentOnEtaleCharts B S hS F x,
      IsUnibranchOnEtaleCharts B S hS F x,
      IsGeometricallyUnibranchAt B S hS F x,
      HasUniqueMinimalPrimeAtGeometricPoints B S hS F x]

Tag 06DL, a definition

Tag 06DL in the Stacks Project.

AlgebraicGeometry.Space.IsGeometricallyUnibranchAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unibranch.lean, line 66. The attribute's comment: “at a point”.

Stacks 06DL, at a point. The presheaf F is geometrically unibranch at a point x of |F| when the local ring of every étale chart of F at every point above x is geometrically unibranch. This is condition (4) of Tag 06DK, which for an algebraic space is equivalent to the four other branch criteria there.

noncomputable def IsGeometricallyUnibranchAt (x : points B S hS F) : Prop

AlgebraicGeometry.Space.IsGeometricallyUnibranch, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unibranch.lean, line 78. The attribute's comment: “at every point”.

Stacks 06DL, at every point. The presheaf F is geometrically unibranch when it is geometrically unibranch at every point of |F|.

noncomputable abbrev IsGeometricallyUnibranch : Prop

Tag 0DQ3, a lemma

Tag 0DQ3 in the Stacks Project.

AlgebraicGeometry.Space.minimalPrimeCount_iff_componentCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BranchCount.lean, line 261. The attribute's comment: “conditions (1) and (2)”.

Stacks 0DQ3, conditions (1) and (2). A point of a presheaf on the big fppf site has minimal-prime count n on its étale scheme charts exactly when it has irreducible-component count n on them: the two counts agree at each chart point separately.

theorem minimalPrimeCount_iff_componentCount (x : points B S hS F) (n : ℕ) :
    HasMinimalPrimeCount B S hS x n ↔ HasComponentCount B S hS x n

AlgebraicGeometry.Space.componentCount_iff_branchCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BranchCount.lean, line 382. The attribute's comment: “conditions (2) and (3)”.

Stacks 0DQ3, conditions (2) and (3). A point of a presheaf on the big fppf site has irreducible-component count n on its étale scheme charts exactly when it has branch count n on them.

No algebraicity hypothesis is needed: both directions only use that an étale neighbourhood of a point of a chart above x is refined by an open subscheme of a chart above x.

theorem componentCount_iff_branchCount (x : points B S hS F) (n : ℕ) :
    HasComponentCount B S hS x n ↔ HasBranchCount B S hS x n

AlgebraicGeometry.Space.branchCount_iff_geometricBranchCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BranchCount.lean, line 400. The attribute's comment: “conditions (3) and (4)”.

Stacks 0DQ3, conditions (3) and (4). A point of an algebraic space has branch count n on its étale scheme charts exactly when every chart has exactly n geometric branches at every point above it.

theorem branchCount_iff_geometricBranchCount (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) (n : ℕ) :
    HasBranchCount B S hS x n ↔ HasGeometricBranchCount B S hS x n

AlgebraicGeometry.Space.geometricBranchCount_iff_etaleLocalRingMinimalPrimeCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BranchCount.lean, line 520. The attribute's comment: “conditions (4) and (5)”.

Stacks 0DQ3, conditions (4) and (5). Every étale scheme chart of an algebraic space has exactly n geometric branches at every point above x exactly when the étale local ring at every geometric point above x has exactly n minimal primes.

theorem geometricBranchCount_iff_etaleLocalRingMinimalPrimeCount
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) (n : ℕ) :
    HasGeometricBranchCount B S hS x n ↔
      HasEtaleLocalRingMinimalPrimeCount B S hS x n

Tag 0DQ4, a definition

Tag 0DQ4 in the Stacks Project.

AlgebraicGeometry.Space.numberOfGeometricBranches, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumberOfGeometricBranches.lean, line 98.

Stacks 0DQ4. The number of geometric branches of an algebraic space at a point: the natural number satisfying the equivalent conditions of Tag 0DQ3 if there is one, and ⊤ otherwise.

def numberOfGeometricBranches (x : points B S hS F) : ℕ∞

AlgebraicGeometry.Space.numberOfGeometricBranches_eq_nat_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumberOfGeometricBranches.lean, line 104. The attribute's comment: “finite value”.

Stacks 0DQ4. A finite value of the number of geometric branches of an algebraic space at a point is exactly the value appearing in the equivalent conditions of Tag 0DQ3.

theorem numberOfGeometricBranches_eq_nat_iff (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) (n : ℕ) :
    numberOfGeometricBranches B S hS x = (n : ℕ∞) ↔ HasGeometricBranchCount B S hS x n

AlgebraicGeometry.Space.numberOfGeometricBranches_eq_top_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NumberOfGeometricBranches.lean, line 113. The attribute's comment: “infinite value”.

Stacks 0DQ4. The number of geometric branches of an algebraic space at a point is infinite exactly when no natural number satisfies the equivalent conditions of Tag 0DQ3.

theorem numberOfGeometricBranches_eq_top_iff (x : points B S hS F) :
    numberOfGeometricBranches B S hS x = ⊤ ↔
      ∀ n : ℕ, ¬ HasGeometricBranchCount B S hS x n

Sources

LeanAlgebraicGeometry.Space.uniqueBranch_tfae · AlgebraicGeometry.Space.IsGeometricallyUnibranchAt · AlgebraicGeometry.Space.IsGeometricallyUnibranch · AlgebraicGeometry.Space.minimalPrimeCount_iff_componentCount · AlgebraicGeometry.Space.componentCount_iff_branchCount · AlgebraicGeometry.Space.branchCount_iff_geometricBranchCount · AlgebraicGeometry.Space.geometricBranchCount_iff_etaleLocalRingMinimalPrimeCount · AlgebraicGeometry.Space.numberOfGeometricBranches

Section66.24 Noetherian spaces #

Section 66.24 of the Stacks Project, Tag 03E9. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03EA, a definition

Tag 03EA in the Stacks Project.

AlgebraicGeometry.Space.IsNoetherian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianSpaces.lean, line 56.

An algebraic space over S is Noetherian when it is quasi-compact, quasi-separated and locally Noetherian. Quasi-separatedness is the absolute notion of Stacks 03BS, part (3), which is why the containment hZ of the terminal scheme in the site is required; local Noetherianity is the étale-local scheme property AlgebraicGeometry.IsLocallyNoetherian.

abbrev IsNoetherian (hZ : B.Contains (⊤_ Scheme.{u}))
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

Tag 04ZF, a lemma

Tag 04ZF in the Stacks Project.

AlgebraicGeometry.Space.isLocallyNoetherianSpace_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianPoints.lean, line 59. The attribute's comment: “part (1)”.

Stacks 04ZF, part (1). The space of points of a locally Noetherian algebraic space over S is a locally Noetherian topological space.

theorem isLocallyNoetherianSpace_of_isLocallyNoetherian
    (hN : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} ↦ IsLocallyNoetherian X)) :
    IsLocallyNoetherianSpace (points B S hS F)

AlgebraicGeometry.Space.noetherianSpace_of_isQuasiCompact_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianPoints.lean, line 75. The attribute's comment: “part (2)”.

Stacks 04ZF, part (2). The space of points of a quasi-compact locally Noetherian algebraic space over S is a Noetherian topological space.

theorem noetherianSpace_of_isQuasiCompact_of_isLocallyNoetherian
    (hqc : IsQuasiCompactSpace B S hS F)
    (hN : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} ↦ IsLocallyNoetherian X)) :
    NoetherianSpace (points B S hS F)

Tag 04ZG, a lemma

Tag 04ZG in the Stacks Project.

AlgebraicGeometry.Space.stacksSober_points_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianPointSpaceSober.lean, line 70. The attribute's comment: “sobriety”.

Stacks 04ZG, sobriety. The space of points of a Noetherian algebraic space over S is sober in the sense of Definition 004X: every irreducible closed subset of it has a unique generic point.

Only quasi-separatedness is used: it makes the space Zariski locally quasi-separated by Tag 03JX, (η) ⇒ (ζ) and Tag 03W7, so Tag 06NJ applies.

theorem stacksSober_points_of_isNoetherian (hF : IsAlgebraicSpace B S hS F)
    (hN : IsNoetherian B S hS hZ F) : StacksSober (points B S hS F)

AlgebraicGeometry.Space.noetherianSpace_points_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianPointSpaceSober.lean, line 82. The attribute's comment: “Noetherianity”.

Stacks 04ZG, Noetherianity. The space of points of a Noetherian algebraic space over S is a Noetherian topological space.

Only quasi-compactness and local Noetherianity are used, which is Tag 04ZF (2).

theorem noetherianSpace_points_of_isNoetherian (hF : IsAlgebraicSpace B S hS F)
    (hN : IsNoetherian B S hS hZ F) : NoetherianSpace (points B S hS F)

AlgebraicGeometry.Space.stacksSober_and_noetherianSpace_points_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianPointSpaceSober.lean, line 89.

Stacks 04ZG. The space of points of a Noetherian algebraic space over S is a sober Noetherian topological space.

theorem stacksSober_and_noetherianSpace_points_of_isNoetherian
    (hF : IsAlgebraicSpace B S hS F) (hN : IsNoetherian B S hS hZ F) :
    StacksSober (points B S hS F) ∧ NoetherianSpace (points B S hS F)

Tag 08AH, a lemma

Tag 08AH in the Stacks Project.

AlgebraicGeometry.Space.isLocalRing_etaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingNoetherian.lean, line 119. The attribute's comment: “local ring”.

Stacks 08AH. The étale local ring of an algebraic space at a geometric point is a local ring.

theorem isLocalRing_etaleLocalRing (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) (x : GeometricPoint B S hS F) :
    IsLocalRing (etaleLocalRing B S hS F x)

AlgebraicGeometry.Space.isNoetherianRing_etaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingNoetherian.lean, line 134. The attribute's comment: “Noetherian ring”.

Stacks 08AH. The étale local ring of a Noetherian algebraic space at a geometric point is a Noetherian ring.

theorem isNoetherianRing_etaleLocalRing (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hNoetherian : IsNoetherian B S hS hZ F) (x : GeometricPoint B S hS F) :
    IsNoetherianRing (etaleLocalRing B S hS F x)

Sources

LeanAlgebraicGeometry.Space.IsNoetherian · AlgebraicGeometry.Space.isLocallyNoetherianSpace_of_isLocallyNoetherian · AlgebraicGeometry.Space.noetherianSpace_of_isQuasiCompact_of_isLocallyNoetherian · AlgebraicGeometry.Space.stacksSober_points_of_isNoetherian · AlgebraicGeometry.Space.noetherianSpace_points_of_isNoetherian · AlgebraicGeometry.Space.stacksSober_and_noetherianSpace_points_of_isNoetherian · AlgebraicGeometry.Space.isLocalRing_etaleLocalRing · AlgebraicGeometry.Space.isNoetherianRing_etaleLocalRing

Section66.25 Regular algebraic spaces #

Section 66.25 of the Stacks Project, Tag 06LP. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06LQ, a lemma

Tag 06LQ in the Stacks Project.

AlgebraicGeometry.Space.isRegular_iff_etaleLocalRings_regular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalRingRegular.lean, line 88.

A locally Noetherian algebraic space is regular exactly when its étale local rings at all geometric points are regular local rings.

theorem isRegular_iff_etaleLocalRings_regular (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F)
    (hnoeth : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} ↦ IsLocallyNoetherian X)) :
    HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} ↦ IsRegular X) ↔
      ∀ x : GeometricPoint B S hS F, IsRegularLocalRing (etaleLocalRing B S hS F x)

Tag 0AH9, a definition

Tag 0AH9 in the Stacks Project.

AlgebraicGeometry.Space.IsRegularAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularLocalRings.lean, line 72.

An algebraic space is regular at a point when every étale scheme chart has a regular local ring at every point of it above that point.

abbrev IsRegularAt (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (x : points B S hS F) : Prop

AlgebraicGeometry.Space.isRegularAt_iff_exists_etale_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularLocalRings.lean, line 85. The attribute's comment: “some étale chart characterization”.

An algebraic space is regular at a point if and only if some étale scheme chart has a regular local ring at some point of it above that point.

theorem isRegularAt_iff_exists_etale_chart (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    IsRegularAt B S hS F x ↔
      ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ F),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) a ∧
        ∃ p : FieldValuedPoint B S hS (yoneda.obj U),
          pointsMap B S hS (yoneda.obj U) a (p.class B S hS (yoneda.obj U)) = x ∧
          IsRegularLocalRing
            (((BigFppfOver.toScheme B S hS).obj U).presheaf.stalk (schemePoint B S hS U p))

Tag 0AHA, a lemma

Tag 0AHA in the Stacks Project.

AlgebraicGeometry.Space.isRegularAt_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularAtGeometricPoints.lean, line 112.

Stacks 0AHA. For a point x of an algebraic space F the three conditions are equivalent: F is regular at x; the étale local ring of F is a regular local ring at every geometric point above x; and it is a regular local ring at some geometric point above x.

theorem isRegularAt_tfae (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) :
    List.TFAE
      [IsRegularAt B S hS F x,
        ∀ xbar : GeometricPoint B S hS F, xbar.LiesOver x →
          IsRegularLocalRing (etaleLocalRing B S hS F xbar),
        ∃ xbar : GeometricPoint B S hS F, xbar.LiesOver x ∧
          IsRegularLocalRing (etaleLocalRing B S hS F xbar)]

Tag 0BGT, a lemma

Tag 0BGT in the Stacks Project.

AlgebraicGeometry.Space.isNormal_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Normal.lean, line 160.

Stacks 0BGT. A regular algebraic space is normal: a surjective étale atlas by a regular scheme is one by a normal scheme.

theorem isNormal_of_isRegular (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hreg : HasEtaleLocalProperty B S hS F (fun X : Scheme.{u} => IsRegular X)) :
    HasEtaleLocalProperty B S hS F
      (fun X : Scheme.{u} => _root_.AlgebraicGeometry.IsNormal X)

Sources

LeanAlgebraicGeometry.Space.isRegular_iff_etaleLocalRings_regular · AlgebraicGeometry.Space.IsRegularAt · AlgebraicGeometry.Space.isRegularAt_iff_exists_etale_chart · AlgebraicGeometry.Space.isRegularAt_tfae · AlgebraicGeometry.Space.isNormal_of_isRegular

Section66.26 Sheaves of modules on algebraic spaces #

Section 66.26 of the Stacks Project, Tag 03LT. 5 tags here are carried by 40 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03LU, an equation

Tag 03LU in the Stacks Project.

AlgebraicGeometry.Space.modulePushforward_additive, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PushforwardPresentationExact.lean, line 498. The attribute's comment: “additivity of the direct image”.

The direct image of 𝒪-modules along a morphism of algebraic spaces is an additive functor.

instance modulePushforward_additive (f : X ⟶ Y) :
    (modulePushforward B S hS f).Additive

AlgebraicGeometry.Space.moduleSheafFunctor_map_compIsoCongr_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafOfDifferentialsComp.lean, line 271. The attribute's comment: “the composition comparison for direct images is the geometric comparison”.

Stacks 03LU. The comparison f_* ∘ g_* ≅ (f ≫ g)_* of direct images of 𝒪-modules is the geometric comparison AlgebraicGeometry.Space.smallToposMorphismTypeU_comp of Stacks 03G2, part (3), on underlying sheaves of sets. The comparison appears in the transported form that AlgebraicGeometry.Space.modulePushforwardCompIso_eq_compIsoCongr identifies it with, and AlgebraicGeometry.Space.modulePushforwardCompIso_hom_app_eq is that identification at a single module.

theorem moduleSheafFunctor_map_compIsoCongr_hom_app (f : X ⟶ Y) (g : Y ⟶ Z)
    (F : Modules.{u, u} B S hS X.1 X.2) :
    (Sheaf.moduleSheafFunctor (structureRingSheaf B S hS Z)).map
        ((CategoryTheory.Functor.compIsoCongr
          (pushforwardModules_eq_modulePushforward B S hS f)
          (pushforwardModules_eq_modulePushforward B S hS g)
          (pushforwardModules_eq_modulePushforward B S hS (f ≫ g))
          (pushforwardModulesCompAt B S hS f g)).hom.app F) =
      (smallToposMorphismTypeU_comp B S hS f g).hom.app
        ((Sheaf.moduleSheafFunctor (structureRingSheaf B S hS X)).obj F)

AlgebraicGeometry.Space.modulePushforwardCompIso', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModuleCompIso.lean, line 153. The attribute's comment: “pushforward composition”.

Stacks 03LU, the composition comparison for the direct image of modules. The composite of the direct images of 𝒪-modules along f : X ⟶ Y and then g : Y ⟶ Z is canonically isomorphic to the direct image along f ≫ g.

The comparison is the composition law for the direct image of modules along a composite morphism of ringed topoi, followed by the transport of the direct image of modules along Stacks 03G8's cartesian comparison of the direct images of sheaves of sets.

This is the statement in the RingedToposHom.pushforwardModules presentation. The same part key also sits on AlgebraicGeometry.Space.modulePushforwardCompIso of StacksFrontier.AlgebraicGeometry.Spaces.SmallEtaleModulePullbackComp, which states the same comparison in the library's primary AlgebraicGeometry.Space.modulePushforward vocabulary and is what consumers outside this presentation use; the two are identified by AlgebraicGeometry.Space.modulePushforwardCompIso_eq_modulePushforwardCompIso'. A tag carried by both is correct, not a duplication: each presentation states the clause in its own vocabulary.

noncomputable def modulePushforwardCompIso' (f : X ⟶ Y) (g : Y ⟶ Z) :
    (smallEtaleRingedToposHom B S hS f).pushforwardModules ⋙
        (smallEtaleRingedToposHom B S hS g).pushforwardModules ≅
      (smallEtaleRingedToposHom B S hS (f ≫ g)).pushforwardModules

AlgebraicGeometry.Space.modulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullback.lean, line 78. The attribute's comment: “pullback”.

The pullback f^*G = 𝒪_X ⊗_{f⁻¹𝒪_Y} f⁻¹G of 𝒪_Y-modules along a morphism f : X ⟶ Y of algebraic spaces.

noncomputable def modulePullback (f : X ⟶ Y) :
    Modules.{u, u} B S hS Y.1 Y.2 ⥤ Modules.{u, u} B S hS X.1 X.2

AlgebraicGeometry.Space.modulePullbackAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullback.lean, line 206. The attribute's comment: “the adjunction”.

Pullback of 𝒪-modules along a morphism of algebraic spaces is left adjoint to the pushforward AlgebraicGeometry.Space.modulePushforward: there is a bijection Hom_{𝒪_X}(f^*G, F) = Hom_{𝒪_Y}(G, f_*F), natural in both variables.

noncomputable def modulePullbackAdjunction (f : X ⟶ Y) :
    modulePullback B S hS f ⊣ modulePushforward B S hS f

AlgebraicGeometry.Space.modulePushforwardCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackComp.lean, line 366. The attribute's comment: “pushforward composition”.

The canonical comparison f_* ∘ g_* ≅ (f ≫ g)_* of direct images of 𝒪-modules along a composite of morphisms of algebraic spaces.

Both sides have the direct image of sheaves of sets of the composite as their underlying sheaf, and the comparison is AlgebraicGeometry.Space.smallToposMorphismTypeU_comp, the comparison of Stacks 03G2, part (3), on it.

noncomputable def modulePushforwardCompIso (f : X ⟶ Y) (g : Y ⟶ Z) :
    modulePushforward B S hS f ⋙ modulePushforward B S hS g ≅
      modulePushforward B S hS (f ≫ g)

AlgebraicGeometry.Space.modulePushforwardCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackComp.lean, line 366. The attribute's comment: “the composition comparison for direct images”.

The canonical comparison f_* ∘ g_* ≅ (f ≫ g)_* of direct images of 𝒪-modules along a composite of morphisms of algebraic spaces.

Both sides have the direct image of sheaves of sets of the composite as their underlying sheaf, and the comparison is AlgebraicGeometry.Space.smallToposMorphismTypeU_comp, the comparison of Stacks 03G2, part (3), on it.

noncomputable def modulePushforwardCompIso (f : X ⟶ Y) (g : Y ⟶ Z) :
    modulePushforward B S hS f ⋙ modulePushforward B S hS g ≅
      modulePushforward B S hS (f ≫ g)

AlgebraicGeometry.Space.modulePullbackCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackComp.lean, line 457. The attribute's comment: “pullback composition”.

The canonical comparison g^* ∘ f^* ≅ (f ≫ g)^* of inverse images of 𝒪-modules along a composite of morphisms of algebraic spaces.

Both functors are left adjoint to (f ≫ g)_*: the left-hand side by AlgebraicGeometry.Space.moduleCompAdjunction, which composes the two adjunctions and reads the resulting right adjoint through modulePushforwardCompIso, and the right-hand side by AlgebraicGeometry.Space.modulePullbackAdjunction. The comparison is the uniqueness of a left adjoint, so it is the mate of the comparison of direct images.

noncomputable def modulePullbackCompIso (f : X ⟶ Y) (g : Y ⟶ Z) :
    modulePullback B S hS g ⋙ modulePullback B S hS f ≅ modulePullback B S hS (f ≫ g)

AlgebraicGeometry.Space.modulePullbackCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackComp.lean, line 457. The attribute's comment: “the composition comparison for pullbacks”.

The canonical comparison g^* ∘ f^* ≅ (f ≫ g)^* of inverse images of 𝒪-modules along a composite of morphisms of algebraic spaces.

Both functors are left adjoint to (f ≫ g)_*: the left-hand side by AlgebraicGeometry.Space.moduleCompAdjunction, which composes the two adjunctions and reads the resulting right adjoint through modulePushforwardCompIso, and the right-hand side by AlgebraicGeometry.Space.modulePullbackAdjunction. The comparison is the uniqueness of a left adjoint, so it is the mate of the comparison of direct images.

noncomputable def modulePullbackCompIso (f : X ⟶ Y) (g : Y ⟶ Z) :
    modulePullback B S hS g ⋙ modulePullback B S hS f ≅ modulePullback B S hS (f ≫ g)

AlgebraicGeometry.Space.modulePushforwardIdIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackId.lean, line 307. The attribute's comment: “the unit law for the direct image”.

The unit law of Stacks 03LU for the direct image: the direct image of 𝒪-modules along an identity morphism of algebraic spaces is the identity functor.

The direct image of sheaves of sets along an identity is the identity functor, and the structure map of the identity is the corresponding identification of the structure sheaves (AlgebraicGeometry.Space.structureSharpSet_id), which is exactly the input AlgebraicGeometry.RingedToposHom.pushforwardModulesIsoId asks for.

This is the datum that the idIso field of AlgebraicGeometry.Space.ModulePushforwardCoherence assumes.

def modulePushforwardIdIso (X : AlgebraicSpaces B S hS) :
    modulePushforward B S hS (𝟙 X) ≅ 𝟭 (Modules.{u, u} B S hS X.1 X.2)

AlgebraicGeometry.Space.modulePullbackIdIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackId.lean, line 323. The attribute's comment: “the unit law: the inverse image of modules along an identity is the identity functor”.

The unit law of Stacks 03LU: the inverse image of 𝒪-modules along an identity morphism of algebraic spaces is the identity functor.

The inverse image is a left adjoint of the direct image by AlgebraicGeometry.Space.modulePullbackAdjunction, the direct image along an identity is the identity functor by AlgebraicGeometry.Space.modulePushforwardIdIso, and a left adjoint of the identity functor is the identity functor.

def modulePullbackIdIso (X : AlgebraicSpaces B S hS) :
    modulePullback B S hS (𝟙 X) ≅ 𝟭 (Modules.{u, u} B S hS X.1 X.2)

AlgebraicGeometry.Space.modulePushforwardCompIso_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePushforwardCompIsoAssoc.lean, line 287. The attribute's comment: “the associativity of the composition comparison for direct images”.

Stacks 03LU, associativity of the composition comparison for direct images. For three composable morphisms f : W ⟶ X, g : X ⟶ Y, h : Y ⟶ Z of algebraic spaces the two ways of comparing f_* ∘ g_* ∘ h_* with (f ≫ g ≫ h)_* agree.

This is the assoc field of AlgebraicGeometry.Space.ModulePushforwardCoherence, so it is no longer a hypothesis. It is the cocycle law at the morphisms of ringed topoi of Stacks 03G8, AlgebraicGeometry.Space.pushforwardModulesCompAt_assoc, transported along the identifications of the two direct images.

theorem modulePushforwardCompIso_assoc (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
    isoWhiskerLeft (modulePushforward B S hS f) (modulePushforwardCompIso B S hS g h) ≪≫
        modulePushforwardCompIso B S hS f (g ≫ h) =
      (associator (modulePushforward B S hS f) (modulePushforward B S hS g)
          (modulePushforward B S hS h)).symm ≪≫
        isoWhiskerRight (modulePushforwardCompIso B S hS f g)
          (modulePushforward B S hS h) ≪≫
        modulePushforwardCompIso B S hS (f ≫ g) h

AlgebraicGeometry.Space.modulePushforwardCoherence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePushforwardIdIso.lean, line 45. The attribute's comment: “the pseudofunctoriality of the direct image, assembled: the identity comparison together with the associativity and the two unit laws of the composition comparison, as one datum with no hypothesis”.

Pseudofunctoriality of the direct image of 𝒪-modules of Stacks 03LU, with no hypothesis. The identity datum is AlgebraicGeometry.Space.modulePushforwardIdIso, and AlgebraicGeometry.Space.modulePushforwardCoherenceOfIdIso supplies the associativity coherence and the two unit laws from it.

noncomputable def modulePushforwardCoherence : ModulePushforwardCoherence B S hS

AlgebraicGeometry.Space.modulePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StructureMapSharp.lean, line 573. The attribute's comment: “pushforward”.

Stacks 03D6, part (1), unconditionally, and the direct-image half of Stacks 03LU: the direct image of 𝒪_X-modules along a morphism of algebraic spaces, read as 𝒪_Y-modules by restriction of scalars along the structure map.

The inverse-image half of Stacks 03LU is AlgebraicGeometry.Space.modulePullback, and the adjunction is AlgebraicGeometry.Space.modulePullbackAdjunction (StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullback.lean). That adjunction is stated for the direct image of Stacks 03D6, part (1) attached to the morphism of ringed topoi, which is this functor up to a comparison that is not yet supplied; see the implementation notes of that file.

noncomputable def modulePushforward (f : X ⟶ Y) :
    Modules.{u, u} B S hS X.1 X.2 ⥤ Modules.{u, u} B S hS Y.1 Y.2

AlgebraicGeometry.RingedSite.HomGeneral.pullbackModulesToposIsoGeneral_hom_app_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/RingedToposModulesPullbackToposGeneralUnit.lean, line 305. The attribute's comment: “the corepresentability construction of f^*𝒪_Y ≅ 𝒪_X for the pullback of the modules development and Mathlib's adjoint-transpose construction for the site-presented pullback agree under the comparison of the two pullbacks, for a morphism of ringed sites at independent universes”.

The two constructions of Stacks 03LU along a morphism of ringed sites agree. The comparison AlgebraicGeometry.RingedSite.HomGeneral.pullbackModulesToposIsoGeneral of the two pullbacks of sheaves of modules carries the corepresentability identification Stacks.Sheaves.RingedToposModules.pullbackModulesObjUnitIso of f^*𝒪_Y ≅ 𝒪_X to Mathlib's adjoint-transpose one, SheafOfModules.pullbackObjUnitToUnit at f^♯.

Both are pinned by their transposes along Stacks 03D7, those two transposes are compared by homEquiv_pullbackModulesToposIsoGeneral_hom_app_unit, and they agree because both are the unit section of 𝒪_X.

public theorem HomGeneral.pullbackModulesToposIsoGeneral_hom_app_unit :
    f.pullbackModulesToposIsoGeneral.hom.app
          (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf (toRingedTopos Y).O)) ≫
        SheafOfModules.pullbackObjUnitToUnit f.toRingedToposSiteHom.fSharpRing =
      (pullbackModulesObjUnitIso f.toRingedToposHom.toRingedToposModulesHom).inv

Tag 03LV, a lemma

Tag 03LV in the Stacks Project.

AlgebraicGeometry.Space.etaleInverseImageStructureSheafIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleInverseImageStructureSheaf.lean, line 154. The attribute's comment: “the canonical structure map”.

The forward map of AlgebraicGeometry.Space.etaleInverseImageStructureSheafIso is the inverse-image form of the structure map of Stacks 03G8. This is what makes that isomorphism the canonical one of Stacks 03LV rather than an arbitrary one.

theorem etaleInverseImageStructureSheafIso_hom (h : U ⟶ V) (hh : IsEtale B S hS h.hom) :
    (etaleInverseImageStructureSheafIso B S hS h hh).hom =
      (smallEtaleRingedToposHom B S hS h).fSharpInverseImage

AlgebraicGeometry.Space.modulePullbackIsoEtaleModuleInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackComparison.lean, line 166. The attribute's comment: “pullback of modules is inverse image”.

Stacks 03LV. Along an étale morphism of algebraic spaces, the pullback of 𝒪_Y-modules of Stacks 03LU is naturally isomorphic to the inverse image of modules with its scalars transported along the canonical isomorphism of structure sheaves.

noncomputable def modulePullbackIsoEtaleModuleInverseImage :
    modulePullback B S hS f ≅ etaleModuleInverseImage B S hS f hf

AlgebraicGeometry.Space.modulePullbackIsoEtaleModuleInverseImage_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackComparison.lean, line 178. The attribute's comment: “canonical module comparison”.

Stacks 03LV. The comparison of the pullback of modules with the inverse image sends the canonical image of every section of the inverse image to that same section. This specifies the comparison, rather than merely asserting that the two functors are isomorphic: a scalar-unit twist of the natural isomorphism is excluded.

theorem modulePullbackIsoEtaleModuleInverseImage_unit_app
    (G : Modules.{u, u} B S hS Y.1 Y.2) (U : (SmallEtale B S hS X.1)ᵒᵖ)
    (m : ((inverseImageModules (smallEtaleRingedToposHom B S hS f).toToposHom
      (structureRingSheaf B S hS Y)).obj G).val.obj U) :
    ((extendScalarsFSharpAdjunction B S hS f).unit.app
          ((inverseImageModules (smallEtaleRingedToposHom B S hS f).toToposHom
            (structureRingSheaf B S hS Y)).obj G) ≫
        (SheafOfModules.restrictScalars
          (smallEtaleRingedToposModulesHom B S hS f).fSharpInverseImage).map
            ((modulePullbackIsoEtaleModuleInverseImage B S hS f hf).hom.app G)).val.app U m =
      m

AlgebraicGeometry.Space.modulePullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackComparison.lean, line 200. The attribute's comment: “exactness”.

Stacks 03LV. Pullback of sheaves of modules along an étale morphism of algebraic spaces is exact. Through the comparison with the inverse image both halves are the exactness of the inverse image of modules of Stacks 04JC, restriction of scalars along an isomorphism being an equivalence.

theorem modulePullback_exact :
    exactFunctor (Modules.{u, u} B S hS Y.1 Y.2) (Modules.{u, u} B S hS X.1 X.2)
      (modulePullback B S hS f)

AlgebraicGeometry.Space.modulePullbackIsoEtaleModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackRestriction.lean, line 370. The attribute's comment: “the identification f^*G = G|_{X_étale}”.

Stacks Equation 03LW, that is clause (2) of Stacks 03LV. Along an étale morphism f : X ⟶ Y of algebraic spaces the pullback of 𝒪_Y-modules of Stacks 03LU is naturally isomorphic to étale restriction: f^*G is the sheaf whose sections over an étale chart U of X are the sections of G over the composite chart of Y.

The comparison factors through the inverse image of modules by AlgebraicGeometry.Space.modulePullbackIsoEtaleModuleInverseImage, which is clause (2) of Stacks 03LV in its inverse-image reading.

noncomputable def modulePullbackIsoEtaleModulePullback :
    modulePullback B S hS f ≅ etaleModulePullback.{u, u} B S hS f hf

AlgebraicGeometry.Space.isIso_fSharpInverseImage_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleStructureSheafInverseImage.lean, line 377. The attribute's comment: “the inverse image of the structure sheaf, h⁻¹𝒪_V = 𝒪_U”.

Stacks 03LV. For an étale morphism of algebraic spaces the inverse-image form f⁻¹𝒪_Y ⟶ 𝒪_X of the structure map of the morphism of small étale ringed topoi of Stacks 03G8 is an isomorphism.

The proof exhibits it as a universal arrow: composition with it is identified with the inverse of the composite of AlgebraicGeometry.Space.fMapRestrictionEquiv with the chart correspondence and the adjunction, and the chartwise formula for the structure map says that the identification sends the structure map itself to the identity.

theorem isIso_fSharpInverseImage_of_isEtale :
    IsIso (smallEtaleRingedToposHom B S hS f).fSharpInverseImage

AlgebraicGeometry.Space.etaleStructureSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleStructureSheafInverseImage.lean, line 424. The attribute's comment: “inverse image of the structure sheaf”.

Stacks 03LV. For an étale morphism of algebraic spaces the inverse image of the structure sheaf of the target along the morphism of small étale ringed topoi of Stacks 03G8 is canonically isomorphic to the structure sheaf of the source.

noncomputable def etaleStructureSheafIso :
    (Stacks.Sheaves.ToposPushforward.inverseImageCommRingFunctor
        (smallEtaleRingedToposHom B S hS f).toToposHom).obj
      (smallEtaleRingedTopos B S hS Y).O ≅ (smallEtaleRingedTopos B S hS X).O

AlgebraicGeometry.Space.etaleStructureSheafIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleStructureSheafInverseImage.lean, line 435. The attribute's comment: “canonical structure map”.

Stacks 03LV. The forward map of the canonical isomorphism of structure sheaves along an étale morphism is the inverse-image form of the structure map; the isomorphism is not an extra choice.

theorem etaleStructureSheafIso_hom :
    (etaleStructureSheafIso B S hS f hf).hom =
      (smallEtaleRingedToposHom B S hS f).fSharpInverseImage

Tag 03LW, an equation

Tag 03LW in the Stacks Project.

AlgebraicGeometry.Space.modulePullbackIsoEtaleModuleInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackComparison.lean, line 166. The attribute's comment: “the identification f^*G = f_small^{-1}G along an étale morphism”.

Stacks 03LV. Along an étale morphism of algebraic spaces, the pullback of 𝒪_Y-modules of Stacks 03LU is naturally isomorphic to the inverse image of modules with its scalars transported along the canonical isomorphism of structure sheaves.

noncomputable def modulePullbackIsoEtaleModuleInverseImage :
    modulePullback B S hS f ≅ etaleModuleInverseImage B S hS f hf

AlgebraicGeometry.Space.etaleModuleInverseImageIsoEtaleModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackRestriction.lean, line 341. The attribute's comment: “the inverse image of modules is étale restriction”.

Stacks' Equation 03LW, the outer identification G|_{X_étale} = f_{small}^{-1}G: the inverse image of 𝒪_Y-modules along an étale morphism, read over 𝒪_X through the canonical isomorphism of structure sheaves, is étale restriction of modules.

noncomputable def etaleModuleInverseImageIsoEtaleModulePullback :
    etaleModuleInverseImage B S hS f hf ≅ etaleModulePullback.{u, u} B S hS f hf

AlgebraicGeometry.Space.modulePullbackIsoEtaleModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackRestriction.lean, line 370. The attribute's comment: “pullback of modules along an étale morphism is étale restriction”.

Stacks Equation 03LW, that is clause (2) of Stacks 03LV. Along an étale morphism f : X ⟶ Y of algebraic spaces the pullback of 𝒪_Y-modules of Stacks 03LU is naturally isomorphic to étale restriction: f^*G is the sheaf whose sections over an étale chart U of X are the sections of G over the composite chart of Y.

The comparison factors through the inverse image of modules by AlgebraicGeometry.Space.modulePullbackIsoEtaleModuleInverseImage, which is clause (2) of Stacks 03LV in its inverse-image reading.

noncomputable def modulePullbackIsoEtaleModulePullback :
    modulePullback B S hS f ≅ etaleModulePullback.{u, u} B S hS f hf

AlgebraicGeometry.Space.modulePullbackIsoEtaleModulePullback_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleModulePullbackRestriction.lean, line 385. The attribute's comment: “canonical module comparison”.

Stacks Equation 03LW, canonicity. The comparison of the pullback of modules with étale restriction sends the canonical image of a section of the inverse image of modules to the comparison of Stacks 03LQ applied to that section, so it introduces no twist of its own: it is the canonical identification and not merely some natural isomorphism of the two functors.

This is AlgebraicGeometry.Space.modulePullbackIsoEtaleModuleInverseImage_unit_app, which pins the extension-of-scalars half, followed by AlgebraicGeometry.Space.etaleModuleInverseImageIsoEtaleModulePullback_val_app, which pins the transport half.

theorem modulePullbackIsoEtaleModulePullback_unit_app (G : Modules.{u, u} B S hS Y.1 Y.2)
    (U : (SmallEtale B S hS X.1)ᵒᵖ)
    (m : ((inverseImageModules.{u, u, u, u + 1, u, u + 1}
      (smallEtaleRingedToposHom B S hS f).toToposHom
      (structureRingSheaf B S hS Y)).obj G).val.obj U) :
    ((extendScalarsFSharpAdjunction B S hS f).unit.app
          ((inverseImageModules.{u, u, u, u + 1, u, u + 1}
            (smallEtaleRingedToposHom B S hS f).toToposHom
            (structureRingSheaf B S hS Y)).obj G) ≫
        (SheafOfModules.restrictScalars
          (smallEtaleRingedToposModulesHom B S hS f).fSharpInverseImage).map
            ((modulePullbackIsoEtaleModulePullback B S hS f hf).hom.app G)).val.app U m =
      ((etaleModuleInverseImageIsoRestrictionTransport B S hS f hf).hom.app G).val.app U m

Tag 03LX, a lemma

Tag 03LX in the Stacks Project.

AlgebraicGeometry.Space.isIso_moduleEtaleBaseChangeComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleEtaleBaseChangeHFace.lean, line 692. The attribute's comment: “the ordinary direct image, for the CANONICAL comparison map and for an ÉTALE square: g étale, not merely flat, so this is a special case of Stacks 073K part (1) and not that tag. The existing 03LX attributes carry isomorphisms with the right endpoints that are not identified with the canonical map”.

Stacks 03LX for the ordinary direct image, read as a statement about the canonical map, in the étale case. For a cartesian square of algebraic spaces whose bottom arrow g is étale, the canonical base-change comparison

(f_*F)|_{Y'} ⟶ f'_*(F|_{X'})

of AlgebraicGeometry.Space.moduleEtaleBaseChangeComparison is an isomorphism.

This is what StacksFrontier/AlgebraicGeometry/Spaces/ModuleHigherPushforwardBaseChangeCanonical.lean records as the single underived statement the canonical reading of Stacks 03LX and Stacks 071Z was owed. It is AlgebraicGeometry.Space.isIso_moduleBaseChangeMap_of_isEtale conjugated into the étale-restriction spelling by Stacks 03LW, AlgebraicGeometry.Space.modulePullbackIsoEtaleModulePullback, which is canonical, so the conjugation introduces no twist.

This is the étale case and not Stacks 073K, part (1). Stacks 073K, part (1) asserts base change for g merely flat and f quasi-compact and quasi-separated; hg here is AlgebraicGeometry.Space.IsEtale, and étale is strictly stronger than flat. So this is a special case of that tag and carries no attribute for it.

theorem isIso_moduleEtaleBaseChangeComparison (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom) :
    IsIso (moduleEtaleBaseChangeComparison B S hS i f' f g sq hg)

AlgebraicGeometry.Space.moduleHigherPushforwardEtaleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleHigherPushforwardEtaleBaseChange.lean, line 147. The attribute's comment: “the higher direct images”.

Let
X' --i--> X
|f'       |f
Y' --g--> Y
be a cartesian square of algebraic spaces over S with g étale. Then for every n the n-th higher direct image of 𝒪_X-modules commutes with restriction along the étale base change,

R^n f'_*(F|_{X'}) = (R^n f_*F)|_{Y'}

in Mod(𝒪_{Y'}), naturally in the 𝒪_X-module F. The morphism f is not assumed representable, quasi-compact or quasi-separated, and F is not assumed quasi-coherent.

noncomputable def moduleHigherPushforwardEtaleBaseChangeIso (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom) (n : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    have := hasInjectiveResolutions_modules B S hS X'.1 X'.2
    etaleModulePullback B S hS i (isEtale_of_isPullback B S hS f' i g f sq.flip hg) ⋙
        (modulePushforward B S hS f').rightDerived n ≅
      (modulePushforward B S hS f).rightDerived n ⋙ etaleModulePullback B S hS g hg

AlgebraicGeometry.Space.modulePullbackSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModulePushforwardEtaleBaseChange.lean, line 820. The attribute's comment: “the footnote, with both restrictions read as the inverse image of modules (Stacks 03LW)”.

Stacks 03LX, the footnote. For a commutative — in particular a cartesian — square
X' --i--> X
|f'       |f
Y' --g--> Y
of algebraic spaces, the inverse image of modules around the square agrees: (f')^*(G|_{Y'}) = (f^*G)|_{X'} for every 𝒪_Y-module G, naturally in G.

Both restrictions are read as the inverse image of modules, so all four functors in the statement are AlgebraicGeometry.Space.modulePullback — the source's G|_{Y'} is g^*G and its (-)|_{X'} is i^*. That is the reading of Stacks 03LW, which the source's own footnote invokes to derive this identity, and which this development does not supply: no comparison of AlgebraicGeometry.Space.modulePullback with the étale restriction AlgebraicGeometry.Space.etaleModulePullback used elsewhere in this file is proved anywhere, and the two are different functors (the tensor inverse image of Stacks 03D6, part (2) against restriction along AlgebraicGeometry.Space.smallEtalePostcomp). So what is proved here is the footnote in the inverse-image reading, not in the restriction reading, and the attribute says so.

No étaleness is used: as in the source, the comparison is the Stacks 03LU composition isomorphism AlgebraicGeometry.Space.modulePullbackCompIso for the two factorizations of the diagonal X' ⟶ Y of the square, glued by the commutativity sq.w of the square; only sq.w is consumed, so the cartesian hypothesis is stronger than the proof needs. The module universe is the universe u of the structure rings, which is the only one at which AlgebraicGeometry.Space.modulePullback exists.

noncomputable def modulePullbackSquareIso (sq : IsPullback i f' f g) :
    modulePullback B S hS g ⋙ modulePullback B S hS f' ≅
      modulePullback B S hS f ⋙ modulePullback B S hS i

AlgebraicGeometry.Space.modulePushforwardEtaleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StructureSharpBaseChange.lean, line 825. The attribute's comment: “the ordinary direct image”.

Stacks 03LX, the ordinary direct image, unconditionally. Let
X' --i--> X
|f'       |f
Y' --g--> Y
be a cartesian square of algebraic spaces over a scheme S contained in a big fppf site B, with g étale. Then for every 𝒪_X-module F

f'_*(F|_{X'}) = (f_*F)|_{Y'}

in Mod(𝒪_{Y'}), naturally in F.

This is AlgebraicGeometry.Space.modulePushforwardEtaleBaseChangeIsoOfStructureSharp with its hypothesis discharged by AlgebraicGeometry.Space.baseChangeStructureSharp_comp_baseChangeRingMap. The higher direct images of Stacks 03LX are not treated, so the attribute carries a part string; the footnote is AlgebraicGeometry.Space.modulePullbackSquareIso.

The restriction (-)|_{X'} is read here as AlgebraicGeometry.Space.etaleModulePullback, restriction of modules along small étale postcomposition, which is the reading of the ordinary clause; the footnote is proved in the inverse-image reading instead, for the reason recorded in its own docstring.

Inherited caveat. The source asserts an equality, and this isomorphism has the right endpoints but is not proved to be the adjunction mate of the inverse-image identification around the square: that is already the standing in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePushforwardBaseChange.lean, whose implementation notes record it for AlgebraicGeometry.Space.smallEtalePushforwardBaseChangeIso, and the same applies to the Type u instance of Stacks 03LR, part (1) that this isomorphism is built from.

The module universe is the universe u of the structure rings, which is the only one at which AlgebraicGeometry.Space.modulePushforward exists.

noncomputable def modulePushforwardEtaleBaseChangeIso (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom) :
    etaleModulePullback B S hS i (isEtale_of_isPullback B S hS f' i g f sq.flip hg) ⋙
        modulePushforward B S hS f' ≅
      modulePushforward B S hS f ⋙ etaleModulePullback B S hS g hg

Tag 03LY, a lemma

Tag 03LY in the Stacks Project.

AlgebraicGeometry.Space.chartModuleInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 241. The attribute's comment: “the chartwise pullback of modules”.

Stacks 03LY. The pullback of 𝒪-modules of Stacks 03LU along the morphism of algebraic spaces represented by a morphism of étale scheme charts of X. This is the functor f_{small}^* in which the source states the transition isomorphisms.

noncomputable def chartModuleInverseImage {V U : SmallEtale B S hS X.1} (f : V ⟶ U) :
    Modules.{u, u} B S hS (chartSpace B S hS X U).1 (chartSpace B S hS X U).2 ⥤
      Modules.{u, u} B S hS (chartSpace B S hS X V).1 (chartSpace B S hS X V).2

AlgebraicGeometry.Space.chartModuleInverseImageComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 253. The attribute's comment: “canonical comparison of chartwise pullbacks”.

Stacks 03LY. The canonical comparison of successive chartwise pullbacks of modules with the pullback along the composite morphism of charts: it is the composition comparison of Stacks 03LU, read through the equality chartMap g ≫ chartMap f = chartMap (g ≫ f).

It is this comparison that makes the cocycle condition AlgebraicGeometry.Space.IsChartModuleCocycle a statement rather than a type error.

noncomputable def chartModuleInverseImageComp {W V U : SmallEtale B S hS X.1} (f : V ⟶ U)
    (g : W ⟶ V) :
    chartModuleInverseImage B S hS X f ⋙ chartModuleInverseImage B S hS X g ≅
      chartModuleInverseImage B S hS X (g ≫ f)

AlgebraicGeometry.Space.chartModuleRestrictionComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 271. The attribute's comment: “compatibility of chart restriction with the chartwise pullback”.

Stacks 03LY. Restriction of a module to a chart commutes canonically with further chartwise pullback along a morphism of charts: the composite of the structure morphism of the larger chart with the morphism of charts is the structure morphism of the smaller chart.

noncomputable def chartModuleRestrictionComp {V U : SmallEtale B S hS X.1} (f : V ⟶ U) :
    chartModuleRestriction B S hS X U ⋙ chartModuleInverseImage B S hS X f ≅
      chartModuleRestriction B S hS X V

AlgebraicGeometry.Space.ChartModuleGlueingData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 334. The attribute's comment: “the data (1), (2) and the cocycle condition”.

The data of Stacks 03LY: a sheaf of 𝒪_U-modules on the small étale site of every étale scheme chart U of X, transition isomorphisms along the chartwise pullbacks of modules, and the cocycle condition relating them.

structure ChartModuleGlueingData

AlgebraicGeometry.Space.chartModuleRestrictionComp_cocycle_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 446. The attribute's comment: “the cocycle condition for the chartwise restrictions of a module”.

Stacks 03LY, the cocycle condition for the chartwise restrictions. For composable morphisms g : W ⟶ V and f : V ⟶ U of étale scheme charts of X and an 𝒪_X-module F, the transition c_g of the restriction family after the chartwise pullback g^*c_f of the transition c_f is the transition c_{g ≫ f}, read through the canonical comparison AlgebraicGeometry.Space.chartModuleInverseImageComp.

This is the condition that AlgebraicGeometry.Space.IsChartModuleCocycle names, written out at the family of restrictions; see the discussion in the module documentation of why the term of that predicate's type does not follow.

theorem chartModuleRestrictionComp_cocycle_app (F : Modules.{u, u} B S hS X.1 X.2)
    {W V U : SmallEtale B S hS X.1} (f : V ⟶ U) (g : W ⟶ V) :
    (chartModuleInverseImage B S hS X g).map
          ((chartModuleRestrictionComp B S hS X f).app F).hom ≫
        ((chartModuleRestrictionComp B S hS X g).app F).hom =
      (chartModuleInverseImageComp B S hS X f g).hom.app
          ((chartModuleRestriction B S hS X U).obj F) ≫
        ((chartModuleRestrictionComp B S hS X (g ≫ f)).app F).hom

AlgebraicGeometry.Space.isChartModuleCocycle_chartModuleRestrictionTransitionFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 553. The attribute's comment: “the cocycle condition for the chartwise restrictions, as a term of the predicate”.

The cocycle condition of Stacks 03LY for the chartwise restrictions of an 𝒪_X-module, as a term of the predicate. This is AlgebraicGeometry.Space.chartModuleRestrictionTransitions_cocycle transported from the spelling in which it is proved to the one the predicate's instantiation produces, by CategoryTheory.Functor.map_comp_eq_comp_of_heq.

theorem isChartModuleCocycle_chartModuleRestrictionTransitionFamily
    (F : Modules.{u, u} B S hS X.1 X.2) :
    IsChartModuleCocycle B S hS X (chartModuleRestrictionFamily B S hS X F)
      (chartModuleRestrictionTransitionFamily B S hS X F)

AlgebraicGeometry.Space.canonicalChartModuleGlueingData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 570. The attribute's comment: “the chartwise glueing datum of a module”.

The chartwise glueing datum of an 𝒪_X-module: its restrictions to the étale scheme charts of X, the comparisons AlgebraicGeometry.Space.chartModuleRestrictionComp as the transition isomorphisms, and the cocycle condition they satisfy.

noncomputable def canonicalChartModuleGlueingData (F : Modules.{u, u} B S hS X.1 X.2) :
    ChartModuleGlueingData B S hS X

AlgebraicGeometry.Space.chartModuleGlueingFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueing.lean, line 594. The attribute's comment: “the canonical chartwise description of modules”.

The canonical chartwise description of 𝒪_X-modules: the functor sending an 𝒪_X-module to the family of its restrictions to the étale scheme charts of X, with the comparisons AlgebraicGeometry.Space.chartModuleRestrictionComp as transitions. That this functor is an equivalence is Stacks 03LY.

noncomputable def chartModuleGlueingFunctor :
    Modules.{u, u} B S hS X.1 X.2 ⥤ ChartModuleGlueingData B S hS X

AlgebraicGeometry.Space.chartModuleGlueingEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartModuleGlueingEquivalence.lean, line 476. The attribute's comment: “the equivalence of modules with chartwise glueing data”.

A sheaf of 𝒪_X-modules on the small étale site of an algebraic space X is the same thing as a family of 𝒪_U-modules F_U on the small étale sites of the étale scheme charts U of X, together with isomorphisms c_f : f^*F_U ≅ F_V for the morphisms f : V ⟶ U of charts satisfying the cocycle condition c_g ∘ g^*c_f = c_{g ≫ f}: an equivalence of categories, given by sending a module to the family of its restrictions to the charts.

def chartModuleGlueingEquivalence :
    Modules.{u, u} B S hS X.1 X.2 ≌ ChartModuleGlueingData B S hS X

Sources

LeanAlgebraicGeometry.Space.modulePushforward_additive · AlgebraicGeometry.Space.moduleSheafFunctor_map_compIsoCongr_hom_app · AlgebraicGeometry.Space.modulePushforwardCompIso' · AlgebraicGeometry.Space.modulePullback · AlgebraicGeometry.Space.modulePullbackAdjunction · AlgebraicGeometry.Space.modulePushforwardCompIso · AlgebraicGeometry.Space.modulePullbackCompIso · AlgebraicGeometry.Space.modulePushforwardIdIso

Section66.27 Étale localization #

Section 66.27 of the Stacks Project, Tag 04LX. 9 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04LY, an equation

Tag 04LY in the Stacks Project.

AlgebraicGeometry.Space.spacesEtaleLocalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleLocalization.lean, line 449. The attribute's comment: “equivalence of categories”.

Stacks 04LY. For an étale morphism f : X ⟶ Y of algebraic spaces, the spaces-étale site of X is equivalent to the localization of the spaces-étale site of Y at the object f.

noncomputable def spacesEtaleLocalization :
    SpacesEtale B S hS X ≌ Over (etaleObject B S hS f hf)

AlgebraicGeometry.Space.spacesEtaleLocalization_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleLocalization.lean, line 479. The attribute's comment: “canonical identification”.

Stacks 04LY. Under the localization equivalence an algebraic space étale over X is unchanged, and its structure morphism to Y is the composite with f.

theorem spacesEtaleLocalization_forget :
    (spacesEtaleLocalization B S hS f hf).functor ⋙
        Over.forget (etaleObject B S hS f hf) ⋙ SpacesEtale.inclusion B S hS Y =
      SpacesEtale.inclusion B S hS X ⋙ Over.map f

AlgebraicGeometry.Space.spacesEtaleLocalization_slice, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleLocalization.lean, line 498. The attribute's comment: “slice arrows”.

Stacks 04LY. The localization equivalence preserves the whole arrow to X, not only its composite with f; this is what makes it canonical.

theorem spacesEtaleLocalization_slice :
    (spacesEtaleLocalization B S hS f hf).functor ⋙
        Over.post (SpacesEtale.toSpaces B S hS Y) =
      SpacesEtale.inclusion B S hS X

AlgebraicGeometry.Space.spacesEtaleLocalization_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleLocalization.lean, line 523. The attribute's comment: “forward topology”.

Stacks 04LY. The localization equivalence carries covering sieves of the spaces-étale site of X to covering sieves of the slice topology.

theorem spacesEtaleLocalization_isContinuous :
    (spacesEtaleLocalization B S hS f hf).functor.IsContinuous
      (SpacesEtale.topology B S hS X)
      ((SpacesEtale.topology B S hS Y).over (etaleObject B S hS f hf))

AlgebraicGeometry.Space.spacesEtaleLocalization_inverse_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleLocalization.lean, line 549. The attribute's comment: “inverse topology”.

Stacks 04LY. The inverse of the localization equivalence carries covering sieves of the slice topology to covering sieves of the spaces-étale site of X.

theorem spacesEtaleLocalization_inverse_isContinuous :
    (spacesEtaleLocalization B S hS f hf).inverse.IsContinuous
      ((SpacesEtale.topology B S hS Y).over (etaleObject B S hS f hf))
      (SpacesEtale.topology B S hS X)

Tag 04LZ, an equation

Tag 04LZ in the Stacks Project.

AlgebraicGeometry.Space.spacesEtaleLocalization_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleStructureSheaf.lean, line 390. The attribute's comment: “the structure sheaves”.

Stacks 04LZ. For an étale morphism f : X ⟶ Y of algebraic spaces, the structure sheaf of the spaces-étale site of X is the restriction of the structure sheaf of Y along the localization equivalence of Stacks 04LY: 𝒪_X = 𝒪_Y|_{Y_{spaces,étale}/X}.

theorem spacesEtaleLocalization_structureSheaf :
    ((spacesEtaleLocalization B S hS f hf).functor.sheafPushforwardContinuous
          CommRingCat.{u + 1} (SpacesEtale.topology B S hS X)
          ((SpacesEtale.topology B S hS Y).over (etaleObject B S hS f hf))).obj
        ((SpacesEtale.structureSheaf B S hS Y).over (etaleObject B S hS f hf)) =
      SpacesEtale.structureSheaf B S hS X

AlgebraicGeometry.Space.spacesEtaleLocalizationRingedHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleStructureSheaf.lean, line 406. The attribute's comment: “the identification of ringed sites”.

Stacks 04LZ. For an étale morphism f : X ⟶ Y of algebraic spaces, the ringed site (X_{spaces,étale}, 𝒪_X) is the localized ringed site (Y_{spaces,étale}/X, 𝒪_Y|_{Y_{spaces,étale}/X}): the identification of sites of Stacks 04LY matches the two structure sheaves.

noncomputable def spacesEtaleLocalizationRingedHom :
    RingedToposSiteHom (spacesEtaleRingedToposOver B S hS f hf)
      (spacesEtaleRingedTopos B S hS X)

Tag 04M0, an equation

Tag 04M0 in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleEquivalenceOverChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartEquivalence.lean, line 371.

Stacks 04M0. The small étale site of an étale scheme chart X → F is canonically the localization of the small étale site of F at that chart. The equivalence preserves the entire arrow to X, not just the underlying scheme over S.

theorem smallEtaleEquivalenceOverChart
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hF : IsAlgebraicSpace B S hS F)
    (X : SmallEtale B S hS F) :
    ∃ e : SmallEtale B S hS
        (yoneda.obj ((SmallEtale.toOver B S hS F).obj X)) ≌ Over X,
      e.functor.inducedTopology ((SmallEtale.topology B S hS F).over X) =
        SmallEtale.topology B S hS
          (yoneda.obj ((SmallEtale.toOver B S hS F).obj X)) ∧
      e.functor ⋙ Over.forget X ⋙ SmallEtale.toOver B S hS F =
        SmallEtale.toOver B S hS
          (yoneda.obj ((SmallEtale.toOver B S hS F).obj X)) ∧
      e.functor ⋙ Over.post (SmallEtale.toOver B S hS F ⋙ yoneda) =
        SmallEtale.inclusion B S hS
            (yoneda.obj ((SmallEtale.toOver B S hS F).obj X)) ⋙
          CostructuredArrow.toOver yoneda
            (yoneda.obj ((SmallEtale.toOver B S hS F).obj X))

Tag 04M1, an equation

Tag 04M1 in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleRingedEquivalenceOverChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartLocalization.lean, line 56.

The small étale ringed site of an étale scheme chart X → Y of an algebraic space is the localization of the ringed small étale site of Y at that chart: the localization equivalence of Tag 04M0 matches the two structure presheaves, naturally in the chart.

theorem smallEtaleRingedEquivalenceOverChart
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hY : IsAlgebraicSpace B S hS Y)
    (X : SmallEtale B S hS Y) :
    ∃ e : SmallEtale B S hS (yoneda.obj ((SmallEtale.toOver B S hS Y).obj X)) ≌ Over X,
      e.functor.inducedTopology ((SmallEtale.topology B S hS Y).over X) =
        SmallEtale.topology B S hS (yoneda.obj ((SmallEtale.toOver B S hS Y).obj X)) ∧
      (e.functor ⋙ Over.forget X ⋙ SmallEtale.toOver B S hS Y =
        SmallEtale.toOver B S hS (yoneda.obj ((SmallEtale.toOver B S hS Y).obj X))) ∧
      (e.functor.op ⋙ (Over.forget X).op ⋙ structurePresheaf B S hS Y =
        structurePresheaf B S hS (yoneda.obj ((SmallEtale.toOver B S hS Y).obj X)))

Tag 04M2, an equation

Tag 04M2 in the Stacks Project.

AlgebraicGeometry.Space.affineEtaleEquivalenceOverChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartLocalization.lean, line 103.

The affine étale site of an affine étale chart X → Y of an algebraic space is the localization of the affine étale site of Y at that chart, by an equivalence preserving both the topology and the underlying objects of the big fppf site.

theorem affineEtaleEquivalenceOverChart
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hY : IsAlgebraicSpace B S hS Y)
    (X : AffineEtale B S hS Y) :
    ∃ e : AffineEtale B S hS (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X)) ≌ Over X,
      e.functor.inducedTopology ((AffineEtale.topology B S hS Y).over X) =
        AffineEtale.topology B S hS (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X)) ∧
      e.functor ⋙ Over.forget X ⋙ AffineEtale.toOver B S hS Y =
        AffineEtale.toOver B S hS (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X))

Tag 04M3, an equation

Tag 04M3 in the Stacks Project.

AlgebraicGeometry.Space.affineEtaleRingedEquivalenceOverChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartLocalization.lean, line 220.

The affine étale ringed site of an affine étale chart X → Y of an algebraic space is the localization of the ringed affine étale site of Y at that chart: the equivalence of Tag 04M2 matches the two structure presheaves, naturally under restriction.

theorem affineEtaleRingedEquivalenceOverChart
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hY : IsAlgebraicSpace B S hS Y)
    (X : AffineEtale B S hS Y) :
    ∃ e : AffineEtale B S hS (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X)) ≌ Over X,
      e.functor.inducedTopology ((AffineEtale.topology B S hS Y).over X) =
        AffineEtale.topology B S hS (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X)) ∧
      (e.functor ⋙ Over.forget X ⋙ AffineEtale.toOver B S hS Y =
        AffineEtale.toOver B S hS (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X))) ∧
      (e.functor.op ⋙ (Over.forget X).op ⋙ (AffineEtale.inclusion B S hS Y).op ⋙
          structurePresheaf B S hS Y =
        (AffineEtale.inclusion B S hS
          (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X))).op ⋙
          structurePresheaf B S hS
            (yoneda.obj ((AffineEtale.toOver B S hS Y).obj X)))

Tag 04M4, a lemma

Tag 04M4 in the Stacks Project.

AlgebraicGeometry.Space.spacesEtaleComparisonMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleRelocalization.lean, line 211. The attribute's comment: “the map c : U ⟶ V ×_Y X corresponding to g, and nothing else”.

The map c : U ⟶ V ×_Y X corresponding to g, as an arrow of the spaces-étale site of X from U to the cartesian base change of V along f.

noncomputable def spacesEtaleComparisonMap (hsq : g ≫ q = p ≫ f) :
    etaleObject B S hS p hp ⟶
      (spacesBaseChange B S hS f).functor.obj (etaleObject B S hS q hq)

AlgebraicGeometry.Space.spacesEtaleRelocalizedTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleRelocalization.lean, line 512. The attribute's comment: “the two morphisms of ringed topoi are 2-isomorphic, via the identifications of 04LZ read as the two vertical arrows of a commuting square”.

Via the identifications of Stacks 04LZ for U ⟶ X and for V ⟶ Y, the morphism of ringed topoi (g_{spaces,étale}, g^♯) is 2-isomorphic to the morphism (f_{spaces,étale,c}, f_c^♯) of Stacks 04J1 built from (f_{spaces,étale}, f^♯) and the map c : U ⟶ V ×_Y X corresponding to g: the square of ringed topoi whose vertical arrows are the two identifications commutes, up to an invertible 2-morphism.

noncomputable def spacesEtaleRelocalizedTwoIso :
    AlgebraicGeometry.RingedToposHom.TwoIso
      (A := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
        ((spacesEtaleRingedSite B S hS X).over (etaleObject B S hS p hp)))
      (B := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
        (spacesEtaleRingedSite B S hS V))
      (AlgebraicGeometry.RingedToposHom.comp
        (X := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
          ((spacesEtaleRingedSite B S hS X).over (etaleObject B S hS p hp)))
        (Y := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
          ((spacesEtaleRingedSite B S hS Y).over (etaleObject B S hS q hq)))
        (Z := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
          (spacesEtaleRingedSite B S hS V))
        (spacesEtaleLocalizationRingedSiteHom B S hS q hq).ringedToposHom
        ((spacesEtaleRingedSiteHom B S hS f).relocalized c))
      (AlgebraicGeometry.RingedToposHom.comp
        (X := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
          ((spacesEtaleRingedSite B S hS X).over (etaleObject B S hS p hp)))
        (Y := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
          (spacesEtaleRingedSite B S hS U))
        (Z := AlgebraicGeometry.RingedSite.ringedTopos.{u + 1, u + 1, u + 1}
          (spacesEtaleRingedSite B S hS V))
        (spacesEtaleRingedSiteHom B S hS g).ringedToposHom
        (spacesEtaleLocalizationRingedSiteHom B S hS p hp).ringedToposHom)

Tag 04M5, a lemma

Tag 04M5 in the Stacks Project.

AlgebraicGeometry.Space.chartRelocalizedTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartRelocalization.lean, line 294. The attribute's comment: “via the identifications of 04M1 at U and V, the morphism (g_small, g^sharp) is 2-isomorphic to the morphism (f_{small,s}, f_s^sharp) of 04J8 for the map s : h_U -> f^{-1}h_V corresponding to g”.

Stacks 04M5. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let U ⟶ X and V ⟶ Y be étale morphisms from schemes (objects of the small étale sites of X and Y) and let g : U ⟶ V be a morphism of schemes with q ∘ g = f ∘ p. Via the identifications of Stacks 04M1 of the small étale ringed topoi of U and V with the localizations of those of X at h_U and of Y at h_V (AlgebraicGeometry.Space.chartLocalizationHom, an equivalence of topoi), the morphism of small étale ringed topoi (g_small, g♯) is 2-isomorphic to the morphism (f_{small,s}, f_s♯) of Stacks 04J8 built from (f_small, f♯) and the map s : h_U ⟶ f_small⁻¹h_V corresponding to g (AlgebraicGeometry.Space.chartRelocalizationSheafMap).

noncomputable def chartRelocalizedTwoIso :
    RingedToposHom.TwoIso (A := 𝒰) (B := 𝒴ᵥ) (chartRelocalizedHom B S hS f U V g hg)
      (chartMorphismHom B S hS U V g)

Tag 0GF6, a lemma

Tag 0GF6 in the Stacks Project.

AlgebraicGeometry.Space.sheafGivesSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SheafGivesSpace.lean, line 205.

Let Y be an algebraic space over S and 𝓕 a sheaf of sets on its small étale site, satisfying the set-theoretic condition of the source's proof. Write G for the corresponding sheaf on the spaces-étale site (Stacks 03G1) and X for the functor T ↦ {(y, s) | y : T → Y, s ∈ Γ(T, y⁻¹ 𝓕)} on (Sch/S)_fppf. Then

X is an algebraic space;

the map X → Y, (y, s) ↦ y, is étale;

via Sh(Y_étale) = Sh(Y_{spaces,étale}), 𝓕 ≅ h_X, where h_X(U) is the set of morphisms U → X over Y of functors on (Sch/S)_fppf;

X is the (universe-lifted) functor of points of an algebraic space X', under which the map X → Y is an étale morphism f : X' → Y; the inverse image f_small⁻¹ has a left adjoint f_{small,!} (Stacks 03LP), and for every such left adjoint 𝓕 ≅ f_{small,!} *, where * is the terminal sheaf on X'_étale.

theorem sheafGivesSpace (F : Sheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)))
    (hF : SheafGivesSpace.SatisfiesSetTheoreticCondition B S hS Y F) :
    IsAlgebraicSpaceULift.{u + 1} B S hS
        (sheafPairsFunctor B S hS ((smallEtaleToposEquiv B S hS Y).inverse.obj F)) ∧
      IsEtaleULift.{u + 1} B S hS
        (sheafPairsFunctorToBase B S hS ((smallEtaleToposEquiv B S hS Y).inverse.obj F)) ∧
      Nonempty (((smallEtaleToposEquiv B S hS Y).inverse.obj F).obj ≅
        sheafPairsHom B S hS ((smallEtaleToposEquiv B S hS Y).inverse.obj F)) ∧
      ∃ (X' : AlgebraicSpaces B S hS) (f : X' ⟶ Y) (_ : IsEtale B S hS f.hom)
        (ι : sheafPairsFunctor B S hS ((smallEtaleToposEquiv B S hS Y).inverse.obj F) ≅
          X'.obj ⋙ uliftFunctor.{u + 1}),
        sheafPairsFunctorToBase B S hS ((smallEtaleToposEquiv B S hS Y).inverse.obj F) =
            ι.hom ≫ Functor.whiskerRight f.hom uliftFunctor.{u + 1} ∧
          (∃ L : Sheaf (SmallEtale.topology B S hS X'.1) (Type (u + 1)) ⥤
              Sheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)),
            Nonempty (L ⊣ (smallToposMorphism B S hS f).inverseImage)) ∧
          ∀ (L : Sheaf (SmallEtale.topology B S hS X'.1) (Type (u + 1)) ⥤
              Sheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)))
            (_ : L ⊣ (smallToposMorphism B S hS f).inverseImage),
            Nonempty (F ≅ L.obj (⊤_ (Sheaf (SmallEtale.topology B S hS X'.1) (Type (u + 1)))))

Sources

LeanAlgebraicGeometry.Space.spacesEtaleLocalization · AlgebraicGeometry.Space.spacesEtaleLocalization_forget · AlgebraicGeometry.Space.spacesEtaleLocalization_slice · AlgebraicGeometry.Space.spacesEtaleLocalization_isContinuous · AlgebraicGeometry.Space.spacesEtaleLocalization_inverse_isContinuous · AlgebraicGeometry.Space.spacesEtaleLocalization_structureSheaf · AlgebraicGeometry.Space.spacesEtaleLocalizationRingedHom · AlgebraicGeometry.Space.smallEtaleEquivalenceOverChart

Section66.28 Recovering morphisms #

Section 66.28 of the Stacks Project, Tag 04KI. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04KJ, a lemma

Tag 04KJ in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleRingedToposHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHomLocallyRinged.lean, line 131.

For a morphism f : X ⟶ Y of algebraic spaces over a scheme S, the morphism of small étale ringed topoi (f_small, f♯) attached to f is a morphism of locally ringed topoi: its square of units subsheaves is cartesian.

The geometric points of X are a conservative family of points of its small étale site, and at each of them the fibre of f⁻¹𝒪_Y ⟶ 𝒪_X is the map of étale local rings 𝒪_{Y, f(x̄)} ⟶ 𝒪_{X, x̄}, which is a local ring map.

theorem smallEtaleRingedToposHom_isLocallyRinged :
    (smallEtaleRingedToposHom B S hS f).IsLocallyRinged

Tag 04KK, a lemma

Tag 04KK in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleRingedToposHom_twoMorphism_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHomRigidity.lean, line 529.

Stacks 04KK. A 2-endomorphism of the morphism of small étale ringed topoi induced by a morphism of algebraic spaces is the identity.

theorem smallEtaleRingedToposHom_twoMorphism_eq_id
    (t : AlgebraicGeometry.RingedToposHom.TwoMorphism.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS f)
      (smallEtaleRingedToposHom B S hS f)) :
    t = AlgebraicGeometry.RingedToposHom.TwoMorphism.id
      (smallEtaleRingedToposHom B S hS f)

AlgebraicGeometry.Space.smallEtaleRingedToposHom_twoMorphismOfRingedTopoi_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTwoMorphismRigidity.lean, line 720.

Stacks 04KK. A 2-morphism from the morphism of small étale ringed topoi induced by a morphism of algebraic spaces to itself is the identity.

The 2-morphism is taken over (smallEtaleRingedToposHom B S hS f).toRingedToposModulesHom, since Stacks.Sheaves.RingedToposModules.TwoMorphismOfRingedTopoi (Stacks 04IC) is defined for the four-field Stacks.Sheaves.RingedToposModules.RingedToposHom; the two structures are equivalent.

theorem smallEtaleRingedToposHom_twoMorphismOfRingedTopoi_eq_id (f : X ⟶ Y)
    (t : Stacks.Sheaves.RingedToposModules.TwoMorphismOfRingedTopoi.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS f).toRingedToposModulesHom
      (smallEtaleRingedToposHom B S hS f).toRingedToposModulesHom) :
    t = Stacks.Sheaves.RingedToposModules.TwoMorphismOfRingedTopoi.id.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS f).toRingedToposModulesHom

Tag 04M6, a lemma

Tag 04M6 in the Stacks Project.

AlgebraicGeometry.Space.eq_of_smallEtaleRingedToposHom_twoIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTwoIsoAffineCover.lean, line 171.

Stacks 04M6. Let S be a scheme and let X, Y be algebraic spaces over S. Two morphisms a, b : X ⟶ Y of algebraic spaces over S for which there exists a 2-isomorphism (a_small, a^♯) ≅ (b_small, b^♯) in the 2-category of ringed topoi are equal.

No representability is assumed: the general case is reduced to a scheme source by AlgebraicGeometry.Space.eq_of_twoIso_of_schemeSource, where the two morphisms are automatically representable because the diagonal of an algebraic space is.

theorem eq_of_smallEtaleRingedToposHom_twoIso (a b : X ⟶ Y)
    (t : RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS a) (smallEtaleRingedToposHom B S hS b)) :
    a = b

AlgebraicGeometry.Space.exists_smallBaseChange_iso_of_twoIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTwoIsoChartComparison.lean, line 289. The attribute's comment: “the étale-chart comparison of the proof: for two representable morphisms the 2-isomorphism of the morphisms of small étale ringed topoi is, through the 03G8 identification of the direct images with étale-chart base change, restriction along an isomorphism of the chart base-change functors”.

The étale-chart comparison of Stacks 04M6. Let a, b : X ⟶ Y be two representable morphisms of algebraic spaces whose morphisms of small étale ringed topoi are 2-isomorphic. Through the Stacks 03G8 identification of the two direct images with base change of étale scheme charts, the 2-isomorphism is restriction along an isomorphism V ×_{Y,b} X ≅ V ×_{Y,a} X of the chart base-change functors, natural in the étale chart V of Y.

theorem exists_smallBaseChange_iso_of_twoIso {X Y : AlgebraicSpaces B S hS} (a b : X ⟶ Y)
    (ha : yoneda.relativelyRepresentable a.hom) (hb : yoneda.relativelyRepresentable b.hom)
    (t : RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u}
      (smallEtaleRingedToposHom B S hS a) (smallEtaleRingedToposHom B S hS b)) :
    letI := (smallBaseChange_isMorphismOfSites B S hS a ha).toIsContinuous
    letI := (smallBaseChange_isMorphismOfSites B S hS b hb).toIsContinuous
    ∃ e : smallBaseChange B S hS b hb ≅ smallBaseChange B S hS a ha,
      ∀ (H : Sheaf (SmallEtale.topology B S hS X.obj) (Type u))
        (V : SmallEtale B S hS Y.obj)
        (x : (((smallBaseChange B S hS a ha).sheafPushforwardContinuous (Type u)
          (SmallEtale.topology B S hS Y.obj)
          (SmallEtale.topology B S hS X.obj)).obj H).obj.obj (op V)),
        ((((smallEtaleRingedToposHom_representable B S hS a ha).symm ≪≫ t.e ≪≫
            smallEtaleRingedToposHom_representable B S hS b hb).hom.app H).hom.app (op V)) x =
          H.obj.map (op (e.hom.app V)) x

Tag 04KL, a theorem

Tag 04KL in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_spaceHom_twoIso_of_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RecoveringMorphisms/Main.lean, line 172.

Stacks 04KL. Let X and Y be algebraic spaces over Spec ℤ (here Spec (ULift ℤ), the terminal scheme at the universe of the site) and let (g, g♯) : (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y) be a morphism of locally ringed topoi. Then there is a unique morphism of algebraic spaces f : X ⟶ Y such that (g, g♯) is 2-isomorphic to (f_small, f♯) (Stacks 04IC, 03G8).

theorem existsUnique_spaceHom_twoIso_of_isLocallyRinged (B : BigFppfSite.{u})
    (hZ : B.Contains (Spec (CommRingCat.of (ULift.{u} ℤ))))
    {X Y : AlgebraicSpaces B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ}
    (g : RingedToposHom (smallEtaleRingedTopos B _ hZ X) (smallEtaleRingedTopos B _ hZ Y))
    (hg : g.IsLocallyRinged) :
    ∃! f : X ⟶ Y, Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
      (smallEtaleRingedToposHom B _ hZ f))

AlgebraicGeometry.Space.bijective_smallEtaleLocallyRingedClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RecoveringMorphisms/Main.lean, line 216. The attribute's comment: “the reformulation: X ↦ (X_étale, 𝒪_X) is fully faithful, morphisms of locally ringed topoi being taken up to 2-isomorphism”.

Stacks 04KL, in the form of full faithfulness. Over Spec ℤ, the construction X ↦ (X_étale, 𝒪_X) is fully faithful from algebraic spaces to locally ringed topoi, morphisms of the latter being taken up to 2-isomorphism: f ↦ [(f_small, f♯)] is a bijection from the morphisms X ⟶ Y of algebraic spaces onto the 2-isomorphism classes of morphisms of locally ringed topoi (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y).

theorem bijective_smallEtaleLocallyRingedClass (B : BigFppfSite.{u})
    (hZ : B.Contains (Spec (CommRingCat.of (ULift.{u} ℤ))))
    (X Y : AlgebraicSpaces B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ) :
    Function.Bijective (smallEtaleLocallyRingedClass B _ hZ X Y)

Declarations registered for the tag:

AlgebraicGeometry.Space.eq_of_twoIso_smallEtaleRingedToposHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTwoIsoAffineCover.lean, line 201 (StacksFrontier): “the uniqueness clause over a base: at most one morphism of algebraic spaces over S induces a given morphism of the small étale ringed topoi. This is the faithfulness half of the asserted full faithfulness, and it needs neither of the theorem's hypotheses — not local ringedness of the morphism of topoi, and not 2-compatibility with structure morphisms to a further base”.

Tag 05YZ, a lemma

Tag 05YZ in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_spaceHom_twoIso_of_smallEtaleRingedToposIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposIsoLocallyRinged.lean, line 644.

Stacks 05YZ. Let X and Y be algebraic spaces over ℤ, and let (g, g♯) : (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y) be an isomorphism of ringed topoi: its direct image is an equivalence and g♯ : 𝒪_Y ⟶ g_*𝒪_X is an isomorphism. Then there is a unique morphism f : X ⟶ Y of algebraic spaces such that (g, g♯) is 2-isomorphic to (f_small, f♯) — the morphism of small étale ringed topoi AlgebraicGeometry.Space.smallEtaleRingedToposHom of Stacks 03G8, a 2-isomorphism being one of Stacks 04IC — and that morphism is an isomorphism of algebraic spaces.

As in the source, the existence and uniqueness is Stacks 04KL (AlgebraicGeometry.Space.existsUnique_spaceHom_twoIso_of_isLocallyRinged), applicable because (g, g♯) is a morphism of locally ringed topoi (AlgebraicGeometry.Space.isLocallyRinged_of_smallEtaleRingedToposIso). For the last clause, Stacks 04KL applied to the inverse of (g, g♯) and to the inverse of that gives f' and f'', and AlgebraicGeometry.Space.isIso_of_twoIso_of_inverse shows that f is invertible.

theorem existsUnique_spaceHom_twoIso_of_smallEtaleRingedToposIso (B : BigFppfSite.{u})
    (hZ : B.Contains (Spec (CommRingCat.of (ULift.{u} ℤ))))
    {X Y : AlgebraicSpaces B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ}
    (g : RingedToposHom (smallEtaleRingedTopos B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ X)
      (smallEtaleRingedTopos B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ Y))
    [g.toToposHom.pushforward.IsEquivalence] [IsIso g.fSharp] :
    (∃! f : X ⟶ Y, Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
      (smallEtaleRingedToposHom B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ f))) ∧
    ∀ f : X ⟶ Y, Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
      (smallEtaleRingedToposHom B (Spec (CommRingCat.of (ULift.{u} ℤ))) hZ f)) → IsIso f

AlgebraicGeometry.Space.existsUnique_spaceHom_twoIso_of_smallEtaleRingedToposIso', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpaceRecoveredFromSmallEtale.lean, line 188. The attribute's comment: “the clause about f ALONE: its existence and uniqueness, together with the 2-isomorphism of (g, g sharp) with (f_small, f sharp) (Stacks 04IC). Stacks 04KL over a base, which the existence needs, is isRecoveredFromSmallEtale_holds. The source's further clause that f is an ISOMORPHISM of algebraic spaces lies outside this registration. NARROWER than the source in one further respect: the source states 05YZ for spaces over Spec(Z), where f is an absolute morphism and no compatibility is asked of (g, g sharp), while f here is a morphism over S, so the 2-compatibility hbase is assumed in addition -- it is what Stacks 04SG supplies, and without it the conclusion is FALSE”.

[Stacks Project, Tag 05YZ], the clause about f. If g is a morphism of the small étale ringed topoi of X and Y whose direct image is an equivalence and whose structure map is an isomorphism, and g is 2-compatible with a pair of structure morphisms pX : X ⟶ A, pY : Y ⟶ A, then there is exactly one morphism of algebraic spaces f : X ⟶ Y with g 2-isomorphic to the morphism of small étale ringed topoi of f.

This is AlgebraicGeometry.Space.IsRecoveredFromSmallEtaleOver at A, supplied by AlgebraicGeometry.Space.isRecoveredFromSmallEtale_holds, applied to g: the hypothesis that g is locally ringed is AlgebraicGeometry.Space.isLocallyRinged_of_smallEtaleRingedToposIso, and the two 2-isomorphisms are read in the opposite direction from AlgebraicGeometry.Space.InducesSmallEtaleRingedToposHom.

Only the source's clause about f is registered here; its further clause that f is an isomorphism of algebraic spaces lies outside this statement.

The 2-compatibility hbase is not optional: the source states Stacks 05YZ for algebraic spaces over Spec(ℤ), where f is an absolute morphism, whereas f : X ⟶ Y here is a morphism over S. Without it the conclusion is false — see the σ-twist counterexample recorded with AlgebraicGeometry.Space.IsRecoveredFromSmallEtale. Since AlgebraicGeometry.Space.baseSpace is terminal, hbase can always be asked of the structure morphisms to the base itself.

theorem existsUnique_spaceHom_twoIso_of_smallEtaleRingedToposIso' {A : AlgebraicSpaces B S hS}
    (pX : X ⟶ A) (pY : Y ⟶ A)
    (g : RingedToposHom (smallEtaleRingedTopos B S hS X) (smallEtaleRingedTopos B S hS Y))
    [g.toToposHom.pushforward.IsEquivalence] [IsIso g.fSharp]
    (hbase : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS (smallEtaleRingedToposHom B S hS pY) g)
      (smallEtaleRingedToposHom B S hS pX))) :
    ∃! f : X ⟶ Y, Nonempty (RingedToposHom.TwoIso.{u, u + 1, u, u, u + 1, u} g
      (smallEtaleRingedToposHom B S hS f))

Sources

Section66.29 Quasi-coherent sheaves on algebraic spaces #

Section 66.29 of the Stacks Project, Tag 03G5. 7 tags here are carried by 47 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03G9, a definition

Tag 03G9 in the Stacks Project.

AlgebraicGeometry.Space.QuasicoherentSheaves, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RingedSite.lean, line 82.

The category QCoh(𝒪_F) of quasi-coherent sheaves on the algebraic space F: the full subcategory of the 𝒪_F-modules cut out by quasi-coherence on the small étale ringed site.

noncomputable abbrev QuasicoherentSheaves (hF : IsAlgebraicSpace B S hS F)

Tag 03GA, a lemma

Tag 03GA in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionQuasicoherentPushforward.lean, line 81. The attribute's comment: “the inverse image along a closed immersion of algebraic spaces”.

Stacks 03GA along a closed immersion of algebraic spaces. The inverse image i^*F of a quasi-coherent 𝒪_X-module along a closed immersion i : Z ⟶ X is quasi-coherent.

Quasi-coherence is local on Z, the base changes of the affine étale charts of X cover Z, and over such a chart the composite to X factors through an affine chart, which is the case of Stacks 03GA already available.

theorem isQuasicoherentOnSite_modulePullback_of_isClosedImmersion (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) :
    ((modulePullback B S hS i).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModulePullbackQuasicoherentFromChartDiagrams.lean, line 109. The attribute's comment: “the pullback functor preserves quasi-coherence”.

[Stacks, Tag 03GA]. The pullback f^*F of Stacks 03LU of a quasi-coherent 𝒪_Y-module along an arbitrary morphism f : X ⟶ Y of algebraic spaces is quasi-coherent.

On the chart space of a chart of X carrying an affine chart diagram over f the pullback of F along the composite with f is quasi-coherent, because that composite factors through the structure morphism of an affine étale chart of Y; the composition comparison of Stacks 03LU turns that into quasi-coherence of the pullback of f^*F to the chart space, and those charts cover the final object of the small étale site of X.

theorem isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS Y.1 Y.2) (hF : F.IsQuasicoherentOnSite) :
    ((modulePullback B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.quasicoherentPullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModulePullbackQuasicoherentFromChartDiagrams.lean, line 131. The attribute's comment: “the induced functor on quasi-coherent modules”.

[Stacks, Tag 03GA], in the form the source states it. The pullback of Stacks 03LU along an arbitrary morphism of algebraic spaces restricts to a functor QCoh(𝒪_Y) ⥤ QCoh(𝒪_X) between the categories of quasi-coherent modules of Stacks 03G9.

noncomputable def quasicoherentPullbackFunctor (f : X ⟶ Y) :
    QuasicoherentSheaves.{u, u} B S hS Y.1 Y.2 ⥤
      QuasicoherentSheaves.{u, u} B S hS X.1 X.2

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackQuasicoherence.lean, line 223. The attribute's comment: “the pullback of a module with a global presentation is quasi-coherent”.

Stacks 03GA for a module with a global presentation. If an 𝒪_Y-module F admits a SheafOfModules.Presentation then its pullback f^*F of Stacks 03LU along an arbitrary morphism f : X ⟶ Y of algebraic spaces is quasi-coherent.

The inverse image of Stacks 03D2 is a left adjoint carrying 𝒪_Y to f⁻¹𝒪_Y, so it carries the presentation along; extension of scalars to 𝒪_X carries it further.

theorem isQuasicoherentOnSite_modulePullback_of_presentation (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS Y.1 Y.2) (P : F.Presentation) :
    ((modulePullback B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackQuasicoherence.lean, line 248. The attribute's comment: “the pullback of a module of finite presentation is quasi-coherent”.

Stacks 03GA for a module of finite presentation. The pullback f^*F of Stacks 03LU of an 𝒪_Y-module of finite presentation along an arbitrary morphism f : X ⟶ Y of algebraic spaces is quasi-coherent.

Unlike the globally presented case this assumes only local presentations, which transport along f⁻¹ because a finite presentation over an object is a point of a sheaf of sets indexed by ℕ × ℕ. The clause 03DL (7) of Stacks 03DO therefore holds outright, and a module of finite presentation is quasi-coherent.

theorem isQuasicoherentOnSite_modulePullback_of_isFinitePresentation (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS Y.1 Y.2) (hF : F.IsFinitePresentation) :
    ((modulePullback B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackQuasicoherence.lean, line 269. The attribute's comment: “the pullback functor preserves quasi-coherence along an étale morphism”.

Stacks 03GA along an étale morphism. The pullback functor f^* : Mod(𝒪_Y) ⟶ Mod(𝒪_X) of Stacks 03LU along an étale morphism f : X ⟶ Y of algebraic spaces preserves quasi-coherence, with no hypothesis on the module beyond quasi-coherence.

Along an étale morphism the pullback of Stacks 03LU is restriction of sections along postcomposition of étale charts, by Stacks' Equation 03LW, and quasi-coherence is inherited by that restriction.

theorem isQuasicoherentOnSite_modulePullback_of_isEtale (f : X ⟶ Y)
    (hf : IsEtale B S hS f.hom) (F : Modules.{u, u} B S hS Y.1 Y.2)
    (hF : F.IsQuasicoherentOnSite) :
    ((modulePullback B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.quasicoherentPullbackOfIsEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackQuasicoherence.lean, line 281. The attribute's comment: “the induced functor on quasi-coherent modules, along an étale morphism”.

Stacks 03GA along an étale morphism, in the form the source states it: the pullback of Stacks 03LU along an étale morphism of algebraic spaces restricts to a functor QCoh(𝒪_Y) ⥤ QCoh(𝒪_X) between the categories of quasi-coherent modules of Stacks 03G9.

noncomputable def quasicoherentPullbackOfIsEtale (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    QuasicoherentSheaves.{u, u} B S hS Y.1 Y.2 ⥤
      QuasicoherentSheaves.{u, u} B S hS X.1 X.2

AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_affineChartFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackQuasicoherence.lean, line 318. The attribute's comment: “the pullback along a morphism factoring through an affine chart of the target”.

Stacks 03GA along a morphism factoring through an affine étale chart of the target. If f : X ⟶ Y factors as k ≫ φ with φ the structure morphism of an étale chart of Y whose underlying scheme is affine, then f^* carries quasi-coherent 𝒪_Y-modules to quasi-coherent 𝒪_X-modules, with no hypothesis on k and none on the module beyond quasi-coherence.

This is the general case of Stacks 03GA localized at one chart of the target; see the implementation notes for what the general case still needs.

theorem isQuasicoherentOnSite_modulePullback_of_affineChartFactorization (f : X ⟶ Y)
    (V : SmallEtale B S hS Y.1)
    (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS Y.1).obj V)))
    (k : X ⟶ chartSpace B S hS Y V) (hk : f = k ≫ chartToSpace B S hS Y V)
    (F : Modules.{u, u} B S hS Y.1 Y.2) (hF : F.IsQuasicoherentOnSite) :
    ((modulePullback B S hS f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.quasicoherentPullbackOfAffineChartFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackQuasicoherence.lean, line 332. The attribute's comment: “the induced functor on quasi-coherent modules, through an affine chart”.

Stacks 03GA along a morphism factoring through an affine étale chart of the target, in the form the source states it: the pullback of Stacks 03LU along k ≫ φ, with φ the structure morphism of an affine étale chart of Y, restricts to a functor QCoh(𝒪_Y) ⥤ QCoh(𝒪_X) between the categories of quasi-coherent modules of Stacks 03G9.

noncomputable def quasicoherentPullbackOfAffineChartFactorization (V : SmallEtale B S hS Y.1)
    (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS Y.1).obj V)))
    (k : X ⟶ chartSpace B S hS Y V) :
    QuasicoherentSheaves.{u, u} B S hS Y.1 Y.2 ⥤
      QuasicoherentSheaves.{u, u} B S hS X.1 X.2

Tag 03LZ, a lemma

Tag 03LZ in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_chartModuleInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueing.lean, line 93. The attribute's comment: “the chartwise pullback preserves quasi-coherence”.

Stacks 03LZ. The chartwise pullback of modules preserves quasi-coherence: a morphism of étale scheme charts of X represents an étale morphism of algebraic spaces, along which the pullback of Stacks 03LU is restriction of sections.

theorem isQuasicoherentOnSite_chartModuleInverseImage {V U : SmallEtale B S hS X.1} (f : V ⟶ U)
    (F : Modules.{u, u} B S hS (chartSpace B S hS X U).1 (chartSpace B S hS X U).2)
    (hF : F.IsQuasicoherentOnSite) :
    ((chartModuleInverseImage B S hS X f).obj F).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_forall_chartModuleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueing.lean, line 112. The attribute's comment: “quasi-coherence of a module is quasi-coherence of its chartwise restrictions”.

Stacks 03LZ. An 𝒪_X-module is quasi-coherent exactly when its restriction to every étale scheme chart of X is quasi-coherent: the chartwise family of restrictions of a module satisfies datum (1) of Stacks 03LZ precisely for the quasi-coherent modules.

theorem isQuasicoherentOnSite_iff_forall_chartModuleRestriction
    (M : Modules.{u, u} B S hS X.1 X.2) :
    M.IsQuasicoherentOnSite ↔
      ∀ U : SmallEtale B S hS X.1,
        ((chartModuleRestriction B S hS X U).obj M).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isChartwiseQuasicoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueing.lean, line 126. The attribute's comment: “datum (1): the chartwise modules are quasi-coherent”.

Datum (1) of Stacks 03LZ: the module of a chartwise glueing datum is quasi-coherent on the small étale site of every étale scheme chart of X.

def isChartwiseQuasicoherent : ObjectProperty (ChartModuleGlueingData B S hS X)

AlgebraicGeometry.Space.QuasicoherentChartModuleGlueingData, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueing.lean, line 133. The attribute's comment: “the data (1), (2) and the cocycle condition”.

The data of Stacks 03LZ: a quasi-coherent 𝒪_U-module on the small étale site of every étale scheme chart U of X, transition isomorphisms along the chartwise pullbacks, and the cocycle condition relating them.

noncomputable abbrev QuasicoherentChartModuleGlueingData

AlgebraicGeometry.Space.quasicoherentChartModuleGlueingFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueing.lean, line 160. The attribute's comment: “the canonical chartwise description of quasi-coherent modules”.

The canonical chartwise description of quasi-coherent 𝒪_X-modules: the functor of Stacks 03LY cut down to the quasi-coherent objects on both sides, so that composing it with the inclusion of the chartwise quasi-coherent data is AlgebraicGeometry.Space.chartModuleGlueingFunctor on the nose. It is well defined because the restriction of a quasi-coherent module to a chart is quasi-coherent, which is AlgebraicGeometry.Space.isQuasicoherentOnSite_chartModuleRestriction. That this functor is an equivalence is Stacks 03LZ, proved as AlgebraicGeometry.Space.quasicoherentChartModuleGlueingFunctor_isEquivalence in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueingEquivalence.lean.

noncomputable def quasicoherentChartModuleGlueingFunctor :
    QuasicoherentSheaves.{u, u} B S hS X.1 X.2 ⥤ QuasicoherentChartModuleGlueingData B S hS X

AlgebraicGeometry.Space.quasicoherentChartModuleGlueingEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueingEquivalence.lean, line 54. The attribute's comment: “quasi-coherent modules are the chartwise quasi-coherent glueing data”.

A quasi-coherent 𝒪_X-module on the small étale site of an algebraic space X is the same thing as a chartwise quasi-coherent glueing datum: a quasi-coherent 𝒪_U-module F_U on the small étale site of every étale scheme chart U of X, transition isomorphisms c_f : f^*F_U ≅ F_V along the chartwise pullbacks of Stacks 03LU for the morphisms f : V ⟶ U of charts, and the cocycle condition c_g ∘ g^*c_f = c_{g ≫ f} — an equivalence of categories, given by sending a quasi-coherent module to the family of its restrictions to the charts.

It is the equivalence AlgebraicGeometry.Space.chartModuleGlueingEquivalence of Stacks 03LY, cut down to the quasi-coherent objects on both sides.

def quasicoherentChartModuleGlueingEquivalence :
    QuasicoherentSheaves.{u, u} B S hS X.1 X.2 ≌ QuasicoherentChartModuleGlueingData B S hS X

AlgebraicGeometry.Space.quasicoherentChartModuleGlueingFunctor_isEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartQuasicoherentGlueingEquivalence.lean, line 70. The attribute's comment: “the canonical chartwise description of quasi-coherent modules is an equivalence”.

The canonical chartwise description of quasi-coherent 𝒪_X-modules AlgebraicGeometry.Space.quasicoherentChartModuleGlueingFunctor — restriction to the étale scheme charts — is an equivalence onto the chartwise quasi-coherent glueing data.

instance quasicoherentChartModuleGlueingFunctor_isEquivalence :
    (quasicoherentChartModuleGlueingFunctor B S hS X).IsEquivalence

Tag 05VP, a lemma

Tag 05VP in the Stacks Project.

AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing_germ_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartLocalRingGermsOnOpens.lean, line 106. The attribute's comment: “the comparison map on germs of functions on an open of the chart”.

The comparison map 𝒪_{U, u} → 𝒪_{X, x̄} on germs of functions on an open of the chart. The ordinary germ at u of a regular function on a Zariski open W ∋ u of the chart is sent to the germ at x̄ of the same function, read on the small étale neighbourhood AlgebraicGeometry.Space.chartOpenNeighborhood given by W. This extends AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing_germ, which is the case W = ⊤.

theorem chartLocalRingToEtaleLocalRing_germ_open {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (W : (chartScheme V.chart).Opens)
    (hw : chartPoint B S hS X V ∈ W) (a : Γ(chartScheme V.chart, W)) :
    chartLocalRingToEtaleLocalRing B S hS X hX V
        ((chartScheme V.chart).presheaf.germ W (chartPoint B S hS X V) hw a) =
      etaleLocalRingGerm B S hS X x (op (chartOpenNeighborhood B S hS V W hw))
        (W.topIso.inv a)

AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing_germ_open', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartLocalRingGermsOnOpens.lean, line 159. The attribute's comment: “the comparison map on germs, through the chart restriction of functions”.

AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing_germ_open with the restricted function written through AlgebraicGeometry.Space.chartRestrictionRingHom, the form in which the sections of a module on the algebraic space carry their scalars over an open of the chart.

theorem chartLocalRingToEtaleLocalRing_germ_open' {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (W : (chartScheme V.chart).Opens)
    (hw : chartPoint B S hS X V ∈ W) (a : Γ(chartScheme V.chart, W)) :
    chartLocalRingToEtaleLocalRing B S hS X hX V
        ((chartScheme V.chart).presheaf.germ W (chartPoint B S hS X V) hw a) =
      etaleLocalRingGerm B S hS X x (op (chartOpenNeighborhood B S hS V W hw))
        (((chartRestrictionRingHom B S hS hX V.chart).app (op W)).hom a)

AlgebraicGeometry.Space.chartStalkTensorComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartStalkTensorComparison.lean, line 311. The attribute's comment: “the comparison map (phi^* F)_u tensor O_{U, u} O_{X, xbar} to F_xbar”.

The comparison map from the Zariski stalk (φ^* F)_u of the restriction of an 𝒪_X-module to an étale scheme chart, base changed along the canonical map 𝒪_{U, u} → 𝒪_{X, x̄}, to the stalk F_{x̄} of F at the geometric point.

noncomputable def chartStalkTensorComparison {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (F : Modules.{u, m} B S hS X hX) :
    chartStalkTensorEtaleLocalRing B S hS X hX V F ⟶
      geometricModuleStalk B S hS ⟨X, hX⟩ x F

AlgebraicGeometry.Space.chartStalkTensorComparison_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartStalkTensorComparison.lean, line 321. The attribute's comment: “the comparison map is the identity on germs of sections”.

The comparison map (φ^* F)_u ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} → F_{x̄} sends the base change of the Zariski germ at u of a section of F over a Zariski open W of the chart containing u to the germ at x̄ of the same section, read on the small étale neighbourhood W.

theorem chartStalkTensorComparison_germ {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (F : Modules.{u, m} B S hS X hX)
    (W : (etaleChartScheme B S hS V.chart).Opens) (hw : chartPoint B S hS X V ∈ W)
    (s : F.val.obj (op ((chartOpens B S hS V.chart).obj W))) :
    chartStalkTensorComparison B S hS hX V F
        ((1 : ↥(etaleLocalRing B S hS X x)) ⊗ₜ[↥(chartLocalRing B S hS X V),
            chartLocalRingToEtaleLocalRing B S hS X hX V]
          chartZariskiSectionGerm B S hS hX V F W hw s :
          chartStalkTensorEtaleLocalRing B S hS X hX V F) =
      geometricModuleStalkGerm B S hS ⟨X, hX⟩ x F
        (chartOpenNeighborhood B S hS V W hw) s

AlgebraicGeometry.Space.isIso_chartStalkTensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartStalkTensorIsomorphism.lean, line 197. The attribute's comment: “the comparison map is an isomorphism”.

Stacks 05VP. Let F be a quasi-coherent 𝒪_X-module on an algebraic space X, let x̄ be a geometric point of X and let φ : (U, ū) → (X, x̄) be an étale neighbourhood whose chart U is a scheme. Then the canonical comparison map

(φ^* F)_u ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} → F_{x̄}

is an isomorphism.

The hypothesis of quasi-coherence is necessary: for a general 𝒪_X-module the comparison map is not even surjective. The statement is at module universe m = u, that is for AlgebraicGeometry.Space.Modules.{u, u}, which is where the cartesian criterion of Stacks 03DX(2) that quasi-coherence is used through is available.

theorem isIso_chartStalkTensorComparison {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (F : Modules.{u, u} B S hS X hX)
    [F.IsQuasicoherentOnSite] :
    IsIso (chartStalkTensorComparison B S hS hX V F)

AlgebraicGeometry.Space.surjective_chartStalkTensorComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartStalkTensorSurjective.lean, line 83. The attribute's comment: “the comparison map is surjective for a quasi-coherent module”.

The comparison map of Stacks 05VP is surjective for a quasi-coherent module. Every germ at the geometric point of a section of a quasi-coherent 𝒪_X-module is the image of a base changed Zariski germ on the chart.

Quasi-coherence is required: it enters through Stacks 03DX(2), which writes a section over a small affine étale neighbourhood as a sum of multiples of restrictions of sections over a fixed affine neighbourhood of the point.

theorem surjective_chartStalkTensorComparison {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (F : Modules.{u, u} B S hS X hX)
    [F.IsQuasicoherentOnSite] :
    Function.Surjective (chartStalkTensorComparison B S hS hX V F)

AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 141. The attribute's comment: “the canonical map O_{U, u} → O_{X, xbar}”.

The canonical map 𝒪_{U, u} → 𝒪_{X, x̄} of Stacks 05VP: the structure map of 𝒪_{U, u} into its strict henselization, followed by the identification of that strict henselization with the étale local ring at the geometric point.

noncomputable def chartLocalRingToEtaleLocalRing {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) :
    ↥(chartLocalRing B S hS X V) →+* ↥(etaleLocalRing B S hS X x)

AlgebraicGeometry.Space.chartLocalRingToEtaleLocalRing_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 151. The attribute's comment: “the comparison map is the identity on germs of regular functions”.

The canonical map 𝒪_{U, u} → 𝒪_{X, x̄} sends the ordinary germ at u of a regular function on the chart to the germ of the same function at the geometric point.

theorem chartLocalRingToEtaleLocalRing_germ {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (a : Γ(chartScheme V.chart, ⊤)) :
    chartLocalRingToEtaleLocalRing B S hS X hX V
        ((chartScheme V.chart).presheaf.germ ⊤ (chartPoint B S hS X V) trivial a) =
      etaleLocalRingGerm B S hS X x (op V) a

AlgebraicGeometry.Space.faithfullyFlat_chartLocalRingToEtaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 164. The attribute's comment: “the base-change map is faithfully flat”.

The base change of Stacks 05VP is faithfully flat. The canonical map 𝒪_{U, u} → 𝒪_{X, x̄} is faithfully flat: the étale local ring is the strict henselization of the chart's local ring, and a strict henselization is faithfully flat over the ring it henselizes.

theorem faithfullyFlat_chartLocalRingToEtaleLocalRing {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) :
    (chartLocalRingToEtaleLocalRing B S hS X hX V).FaithfullyFlat

AlgebraicGeometry.Space.flat_chartLocalRingToEtaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 182. The attribute's comment: “the base-change map is flat”.

The canonical map 𝒪_{U, u} → 𝒪_{X, x̄} is flat, so the base change of Stacks 05VP along it is exact.

theorem flat_chartLocalRingToEtaleLocalRing {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) :
    (chartLocalRingToEtaleLocalRing B S hS X hX V).Flat

AlgebraicGeometry.Space.chartStalkBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 196. The attribute's comment: “the base-change functor - ⊗_{O_{U, u}} O_{X, xbar}”.

The base-change functor - ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} of Stacks 05VP, taking a module over the local ring of the chart to a module over the étale local ring at the geometric point.

noncomputable def chartStalkBaseChange {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) :
    ModuleCat.{max u m} ↥(chartLocalRing B S hS X V) ⥤
      ModuleCat.{max (u + 1) m} ↥(etaleLocalRing B S hS X x)

AlgebraicGeometry.Space.chartZariskiModuleStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 209. The attribute's comment: “the Zariski stalk of the chart restriction, the left factor of the tensor”.

The ordinary (Zariski) stalk (φ^* F)_u of the restriction of an 𝒪_X-module to an étale scheme chart, as a module over the local ring 𝒪_{U, u} of the chart.

It is the stalk of AlgebraicGeometry.Space.restrictToChart at the point AlgebraicGeometry.Space.chartZariskiPoint of the Zariski site of the chart, with its scalars restricted along AlgebraicGeometry.Space.chartZariskiFiberIso.

noncomputable def chartZariskiModuleStalk {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (F : Modules.{u, m} B S hS X hX) :
    ModuleCat.{max u m} ↥(chartLocalRing B S hS X V)

AlgebraicGeometry.Space.chartStalkTensorEtaleLocalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricStalkBaseChange.lean, line 224. The attribute's comment: “the left-hand side (phi^* F)_u ⊗_{O_{U, u}} O_{X, xbar}”.

The left-hand side (φ^* F)_u ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} of Stacks 05VP: the Zariski stalk of the chart restriction, base changed along the canonical map to the étale local ring.

Its type is the category in which AlgebraicGeometry.Space.geometricModuleStalk also lands, so the equation of Stacks 05VP relates two objects of one category.

noncomputable def chartStalkTensorEtaleLocalRing {x : GeometricPoint B S hS X}
    (V : SmallEtaleNeighborhood x) (F : Modules.{u, m} B S hS X hX) :
    ModuleCat.{max (u + 1) m} ↥(etaleLocalRing B S hS X x)

Tag 05VQ, a lemma

Tag 05VQ in the Stacks Project.

AlgebraicGeometry.Space.geometricModuleStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricModuleStalk.lean, line 244. The attribute's comment: “the module stalk at a geometric point”.

Stacks 05VQ. The stalk of an 𝒪_X-module at a geometric point x̄ of an algebraic space, as a module over the étale local ring 𝒪_{X, x̄}: the stalk at the point of the small étale site determined by x̄, with its scalars extended along AlgebraicGeometry.Space.pointStalkRingEquiv.

noncomputable def geometricModuleStalk (X : AlgebraicSpaces B S hS)
    (x : GeometricPoint B S hS X.1) (F : Modules.{u, m} B S hS X.1 X.2) :
    ModuleCat (etaleLocalRing B S hS X.1 x)

AlgebraicGeometry.Space.geometricModuleStalkPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricModuleStalkBaseChange.lean, line 93. The attribute's comment: “the base-change formula (f^*G)_x̄ ≅ 𝒪_{X, x̄} ⊗_{𝒪_{Y, f ∘ x̄}} G_{f ∘ x̄} for the geometric stalk of a pullback of modules”.

The stalk at a geometric point x̄ of the pullback of an 𝒪_Y-module G along a morphism f : X ⟶ Y of algebraic spaces is the base change of the stalk of G at the image point f ∘ x̄ along the canonical homomorphism 𝒪_{Y, f ∘ x̄} ⟶ 𝒪_{X, x̄} of étale local rings of Stacks 04NG:

(f^*G)_{x̄} ≅ 𝒪_{X, x̄} ⊗_{𝒪_{Y, f ∘ x̄}} G_{f ∘ x̄}.

def geometricModuleStalkPullbackIso :
    geometricModuleStalk B S hS X x ((modulePullback B S hS f).obj G) ≅
      (ModuleCat.extendScalars (etaleLocalRingMap X.2 f.hom x)).obj
        (geometricModuleStalk B S hS Y (geometricPointMap f.hom x) G)

Tag 03M0, a lemma

Tag 03M0 in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_over_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentEtaleChart.lean, line 250. The attribute's comment: “(1) iff (3)”.

Stacks 03M0, conditions (1) and (3). A sheaf of 𝒪_F-modules on the small étale site of an algebraic space F is quasi-coherent if and only if its restriction along one étale chart whose structure morphism is surjective on points is quasi-coherent.

The restriction is restriction to the slice of the small étale site at the chart; see the implementation notes.

theorem isQuasicoherentOnSite_iff_over_of_isSurjective (M : Modules.{u, u} B S hS F hF)
    (U : (smallEtaleRingedSite B S hS F hF).C) (hsurj : IsSurjective B S hS U.1.hom) :
    M.IsQuasicoherentOnSite ↔ (M.over U).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_forall_affine_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentEtaleChart.lean, line 264. The attribute's comment: “(1) iff (4)”.

Stacks 03M0, conditions (1) and (4). A sheaf of 𝒪_F-modules on the small étale site of an algebraic space F is quasi-coherent if and only if its restriction along every étale chart whose underlying scheme is affine is quasi-coherent.

The restriction is restriction to the slice of the small étale site at the chart; see the implementation notes.

theorem isQuasicoherentOnSite_iff_forall_affine_over (M : Modules.{u, u} B S hS F hF) :
    M.IsQuasicoherentOnSite ↔
      ∀ U : (smallEtaleRingedSite B S hS F hF).C,
        IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS F).obj U)) →
        (M.over U).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_etaleModulePullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentEtaleMorphism.lean, line 256. The attribute's comment: “(1) iff (2)”.

Stacks 03M0, conditions (1) and (2). A sheaf of 𝒪_X-modules on the small étale site of an algebraic space X is quasi-coherent if and only if its pullback along an étale morphism f : Y ⟶ X of algebraic spaces which is surjective on points is quasi-coherent.

The forward implication needs no surjectivity: quasi-coherence of a module is inherited by every étale pullback, because a covering of the composite chart of X lifts to a covering of the chart of Y (AlgebraicGeometry.Space.SmallEtale.smallEtalePostcomp_cover_lift) and global presentations transfer by AlgebraicGeometry.Space.hasGlobalPresentation_over_postcomp_iff. The converse is where surjectivity enters: an étale chart of Y surjective on points composes with f to an étale chart of X surjective on points, which covers the final object of the small étale site of X by AlgebraicGeometry.Space.SmallEtale.coversTop_of_isSurjective, so every chart of X is covered by charts that map to it; those are, up to isomorphism, the composites of the charts of Y, which carry global presentations by hypothesis.

theorem isQuasicoherentOnSite_etaleModulePullback_iff (f : Y ⟶ X) (hf : IsEtale B S hS f.hom)
    (hsurj : IsSurjective B S hS f.hom) (M : Modules.{u, u} B S hS X.1 X.2) :
    M.IsQuasicoherentOnSite ↔
      ((etaleModulePullback B S hS f hf).obj M).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_exists_etale_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentEtaleMorphism.lean, line 295. The attribute's comment: “(1) iff (2), existential form”.

Stacks 03M0, conditions (1) and (2), in the existential form of the source. A sheaf of 𝒪_X-modules on the small étale site of an algebraic space X is quasi-coherent if and only if there is an étale morphism f : Z ⟶ X of algebraic spaces, surjective on points, whose pullback of the module is quasi-coherent.

The witness for the forward implication is the identity of X, which is étale because precomposing an étale chart with it returns the chart, and surjective on points because AlgebraicGeometry.Space.pointsMap_id is the identity. No comparison of AlgebraicGeometry.Space.smallEtalePostcomp with the identity functor is needed: the pullback along the identity is quasi-coherent because AlgebraicGeometry.Space.isQuasicoherentOnSite_etaleModulePullback_iff applies to every étale morphism, the identity included.

theorem isQuasicoherentOnSite_iff_exists_etale_surjective
    (M : Modules.{u, u} B S hS X.1 X.2) :
    M.IsQuasicoherentOnSite ↔
      ∃ (Z : AlgebraicSpaces B S hS) (f : Z ⟶ X) (hf : IsEtale B S hS f.hom),
        IsSurjective B S hS f.hom ∧
          ((etaleModulePullback B S hS f hf).obj M).IsQuasicoherentOnSite

Tag 03M1, a lemma

Tag 03M1 in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_smallEtaleInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InternalHomQuasicoherentChartLocal.lean, line 206. The attribute's comment: “(6) internal hom out of a module of finite presentation”. References: SGA 3 III (0.6), “more general”.

Stacks 03M1, the internal Hom. Let F be an algebraic space over a scheme S and let M, N be quasi-coherent 𝒪_F-modules with M of finite presentation, Stacks 03DL(7). Then the internal Hom 𝓗om_{𝒪_F}(M, N) is quasi-coherent.

The internal Hom is AlgebraicGeometry.Space.smallEtaleInternalHom, formed on the small étale ringed site of F; its sections over an étale chart U are the morphisms M|_U ⟶ N|_U, so they lie in u + 1 even though those of M and N lie in u.

The proof is the source's. Quasi-coherence is local on a covering of each object (Stacks.SheafOfModules.isQuasicoherentOnSite_of_locally_over), the finite-presentation hypothesis supplies for each étale chart a covering on whose members M has a finite global presentation, and on such a member the conclusion is isQuasicoherentOnSite_smallEtaleInternalHom_over_of_hasFiniteGlobalPresentation: restriction to an étale chart is a localization and formation of internal Hom commutes with localization (Stacks 04M1 and 0E8H), so the chart case is the globally presented case AlgebraicGeometry.Space.isQuasicoherentOnSite_smallEtaleInternalHom_of_presentation' on the small étale site of the chart.

The quasi-coherence of M is one of the source's hypotheses and is listed; the proof does not use it, since finite presentation already implies it.

theorem isQuasicoherentOnSite_smallEtaleInternalHom (M N : Modules.{u, u} B S hS F hF)
    (hM : M.IsQuasicoherentOnSite) (hN : N.IsQuasicoherentOnSite)
    (hMfp : M.IsFinitePresentationOnSite) :
    (smallEtaleInternalHom B S hS F hF M N).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherent_left_of_shortExact', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentClausesUnconditional.lean, line 171. The attribute's comment: “clause (4), left term, for the small étale site of an algebraic space, at module universe u”.

Stacks 03M1 for short exact sequences, left term, at m := u, with nothing assumed. The kernel term of a short exact sequence of 𝒪_F-modules on an algebraic space is quasi-coherent if the other two terms are.

No instance of Stacks 03DW occurs, because sections of a short exact sequence are left exact; this is AlgebraicGeometry.Space.isQuasicoherent_left_of_shortExact with its h03DX supplied by AlgebraicGeometry.Space.isCartesianOnAffineCharts_of_isQuasicoherentOnSite.

theorem isQuasicoherent_left_of_shortExact'
    (T : ShortComplex (Modules.{u, u} B S hS F hF)) (hT : T.ShortExact)
    [T.X₂.IsQuasicoherentOnSite] [T.X₃.IsQuasicoherentOnSite] :
    T.X₁.IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherent_middle_of_shortExact', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentClausesUnconditional.lean, line 187. The attribute's comment: “clause (4), middle term, for the small étale site of an algebraic space, at module universe u”.

Stacks 03M1 for short exact sequences, middle term, at m := u, with nothing assumed. An extension of quasi-coherent 𝒪_F-modules on an algebraic space is quasi-coherent.

This is AlgebraicGeometry.Space.isQuasicoherent_middle_of_shortExact with its h03DX supplied by AlgebraicGeometry.Space.isCartesianOnAffineCharts_of_isQuasicoherentOnSite and its T.g-specific instance of Stacks 03DW by AlgebraicGeometry.Space.surjective_g_val_app_of_shortExact_of_isCartesian.

theorem isQuasicoherent_middle_of_shortExact'
    (T : ShortComplex (Modules.{u, u} B S hS F hF)) (hT : T.ShortExact)
    [T.X₁.IsQuasicoherentOnSite] [T.X₃.IsQuasicoherentOnSite] :
    T.X₂.IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherent_right_of_shortExact', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentClausesUnconditional.lean, line 205. The attribute's comment: “clause (4), right term, for the small étale site of an algebraic space, at module universe u”.

Stacks 03M1 for short exact sequences, right term, at m := u, with nothing assumed. The quotient term of a short exact sequence of 𝒪_F-modules on an algebraic space is quasi-coherent if the other two terms are.

Its two hypotheses are supplied as in AlgebraicGeometry.Space.isQuasicoherent_middle_of_shortExact'.

theorem isQuasicoherent_right_of_shortExact'
    (T : ShortComplex (Modules.{u, u} B S hS F hF)) (hT : T.ShortExact)
    [T.X₁.IsQuasicoherentOnSite] [T.X₂.IsQuasicoherentOnSite] :
    T.X₃.IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_of_isColimit_cofan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSheavesProperties.lean, line 154. The attribute's comment: “(1) any direct sum of quasi-coherent 𝒪_X-modules is quasi-coherent”.

Stacks 03M1 (1). Any direct sum of quasi-coherent 𝒪_X-modules on an algebraic space X is quasi-coherent: the vertex of a colimiting cofan on a family of quasi-coherent 𝒪_X-modules, indexed by an arbitrary type, is quasi-coherent.

This is AlgebraicGeometry.Space.isQuasicoherentOnSite_of_isColimit_cofan_of_h03DX with Descent, Proposition 03DX(2) supplied by AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_isCartesianOnAffineCharts.

theorem isQuasicoherentOnSite_of_isColimit_cofan {ι : Type w}
    {G : ι → Modules.{u, u} B S hS F hF} (c : Cofan G) (hc : IsColimit c)
    (hG : ∀ i, (G i).IsQuasicoherentOnSite) :
    c.pt.IsQuasicoherentOnSite

AlgebraicGeometry.Space.isClosedUnderColimitsOfShape_quasicoherentSheaves_of_essentiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSheavesProperties.lean, line 170. The attribute's comment: “(2) any colimit of quasi-coherent 𝒪_X-modules is quasi-coherent”.

Stacks 03M1 (2). Any colimit of quasi-coherent 𝒪_X-modules on an algebraic space X is quasi-coherent: quasi-coherence is closed under colimits of every small shape K.

The shape K is replaced by its small model, for which this is AlgebraicGeometry.Space.isClosedUnderColimitsOfShape_quasicoherentSheaves_schemeUniverse: a colimit is the cokernel of a map between two direct sums, and clauses (1) and (3) apply.

theorem isClosedUnderColimitsOfShape_quasicoherentSheaves_of_essentiallySmall (K : Type w)
    [Category.{w'} K] [EssentiallySmall.{u} K] :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B S hS F hF).O))).IsClosedUnderColimitsOfShape K

AlgebraicGeometry.Space.isQuasicoherentOnSite_kernel_and_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSheavesProperties.lean, line 185. The attribute's comment: “(3) the kernel and the cokernel of a morphism of quasi-coherent 𝒪_X-modules are quasi-coherent”.

Stacks 03M1 (3). The kernel and the cokernel of a morphism of quasi-coherent 𝒪_X-modules on an algebraic space X are quasi-coherent.

theorem isQuasicoherentOnSite_kernel_and_cokernel {M N : Modules.{u, u} B S hS F hF}
    (f : M ⟶ N) (hM : M.IsQuasicoherentOnSite) (hN : N.IsQuasicoherentOnSite) :
    (kernel f).IsQuasicoherentOnSite ∧ (cokernel f).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_shortExact_twoOutOfThree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSheavesProperties.lean, line 213. The attribute's comment: “(4) in a short exact sequence of 𝒪_X-modules, if two of the three terms are quasi-coherent so is the third”.

Stacks 03M1 (4). Given a short exact sequence 0 → 𝓕₁ → 𝓕₂ → 𝓕₃ → 0 of 𝒪_X-modules on an algebraic space X, if two out of the three terms are quasi-coherent then so is the third.

theorem isQuasicoherentOnSite_shortExact_twoOutOfThree
    {T : ShortComplex (Modules.{u, u} B S hS F hF)} (hT : T.ShortExact) :
    (T.X₂.IsQuasicoherentOnSite → T.X₃.IsQuasicoherentOnSite → T.X₁.IsQuasicoherentOnSite) ∧
      (T.X₁.IsQuasicoherentOnSite → T.X₃.IsQuasicoherentOnSite →
        T.X₂.IsQuasicoherentOnSite) ∧
      (T.X₁.IsQuasicoherentOnSite → T.X₂.IsQuasicoherentOnSite →
        T.X₃.IsQuasicoherentOnSite)

AlgebraicGeometry.Space.isQuasicoherentOnSite_tensorModule_schemeUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSheavesProperties.lean, line 236. The attribute's comment: “(5) the tensor product of two quasi-coherent 𝒪_X-modules is quasi-coherent”.

Stacks 03M1 (5). The tensor product of two quasi-coherent 𝒪_X-modules on an algebraic space X is quasi-coherent.

The tensor product is AlgebraicGeometry.Space.tensorModule, the sheafified objectwise tensor product on the small étale ringed site; the two sheafification conditions it uses hold at the universe of the schemes.

theorem isQuasicoherentOnSite_tensorModule_schemeUniverse (M N : Modules.{u, u} B S hS F hF)
    (hM : M.IsQuasicoherentOnSite) (hN : N.IsQuasicoherentOnSite) :
    (tensorModule.{u, u, u} B S hS F hF M N).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_internalHomSheafSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSheavesProperties.lean, line 303. The attribute's comment: “(6) the internal Hom 𝓗om(𝓕, 𝓖) of two quasi-coherent 𝒪_X-modules with 𝓕 of finite presentation is quasi-coherent”. References: SGA 3 III (0.6), “more general”.

Stacks 03M1 (6). Let 𝓕, 𝓖 be quasi-coherent 𝒪_X-modules on an algebraic space X with 𝓕 of finite presentation (Stacks 03DL(7)). Then the internal Hom 𝓗om_{𝒪_X}(𝓕, 𝓖) is quasi-coherent.

The internal Hom is the one of Stacks 03EM in Mod(𝒪_X), AlgebraicGeometry.RingedSite.internalHomSheafSmall; see the module documentation. The quasi-coherence of 𝓕 is part of the source's statement; the argument does not use it, a module of finite presentation being quasi-coherent. Quasi-coherence is local on the members of a covering family (Stacks 03DN), the charts over which 𝓕 has a finite presentation cover X, and over each of them AlgebraicGeometry.Space.isQuasicoherentOnSite_over_internalHomSheafSmall applies.

theorem isQuasicoherentOnSite_internalHomSheafSmall (M N : Modules.{u, u} B S hS F hF)
    (_hM : M.IsQuasicoherentOnSite) (hN : N.IsQuasicoherentOnSite)
    (hfp : M.IsFinitePresentationOnSite) :
    letI := smallEtaleRingedSite_essentiallySmall B S hS F hF
    (RingedSite.internalHomSheafSmall (smallEtaleRingedSite B S hS F hF) M
      N).IsQuasicoherentOnSite

AlgebraicGeometry.Space.isQuasicoherentOnSite_tensorModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentTensorProduct.lean, line 132. The attribute's comment: “(5) tensor products”.

Stacks 03M1, tensor products. The tensor product of two quasi-coherent 𝒪_F-modules on an algebraic space is quasi-coherent.

The tensor product is AlgebraicGeometry.Space.tensorModule, formed on the small étale ringed site of F; the sections of the two factors may lie in independent universes.

theorem isQuasicoherentOnSite_tensorModule (M : Modules.{u, m} B S hS F hF)
    (N : Modules.{u, n} B S hS F hF) (hM : M.IsQuasicoherentOnSite)
    (hN : N.IsQuasicoherentOnSite) :
    (tensorModule B S hS F hF M N).IsQuasicoherentOnSite

Sources

Section66.30 Properties of modules #

Section 66.30 of the Stacks Project, Tag 05VR. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05VR, the section

Tag 05VR in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentationOnSite_iff_isFinitePresentationOnCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationOnSiteAffineCharts.lean, line 269. The attribute's comment: “of finite presentation: for a quasi-coherent module on an algebraic space, finite presentation on the small etale site is finite presentation of its restriction to every etale scheme chart, read on the Zariski site of the chart (items (2) and (4) of the section)”.

For a quasi-coherent module, finite presentation on the small étale site is finite presentation on the étale scheme charts. This is the property "of finite presentation" of the section of Stacks 05VR on properties of modules on an algebraic space: it may be read on the small étale site, or on every étale scheme chart, where for a quasi-coherent module it is the property of the corresponding module on the scheme (the scheme case being Stacks 05VG).

theorem isFinitePresentationOnSite_iff_isFinitePresentationOnCharts
    (M : Modules.{u, u} B S hS X.1 X.2) (hqc : M.IsQuasicoherentOnSite) :
    SheafOfModules.IsFinitePresentationOnSite M ↔ IsFinitePresentationOnCharts B S hS X.2 M

AlgebraicGeometry.Space.isFiniteTypeOnSite_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ModuleFiniteTypeQuotient.lean, line 94. The attribute's comment: “finite type, quotients”.

Properties of Spaces, Section 66.30, the finite type clause for a quotient. A quotient of an 𝒪_X-module of finite type on the small étale site of an algebraic space X is again of finite type.

On each member of a covering witnessing finite type for the source, the restricted epimorphism composes with the finite coproduct presenting the source to present the target.

theorem isFiniteTypeOnSite_of_epi {M N : Modules.{u, u} B S hS X hX} (p : M ⟶ N) [Epi p]
    (hM : SheafOfModules.IsFiniteTypeOnSite M) :
    SheafOfModules.IsFiniteTypeOnSite N

Sources

LeanAlgebraicGeometry.Space.isFinitePresentationOnSite_iff_isFinitePresentationOnCharts · AlgebraicGeometry.Space.isFiniteTypeOnSite_of_epi

Section66.31 Locally projective modules #

Section 66.31 of the Stacks Project, Tag 060P. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 060Q, a lemma

Tag 060Q in the Stacks Project.

AlgebraicGeometry.Space.exists_surjective_isLocallyProjective_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyProjectiveEtaleChart.lean, line 252.

Stacks Project, Tag 060Q. The restriction of an 𝒪_F-module to the Zariski site of an étale chart scheme is locally projective for some chart whose structure morphism is surjective on points if and only if it is locally projective for every étale chart.

The implication from one chart to all of them is AlgebraicGeometry.Space.isLocallyProjective_restrictToChartScheme_of_isSurjective; the converse needs only that an algebraic space has a chart surjective on points at all, namely its atlas. Quasi-coherence of M is the source's standing hypothesis on the module.

theorem exists_surjective_isLocallyProjective_iff_forall
    (hF : IsAlgebraicSpace B S hS F) (M : Modules.{u, u} B S hS F hF)
    (hM : M.IsQuasicoherentOnSite) :
    (∃ U : SmallEtale B S hS F, IsSurjective B S hS U.1.hom ∧
        Scheme.Modules.IsLocallyProjective (restrictToChartScheme B S hS F hF M U)) ↔
      ∀ U : SmallEtale B S hS F,
        Scheme.Modules.IsLocallyProjective (restrictToChartScheme B S hS F hF M U)

Tag 060R, a definition

Tag 060R in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyProjective.lean, line 49.

Stacks 060R. A quasi-coherent module on an algebraic space is locally projective if its restriction to every étale scheme chart is locally projective.

noncomputable abbrev IsLocallyProjective (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (F : QuasicoherentSheaves.{u, m} B S hS X hX) : Prop

Tag 060S, a lemma

Tag 060S in the Stacks Project.

AlgebraicGeometry.Space.isLocallyProjective_restrictToChartScheme_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyProjectiveEtaleChart.lean, line 278.

Stacks Project, Tag 060S. The pullback of a locally projective 𝒪_Y-module along a morphism f : X ⟶ Y of algebraic spaces is locally projective.

The source's reduction: choose an étale chart V of Y surjective on points and lift it through f to an étale chart U of X surjective on points together with ψ : U ⟶ V making the square commute (Stacks 02X1). Then (f^*G)|_U is the pullback of G|_V along ψ, so it is locally projective by Stacks 060M, and Stacks 060Q propagates that to every chart of X.

See the implementation notes for the carried hypotheses: hqcY is Zariski quasi-coherence of the chart restrictions of G, hqcX is quasi-coherence of f^*G on the small étale site of X, and hsquare is the base-change identity (f^*G)|_U ≅ ψ^*(G|_V) at a commuting square of charts of f.

theorem isLocallyProjective_restrictToChartScheme_modulePullback
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (G : Modules.{u, u} B S hS Y.1 Y.2)
    (hqcY : ∀ V : SmallEtale B S hS Y.1,
      (restrictToChartScheme B S hS Y.1 Y.2 G V).IsQuasicoherent)
    (hqcX : ((modulePullback B S hS f).obj G).IsQuasicoherentOnSite)
    (hsquare : ∀ (U : SmallEtale B S hS X.1) (V : SmallEtale B S hS Y.1)
        (ψ : U.1.left ⟶ V.1.left), U.1.hom ≫ f.hom = yoneda.map ψ ≫ V.1.hom →
      (restrictToChartScheme B S hS X.1 X.2 ((modulePullback B S hS f).obj G) U ≅
        (Scheme.Modules.pullback ((BigFppfOver.toScheme B S hS).map ψ)).obj
          (restrictToChartScheme B S hS Y.1 Y.2 G V)))
    (hG : ∀ V : SmallEtale B S hS Y.1,
      Scheme.Modules.IsLocallyProjective (restrictToChartScheme B S hS Y.1 Y.2 G V))
    (U : SmallEtale B S hS X.1) :
    Scheme.Modules.IsLocallyProjective
      (restrictToChartScheme B S hS X.1 X.2 ((modulePullback B S hS f).obj G) U)

AlgebraicGeometry.Space.isLocallyProjective_restrictToChartScheme_modulePullback_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyProjectivePullbackSpaces.lean, line 133.

Stacks Project, Tag 060S. The inverse image of Stacks 03LU of a quasi-coherent 𝒪_Y-module whose chart restrictions are locally projective has locally projective chart restrictions: local projectivity of a quasi-coherent module on an algebraic space is stable under pullback along an arbitrary morphism of algebraic spaces.

Choose an étale chart V of Y surjective on points and lift it through f to an étale chart U₀ of X surjective on points with ψ : U₀ ⟶ V making the square commute (Stacks 02X1). Then (f^*G)|_{U₀} is the pullback of G|_V along ψ, so it is locally projective by Stacks 060M, and Stacks 060Q propagates that to every chart of X; quasi-coherence of f^*G, which the latter step needs, is Stacks 03GA.

theorem isLocallyProjective_restrictToChartScheme_modulePullback_of_isQuasicoherentOnSite
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (G : Modules.{u, u} B S hS Y.1 Y.2)
    (hG : G.IsQuasicoherentOnSite)
    (hproj : ∀ V : SmallEtale B S hS Y.1,
      Scheme.Modules.IsLocallyProjective (restrictToChartScheme B S hS Y.1 Y.2 G V))
    (U : SmallEtale B S hS X.1) :
    Scheme.Modules.IsLocallyProjective
      (restrictToChartScheme B S hS X.1 X.2 ((modulePullback B S hS f).obj G) U)

Sources

LeanAlgebraicGeometry.Space.exists_surjective_isLocallyProjective_iff_forall · AlgebraicGeometry.Space.IsLocallyProjective · AlgebraicGeometry.Space.isLocallyProjective_restrictToChartScheme_modulePullback · AlgebraicGeometry.Space.isLocallyProjective_restrictToChartScheme_modulePullback_of_isQuasicoherentOnSite

Section66.32 Quasi-coherent sheaves and presentations #

Section 66.32 of the Stacks Project, Tag 03M2. 2 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03M3, a proposition

Tag 03M3 in the Stacks Project.

Stacks.Groupoids.GroupoidScheme.quasicoherentModuleOfBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuasicoherentFromBase.lean, line 244. The attribute's comment: “the canonical descent datum on φ^*ℱ and the two conditions of Stacks 03LI, for a target which is a scheme”.

Stacks 03M3, the descent datum. For a quasi-coherent module ℱ on a scheme X and a morphism φ : U ⟶ X from the object scheme of a groupoid with t ≫ φ = s ≫ φ, the pullback φ^*ℱ together with its canonical descent morphism is a quasi-coherent module on the groupoid.

def quasicoherentModuleOfBase (F : X.Modules) (hF : F.IsQuasicoherent) :
    QuasicoherentModule G

Stacks.Groupoids.GroupoidScheme.quasicoherentModuleOfBaseFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuasicoherentFromBase.lean, line 257. The attribute's comment: “the functor ℱ ↦ (φ^*ℱ, α), for a target which is a scheme”.

Stacks 03M3, the functor. Pullback along φ together with the canonical descent morphism is functorial in the quasi-coherent module on the base.

def quasicoherentModuleOfBaseFunctor :
    ObjectProperty.FullSubcategory (fun F : X.Modules => F.IsQuasicoherent) ⥤
      QuasicoherentModule G

AlgebraicGeometry.Space.quasicoherentModuleOfSpaceBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentFromSpaceBase.lean, line 341. The attribute's comment: “the canonical descent datum on φ^*ℱ and the two conditions of Stacks 0441, for a target which is an algebraic space”.

Stacks 03M3, the descent datum, for a target which is an algebraic space. For a quasi-coherent module ℱ on an algebraic space X and a morphism φ : U ⟶ X from the object space of a groupoid in algebraic spaces with t ≫ φ = s ≫ φ, the inverse image φ^*ℱ together with its canonical transition morphism is a quasi-coherent module on the groupoid.

def quasicoherentModuleOfSpaceBase (φ : G.objects ⟶ X)
    (hφ : G.target ≫ φ = G.source ≫ φ) (M : Modules.{u, u} B S hS X.1 X.2)
    (hM : M.IsQuasicoherentOnSite) : QuasicoherentModule B S hS G

AlgebraicGeometry.Space.isEquivalence_quasicoherentFromSpaceBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentFromSpaceBaseEquivalence.lean, line 252. The attribute's comment: “the functor QCoh(𝒪_X) ⥤ QCoh(U, R, s, t, c) is an equivalence of categories, for a target which is an algebraic space: full faithfulness and essential surjectivity at the hypotheses of the source”.

The functor ℱ ↦ (φ^*ℱ, α) from the quasi-coherent 𝒪_X-modules to the quasi-coherent modules on (U, R, s, t, c) is an equivalence of categories, for φ : U ⟶ X étale with t ≫ φ = s ≫ φ, {φ} a surjective étale covering of X, φ relatively representable, and the arrow space the kernel pair R = U ×_X U with t, s the two projections.

theorem isEquivalence_quasicoherentFromSpaceBase
    (hcov : IsEtaleCovering B S hS (fun _ : Unit => G.objects.1) (fun _ => φ.hom))
    (hrep : yoneda.relativelyRepresentable φ.hom)
    (hpb : IsPullback G.target.hom G.source.hom φ.hom φ.hom) :
    (quasicoherentFromSpaceBase B S hS G φ hφ).IsEquivalence

AlgebraicGeometry.Space.equivalenceQuasicoherentFromSpaceBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentFromSpaceBaseEquivalence.lean, line 269. The attribute's comment: “the equivalence QCoh(𝒪_X) ≌ QCoh(U, R, s, t, c) itself, for a target which is an algebraic space, at the hypotheses of the source”.

The equivalence QCoh(𝒪_X) ≌ QCoh(U, R, s, t, c) whose functor is AlgebraicGeometry.Space.quasicoherentFromSpaceBase, under the hypotheses of AlgebraicGeometry.Space.isEquivalence_quasicoherentFromSpaceBase.

def equivalenceQuasicoherentFromSpaceBase
    (hcov : IsEtaleCovering B S hS (fun _ : Unit => G.objects.1) (fun _ => φ.hom))
    (hrep : yoneda.relativelyRepresentable φ.hom)
    (hpb : IsPullback G.target.hom G.source.hom φ.hom φ.hom) :
    QuasicoherentSheaves.{u, u} B S hS X.obj X.property ≌ QuasicoherentModule B S hS G

AlgebraicGeometry.Space.quasicoherentFromSpaceBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuasicoherentFromSpaceBaseFunctor.lean, line 169. The attribute's comment: “the functor QCoh(𝒪_X) ⥤ QCoh(U, R, s, t, c) of the equivalence, for a target which is an algebraic space; this declaration is the functor itself, that it is an equivalence being proved in QuasicoherentFromSpaceBaseEquivalence.lean”.

The functor QCoh(𝒪_X) ⥤ QCoh(U, R, s, t, c) attached to an étale φ : U ⟶ X with t ≫ φ = s ≫ φ: it sends a quasi-coherent 𝒪_X-module ℱ to φ^*ℱ with its canonical transition morphism, and a morphism to its inverse image along φ.

def quasicoherentFromSpaceBase :
    QuasicoherentSheaves.{u, u} B S hS X.obj X.property ⥤ QuasicoherentModule B S hS G

Tag 077V, a proposition

Tag 077V in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentSheaves_isGrothendieckAbelian_enoughInjectives_hasLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSeparator.lean, line 1010. The attribute's comment: “(1) QCoh(𝒪_X) is a Grothendieck abelian category; consequently it has enough injectives and all limits”. References: SGA 4 I (7.13), “special case”; SGA 4 V (0.2.1), “special case”.

Stacks 077V, part (1). Let F be an algebraic space over a scheme S. The category QCoh(𝒪_F) of quasi-coherent 𝒪_F-modules is a Grothendieck abelian category; consequently it has enough injectives and all limits.

The abelian structure is the one given by the kernel and cokernel clauses of Stacks 03M1. The three conditions of a Grothendieck abelian category are: colimits, which exist and agree with those of 𝒪_F-modules by Stacks 03M1; exactness of filtered colimits; and a generator, which is AlgebraicGeometry.Space.hasSeparator_quasicoherentSheaves, built from a presentation F = U/R through Stacks 03M3 and 077U. The assertions on injectives and limits hold in every Grothendieck abelian category (Stacks 079H, 07D8).

theorem quasicoherentSheaves_isGrothendieckAbelian_enoughInjectives_hasLimits :
    letI := isClosedUnderKernels_quasicoherentSheaves_schemeUniverse B S hS F hF
    letI := isClosedUnderCokernels_quasicoherentSheaves B S hS F hF
    letI := quasicoherentSheaves_abelian_of_closure B S hS F hF
    IsGrothendieckAbelian.{u} (QuasicoherentSheaves.{u, u} B S hS F hF) ∧
      EnoughInjectives (QuasicoherentSheaves.{u, u} B S hS F hF) ∧
      HasLimitsOfSize.{u, u} (QuasicoherentSheaves.{u, u} B S hS F hF)

AlgebraicGeometry.Space.exists_coherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentSeparator.lean, line 1032. The attribute's comment: “(2) the inclusion QCoh(𝒪_X) ⥤ Mod(𝒪_X) has a right adjoint Q whose adjunction morphism Q(F) ⟶ F is an isomorphism for every quasi-coherent F”.

Stacks 077V, part (2). Let F be an algebraic space over a scheme S. The inclusion functor QCoh(𝒪_F) ⥤ Mod(𝒪_F) has a right adjoint Q, the coherator, such that for every quasi-coherent 𝒪_F-module 𝓕 the adjunction morphism Q(𝓕) ⟶ 𝓕 is an isomorphism.

The right adjoint exists by the special adjoint functor theorem applied to the Grothendieck abelian category of part (1), AlgebraicGeometry.Space.isLeftAdjoint_ι_quasicoherentSheaves; the inclusion is fully faithful, so the counit is an isomorphism exactly on its essential image, AlgebraicGeometry.Space.isIso_quasicoherentCoheratorCounit_app.

theorem exists_coherator :
    ∃ (Q : Modules.{u, u} B S hS F hF ⥤ QuasicoherentSheaves.{u, u} B S hS F hF)
      (adj : (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O))).ι ⊣ Q),
      ∀ (M : Modules.{u, u} B S hS F hF), M.IsQuasicoherentOnSite → IsIso (adj.counit.app M)

Sources

LeanStacks.Groupoids.GroupoidScheme.quasicoherentModuleOfBase · Stacks.Groupoids.GroupoidScheme.quasicoherentModuleOfBaseFunctor · AlgebraicGeometry.Space.quasicoherentModuleOfSpaceBase · AlgebraicGeometry.Space.isEquivalence_quasicoherentFromSpaceBase · AlgebraicGeometry.Space.equivalenceQuasicoherentFromSpaceBase · AlgebraicGeometry.Space.quasicoherentFromSpaceBase · AlgebraicGeometry.Space.quasicoherentSheaves_isGrothendieckAbelian_enoughInjectives_hasLimits · AlgebraicGeometry.Space.exists_coherator

Section66.33 Morphisms towards schemes #

Section 66.33 of the Stacks Project, Tag 05Z0. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05Z1, a lemma

Tag 05Z1 in the Stacks Project.

AlgebraicGeometry.Space.morphismToAffineEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MorphismToAffineScheme.lean, line 522. References: EGA II (1.2.7), “absolute case S=Spec ℤ”; EGA I (2.2.4).

Stacks 05Z1. Pullback of regular functions is a bijection between morphisms of algebraic spaces X ⟶ T into an affine object of the site and ring homomorphisms Γ(T, 𝒪_T) →+* Γ(X, 𝒪_X).

The bijection is specified, not merely asserted: its forward map restricts on every étale scheme chart of X to pullback of regular functions along the induced morphism of schemes.

def morphismToAffineEquiv (X : AlgebraicSpaces B S hS) (T : BigFppfOver B S hS)
    (hterminal : IsTerminal S) [IsAffine ((BigFppfOver.toScheme B S hS).obj T)] :
    { e : (X ⟶ schemeSpace T) ≃
        (Γ((BigFppfOver.toScheme B S hS).obj T, ⊤) →+* globalFunctions B S hS X.1) //
      ∀ (f : X ⟶ schemeSpace T) (U : SmallEtale B S hS X.1)
        (s : Γ((BigFppfOver.toScheme B S hS).obj T, ⊤)),
        ((e f) s).1 (op U) = Scheme.Γ.map (op ((BigFppfOver.toScheme B S hS).map
          (yoneda.preimage (U.1.hom ≫ f.hom)))) s }

Sources

LeanAlgebraicGeometry.Space.morphismToAffineEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

66.19 Points of the small étale… to 66.33 Morphisms towards schemes

Section66.19 Points of the small étale site#

Tag 0486, a definition

Tag 04JV, a definition

Tag 04JW, a lemma

Tag 05VN, a lemma

Tag 04JX, a lemma

Tag 04JY, a definition

Tag 04JZ, an equation

Tag 04K0, a lemma

Tag 04K1, a lemma

Tag 04K2, a lemma

Tag 04K3, a remark

Tag 04K4, a remark

Tag 04K5, a theorem

Tag 04K6, a lemma

Sources

Section66.20 Supports of abelian sheaves#

Tag 04K8, a lemma

Tag 04K9, a lemma

Tag 04KA, a definition

Tag 04KB, a lemma

Tag 04KC, a lemma

Sources

Section66.21 The structure sheaf of an algebraic space#

Tag 03G6, a lemma

Tag 03G7, a definition

Tag 03G8, a lemma

Tag 0BGS, a lemma

Sources

Section66.22 Stalks of the structure sheaf#

Tag 04KF, a lemma

Tag 04KG, a definition

Tag 04KH, a lemma

Tag 04N9, a lemma

Tag 0A4H, a lemma

Tag 0E01, a lemma

Sources

Section66.23 Local irreducibility#

Tag 06DK, a lemma

Tag 06DL, a definition

Tag 0DQ3, a lemma

Tag 0DQ4, a definition

Sources

Section66.24 Noetherian spaces#

Tag 03EA, a definition

Tag 04ZF, a lemma

Tag 04ZG, a lemma

Tag 08AH, a lemma

Sources

Section66.25 Regular algebraic spaces#

Tag 06LQ, a lemma

Tag 0AH9, a definition

Tag 0AHA, a lemma

Tag 0BGT, a lemma

Sources

Section66.26 Sheaves of modules on algebraic spaces#

Tag 03LU, an equation

Tag 03LV, a lemma

Tag 03LW, an equation

Tag 03LX, a lemma

Tag 03LY, a lemma

Sources

Section66.27 Étale localization#

Tag 04LY, an equation

Tag 04LZ, an equation

Tag 04M0, an equation

Tag 04M1, an equation

Tag 04M2, an equation

Tag 04M3, an equation

Tag 04M4, a lemma

Tag 04M5, a lemma

Tag 0GF6, a lemma

Sources

Section66.28 Recovering morphisms#

Tag 04KJ, a lemma

Tag 04KK, a lemma

Tag 04M6, a lemma

Tag 04KL, a theorem

Tag 05YZ, a lemma

Section66.19 Points of the small étale site #

Section66.20 Supports of abelian sheaves #

Section66.21 The structure sheaf of an algebraic space #

Section66.22 Stalks of the structure sheaf #

Section66.23 Local irreducibility #

Section66.24 Noetherian spaces #

Section66.25 Regular algebraic spaces #

Section66.26 Sheaves of modules on algebraic spaces #

Section66.27 Étale localization #

Section66.28 Recovering morphisms #

Section66.29 Quasi-coherent sheaves on algebraic spaces #

Section66.30 Properties of modules #

Section66.31 Locally projective modules #

Section66.32 Quasi-coherent sheaves and presentations #

Section66.33 Morphisms towards schemes #