66.3 Separation axioms to 66.18 The étale site of an…

Section66.3 Separation axioms #

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

Tag 03BS, a definition

Tag 03BS in the Stacks Project.

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PresentationQuasiCompact.lean, line 125. The attribute's comment: “part (3): quasi-separated”.

Stacks 07S4 for a presentation. An algebraic space presented by a chart whose underlying space is quasi-separated, with quasi-compact source projection, is quasi-separated.

The relation of the presentation is the kernel pair of the chart, so presheaf_quasiCompact_pullback_snd_of_presentation supplies the hypothesis of Stacks 07S4.

theorem isAbsolutelyQuasiSeparated_of_presentation (hZ : B.Contains (⊤_ Scheme.{u}))
    (hseparated : QuasiSeparatedSpace ((BigFppfOver.toScheme B S hS).obj P.U))
    (hsource : QuasiCompact ((BigFppfOver.toScheme B S hS).map P.source)) :
    IsAbsolutelyQuasiSeparated B S hS hZ F

AlgebraicGeometry.Space.IsAbsolutelySeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 95. The attribute's comment: “part (1): separated”.

An algebraic space is separated when it is separated over the terminal scheme, that is, when its absolute diagonal is a closed immersion.

abbrev IsAbsolutelySeparated (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.IsAbsolutelyLocallySeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 101. The attribute's comment: “part (2): locally separated”.

An algebraic space is locally separated when it is locally separated over the terminal scheme, that is, when its absolute diagonal is an immersion.

abbrev IsAbsolutelyLocallySeparated (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 107. The attribute's comment: “part (3): quasi-separated”.

An algebraic space is quasi-separated when it is quasi-separated over the terminal scheme, that is, when its absolute diagonal is quasi-compact.

abbrev IsAbsolutelyQuasiSeparated (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.IsAbsolutelyZariskiLocallyQuasiSeparated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 113. The attribute's comment: “part (4): Zariski locally quasi-separated”.

An algebraic space is Zariski locally quasi-separated when its absolute form admits a Zariski covering by quasi-separated open subspaces.

abbrev IsAbsolutelyZariskiLocallyQuasiSeparated
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

Tag 03DY, a lemma

Tag 03DY in the Stacks Project.

AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Decent/ConditionComparisons.lean, line 101. The attribute's comment: “part (2): Zariski locally quasi-separated”.

Condition (η) implies condition (ζ): a quasi-separated algebraic space is Zariski locally quasi-separated.

theorem isAbsolutelyZariskiLocallyQuasiSeparated_of_isAbsolutelyQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (h : IsAbsolutelyQuasiSeparated B S hS hZ X) :
    IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ X

AlgebraicGeometry.Space.isAbsolutelyLocallySeparated_of_isAbsolutelySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedVariants.lean, line 89. The attribute's comment: “part (1): locally separated”.

A separated algebraic space is locally separated.

theorem isAbsolutelyLocallySeparated_of_isAbsolutelySeparated
    (hZ : B.Contains (⊤_ Scheme.{u})) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAbsolutelySeparated B S hS hZ F) :
    IsAbsolutelyLocallySeparated B S hS hZ F

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isAbsolutelySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedVariants.lean, line 97. The attribute's comment: “part (1): quasi-separated”.

A separated algebraic space is quasi-separated.

theorem isAbsolutelyQuasiSeparated_of_isAbsolutelySeparated
    (hZ : B.Contains (⊤_ Scheme.{u})) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAbsolutelySeparated B S hS hZ F) :
    IsAbsolutelyQuasiSeparated B S hS hZ F

Tag 0AHR, a lemma

Tag 0AHR in the Stacks Project.

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_iff_compactSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiSeparatedFibreProducts.lean, line 249. The attribute's comment: “equivalence of (1) and (2)”.

Stacks 0AHR, equivalence of (1) and (2). An algebraic space over S is quasi-separated exactly when the fibre product of any two quasi-compact schemes over it is a quasi-compact scheme.

theorem isAbsolutelyQuasiSeparated_iff_compactSpace_pullback
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    IsAbsolutelyQuasiSeparated B S hS hZ X ↔
      ∀ (U V : BigFppfOver B S hS)
        (f : yoneda.obj U ⟶ X) (g : yoneda.obj V ⟶ X),
        CompactSpace ((BigFppfOver.toScheme B S hS).obj U) →
        CompactSpace ((BigFppfOver.toScheme B S hS).obj V) →
        ∃ W : BigFppfOver B S hS,
          CompactSpace ((BigFppfOver.toScheme B S hS).obj W) ∧
          Nonempty (yoneda.obj W ≅ pullback f g)

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_iff_compactSpace_pullback_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiSeparatedFibreProducts.lean, line 270. The attribute's comment: “equivalence of (1) and (3)”.

Stacks 0AHR, equivalence of (1) and (3). It is enough to test quasi-compactness of the fibre products of Stacks 0AHR on pairs of affine schemes over the algebraic space.

theorem isAbsolutelyQuasiSeparated_iff_compactSpace_pullback_affine
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    IsAbsolutelyQuasiSeparated B S hS hZ X ↔
      ∀ (U V : BigFppfOver B S hS)
        (f : yoneda.obj U ⟶ X) (g : yoneda.obj V ⟶ X),
        IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        IsAffine ((BigFppfOver.toScheme B S hS).obj V) →
        ∃ W : BigFppfOver B S hS,
          CompactSpace ((BigFppfOver.toScheme B S hS).obj W) ∧
          Nonempty (yoneda.obj W ≅ pullback f g)

AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedAffineIntersections.lean, line 570.

Stacks 0AHR. For an algebraic space X over S the following are equivalent: X is a quasi-separated algebraic space; for every pair of morphisms into X from objects of the big fppf site with quasi-compact underlying scheme the fibre product has quasi-compact underlying scheme; and the same for every pair of morphisms from objects with affine underlying scheme.

Condition (1) implies condition (2) because the fibre product maps to the product of the two factors by a base change of the absolute diagonal, so that morphism is quasi-compact, and the product of two quasi-compact objects over the terminal scheme is quasi-compact. Condition (2) implies condition (3) because an affine scheme is quasi-compact. Condition (3) implies condition (1) because quasi-compactness is Zariski local at the target, so the diagonal need only be tested on objects of the site with affine underlying scheme, and over such an object the criterion applies to the two morphisms the test factors through.

theorem isAbsolutelyQuasiSeparated_tfae (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) :
    List.TFAE
      [ IsAbsolutelyQuasiSeparated B S hS hZ X,
        HasQuasiCompactIntersections B S hS
          (fun Z : Scheme.{u} ↦ CompactSpace (Z : Type u)) X,
        HasQuasiCompactIntersections B S hS (fun Z : Scheme.{u} ↦ IsAffine Z) X ]

Tag 0AHS, a lemma

Tag 0AHS in the Stacks Project.

AlgebraicGeometry.Space.isAbsolutelySeparated_iff_hasAffineIntersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedAffineIntersections.lean, line 384.

Stacks 0AHS. An algebraic space over S is separated if and only if for every pair of objects of the big fppf site with affine underlying scheme mapping to it the fibre product has affine underlying scheme and the canonical map from the tensor product over ℤ of the two rings of global sections to the ring of global sections of the fibre product is surjective.

Necessity: the morphism from the fibre product to the product U ×_{Spec ℤ} V is a base change of the absolute diagonal, hence a closed immersion; and a closed immersion into a product of two affine schemes is exactly an affine source together with a surjective map on global sections.

Sufficiency: being a closed immersion is Zariski local at the target, so the diagonal need only be tested on objects of the site with affine underlying scheme, and over such an object the criterion applies to the two morphisms the test factors through.

theorem isAbsolutelySeparated_iff_hasAffineIntersections
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    IsAbsolutelySeparated B S hS hZ X ↔ HasAffineIntersections B S hS X

Sources

LeanAlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_presentation · AlgebraicGeometry.Space.IsAbsolutelySeparated · AlgebraicGeometry.Space.IsAbsolutelyLocallySeparated · AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.IsAbsolutelyZariskiLocallyQuasiSeparated · AlgebraicGeometry.Space.isAbsolutelyZariskiLocallyQuasiSeparated_of_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.isAbsolutelyLocallySeparated_of_isAbsolutelySeparated · AlgebraicGeometry.Space.isAbsolutelyQuasiSeparated_of_isAbsolutelySeparated

Section66.4 Points of algebraic spaces #

Section 66.4 of the Stacks Project, Tag 03BT. 12 tags here are carried by 29 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03BU, a definition

Tag 03BU in the Stacks Project.

AlgebraicGeometry.Space.points, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Points.lean, line 222. The attribute's comment: “set of points”.

Stacks 03BU. Points of an algebraic space are equivalence classes of its field-valued points.

abbrev points : Type (u + 1)

AlgebraicGeometry.Space.FieldValuedPoint.hasCommonExtension_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Points.lean, line 232. The attribute's comment: “equivalence of field-valued points”.

Stacks 03BU. Common extension is transitive: two extensions of a field-valued point can be amalgamated over that point.

theorem FieldValuedPoint.hasCommonExtension_trans
    {p q r : FieldValuedPoint B S hS F}
    (hpq : FieldValuedPoint.HasCommonExtension B S hS F p q)
    (hqr : FieldValuedPoint.HasCommonExtension B S hS F q r) :
    FieldValuedPoint.HasCommonExtension B S hS F p r

AlgebraicGeometry.Space.FieldValuedPoint.class_eq_class_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Points.lean, line 276. The attribute's comment: “equality of points”.

Stacks 03BU. Two field-valued representatives define the same point exactly when they admit a common field-valued extension.

theorem FieldValuedPoint.class_eq_class_iff
    (p q : FieldValuedPoint B S hS F) :
    p.class B S hS F = q.class B S hS F ↔
      FieldValuedPoint.HasCommonExtension B S hS F p q

Tag 03BV, a lemma

Tag 03BV in the Stacks Project.

AlgebraicGeometry.Space.bijective_pointsToScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsRepresentable.lean, line 184.

The points of a scheme, viewed as an algebraic space through its functor of points, are in canonical one-to-one correspondence with the points of the representing scheme, the correspondence being AlgebraicGeometry.Space.pointsToScheme.

theorem bijective_pointsToScheme (U : BigFppfOver B S hS) :
    Function.Bijective (pointsToScheme B S hS U)

Tag 03H4, a lemma

Tag 03H4 in the Stacks Project.

AlgebraicGeometry.Space.exists_pointsULift_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedEtaleOpenPoints.lean, line 118. The attribute's comment: “for a value universe independent of the universe of the schemes”.

Stacks 03H4 for presheaves with values in a universe max w u independent of the universe u of the schemes: a point of one middle term of a cartesian square and a point of the other with the same image in the base are the images of a common point of the fibre product. This is AlgebraicGeometry.Space.exists_point_of_isPullbackULift with the two middle terms in the order of AlgebraicGeometry.Space.exists_points_of_isPullback.

theorem exists_pointsULift_of_isPullback
    {W X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    {p : W ⟶ X} {q : W ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ Y} (sq : IsPullback p q f g)
    (a : pointsULift.{w} B S hS X) (b : pointsULift.{w} B S hS Z)
    (hab : pointsMapULift B S hS X f a = pointsMapULift B S hS Z g b) :
    ∃ v : pointsULift.{w} B S hS W,
      pointsMapULift B S hS W p v = a ∧ pointsMapULift B S hS W q v = b

AlgebraicGeometry.Space.exists_points_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsBaseChange.lean, line 116.

The comparison map from the points of a fibre product of presheaves to the fibre product of the point sets is surjective: a point of X and a point of Z with the same image in Y are the images of a common point of a presheaf W sitting in a cartesian square over them.

theorem exists_points_of_isPullback {p : W ⟶ X} {q : W ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ Y}
    (sq : IsPullback p q f g) (a : points B S hS X) (b : points B S hS Z)
    (hab : pointsMap B S hS X f a = pointsMap B S hS Z g b) :
    ∃ w : points B S hS W,
      pointsMap B S hS W p w = a ∧ pointsMap B S hS W q w = b

AlgebraicGeometry.Space.exists_point_of_isPullback_presheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsOfPullback.lean, line 63.

Stacks 03H4. Compatible points of the two middle terms of a cartesian square of presheaves on the big fppf site of S lift to a point of its upper left corner.

This is surjectivity of |Z ×_Y X| → |Z| ×_{|Y|} |X|, stated elementwise for an arbitrary cartesian square of presheaves. The companion statement for a cartesian square in the category of algebraic spaces is AlgebraicGeometry.Space.exists_point_of_isPullback.

theorem exists_point_of_isPullback_presheaf
    {W Z X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y}
    (sq : IsPullback p q g f)
    (z : points B S hS Z) (x : points B S hS X)
    (h : pointsMap B S hS Z g z = pointsMap B S hS X f x) :
    ∃ w : points B S hS W,
      pointsMap B S hS W p w = z ∧ pointsMap B S hS W q w = x

AlgebraicGeometry.Space.exists_point_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsPullback.lean, line 36.

In a cartesian square of algebraic spaces over S, a point of Z and a point of X with the same image in Y are the two images of a point of W.

theorem exists_point_of_isPullback (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {W Z X Y : AlgebraicSpaces B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y}
    (sq : IsPullback p q g f)
    (z : points B S hS Z.1) (x : points B S hS X.1)
    (h : pointsMap B S hS Z.1 g.hom z = pointsMap B S hS X.1 f.hom x) :
    ∃ w : points B S hS W.1,
      pointsMap B S hS W.1 p.hom w = z ∧ pointsMap B S hS W.1 q.hom w = x

Tag 03H5, a lemma

Tag 03H5 in the Stacks Project.

AlgebraicGeometry.Space.presheafSurjective_iff_isSurjective_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurjectiveOnPoints.lean, line 292.

A morphism from a scheme over S to an algebraic space over S is surjective, in the sense that every represented base change of it is a surjective morphism of schemes, if and only if the induced map on points is surjective.

theorem presheafSurjective_iff_isSurjective_yoneda (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) (T : BigFppfOver B S hS) (f : yoneda.obj T ⟶ F) :
    (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f ↔ IsSurjective B S hS f

Tag 03BW, a lemma

Tag 03BW in the Stacks Project.

AlgebraicGeometry.Space.Presentation.pointsRelation_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Points.lean, line 72. The attribute's comment: “image equivalence relation”.

Stacks 03BW. Two points of the presenting scheme are related by the relation scheme exactly when they have the same image in the algebraic space.

theorem pointsRelation_iff (P : Presentation B S hS F hF)
    (x y : points B S hS (yoneda.obj P.U)) :
    P.pointsRelation x y ↔
      pointsMap B S hS (yoneda.obj P.U) P.toSpace x =
        pointsMap B S hS (yoneda.obj P.U) P.toSpace y

AlgebraicGeometry.Space.Presentation.pointsMap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Points.lean, line 95. The attribute's comment: “surjectivity on points”.

Stacks 03BW. The atlas of a presentation is surjective on points.

theorem pointsMap_surjective (P : Presentation B S hS F hF) :
    Function.Surjective (pointsMap B S hS (yoneda.obj P.U) P.toSpace)

Declarations registered for the tag:

Setoid.ker registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Points.lean, line 51 (StacksFrontier): “equivalence relation on points”. References: SGA 3 IV (3.3.1), “category of sets”; SGA 4 I (10.9), “special case”.
Setoid.quotientKerEquivOfSurjective registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Points.lean, line 54 (StacksFrontier): “canonical quotient equivalence”.

Tag 03BX, a lemma

Tag 03BX in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_pointTopologyFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsTopologyUnique.lean, line 293.

Stacks 03BX. There is a unique family of topologies on the points of the algebraic spaces over S which is the scheme topology on a scheme, makes every morphism of algebraic spaces continuous on points, and makes an étale morphism from a scheme open on points.

theorem existsUnique_pointTopologyFamily :
    ∃! _t : PointTopologyFamily B S hS, True

Tag 03BY, a definition

Tag 03BY in the Stacks Project.

AlgebraicGeometry.Space.pointTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsTopology.lean, line 79. The attribute's comment: “the underlying topological space of an algebraic space”.

The topology on the points of a presheaf on the big fppf site of S: a set of points is open when its preimage under every scheme-valued point is scheme open.

def pointTopology (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) :
    TopologicalSpace (points B S hS F)

Tag 03BZ, a lemma

Tag 03BZ in the Stacks Project.

AlgebraicGeometry.Space.openSubspacesOrderIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenSubspaceCorrespondence.lean, line 397. The attribute's comment: “part (1)”.

The order isomorphism from the open subspaces of an algebraic space over S to the open subsets of its space of points, sending an open subspace to the image of its point set.

noncomputable def openSubspacesOrderIso (hF : IsAlgebraicSpace B S hS F) :
    {G : Subfunctor F // IsOpenSubspace B S hS G} ≃o
      TopologicalSpace.Opens (points B S hS F)

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

The open subset of points attached to an open subspace is the image of its points.

theorem openSubspacesOrderIso_apply (hF : IsAlgebraicSpace B S hS F)
    (G : {G : Subfunctor F // IsOpenSubspace B S hS G}) :
    (openSubspacesOrderIso B S hS F hF G).1 =
      Set.range (pointsMap B S hS G.1.toFunctor G.1.ι)

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

Taking the image of the points of an open subspace is an inclusion-preserving bijection from the open subspaces of an algebraic space over S to the open subsets of its space of points, and it is the unique order isomorphism doing so.

theorem existsUnique_openSubspacesOrderIso (hF : IsAlgebraicSpace B S hS F) :
    ∃! e : {G : Subfunctor F // IsOpenSubspace B S hS G} ≃o
      TopologicalSpace.Opens (points B S hS F),
      ∀ G, (e G).1 = Set.range (pointsMap B S hS G.1.toFunctor G.1.ι)

AlgebraicGeometry.Space.openSubspacesOrderIso_and_isZariskiCover_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenSubspaceZariskiSite.lean, line 66.

Stacks Tag 03BZ. Let X be an algebraic space over S.

Part (1): taking the image of the point set is an inclusion-preserving bijection from the open subspaces of X to the open subsets of |X|; it is the unique order isomorphism doing so.

Part (2): a family of open subspaces of X is a Zariski covering exactly when the images of the point sets of its members cover |X|.

Together these identify the small Zariski site of X with the site attached to the topological space |X|.

theorem openSubspacesOrderIso_and_isZariskiCover_iff
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F) :
    (∃! e : {G : Subfunctor F // IsOpenSubspace B S hS G} ≃o
        TopologicalSpace.Opens (points B S hS F),
        ∀ G, (e G).1 = Set.range (pointsMap B S hS G.1.toFunctor G.1.ι)) ∧
      ∀ (I : Type u) (X : I → Subfunctor F), (∀ i, IsOpenSubspace B S hS (X i)) →
        (IsZariskiCover B S hS I X ↔
          (⋃ i, Set.range (pointsMap B S hS (X i).toFunctor (X i).ι)) = Set.univ)

AlgebraicGeometry.Space.isZariskiCover_iff_iUnion_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoveringPoints.lean, line 443. The attribute's comment: “zariski_coverings”.

Open subspaces cover an algebraic space in the Zariski topology if and only if their images on the space of points cover all points.

theorem isZariskiCover_iff_iUnion_points
    (hF : IsAlgebraicSpace B S hS F) (I : Type u)
    (U : I → Subfunctor F)
    (hU : ∀ i, IsOpenSubspace B S hS (U i)) :
    IsZariskiCover B S hS I U ↔
      (⋃ i, Set.range (pointsMap B S hS (U i).toFunctor (U i).ι)) =
        Set.univ

AlgebraicGeometry.Space.isCovering_iff_iSup_openSubspacesOrderIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoveringPoints.lean, line 457. The attribute's comment: “zariski_coverings”.

Via the canonical identification with open subsets of the point space, covering families of the small Zariski site are precisely open covers.

theorem isCovering_iff_iSup_openSubspacesOrderIso
    (hF : IsAlgebraicSpace B S hS F)
    (E : Covering.{u + 1, u + 1, u} (OpenSubspaces B S hS F)) :
    let : TopologicalSpace (points B S hS F) :=
      pointTopology B S hS F
    OpenSubspaces.IsCovering B S hS F E ↔
      (⨆ i, openSubspacesOrderIso B S hS F hF
        (E.2.X i)) =
        openSubspacesOrderIso B S hS F hF E.1

Tag 03IE, a lemma

Tag 03IE in the Stacks Project.

AlgebraicGeometry.Space.factorsThrough_openSubspace_iff_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FactorThroughOpenSubspace.lean, line 52.

A morphism of algebraic spaces factors through an open subspace if and only if its map on points has image in the point set of that subspace.

theorem factorsThrough_openSubspace_iff_points
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (U : Subfunctor X) (hU : IsOpenSubspace B S hS U)
    (f : Y ⟶ X) :
    (∃ g : Y ⟶ U.toFunctor, g ≫ U.ι = f) ↔
      (Set.range (pointsMap B S hS Y f) ⊆
        Set.range (pointsMap B S hS U.toFunctor U.ι))

Tag 06NF, a lemma

Tag 06NF in the Stacks Project.

AlgebraicGeometry.Space.factorThroughEtaleImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 90. The attribute's comment: “induced morphism”.

The morphism from a scheme to the open subspace corresponding to the image of its étale map.

noncomputable def factorThroughEtaleImage :
    yoneda.obj U ⟶ X'.toFunctor

AlgebraicGeometry.Space.factorThroughEtaleImage_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 99. The attribute's comment: “factorization”.

The induced morphism composes with the inclusion to give the original étale map.

theorem factorThroughEtaleImage_comp :
    factorThroughEtaleImage B S hS hX U f X' hX' hX'image ≫ X'.ι = f

AlgebraicGeometry.Space.surjective_factor_through_etaleImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 107. The attribute's comment: “surjective”.

The induced map to the image open subspace is surjective.

theorem surjective_factor_through_etaleImage
    (f' : yoneda.obj U ⟶ X'.toFunctor) (hfactor : f' ≫ X'.ι = f) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) f'

AlgebraicGeometry.Space.etale_factor_through_etaleImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 132. The attribute's comment: “étale”.

The induced map to the image open subspace is étale.

theorem etale_factor_through_etaleImage
    (f' : yoneda.obj U ⟶ X'.toFunctor) (hfactor : f' ≫ X'.ι = f) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) f'

AlgebraicGeometry.Space.isEtaleEquivalenceRelation_etaleImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 162. The attribute's comment: “étale equivalence relation”.

The kernel pair of an étale scheme morphism is an étale equivalence relation on its source.

theorem isEtaleEquivalenceRelation_etaleImage
    {R : BigFppfOver B S hS} (s t : R ⟶ U)
    (hR : IsPullback (yoneda.map s) (yoneda.map t) f f) :
    Stacks.Groupoids.IsEtaleEquivalenceRelation
      (prod.lift ((Over.post B.inclusion).map s)
        ((Over.post B.inclusion).map t))

AlgebraicGeometry.Space.isCoequalizer_factor_through_etaleImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 186. The attribute's comment: “presentation as a quotient”.

The image open subspace is the fppf sheaf quotient of U by the kernel pair of the original map.

theorem isCoequalizer_factor_through_etaleImage
    {R : BigFppfOver B S hS} (s t : R ⟶ U)
    (hR : IsPullback (yoneda.map s) (yoneda.map t) f f)
    (f' : yoneda.obj U ⟶ X'.toFunctor) (hfactor : f' ≫ X'.ι = f) :
    let J := BigFppfOver.topology B S hS
    ∃ (hRsh : Presheaf.IsSheaf J (yoneda.obj R))
      (hUsh : Presheaf.IsSheaf J (yoneda.obj U)),
      let RF : Sheaf J (Type u) := ⟨yoneda.obj R, hRsh⟩
      let UF : Sheaf J (Type u) := ⟨yoneda.obj U, hUsh⟩
      let XF : Sheaf J (Type u) := ⟨X'.toFunctor, hX'.1.isSheaf⟩
      let sf : RF ⟶ UF := ⟨yoneda.map s⟩
      let tf : RF ⟶ UF := ⟨yoneda.map t⟩
      let ff : UF ⟶ XF := ⟨f'⟩
      let w : sf ≫ ff = tf ≫ ff := by
        apply Sheaf.hom_ext
        change yoneda.map s ≫ f' = yoneda.map t ≫ f'
        exact (isPullback_of_factors_comp_mono X'.ι hfactor hfactor hR).w
      Nonempty (IsColimit (Cofork.ofπ ff w))

AlgebraicGeometry.Space.isOpenSubspace_etale_surjective_lift_openSubspaceOfPoints_range_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoveringAffineCharts.lean, line 174. The attribute's comment: “factorisation: induced morphism, factorization, surjective, étale”.

Stacks 06NF, the whole of its factorisation clause. Let U be an object of the big fppf category over S and f : h_U ⟶ X an étale morphism to an algebraic space over S. Then the subspace X' of X cut out by the image of |U| is an open subspace, and f factors through it by a morphism which is surjective — both on point sets and after every represented base change — and étale.

The four assertions correspond exactly to the four declarations into which the source's sentence "then f factors through a surjective étale morphism f' : U → X'" is split: the induced morphism, which here is the canonical CategoryTheory.Subfunctor.lift and so needs no choice; the factorisation f' ≫ X'.ι = f, which is CategoryTheory.Subfunctor.lift_ι and holds by rfl; surjectivity; and étaleness. That X' is an open subspace with point set the image of |U| is the source's own appeal to Tag 03BZ, and is AlgebraicGeometry.Space.isOpenSubspace_openSubspaceOfPoints together with AlgebraicGeometry.Space.range_pointsMap_ι_openSubspaceOfPoints.

What is not proved. The source's second sentence — that R = U ×_X U equals U ×_{X'} U, that it is an étale equivalence relation, and that X' is the quotient U/R — is not addressed. So the covering set of Tag 06NF is incomplete and the attribute carries a part string naming only the factorisation clause. Closing the rest needs Tag 0262, whose three parts are proved in StacksFrontier.AlgebraicGeometry.Spaces.Presentation.KernelPair.

theorem isOpenSubspace_etale_surjective_lift_openSubspaceOfPoints_range_yoneda
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ X)
    (hf : (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f) :
    IsOpenSubspace B S hS
        (openSubspaceOfPoints B S hS X
          (Set.range (pointsMap B S hS (yoneda.obj U) f))) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf
        (Subfunctor.lift f (range_le_openSubspaceOfPoints_range_pointsMap f)) ∧
      Function.Surjective (pointsMap B S hS (yoneda.obj U)
        (Subfunctor.lift f (range_le_openSubspaceOfPoints_range_pointsMap f))) ∧
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf
        (Subfunctor.lift f (range_le_openSubspaceOfPoints_range_pointsMap f))

Declarations registered for the tag:

CategoryTheory.Limits.PullbackCone.isLimitOfFactors registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/EtaleImageSubspace.lean, line 59 (StacksFrontier): “kernel pair”.

Tag 0H2X, a lemma

Tag 0H2X in the Stacks Project.

AlgebraicGeometry.Space.FieldValuedPoint.existsUnique_factor_of_class_eq_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/MonomorphismPoints.lean, line 62.

Stacks 0H2X. Two representatives of the same point factor uniquely through a representative whose map to the algebraic space is a monomorphism.

theorem FieldValuedPoint.existsUnique_factor_of_class_eq_of_mono
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F)
    (p q : FieldValuedPoint B S hS F)
    [Mono (yonedaEquiv.symm p.value)]
    (h : p.class B S hS F = q.class B S hS F) :
    ∃! f : q.siteObject B S hS F ⟶ p.siteObject B S hS F,
      F.map f.op p.value = q.value

Tag 03E1, a lemma

Tag 03E1 in the Stacks Project.

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

Stacks 03E1. Monomorphic field-valued representatives of the same point are isomorphic over the algebraic space.

theorem iso_of_mono_of_point_eq
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F)
    (p q : FieldValuedPoint B S hS F)
    [Mono (yonedaEquiv.symm p.value)] [Mono (yonedaEquiv.symm q.value)]
    (heq : p.class B S hS F = q.class B S hS F) :
    ∃ e : p.siteObject B S hS F ≅ q.siteObject B S hS F,
      F.map e.hom.op q.value = p.value

Sources

LeanAlgebraicGeometry.Space.points · AlgebraicGeometry.Space.FieldValuedPoint.hasCommonExtension_trans · AlgebraicGeometry.Space.FieldValuedPoint.class_eq_class_iff · AlgebraicGeometry.Space.bijective_pointsToScheme · AlgebraicGeometry.Space.exists_pointsULift_of_isPullback · AlgebraicGeometry.Space.exists_points_of_isPullback · AlgebraicGeometry.Space.exists_point_of_isPullback_presheaf · AlgebraicGeometry.Space.exists_point_of_isPullback

Section66.5 Quasi-compact spaces #

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

Tag 03E3, a definition

Tag 03E3 in the Stacks Project.

AlgebraicGeometry.Space.IsQuasiCompactSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 237.

Stacks 03E3. An algebraic space over S is quasi-compact when it admits a surjective étale morphism from a representable presheaf whose underlying scheme is quasi-compact.

abbrev IsQuasiCompactSpace (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

Tag 03E4, a lemma

Tag 03E4 in the Stacks Project.

AlgebraicGeometry.Space.isQuasiCompactSpaceULift_iff_compactSpace_pointsULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedQuasiCompactPoints.lean, line 180. The attribute's comment: “for a value universe independent of the universe of the schemes”.

Stacks 03E4 for a value universe max w u independent of the universe u of the schemes: an algebraic space over S is quasi-compact if and only if its space of points is quasi-compact.

theorem isQuasiCompactSpaceULift_iff_compactSpace_pointsULift
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    (hF : IsAlgebraicSpaceULift.{w} B S hS F) :
    IsQuasiCompactSpaceULift.{w} B S hS F ↔ CompactSpace (pointsULift.{w} B S hS F)

AlgebraicGeometry.Space.isQuasiCompactSpace_iff_compactSpace_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactPointSpace.lean, line 199.

Stacks 03E4. An algebraic space over S is quasi-compact if and only if its space of points is quasi-compact.

theorem isQuasiCompactSpace_iff_compactSpace_points
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    IsQuasiCompactSpace B S hS F ↔ CompactSpace (points B S hS F)

Tag 040T, a lemma

Tag 040T in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_finiteCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductQuasiCompact.lean, line 92. The attribute's comment: “algebraicity”.

Stacks 040T, algebraicity. A coproduct of finitely many algebraic spaces over S is an algebraic space over S.

theorem isAlgebraicSpace_finiteCoproduct {I : Type v} [Finite I]
    (F : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : ∀ i, IsAlgebraicSpace B S hS (F i))
    (G : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, (⟨F i, (hF i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ G)
    (hG : IsColimit (Cofan.mk G ι)) : IsAlgebraicSpace B S hS G.obj

AlgebraicGeometry.Space.isQuasiCompactSpace_finiteCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductQuasiCompact.lean, line 108. The attribute's comment: “quasi-compactness”.

Stacks 040T, quasi-compactness. A coproduct of finitely many quasi-compact algebraic spaces over S is quasi-compact.

theorem isQuasiCompactSpace_finiteCoproduct {I : Type v} [Finite I]
    (F : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : ∀ i, IsAlgebraicSpace B S hS (F i))
    (hqc : ∀ i, IsQuasiCompactSpace B S hS (F i))
    (G : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, (⟨F i, (hF i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ G)
    (hG : IsColimit (Cofan.mk G ι)) : IsQuasiCompactSpace B S hS G.obj

Tag 04NN, a lemma

Tag 04NN in the Stacks Project.

AlgebraicGeometry.Space.hasBasis_nhds_isOpen_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyCompactPoints.lean, line 77. The attribute's comment: “fundamental system of open quasi-compact neighbourhoods”.

The quasi-compact open neighbourhoods of a point of an algebraic space over S are a fundamental system of neighbourhoods of that point.

theorem hasBasis_nhds_isOpen_isCompact (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    (nhds x).HasBasis
      (fun W : Set (points B S hS F) ↦ IsOpen W ∧ IsCompact W ∧ x ∈ W) id

AlgebraicGeometry.Space.locallyCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyCompactPoints.lean, line 89. The attribute's comment: “local quasi-compactness”.

The space of points of an algebraic space over S is locally quasi-compact.

theorem locallyCompactSpace (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) : LocallyCompactSpace (points B S hS F)

Sources

LeanAlgebraicGeometry.Space.IsQuasiCompactSpace · AlgebraicGeometry.Space.isQuasiCompactSpaceULift_iff_compactSpace_pointsULift · AlgebraicGeometry.Space.isQuasiCompactSpace_iff_compactSpace_points · AlgebraicGeometry.Space.isAlgebraicSpace_finiteCoproduct · AlgebraicGeometry.Space.isQuasiCompactSpace_finiteCoproduct · AlgebraicGeometry.Space.hasBasis_nhds_isOpen_isCompact · AlgebraicGeometry.Space.locallyCompactSpace

Section66.6 Special coverings #

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

Tag 03FX, a lemma

Tag 03FX in the Stacks Project.

AlgebraicGeometry.IsAlgebraicSpace.exists_etale_surjective_coproduct_affine_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineAtlas.lean, line 216.

An algebraic space over S has a surjective étale chart whose source is a disjoint union of affine schemes, each mapping into an affine open of S.

theorem IsAlgebraicSpace.exists_etale_surjective_coproduct_affine_cover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    ∃ (U : BigFppfOver B S hS)
      (f : yoneda.obj U ⟶ F)
      (I : Type u) (Y : I → Scheme.{u})
      (e : (∐ Y) ≅ (BigFppfOver.toScheme B S hS).obj U),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f ∧
      (∀ i, IsAffine (Y i)) ∧
      (∀ i, ∃ (V : S.Opens), IsAffineOpen V ∧
        ∀ y : Y i,
          (Sigma.ι Y i ≫ e.hom ≫ B.inclusion.map U.hom) y ∈ V)

AlgebraicGeometry.IsAlgebraicSpace.exists_etale_surjective_isSeparated_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineAtlas.lean, line 242. The attribute's comment: “the cover may be taken separated”.

An algebraic space over S has a surjective étale chart whose underlying scheme is separated.

theorem IsAlgebraicSpace.exists_etale_surjective_isSeparated_cover
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    ∃ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F),
      Scheme.IsSeparated ((BigFppfOver.toScheme B S hS).obj U) ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f

AlgebraicGeometry.Space.exists_etale_surjective_coproduct_affine_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/SpecialCoverings.lean, line 85.

An algebraic space has a surjective étale atlas which is a disjoint union of affine schemes, each mapping into an affine open of the base.

theorem exists_etale_surjective_coproduct_affine_cover
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    ∃ (U : BigFppfOver B S hS)
      (f : yoneda.obj U ⟶ F)
      (I : Type u) (Y : I → Scheme.{u})
      (e : (∐ Y) ≅ (BigFppfOver.toScheme B S hS).obj U),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f ∧
      (∀ i, IsAffine (Y i)) ∧
      (∀ i, ∃ (V : S.Opens), IsAffineOpen V ∧
        ∀ y : Y i,
          (Sigma.ι Y i ≫ e.hom ≫ B.inclusion.map U.hom) y ∈ V)

Tag 03FY, a lemma

Tag 03FY in the Stacks Project.

AlgebraicGeometry.Space.exists_zariski_cover_affine_etale_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoverAffineAtlas.lean, line 45.

Stacks 03FY. An algebraic space over S has a Zariski covering by open subspaces, each of which admits a surjective étale atlas from an affine scheme and maps into an affine open of S.

theorem exists_zariski_cover_affine_etale_atlas
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    ∃ (I : Type u) (X : I → Subfunctor F),
      IsZariskiCover B S hS I X ∧
      ∀ i, ∃ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ (X i).toFunctor) (V : S.Opens),
        IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
        (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f ∧
        (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f ∧
        IsAffineOpen V ∧
        ∀ (T : BigFppfOver B S hS) (_ : (X i).toFunctor.obj (Opposite.op T))
          (t : (BigFppfOver.toScheme B S hS).obj T), (B.inclusion.map T.hom) t ∈ V

AlgebraicGeometry.Space.exists_zariskiCovering_affine_etale_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoveringAffineCharts.lean, line 219. The attribute's comment: “covering on point sets”.

Stacks 03FY. An algebraic space over S is the union of a family of open subspaces each of which carries a surjective étale chart from a single affine scheme, and those affine schemes may be taken to map into affine opens of S. Surjectivity of the chart is recorded both on point sets (Tag 03ME) and in the relatively representable form, the two being equivalent by Tag 03H5.

The family is indexed by the summands of the affine chart of Stacks 03FX in the form AlgebraicGeometry.IsAlgebraicSpace.exists_affine_coproduct_atlas, which keeps the summands as affine objects W i of the site. The member of the covering attached to i is the open subspace swept out by W i, and the chart of that member is the factorisation of yoneda.map (j i) ≫ f through it, by AlgebraicGeometry.Space.isOpenSubspace_etale_surjective_lift_openSubspaceOfPoints_range. The members cover because the chart f is surjective on points (Tag 03H5) and every point of its source lies in one summand.

The attribute carries a part string rather than being bare because the covering clause is the point-set one; the bare attribute sits on AlgebraicGeometry.Space.exists_zariski_cover_affine_etale_atlas, which states the same thing with the covering clause in the repository's AlgebraicGeometry.Space.IsZariskiCover vocabulary of Tag 02YY. The two are interchangeable by the Zariski-coverings part of Tag 03BZ.

theorem exists_zariskiCovering_affine_etale_chart
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) :
    ∃ (I : Type u) (X : I → Subfunctor F) (W : I → BigFppfOver B S hS)
      (b : ∀ i, yoneda.obj (W i) ⟶ (X i).toFunctor),
      (∀ i, IsOpenSubspace B S hS (X i)) ∧
      (⋃ i, Set.range (pointsMap B S hS (X i).toFunctor (X i).ι)) = Set.univ ∧
      (∀ i, IsAffine ((BigFppfOver.toScheme B S hS).obj (W i))) ∧
      (∀ i, (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf (b i)) ∧
      (∀ i, Function.Surjective (pointsMap B S hS (yoneda.obj (W i)) (b i))) ∧
      (∀ i, (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf (b i)) ∧
      (∀ i, ∃ V : S.Opens, IsAffineOpen V ∧
        (∀ y : (BigFppfOver.toScheme B S hS).obj (W i),
          (B.inclusion.map (W i).hom) y ∈ V) ∧
        ∀ (T : BigFppfOver B S hS) (_x : (X i).toFunctor.obj (Opposite.op T))
          (t : (BigFppfOver.toScheme B S hS).obj T),
          (B.inclusion.map T.hom) t ∈ V)

Tag 03H6, a lemma

Tag 03H6 in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_chart_of_isQuasiCompactSpaceULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedQuasiCompactPoints.lean, line 229. The attribute's comment: “the affine chart of a quasi-compact algebraic space, in a value universe independent of the universe of the schemes”.

Stacks 03H6, the forward implication, for a presheaf with values in a universe max w u independent of the universe u of the schemes: a quasi-compact algebraic space over S admits a surjective étale chart whose source is an object of the site with affine underlying scheme, not merely a quasi-compact one.

The presheaf is isomorphic to the universe lift of a presheaf of Type u, which is a quasi-compact algebraic space; Tag 03H6 supplies an affine surjective étale chart of it, and the universe lift of that chart composed with the isomorphism is the required one.

theorem exists_affine_chart_of_isQuasiCompactSpaceULift
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    (hF : IsAlgebraicSpaceULift.{w} B S hS F) (h : IsQuasiCompactSpaceULift.{w} B S hS F) :
    ∃ (U : BigFppfOver B S hS) (a : (uliftYoneda.{w}).obj U ⟶ F),
      IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).relative (uliftYoneda.{w}) a ∧
      IsEtaleULift.{w} B S hS a

AlgebraicGeometry.Space.isQuasiCompactSpace_iff_exists_affine_etale_surjective_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/SpecialCoverings.lean, line 179.

A quasi-compact algebraic space has an affine, étale, surjective cover, and any algebraic space with such a cover is quasi-compact.

theorem isQuasiCompactSpace_iff_exists_affine_etale_surjective_cover
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hF : IsAlgebraicSpace B S hS F) :
    IsQuasiCompactSpace B S hS F ↔
      ∃ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F),
        IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧
          (MorphismProperty.inverseImage
            (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf f ∧
          IsEtale B S hS f

Tag 03FZ, a lemma

Tag 03FZ in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_isEtale_of_scheme_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartSeparated.lean, line 99. The attribute's comment: “the étale morphism is separated”.

Stacks 03FZ, first assertion. An étale morphism to an algebraic space from an object of the site whose underlying scheme is separated is a separated morphism of algebraic spaces.

theorem isSeparated_of_isEtale_of_scheme_isSeparated
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hX : IsAlgebraicSpace B S hS X)
    (U : BigFppfOver B S hS)
    (hU : Scheme.IsSeparated ((BigFppfOver.toScheme B S hS).obj U))
    (f : yoneda.obj U ⟶ X) (_hf : IsEtale B S hS f) :
    IsSeparated B S hS f

AlgebraicGeometry.Space.isSeparated_scheme_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartSeparated.lean, line 113. The attribute's comment: “the self-fibre product is a separated scheme”.

Stacks 03FZ, second assertion. The object of the site representing the self-fibre product of an étale chart with separated underlying scheme has separated underlying scheme. Its second projection is a base change of the chart, hence a separated morphism, and its target is a separated scheme.

theorem isSeparated_scheme_pullback
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (U : BigFppfOver B S hS)
    (hU : Scheme.IsSeparated ((BigFppfOver.toScheme B S hS).obj U))
    (f : yoneda.obj U ⟶ X) (_hf : IsEtale B S hS f) :
    Scheme.IsSeparated ((BigFppfOver.toScheme B S hS).obj
      ((hX.diagonal_representable.of_diag f).pullback f))

Tag 07S4, a lemma

Tag 07S4 in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparated_of_etaleAtlas_quasiCompact_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiSeparatedAbsolute.lean, line 99.

An algebraic space over S which admits a surjective étale morphism q from an object of the site whose underlying scheme is quasi-separated, and one of whose two kernel-pair projections pullback.fst q q, pullback.snd q q is quasi-compact, is quasi-separated over the terminal scheme.

theorem isQuasiSeparated_of_etaleAtlas_quasiCompact_projection
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (hAtlas : ∃ (U : BigFppfOver B S hS)
        (q : yoneda.obj U ⟶ X),
      QuasiSeparatedSpace ((BigFppfOver.toScheme B S hS).obj U) ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) q ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) q ∧
      ((MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@QuasiCompact.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) (pullback.fst q q) ∨
       (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@QuasiCompact.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) (pullback.snd q q))) :
    IsAbsolutelyQuasiSeparated B S hS hZ X

Tag 03W7, a lemma

Tag 03W7 in the Stacks Project.

AlgebraicGeometry.Space.isZariskiLocallyQuasiSeparatedOver_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedTfae.lean, line 497.

Stacks 03W7. For an algebraic space over a scheme S, Zariski local quasi-separatedness over S, absolute Zariski local quasi-separatedness, and the existence of a Zariski covering by open subspaces carrying quasi-compact surjective étale atlases by affine schemes — with or without the requirement that those affine schemes map into affine opens of S — are equivalent.

theorem isZariskiLocallyQuasiSeparatedOver_tfae
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) :
    List.TFAE
      [IsZariskiLocallyQuasiSeparatedOver B S hS X,
        IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ X,
        HasAffineQuasiCompactEtaleCover B S hS X,
        HasAffineQuasiCompactEtaleCoverIntoAffineBase B S hS X]

Tag 03IJ, a lemma

Tag 03IJ in the Stacks Project.

AlgebraicGeometry.Space.finite_fiber_pointsMap_of_etale_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartFinitePoints.lean, line 193. The attribute's comment: “fibres of the presenting scheme”.

Stacks 03IJ, the fibres of the presenting scheme. An étale morphism φ : h_U ⟶ X of presheaves on the big fppf site of S out of a representable presheaf whose self-fibre-product projections are quasi-compact in the sense of Stacks 03HE has finite fibres on points.

Any point of a fibre of |U| → |X| and a fixed point of that fibre are the two projections of a point of the relation, so the fibre is the image of a fibre of the first projection of the relation.

theorem finite_fiber_pointsMap_of_etale_presentation
    (hφ : IsEtale B S hS φ) (hs : IsQuasiCompact B S hS (pullback.fst φ φ))
    (_ht : IsQuasiCompact B S hS (pullback.snd φ φ)) (x : points B S hS X) :
    (pointsMap B S hS (yoneda.obj U) φ ⁻¹' {x}).Finite

AlgebraicGeometry.Space.finite_fiber_selfPullback_pointsMap_of_etale_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartFinitePoints.lean, line 217. The attribute's comment: “fibres of the relation scheme”.

Stacks 03IJ, the fibres of the relation scheme. Under the same hypotheses the relation h_U ×_X h_U has finite fibres on points over X.

A fibre of |R| → |X| is the union, over the finitely many points of the corresponding fibre of |U| → |X|, of the fibres of |R| → |U|.

theorem finite_fiber_selfPullback_pointsMap_of_etale_presentation
    (hφ : IsEtale B S hS φ) (hs : IsQuasiCompact B S hS (pullback.fst φ φ))
    (ht : IsQuasiCompact B S hS (pullback.snd φ φ)) (x : points B S hS X) :
    (pointsMap B S hS (pullback φ φ) (pullback.fst φ φ ≫ φ) ⁻¹' {x}).Finite

Sources

LeanAlgebraicGeometry.IsAlgebraicSpace.exists_etale_surjective_coproduct_affine_cover · AlgebraicGeometry.IsAlgebraicSpace.exists_etale_surjective_isSeparated_cover · AlgebraicGeometry.Space.exists_etale_surjective_coproduct_affine_cover · AlgebraicGeometry.Space.exists_zariski_cover_affine_etale_atlas · AlgebraicGeometry.Space.exists_zariskiCovering_affine_etale_chart · AlgebraicGeometry.Space.exists_affine_chart_of_isQuasiCompactSpaceULift · AlgebraicGeometry.Space.isQuasiCompactSpace_iff_exists_affine_etale_surjective_cover · AlgebraicGeometry.Space.isSeparated_of_isEtale_of_scheme_isSeparated

Section66.7 Properties of Spaces defined by properties of schemes #

Section 66.7 of the Stacks Project, Tag 03E5. 6 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03E8, a lemma

Tag 03E8 in the Stacks Project.

AlgebraicGeometry.Space.exists_atlas_iff_forall_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/EtaleLocalProperty.lean, line 150. The attribute's comment: “equivalence of atlas conditions”.

Stacks 03E8. An étale-local property holds on some surjective étale atlas exactly when it holds on every étale scheme over the algebraic space.

theorem exists_atlas_iff_forall_etale (hF : IsAlgebraicSpace B S hS F) :
    HasEtaleLocalProperty B S hS F P ↔
    (∀ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ F),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) g →
      P ((BigFppfOver.toScheme B S hS).obj V))

AlgebraicGeometry.Space.exists_atlas_iff_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/EtaleLocalProperty.lean, line 196. The attribute's comment: “representable case”.

Stacks 03E8. For a represented algebraic space, the atlas condition is equivalent to the property of its representing scheme.

theorem exists_atlas_iff_of_representable
    (X : BigFppfOver B S hS) (e : F ≅ yoneda.obj X) :
    HasEtaleLocalProperty B S hS F P ↔ P ((BigFppfOver.toScheme B S hS).obj X)

Tag 03E6, a definition

Tag 03E6 in the Stacks Project.

AlgebraicGeometry.Space.HasEtaleLocalProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/EtaleLocalProperty.lean, line 137.

Stacks 03E6. An algebraic space has an étale-local property of schemes if it has a surjective étale atlas by a scheme with that property.

abbrev HasEtaleLocalProperty : Prop

Tag 03E7, a remark

Tag 03E7 in the Stacks Project.

AlgebraicGeometry.jacobsonSpace_isLocal_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 110. The attribute's comment: “item (2): Jacobson, by Stacks 0368”.

Stacks Project, Tag 03E7, item (2). Being a Jacobson scheme is local for étale coverings of schemes: a scheme is Jacobson if and only if the members of an étale covering family are.

This is Stacks 0368, which gives the fppf case, read through the inclusion of the étale precoverage in the fppf one.

instance jacobsonSpace_isLocal_etale :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => JacobsonSpace X) Scheme.etalePrecoverage

AlgebraicGeometry.isLocallyNoetherian_and_hasPropertySk_isLocal_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 122. The attribute's comment: “item (3): locally Noetherian and (S_k), by Stacks 036A”.

Stacks Project, Tag 03E7, item (3). Being locally Noetherian and satisfying Serre's condition (S_k) is local for étale coverings of schemes.

This is Stacks 036A, which gives the syntomic case, read through the inclusion of the étale precoverage in the syntomic one.

instance isLocallyNoetherian_and_hasPropertySk_isLocal_etale (k : ℕ) :
    ObjectProperty.IsLocal
      (fun X : Scheme.{u} => ∃ h : IsLocallyNoetherian X, @HasPropertySk X h k)
      Scheme.etalePrecoverage

AlgebraicGeometry.isCohenMacaulay_isLocal_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 136. The attribute's comment: “item (4): Cohen-Macaulay, by Stacks 036B”.

Stacks Project, Tag 03E7, item (4). Being a Cohen-Macaulay scheme is local for étale coverings of schemes.

This is Stacks 036B, which gives the syntomic case, read through the inclusion of the étale precoverage in the syntomic one.

instance isCohenMacaulay_isLocal_etale :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsCohenMacaulay X) Scheme.etalePrecoverage

AlgebraicGeometry.isGorenstein_isLocal_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 169. The attribute's comment: “item (5): Gorenstein, the étale case of Stacks 0C01”.

Stacks Project, Tag 03E7, item (5). Being a Gorenstein scheme is local for étale coverings of schemes: a scheme is Gorenstein if and only if the members of an étale covering family are.

The source cites Stacks 0C01, which states the syntomic case; only the étale case is proved here. Ascent is AlgebraicGeometry.isGorenstein_of_etale. For descent, local Noetherianity of the base is item (1), and the Gorenstein condition on the stalk at a point of the base is transported from a point of a member of the family above it.

instance isGorenstein_isLocal_etale :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsGorenstein X) Scheme.etalePrecoverage

AlgebraicGeometry.isLocallyNoetherian_and_isRegularInCodimension_isLocal_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 206. The attribute's comment: “item (8): locally Noetherian and (R_k), by Stacks 036C”. References: EGA IV (17.5.8), “(iii), special case”.

Stacks Project, Tag 03E7, item (8). Being locally Noetherian and regular in codimension k is local for étale coverings of schemes.

This is Stacks 036C, which gives the smooth case, read through the inclusion of the étale precoverage in the smooth one.

instance isLocallyNoetherian_and_isRegularInCodimension_isLocal_etale (k : ℕ) :
    ObjectProperty.IsLocal
      (fun X : Scheme.{u} => IsLocallyNoetherian X ∧ IsRegularInCodimension X k)
      Scheme.etalePrecoverage

Declarations registered for the tag:

isLocallyNoetherian_isLocal_etale registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 99 (StacksFrontier): “item (1): locally Noetherian, by Stacks 034C”.
isReduced_isLocal_etale registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 191 (StacksFrontier): “item (6): reduced, by Stacks 034E”.
isLocal_isNormal_etalePrecoverage registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 195 (StacksFrontier): “item (7): normal, by Stacks 034F”.
isRegular_isLocal_etale registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 214 (StacksFrontier): “item (9): regular, by Stacks 036D”.
isNagataScheme_isLocal_etale registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/EtaleLocalList.lean, line 218 (StacksFrontier): “item (10): Nagata, by Stacks 036E”.

Tag 04N2, a lemma

Tag 04N2 in the Stacks Project.

AlgebraicGeometry.Space.forall_etale_chart_iff_exists_etale_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GermPropertyAtPoint.lean, line 208. The attribute's comment: “equivalence of chart conditions”.

Stacks 04N2, conditions (1) and (2). An étale-local property of germs of schemes holds at every étale scheme chart over a point of an algebraic space exactly when it holds at some such chart.

theorem forall_etale_chart_iff_exists_etale_chart (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)
    (P : GermOfScheme.{u} → Prop) (hP : GermOfScheme.IsEtaleLocal P) :
    (∀ (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 →
        P ⟨(BigFppfOver.toScheme B S hS).obj U, schemePoint B S hS U p⟩) ↔
    (∃ (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 ∧
        P ⟨(BigFppfOver.toScheme B S hS).obj U, schemePoint B S hS U p⟩)

AlgebraicGeometry.Space.forall_etale_chart_iff_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GermPropertyAtPoint.lean, line 247. The attribute's comment: “representable case”.

Stacks 04N2, the representable case. For a represented algebraic space the every-chart condition is the property of the germ of its representing scheme at the corresponding scheme point.

theorem forall_etale_chart_iff_of_representable (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (X : BigFppfOver B S hS)
    (e : yoneda.obj X ≅ F) (p : FieldValuedPoint B S hS (yoneda.obj X))
    (P : GermOfScheme.{u} → Prop) (hP : GermOfScheme.IsEtaleLocal P) :
    (∀ (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 →
      ∀ q : FieldValuedPoint B S hS (yoneda.obj U),
        pointsMap B S hS (yoneda.obj U) a (q.class B S hS (yoneda.obj U)) =
          pointsMap B S hS (yoneda.obj X) e.hom (p.class B S hS (yoneda.obj X)) →
        P ⟨(BigFppfOver.toScheme B S hS).obj U, schemePoint B S hS U q⟩) ↔
      P ⟨(BigFppfOver.toScheme B S hS).obj X, schemePoint B S hS X p⟩

AlgebraicGeometry.Space.exists_etale_chart_iff_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GermPropertyAtPoint.lean, line 271. The attribute's comment: “representable case, existential condition”.

Stacks 04N2, the representable case. For a represented algebraic space the one-chart condition is the property of the germ of its representing scheme at the corresponding scheme point.

theorem exists_etale_chart_iff_of_representable (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (X : BigFppfOver B S hS)
    (e : yoneda.obj X ≅ F) (p : FieldValuedPoint B S hS (yoneda.obj X))
    (P : GermOfScheme.{u} → Prop) (hP : GermOfScheme.IsEtaleLocal P) :
    (∃ (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 ∧
      ∃ q : FieldValuedPoint B S hS (yoneda.obj U),
        pointsMap B S hS (yoneda.obj U) a (q.class B S hS (yoneda.obj U)) =
          pointsMap B S hS (yoneda.obj X) e.hom (p.class B S hS (yoneda.obj X)) ∧
        P ⟨(BigFppfOver.toScheme B S hS).obj U, schemePoint B S hS U q⟩) ↔
      P ⟨(BigFppfOver.toScheme B S hS).obj X, schemePoint B S hS X p⟩

Tag 04RC, a definition

Tag 04RC in the Stacks Project.

AlgebraicGeometry.Space.HasPropertyAtPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GermPropertyAtPoint.lean, line 79.

Stacks 04RC. A property P of germs of schemes holds at a point x of an algebraic space F when it holds at the germ of some étale scheme chart yoneda.obj U ⟶ F at some field-valued point of U lying over x. For an étale-local property the choice of chart is immaterial, by AlgebraicGeometry.Space.forall_etale_chart_iff_exists_etale_chart; stating this one-chart condition needs neither that hypothesis nor that F is an algebraic space.

abbrev HasPropertyAtPoint (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (x : points B S hS F)
    (P : GermOfScheme.{u} → Prop) : Prop

Tag 0BBL, a remark

Tag 0BBL in the Stacks Project.

AlgebraicGeometry.GermOfScheme.isEtaleLocal_stalk_property, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/LocalRingProperty.lean, line 50. The attribute's comment: “germ_criterion”.

Stacks 0BBL, the germ criterion. A property of local rings which is invariant under isomorphisms and unchanged on passing to a prime above it along an étale ring map induces an étale-local property of germs of schemes, by evaluation on the local ring at the marked point.

theorem GermOfScheme.isEtaleLocal_stalk_property (P : (R : Type u) → [CommRing R] → Prop)
    (hP : ∀ {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [Algebra.Etale A B]
      (p : Ideal A) [p.IsPrime] (q : Ideal B) [q.IsPrime],
      q.comap (algebraMap A B) = p →
        (P (Localization.AtPrime p) ↔ P (Localization.AtPrime q)))
    (hP_iso : ∀ {R S : Type u} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S],
      (R ≃+* S) → (P R ↔ P S)) :
    GermOfScheme.IsEtaleLocal (fun g => P (g.scheme.presheaf.stalk g.point))

AlgebraicGeometry.Space.HasLocalRingPropertyAtPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedLocalRings.lean, line 72. The attribute's comment: “local_ring_of_an_algebraic_space_has_p”.

Stacks 0BBL, the local ring of an algebraic space. A property P of local rings which is invariant under étale localization holds for the local ring of an algebraic space F at a point x when it holds for the stalk of some étale scheme chart at some point above x. By Stacks 04N2 the chart is immaterial, and the invariance hypothesis _hP is what makes that so; it is carried as an argument of the predicate rather than assumed of P globally.

abbrev HasLocalRingPropertyAtPoint (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hF : IsAlgebraicSpace B S hS F) (x : points B S hS F)
    (P : (R : Type u) → [CommRing R] → Prop)
    (_hP : ∀ {A C : Type u} [CommRing A] [CommRing C] [Algebra A C] [Algebra.Etale A C]
      (p : Ideal A) [p.IsPrime] (q : Ideal C) [q.IsPrime],
      q.comap (algebraMap A C) = p →
        (P (Localization.AtPrime p) ↔ P (Localization.AtPrime q))) : Prop

isNoetherianRing_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 150. The attribute's comment: “Noetherian”.

Stacks 0BBL, Noetherian. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is Noetherian if and only if the local ring of B at q is Noetherian.

theorem isNoetherianRing_localizationAtPrime_iff_of_etale
    (hq : q.comap (algebraMap A B) = p) :
    IsNoetherianRing (Localization.AtPrime p) ↔ IsNoetherianRing (Localization.AtPrime q)

ringKrullDim_eq_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 167. The attribute's comment: “dimension d”.

Stacks 0BBL, dimension d. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p has dimension d if and only if the local ring of B at q has dimension d.

theorem ringKrullDim_eq_localizationAtPrime_iff_of_etale (d : WithBot ℕ∞)
    (hq : q.comap (algebraMap A B) = p) :
    ringKrullDim (Localization.AtPrime p) = d ↔ ringKrullDim (Localization.AtPrime q) = d

isRegularLocalRing_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 176. The attribute's comment: “regular”.

Stacks 0BBL, regular. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is regular if and only if the local ring of B at q is regular.

theorem isRegularLocalRing_localizationAtPrime_iff_of_etale
    (hq : q.comap (algebraMap A B) = p) :
    IsRegularLocalRing (Localization.AtPrime p) ↔
      IsRegularLocalRing (Localization.AtPrime q)

isDiscreteValuationRing_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 188. The attribute's comment: “discrete valuation ring”.

Stacks 0BBL, discrete valuation ring. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is a discrete valuation ring if and only if the local ring of B at q is one. This is regularity together with dimension one, through item (3) of the characterisation of Tag 00PD.

theorem isDiscreteValuationRing_localizationAtPrime_iff_of_etale
    (hq : q.comap (algebraMap A B) = p) :
    (∃ _ : IsDomain (Localization.AtPrime p),
        IsDiscreteValuationRing (Localization.AtPrime p)) ↔
      (∃ _ : IsDomain (Localization.AtPrime q),
        IsDiscreteValuationRing (Localization.AtPrime q))

isNormalDomain_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 203. The attribute's comment: “normal”.

Stacks 0BBL, normal. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is a normal domain if and only if the local ring of B at q is one. Neither ring is assumed Noetherian.

theorem isNormalDomain_localizationAtPrime_iff_of_etale
    (hq : q.comap (algebraMap A B) = p) :
    IsNormalDomain (Localization.AtPrime p) ↔ IsNormalDomain (Localization.AtPrime q)

isNoetherianRing_and_ringDepth_eq_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 250. The attribute's comment: “Noetherian and depth k”.

Stacks 0BBL, Noetherian and depth k. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is Noetherian of depth k if and only if the local ring of B at q is.

theorem isNoetherianRing_and_ringDepth_eq_localizationAtPrime_iff_of_etale (k : ℕ∞)
    (hq : q.comap (algebraMap A B) = p) :
    (IsNoetherianRing (Localization.AtPrime p) ∧ ringDepth (Localization.AtPrime p) = k) ↔
      (IsNoetherianRing (Localization.AtPrime q) ∧ ringDepth (Localization.AtPrime q) = k)

isCohenMacaulayLocalRing_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 263. The attribute's comment: “Noetherian and Cohen-Macaulay”.

Stacks 0BBL, Noetherian and Cohen-Macaulay. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is Noetherian and Cohen-Macaulay if and only if the local ring of B at q is.

theorem isCohenMacaulayLocalRing_localizationAtPrime_iff_of_etale
    (hq : q.comap (algebraMap A B) = p) :
    (∃ h : IsNoetherianRing (Localization.AtPrime p),
        @IsCohenMacaulayLocalRing (Localization.AtPrime p) _ h _) ↔
      (∃ h : IsNoetherianRing (Localization.AtPrime q),
        @IsCohenMacaulayLocalRing (Localization.AtPrime q) _ h _)

isGorensteinLocalRing_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/LocalRingPropertyList.lean, line 277. The attribute's comment: “Noetherian and Gorenstein”.

Stacks 0BBL, Noetherian and Gorenstein. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is Noetherian and Gorenstein if and only if the local ring of B at q is.

theorem isGorensteinLocalRing_localizationAtPrime_iff_of_etale
    (hq : q.comap (algebraMap A B) = p) :
    (∃ h : IsNoetherianRing (Localization.AtPrime p),
        @Dualizing.IsGorensteinLocalRing (Localization.AtPrime p) _ h _) ↔
      (∃ h : IsNoetherianRing (Localization.AtPrime q),
        @Dualizing.IsGorensteinLocalRing (Localization.AtPrime q) _ h _)

isReduced_localizationAtPrime_iff_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Etale/ReducedLocalization.lean, line 87. The attribute's comment: “reduced”.

Stacks 0BBL, reducedness. For prime ideals p and q corresponding under an étale map A → B, the local ring of A at p is reduced if and only if the local ring of B at q is reduced.

theorem isReduced_localizationAtPrime_iff_of_etale {A : Type u} {B : Type v} [CommRing A]
    [CommRing B] [Algebra A B] [Algebra.Etale A B] (p : Ideal A) [p.IsPrime] (q : Ideal B)
    [q.IsPrime] (hq : q.comap (algebraMap A B) = p) :
    IsReduced (Localization.AtPrime p) ↔ IsReduced (Localization.AtPrime q)

Declarations registered for the tag:

RingHom.Etale.ringKrullDim_localization_atPrime_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/PointsAndCoverings/EtaleLocalProperty.lean, line 216 (StacksFrontier): “dimension”.

Sources

LeanAlgebraicGeometry.Space.exists_atlas_iff_forall_etale · AlgebraicGeometry.Space.exists_atlas_iff_of_representable · AlgebraicGeometry.Space.HasEtaleLocalProperty · AlgebraicGeometry.jacobsonSpace_isLocal_etale · AlgebraicGeometry.isLocallyNoetherian_and_hasPropertySk_isLocal_etale · AlgebraicGeometry.isCohenMacaulay_isLocal_etale · AlgebraicGeometry.isGorenstein_isLocal_etale · AlgebraicGeometry.isLocallyNoetherian_and_isRegularInCodimension_isLocal_etale

Section66.8 Constructible sets #

Section 66.8 of the Stacks Project, Tag 0ECS. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0ECT, a lemma

Tag 0ECT in the Stacks Project.

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

Stacks 0ECT, conditions (1) and (2). Étale-local constructibility can be tested on affine étale charts, where it becomes constructibility.

theorem forall_etale_iff_forall_affine_etale :
    IsEtaleLocallyConstructible B S hS X E ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (f : yoneda.obj U ⟶ X), IsEtale B S hS f →
          IsConstructible (pointsMap B S hS (yoneda.obj U) f ⁻¹' E)

AlgebraicGeometry.Space.forall_etale_iff_exists_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConstructiblePoints.lean, line 139. The attribute's comment: “conditions (1) and (3)”.

Stacks 0ECT, conditions (1) and (3). Étale-local constructibility holds as soon as it holds on a single surjective étale chart.

theorem forall_etale_iff_exists_surjective_etale (hX : IsAlgebraicSpace B S hS X) :
    IsEtaleLocallyConstructible B S hS X E ↔
      ∃ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ X),
        IsSurjective B S hS f ∧ IsEtale B S hS f ∧
          IsLocallyConstructible (pointsMap B S hS (yoneda.obj U) f ⁻¹' E)

Tag 0ECU, a definition

Tag 0ECU in the Stacks Project.

AlgebraicGeometry.Space.IsEtaleLocallyConstructible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConstructiblePoints.lean, line 96.

Stacks 0ECU. A subset of the points of a presheaf on the big fppf site of S is étale locally constructible when its inverse image on every étale chart from a scheme is a locally constructible subset of that chart.

abbrev IsEtaleLocallyConstructible : Prop

Sources

LeanAlgebraicGeometry.Space.forall_etale_iff_forall_affine_etale · AlgebraicGeometry.Space.forall_etale_iff_exists_surjective_etale · AlgebraicGeometry.Space.IsEtaleLocallyConstructible

Section66.9 Dimension at a point #

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

Tag 04N5, a definition

Tag 04N5 in the Stacks Project.

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

Stacks 04N5. The dimension of an algebraic space at one of its points: the infimum of the local dimensions of the étale scheme charts at a point above it. By AlgebraicGeometry.Space.dimensionAtPoint_eq_of_etale_chart every one of those local dimensions equals this infimum.

noncomputable def dimensionAtPoint (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) : WithBot ℕ∞

AlgebraicGeometry.Space.exists_etale_chart_at_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Dimension.lean, line 88. The attribute's comment: “existence of a chart at the point”.

Stacks 04N5. Every point of an algebraic space has an étale scheme chart above it.

theorem exists_etale_chart_at_point (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) :
    ∃ (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

AlgebraicGeometry.Space.dimensionAtPoint_eq_of_etale_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Dimension.lean, line 106. The attribute's comment: “independence of the étale chart”.

Stacks 04N5. The dimension of an algebraic space at a point equals the local dimension of every étale scheme chart at a point above it; this is the property the source uses to define the dimension at a point.

theorem dimensionAtPoint_eq_of_etale_chart (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) (U : BigFppfOver B S hS)
    (a : yoneda.obj U ⟶ F)
    (ha : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) a)
    (p : FieldValuedPoint B S hS (yoneda.obj U))
    (hp : pointsMap B S hS (yoneda.obj U) a (p.class B S hS (yoneda.obj U)) = x) :
    dimensionAtPoint B S hS F hF x =
      topologicalKrullDimAt ((BigFppfOver.toScheme B S hS).obj U)
        (schemePoint B S hS U p)

Tag 04N6, a definition

Tag 04N6 in the Stacks Project.

AlgebraicGeometry.Space.dimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Dimension.lean, line 142.

Stacks 04N6. The dimension of an algebraic space: the supremum of its dimensions at its points.

noncomputable abbrev dimension (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F) : WithBot ℕ∞

Sources

LeanAlgebraicGeometry.Space.dimensionAtPoint · AlgebraicGeometry.Space.exists_etale_chart_at_point · AlgebraicGeometry.Space.dimensionAtPoint_eq_of_etale_chart · AlgebraicGeometry.Space.dimension

Section66.10 Dimension of local rings #

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

Tag 0BAM, a lemma

Tag 0BAM in the Stacks Project.

AlgebraicGeometry.Space.hasChartLocalRingDimension_iff_allChartsLocalRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocalRingDimension.lean, line 165. The attribute's comment: “equivalence of étale-chart conditions”.

Stacks 0BAM. The Krull dimension of the local ring measured on an étale scheme chart of an algebraic space is independent of the chart and of the point above x: one chart realizes the value d exactly when every chart does.

theorem hasChartLocalRingDimension_iff_allChartsLocalRingDimension
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) (d : ℕ∞) :
    HasChartLocalRingDimension B S hS x d ↔ AllChartsLocalRingDimension B S hS x d

AlgebraicGeometry.Space.hasChartLocalRingDimension_iff_ringKrullDim_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocalRingDimension.lean, line 183. The attribute's comment: “representable case”.

Stacks 0BAM, the representable case. For a represented algebraic space the chart condition at a point is the Krull dimension of the local ring of the representing scheme at the corresponding scheme point.

theorem hasChartLocalRingDimension_iff_ringKrullDim_stalk (U : BigFppfOver B S hS)
    (u : (BigFppfOver.toScheme B S hS).obj U) (x : points B S hS (yoneda.obj U))
    (hx : ChartPoint B S hS U (𝟙 (yoneda.obj U)) u x) (d : ℕ∞) :
    HasChartLocalRingDimension B S hS x d ↔
      ringKrullDim (((BigFppfOver.toScheme B S hS).obj U).presheaf.stalk u) =
        (d : WithBot ℕ∞)

Tag 04NA, a definition

Tag 04NA in the Stacks Project.

AlgebraicGeometry.Space.localRingDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocalRingDimension.lean, line 229. The attribute's comment: “dimension”.

Stacks 04NA. The Krull dimension of the local ring of an algebraic space at a point, measured on an étale scheme chart at a point above it.

By AlgebraicGeometry.Space.localRingDimension_eq_iff_hasChartLocalRingDimension exactly one value is realized by such a chart, and it is this infimum.

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

AlgebraicGeometry.Space.localRingDimension_eq_iff_hasChartLocalRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocalRingDimension.lean, line 235. The attribute's comment: “characterization by étale charts”.

Stacks 04NA. The dimension of the local ring of an algebraic space at a point is the value measured on any étale scheme chart at a point above it.

theorem localRingDimension_eq_iff_hasChartLocalRingDimension (hF : IsAlgebraicSpace B S hS F)
    (x : points B S hS F) (d : ℕ∞) :
    localRingDimension B S hS x = d ↔ HasChartLocalRingDimension B S hS x d

Tag 0BAN, a lemma

Tag 0BAN in the Stacks Project.

AlgebraicGeometry.Space.dimension_eq_iSup_localRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionLocalRings.lean, line 55. The attribute's comment: “the dimension of the space is the supremum over its local rings”.

Stacks 0BAN, quantities (1) and (2). The dimension of an algebraic space is the supremum of the Krull dimensions of its local rings.

theorem dimension_eq_iSup_localRingDimension (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    dimension B S hS F hF =
      ⨆ x : points B S hS F, (localRingDimension B S hS x : WithBot ℕ∞)

AlgebraicGeometry.Space.iSup_dimensionAtPoint_eq_iSup_localRingDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DimensionLocalRings.lean, line 97. The attribute's comment: “the supremum over the points of the dimension at the point”.

Stacks 0BAN, quantities (3) and (2). The supremum, over the points x of an algebraic space, of its dimension dim_x(X) at x is the supremum of the Krull dimensions of its local rings. By Definition 04N6 the left-hand side is the dimension of the algebraic space, so together with AlgebraicGeometry.Space.dimension_eq_iSup_localRingDimension this is the equality of all three quantities of the source.

theorem iSup_dimensionAtPoint_eq_iSup_localRingDimension (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, dimensionAtPoint B S hS F hF x) =
      ⨆ x : points B S hS F, (localRingDimension B S hS x : WithBot ℕ∞)

Sources

LeanAlgebraicGeometry.Space.hasChartLocalRingDimension_iff_allChartsLocalRingDimension · AlgebraicGeometry.Space.hasChartLocalRingDimension_iff_ringKrullDim_stalk · AlgebraicGeometry.Space.localRingDimension · AlgebraicGeometry.Space.localRingDimension_eq_iff_hasChartLocalRingDimension · AlgebraicGeometry.Space.dimension_eq_iSup_localRingDimension · AlgebraicGeometry.Space.iSup_dimensionAtPoint_eq_iSup_localRingDimension

Section66.11 Generic points #

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

Tag 0BAQ, a lemma

Tag 0BAQ in the Stacks Project.

AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_exists_etale_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionZeroPoints.lean, line 79. The attribute's comment: “condition (2)”.

Stacks 0BAQ, conditions (1) and (2). A point of an algebraic space has a local ring of dimension zero exactly when some étale scheme chart has, above it, a generic point of an irreducible component.

theorem localRingDimension_eq_zero_iff_exists_etale_genericPoint
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    localRingDimension B S hS x = 0 ↔
      ∃ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ F)
        (u : (BigFppfOver.toScheme B S hS).obj U),
        IsEtale B S hS a ∧ ChartPoint B S hS U a u x ∧
          u ∈ genericPoints ((BigFppfOver.toScheme B S hS).obj U)

AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_all_etale_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionZeroPoints.lean, line 95. The attribute's comment: “condition (3)”.

Stacks 0BAQ, conditions (1) and (3). A point of an algebraic space has a local ring of dimension zero exactly when every point above it in every étale scheme chart is the generic point of an irreducible component.

theorem localRingDimension_eq_zero_iff_all_etale_genericPoints
    (hF : IsAlgebraicSpace B S hS F) (x : points B S hS F) :
    localRingDimension B S hS x = 0 ↔
      ∀ (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ F)
        (u : (BigFppfOver.toScheme B S hS).obj U),
        IsEtale B S hS a → ChartPoint B S hS U a u x →
          u ∈ genericPoints ((BigFppfOver.toScheme B S hS).obj U)

AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_genericPoint_of_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionZeroPoints.lean, line 139. The attribute's comment: “representable case”. References: EGA I (2.4.3).

Stacks 0BAQ, the representable case. For a representable algebraic space, a point has a local ring of dimension zero exactly when it is the generic point of an irreducible component of the space of points.

theorem localRingDimension_eq_zero_iff_genericPoint_of_isRepresentable
    (hF : IsAlgebraicSpace B S hS F) (hrep : F.IsRepresentable) (x : points B S hS F) :
    localRingDimension B S hS x = 0 ↔ x ∈ genericPoints (points B S hS F)

Tag 0BAR, a lemma

Tag 0BAR in the Stacks Project.

AlgebraicGeometry.Space.codimensionZeroPoints_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionZeroPoints.lean, line 148.

Stacks 0BAR. The points of codimension zero of an algebraic space are dense in its space of points.

theorem codimensionZeroPoints_dense (hF : IsAlgebraicSpace B S hS F) :
    Dense {x : points B S hS F | localRingDimension B S hS x = 0}

Sources

LeanAlgebraicGeometry.Space.localRingDimension_eq_zero_iff_exists_etale_genericPoint · AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_all_etale_genericPoints · AlgebraicGeometry.Space.localRingDimension_eq_zero_iff_genericPoint_of_isRepresentable · AlgebraicGeometry.Space.codimensionZeroPoints_dense

Section66.12 Reduced spaces #

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

Tag 03IP, the section

Tag 03IP in the Stacks Project.

AlgebraicGeometry.Space.exists_isQuasicoherentOnSite_idealZeroLocus_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedIdealSheafOfClosedSet.lean, line 105. The attribute's comment: “a section, not a lemma: a closed set is cut out by a quasi-coherent sheaf of ideals”.

Every closed set of points of an algebraic space is the zero locus of a quasi-coherent sheaf of ideals.

theorem exists_isQuasicoherentOnSite_idealZeroLocus_eq (X : AlgebraicSpaces B S hS)
    (T : Set (points B S hS X.1)) (hT : IsClosed T) :
    ∃ I : (SheafOfModules.unit (structureRingSheaf B S hS X)).Submodule,
      I.toSheafOfModules.IsQuasicoherentOnSite ∧ idealZeroLocus B S hS X I = T

Tag 0ABJ, a lemma

Tag 0ABJ in the Stacks Project.

AlgebraicGeometry.Space.isEmbedding_pointsMap_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionPointEmbedding.lean, line 219. The attribute's comment: “homeomorphism onto the image”.

Stacks 0ABJ, part one. The map on points of an immersion of algebraic spaces over S is a topological embedding: a homeomorphism onto its image.

theorem isEmbedding_pointsMap_of_isImmersion (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X)
    (hi : IsImmersion B S hS i) :
    Topology.IsEmbedding (pointsMap B S hS Z i)

AlgebraicGeometry.Space.isLocallyClosed_range_pointsMap_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionPointEmbedding.lean, line 228. The attribute's comment: “locally closed image”.

Stacks 0ABJ, part two. The image on points of an immersion of algebraic spaces over S is a locally closed subset of the point space of the target.

theorem isLocallyClosed_range_pointsMap_of_isImmersion (hX : IsAlgebraicSpace B S hS X)
    (i : Z ⟶ X) (hi : IsImmersion B S hS i) :
    IsLocallyClosed (Set.range (pointsMap B S hS Z i))

Tag 07TW, a lemma

Tag 07TW in the Stacks Project.

AlgebraicGeometry.Space.invariantLocallyClosedSubschemeEquiv_of_isAlgebraicSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ImmersionEtaleDescent.lean, line 351. The attribute's comment: “canonical bijection”.

For an algebraic space X over S with a surjective étale chart φ : U ⟶ X, the invariant locally closed subschemes of U correspond bijectively to the locally closed subspaces of X, and the bijection is characterised by pullback along φ.

This is AlgebraicGeometry.Space.invariantLocallyClosedSubschemeEquiv with its hypothesis hdesc supplied by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isImmersion.

noncomputable def invariantLocallyClosedSubschemeEquiv_of_isAlgebraicSpace
    (hX : IsAlgebraicSpace B S hS X) :
    {e : InvariantLocallyClosedSubscheme B S hS hs ≃
      LocallyClosedQuotientSubspace B S hS (X := X) //
      ∀ Z, ((e Z).1.preimage φ) = subschemePoints B S hS Z.1}

AlgebraicGeometry.Space.closed_iff_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ImmersionEtaleDescent.lean, line 366. The attribute's comment: “closedness”.

The subspace of X corresponding to an invariant subscheme of the chart is closed exactly when that subscheme is closed in the chart.

This is AlgebraicGeometry.Space.closed_iff with its hypothesis hdesc supplied by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isImmersion.

theorem closed_iff_of_isAlgebraicSpace (hX : IsAlgebraicSpace B S hS X)
    (Z : InvariantLocallyClosedSubscheme B S hS hs) :
    IsClosedSubspace B S hS
        ((invariantLocallyClosedSubschemeEquiv_of_isAlgebraicSpace B S hS hs he hX).1 Z).1 ↔
      _root_.AlgebraicGeometry.IsClosedImmersion Z.1.arrow

AlgebraicGeometry.Space.open_iff_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ImmersionEtaleDescent.lean, line 381. The attribute's comment: “openness”.

The subspace of X corresponding to an invariant subscheme of the chart is open exactly when that subscheme is open in the chart.

This is AlgebraicGeometry.Space.open_iff with its hypothesis hdesc supplied by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isImmersion.

theorem open_iff_of_isAlgebraicSpace (hX : IsAlgebraicSpace B S hS X)
    (Z : InvariantLocallyClosedSubscheme B S hS hs) :
    IsOpenSubspace B S hS
        ((invariantLocallyClosedSubschemeEquiv_of_isAlgebraicSpace B S hS hs he hX).1 Z).1 ↔
      _root_.AlgebraicGeometry.IsOpenImmersion Z.1.arrow

AlgebraicGeometry.Space.isOpenSubspace_invariantSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/OpenImmersionEtaleDescent.lean, line 555. The attribute's comment: “forward direction at an invariant open subscheme, unconditionally”.

The subspace cut out by an invariant open subscheme of a chart is an open subspace, unconditionally. Let F be an algebraic space over S with a surjective étale chart φ : U ⟶ F, and let Z ⊆ U be an open subscheme invariant under the relation R = U ×_F U. Then the subfunctor AlgebraicGeometry.Space.invariantSubspace B S hS φ Z of F which Z cuts out is an algebraic space over S and its inclusion into F is an open immersion.

This is AlgebraicGeometry.Space.isAlgebraicSpace_and_presheaf_invariantSubspace at P = AlgebraicGeometry.IsOpenImmersion, where its descent hypothesis is supplied by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isOpenImmersion. It is the open-subscheme case of the forward direction of Stacks 07TW together with the openness clause, and unlike AlgebraicGeometry.Space.invariantLocallyClosedSubschemeEquiv it carries no hypothesis: the general case is Stacks 03I2 at AlgebraicGeometry.IsImmersion, which still needs the effective fppf descent of immersions, Stacks 02W8.

theorem isOpenSubspace_invariantSubspace
    (hs : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) φ)
    (he : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) φ)
    (hF : IsAlgebraicSpace B S hS F)
    (Z : Subobject ((BigFppfOver.toScheme B S hS).obj U))
    (hZ : _root_.AlgebraicGeometry.IsOpenImmersion Z.arrow)
    (hinv : IsInvariantSubscheme B S hS hs Z) :
    IsOpenSubspace B S hS (invariantSubspace B S hS φ Z)

AlgebraicGeometry.Space.Presentation.invariantLocallyClosedSubschemeEquivOfExtendsRelation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantSubschemeGroupoid.lean, line 190. The attribute's comment: “the canonical bijection, with invariance taken in the groupoid sense”.

Stacks 07TW, the canonical bijection, with invariance of the subschemes of the presenting scheme taken in the groupoid sense of Stacks 03BC part (4) against any groupoid scheme extending the presenting relation.

Effective descent of immersions along the surjective étale morphisms of the site, which is Stacks 02W8 in the form Stacks 03I2 consumes, is AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isImmersion.

noncomputable def Presentation.invariantLocallyClosedSubschemeEquivOfExtendsRelation
    (P : Presentation B S hS X hX) {G : GroupoidScheme S}
    (hG : ExtendsRelation (prod.lift ((Over.post B.inclusion).map P.target)
      ((Over.post B.inclusion).map P.source)) G)
    (hobj : G.objects.left = (BigFppfOver.toScheme B S hS).obj P.U) :
    {e : {Z : Subobject ((BigFppfOver.toScheme B S hS).obj P.U) //
            AlgebraicGeometry.IsImmersion Z.arrow ∧
              IsInvariantMonomorphism G (Z.arrow ≫ eqToHom hobj.symm)} ≃
          LocallyClosedQuotientSubspace B S hS (X := X) //
      ∀ Z, ((e Z).1.preimage P.toSpace) = subschemePoints B S hS Z.1}

AlgebraicGeometry.Space.Presentation.closed_iff_of_extendsRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantSubschemeGroupoid.lean, line 211. The attribute's comment: “closedness, with invariance taken in the groupoid sense”.

Stacks 07TW, closedness, with invariance taken in the groupoid sense: the subspace of the presented algebraic space corresponding to an invariant subscheme of the presenting scheme is closed exactly when that subscheme is closed.

theorem Presentation.closed_iff_of_extendsRelation
    (P : Presentation B S hS X hX) {G : GroupoidScheme S}
    (hG : ExtendsRelation (prod.lift ((Over.post B.inclusion).map P.target)
      ((Over.post B.inclusion).map P.source)) G)
    (hobj : G.objects.left = (BigFppfOver.toScheme B S hS).obj P.U)
    (Z : {Z : Subobject ((BigFppfOver.toScheme B S hS).obj P.U) //
      AlgebraicGeometry.IsImmersion Z.arrow ∧
        IsInvariantMonomorphism G (Z.arrow ≫ eqToHom hobj.symm)}) :
    IsClosedSubspace B S hS
        ((P.invariantLocallyClosedSubschemeEquivOfExtendsRelation B S hS hG hobj).1 Z).1 ↔
      AlgebraicGeometry.IsClosedImmersion Z.1.arrow

AlgebraicGeometry.Space.Presentation.open_iff_of_extendsRelation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantSubschemeGroupoid.lean, line 229. The attribute's comment: “openness, with invariance taken in the groupoid sense”.

Stacks 07TW, openness, with invariance taken in the groupoid sense: the subspace of the presented algebraic space corresponding to an invariant subscheme of the presenting scheme is open exactly when that subscheme is open.

theorem Presentation.open_iff_of_extendsRelation
    (P : Presentation B S hS X hX) {G : GroupoidScheme S}
    (hG : ExtendsRelation (prod.lift ((Over.post B.inclusion).map P.target)
      ((Over.post B.inclusion).map P.source)) G)
    (hobj : G.objects.left = (BigFppfOver.toScheme B S hS).obj P.U)
    (Z : {Z : Subobject ((BigFppfOver.toScheme B S hS).obj P.U) //
      AlgebraicGeometry.IsImmersion Z.arrow ∧
        IsInvariantMonomorphism G (Z.arrow ≫ eqToHom hobj.symm)}) :
    IsOpenSubspace B S hS
        ((P.invariantLocallyClosedSubschemeEquivOfExtendsRelation B S hS hG hobj).1 Z).1 ↔
      AlgebraicGeometry.IsOpenImmersion Z.1.arrow

AlgebraicGeometry.Space.invariantLocallyClosedSubschemeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantSubspace.lean, line 915. The attribute's comment: “bijection; conditional on effective descent for immersions”.

Stacks 07TW, the canonical bijection. For an algebraic space X over S with a surjective étale chart φ : U ⟶ X, the invariant locally closed subschemes of U correspond bijectively to the locally closed subspaces of X, and the bijection is characterised by pullback along φ.

The hypothesis hdesc is effective descent of immersions along surjective étale morphisms of the site, Stacks 02W8 in the form Stacks 03I2 consumes; see AlgebraicGeometry.Space.IsEffectiveDescentAlongSurjectiveEtale.

noncomputable def invariantLocallyClosedSubschemeEquiv
    (hdesc : IsEffectiveDescentAlongSurjectiveEtale B S hS
      (@AlgebraicGeometry.IsImmersion.{u}))
    (hX : IsAlgebraicSpace B S hS X) :
    {e : InvariantLocallyClosedSubscheme B S hS hs ≃
      LocallyClosedQuotientSubspace B S hS (X := X) //
      ∀ Z, ((e Z).1.preimage φ) = subschemePoints B S hS Z.1}

AlgebraicGeometry.Space.closed_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantSubspace.lean, line 939. The attribute's comment: “closedness; conditional on effective descent for immersions”.

Stacks 07TW, closedness: the subspace of X corresponding to an invariant subscheme of the chart is closed exactly when that subscheme is closed in the chart.

theorem closed_iff
    (hdesc : IsEffectiveDescentAlongSurjectiveEtale B S hS
      (@AlgebraicGeometry.IsImmersion.{u}))
    (hX : IsAlgebraicSpace B S hS X) (Z : InvariantLocallyClosedSubscheme B S hS hs) :
    IsClosedSubspace B S hS
        ((invariantLocallyClosedSubschemeEquiv B S hS hs he hdesc hX).1 Z).1 ↔
      AlgebraicGeometry.IsClosedImmersion Z.1.arrow

AlgebraicGeometry.Space.open_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvariantSubspace.lean, line 953. The attribute's comment: “openness; conditional on effective descent for immersions”.

Stacks 07TW, openness: the subspace of X corresponding to an invariant subscheme of the chart is open exactly when that subscheme is open in the chart.

theorem open_iff
    (hdesc : IsEffectiveDescentAlongSurjectiveEtale B S hS
      (@AlgebraicGeometry.IsImmersion.{u}))
    (hX : IsAlgebraicSpace B S hS X) (Z : InvariantLocallyClosedSubscheme B S hS hs) :
    IsOpenSubspace B S hS
        ((invariantLocallyClosedSubschemeEquiv B S hS hs he hdesc hX).1 Z).1 ↔
      AlgebraicGeometry.IsOpenImmersion Z.1.arrow

Tag 03IQ, a lemma

Tag 03IQ in the Stacks Project.

AlgebraicGeometry.Space.reducedClosedSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspace.lean, line 830. The attribute's comment: “the subspace itself, on a closed set of points”.

The reduced closed subspace of an algebraic space supported on a closed set of points, as data rather than as a choice of a witness to an existence statement.

It is AlgebraicGeometry.Space.reducedClosedSubspaceOfChart at a chart chosen from the atlas clause of the algebraic-space hypothesis. The choice is of a chart, which the hypothesis provides; it is not a choice of the subspace, and by AlgebraicGeometry.Space.eq_reducedClosedSubspaceOfChart the result does not depend on it.

noncomputable def reducedClosedSubspace (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (T : Set (points B S hS X)) (hT : IsClosed T) : Subfunctor X

AlgebraicGeometry.Space.range_pointsMap_ι_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspace.lean, line 838. The attribute's comment: “property (a): the point set of the subspace is the given closed set”.

The point set of the reduced closed subspace is the closed set one started with.

theorem range_pointsMap_ι_reducedClosedSubspace (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (T : Set (points B S hS X)) (hT : IsClosed T) :
    Set.range (pointsMap B S hS (reducedClosedSubspace B S hS X hX T hT).toFunctor
      (reducedClosedSubspace B S hS X hX T hT).ι) = T

AlgebraicGeometry.Space.hasEtaleLocalProperty_isReduced_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspace.lean, line 849. The attribute's comment: “property (b): the subspace is reduced”.

The reduced closed subspace is reduced, in the étale-local sense of Stacks 03E6.

theorem hasEtaleLocalProperty_isReduced_reducedClosedSubspace
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (T : Set (points B S hS X)) (hT : IsClosed T) :
    HasEtaleLocalProperty B S hS (reducedClosedSubspace B S hS X hX T hT).toFunctor
      (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.isClosedSubspace_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspace.lean, line 901. The attribute's comment: “property (c): the subspace is a closed subspace”.

The reduced closed subspace is a closed subspace, unconditionally: the inclusion of AlgebraicGeometry.Space.reducedClosedSubspace into X is representable and a closed immersion after every representable base change.

This is AlgebraicGeometry.Space.isClosedSubspace_reducedClosedSubspace_of_closedImmersionDescent with its hypothesis discharged by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion.

theorem isClosedSubspace_reducedClosedSubspace
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (T : Set (points B S hS X)) (hT : IsClosed T) :
    IsClosedSubspace B S hS (reducedClosedSubspace B S hS X hX T hT)

AlgebraicGeometry.Space.eq_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspace.lean, line 912. The attribute's comment: “uniqueness, unconditionally”.

Stacks 03IQ, uniqueness, unconditionally. A closed subspace of an algebraic space which is étale-locally reduced and has a given set of points is AlgebraicGeometry.Space.reducedClosedSubspace.

theorem eq_reducedClosedSubspace (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X)
    (T : Set (points B S hS X)) (hT : IsClosed T) (W : Subfunctor X)
    (hWc : IsClosedSubspace B S hS W)
    (hWT : Set.range (pointsMap B S hS W.toFunctor W.ι) = T)
    (hWr : HasEtaleLocalProperty B S hS W.toFunctor (fun Y : Scheme.{u} => IsReduced Y)) :
    W = reducedClosedSubspace B S hS X hX T hT

AlgebraicGeometry.Space.existsUnique_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspace.lean, line 933. The attribute's comment: “existence and uniqueness”.

Stacks 03IQ: a closed subset of the points of an algebraic space carries a unique reduced closed subspace structure, with no hypothesis.

Uniqueness is AlgebraicGeometry.Space.eq_reducedClosedSubspace, the witness is the datum AlgebraicGeometry.Space.reducedClosedSubspace, and the closed-subspace clause of existence is AlgebraicGeometry.Space.isClosedSubspace_reducedClosedSubspace, whose own descent hypothesis is discharged by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion.

theorem existsUnique_reducedClosedSubspace
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (T : Set (points B S hS X)) (hT : IsClosed T) :
    ∃! Z : Subfunctor X,
      IsClosedSubspace B S hS Z ∧
        Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T ∧
          HasEtaleLocalProperty B S hS Z.toFunctor (fun Y : Scheme.{u} => IsReduced Y)

AlgebraicGeometry.Space.existsUnique_reducedClosedSubspace', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspaceDescent.lean, line 91.

Stacks 03IQ. A closed subset of the set of points of an algebraic space over S carries a unique reduced closed subspace structure: there is exactly one subfunctor of X which is a closed subspace, has that closed set as its set of points, and is étale-locally reduced.

The witness is AlgebraicGeometry.Space.reducedClosedSubspace, which is constructed explicitly.

theorem existsUnique_reducedClosedSubspace' (hX : IsAlgebraicSpace B S hS X)
    (T : Set (points B S hS X)) (hT : _root_.IsClosed T) :
    ∃! Z : Subfunctor X,
      IsClosedSubspace B S hS Z ∧
        Set.range (pointsMap B S hS Z.toFunctor Z.ι) = T ∧
          HasEtaleLocalProperty B S hS Z.toFunctor (fun Y : Scheme.{u} => IsReduced Y)

Tag 03JJ, a lemma

Tag 03JJ in the Stacks Project.

AlgebraicGeometry.Space.exists_lift_closedSubspace_iff_pointsMap_range_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ReducedFactorThroughClosedSubspace.lean, line 96.

Stacks 03JJ. A morphism from a reduced algebraic space factors through a closed subspace if and only if its image on underlying points lies in that closed subspace.

theorem exists_lift_closedSubspace_iff_pointsMap_range_subset (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (Z : Subfunctor X) (hZ : IsClosedSubspace B S hS Z)
    (hred : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T))
    (f : Y ⟶ X) :
    (∃ g : Y ⟶ Z.toFunctor, g ≫ Z.ι = f) ↔
      Set.range (pointsMap B S hS Y f) ⊆ Set.range (pointsMap B S hS Z.toFunctor Z.ι)

Tag 047X, a definition

Tag 047X in the Stacks Project.

AlgebraicGeometry.Space.IsAlgebraicSpaceStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reduction.lean, line 85. The attribute's comment: “algebraic space structure on a closed set of points”.

Stacks 047X. An algebraic space structure on a closed set Z of points of an algebraic space X over S is a closed subspace of X whose set of points is Z.

def IsAlgebraicSpaceStructure {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (Z : Set (points B S hS X)) (Z' : Subfunctor X) : Prop

AlgebraicGeometry.Space.isAlgebraicSpaceStructure_reducedClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reduction.lean, line 109. The attribute's comment: “the reduced induced structure”.

Stacks 047X, the reduced induced structure. The subspace of Stacks 03IQ on a closed set of points is an algebraic space structure on that set. That it is moreover reduced is AlgebraicGeometry.Space.hasEtaleLocalProperty_isReduced_reducedClosedSubspace, and that it is the only reduced one is AlgebraicGeometry.Space.existsUnique_isAlgebraicSpaceStructure_isReduced.

theorem isAlgebraicSpaceStructure_reducedClosedSubspace
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (Z : Set (points B S hS X)) (hZ : IsClosed Z) :
    IsAlgebraicSpaceStructure B S hS Z (reducedClosedSubspace B S hS X hX Z hZ)

AlgebraicGeometry.Space.existsUnique_isAlgebraicSpaceStructure_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reduction.lean, line 147. The attribute's comment: “the reduced induced structure is the unique reduced one”.

Stacks 047X, the reduced induced structure characterized. A closed set of points of an algebraic space carries exactly one reduced algebraic space structure, namely the subspace of Stacks 03IQ. This is what makes the reduced induced structure well defined.

theorem existsUnique_isAlgebraicSpaceStructure_isReduced
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (Z : Set (points B S hS X)) (hZ : IsClosed Z) :
    ∃! Z' : Subfunctor X,
      IsAlgebraicSpaceStructure B S hS Z Z' ∧
        HasEtaleLocalProperty B S hS Z'.toFunctor (fun Y : Scheme.{u} => IsReduced Y)

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

Stacks 047X, the reduction. The reduction X_red of an algebraic space X over S is the reduced induced algebraic space structure on the whole of its space of points: the subspace of Stacks 03IQ at the closed set Set.univ.

noncomputable def reduction (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) : Subfunctor X

AlgebraicGeometry.Space.existsUnique_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Reduction.lean, line 218. The attribute's comment: “the reduction is the unique reduced structure on the whole point set”.

Stacks 047X, the reduction characterized. The reduction is the unique reduced algebraic space structure on the whole space of points.

theorem existsUnique_reduction (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) :
    ∃! Z' : Subfunctor X,
      IsAlgebraicSpaceStructure B S hS (Set.univ : Set (points B S hS X)) Z' ∧
        HasEtaleLocalProperty B S hS Z'.toFunctor (fun Y : Scheme.{u} => IsReduced Y)

Sources

LeanAlgebraicGeometry.Space.exists_isQuasicoherentOnSite_idealZeroLocus_eq · AlgebraicGeometry.Space.isEmbedding_pointsMap_of_isImmersion · AlgebraicGeometry.Space.isLocallyClosed_range_pointsMap_of_isImmersion · AlgebraicGeometry.Space.invariantLocallyClosedSubschemeEquiv_of_isAlgebraicSpace · AlgebraicGeometry.Space.closed_iff_of_isAlgebraicSpace · AlgebraicGeometry.Space.open_iff_of_isAlgebraicSpace · AlgebraicGeometry.Space.isOpenSubspace_invariantSubspace · AlgebraicGeometry.Space.Presentation.invariantLocallyClosedSubschemeEquivOfExtendsRelation

Section66.13 The schematic locus #

Section 66.13 of the Stacks Project, Tag 03JG. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03JG, the section

Tag 03JG in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.schematicLocus, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SchematicLocusSection.lean, line 31 (StacksFrontier): “the schematic locus”.
AlgebraicGeometry.Space.exists_isGreatest_isOpenSubspace_isRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SchematicLocusSection.lean, line 32 (StacksFrontier): “a largest open subspace which is a scheme”.
AlgebraicGeometry.Space.denseRange_schematicLocus_of_isZariskiLocallyQuasiSeparatedOver, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SchematicLocusSection.lean, line 34 (StacksFrontier): “density of the schematic locus for quasi-separated spaces”.

Tag 03JH, a lemma

Tag 03JH in the Stacks Project.

AlgebraicGeometry.Space.isOpenSubspace_and_isRepresentable_schematicLocus_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DenseSchematicLocusEquivalence.lean, line 67. The attribute's comment: “openness and representability”.

The schematic locus of an algebraic space over S is an open subspace and is representable.

theorem isOpenSubspace_and_isRepresentable_schematicLocus_of_isAlgebraicSpace
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) :
    IsOpenSubspace B S hS (schematicLocus B S hS X) ∧
      (schematicLocus B S hS X).toFunctor.IsRepresentable

AlgebraicGeometry.Space.exists_isGreatest_isOpenSubspace_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DenseSchematicLocusEquivalence.lean, line 91.

An algebraic space X over a scheme S has a largest open subspace which is a scheme: the set of open subspaces of X that are represented by a scheme over S has a greatest element.

theorem exists_isGreatest_isOpenSubspace_isRepresentable
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) :
    ∃ X' : Subfunctor X, IsGreatest
      {G : Subfunctor X | IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable} X'

AlgebraicGeometry.Space.mem_range_pointsMap_schematicLocus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeSchematicLocus.lean, line 196. The attribute's comment: “points of the schematic locus”.

A point of a presheaf lies in the point set of the schematic locus of Tag 03JH exactly when it lies in the point set of one representable open subspace.

The schematic locus is the supremum of the representable open subspaces, and the supremum of subfunctors is the object-wise union, so a field-valued point of it takes its value in one member of the family.

theorem mem_range_pointsMap_schematicLocus_iff
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (y : points B S hS F) :
    y ∈ Set.range (pointsMap B S hS (schematicLocus B S hS F).toFunctor
        (schematicLocus B S hS F).ι) ↔
      ∃ G : Subfunctor F, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
        y ∈ Set.range (pointsMap B S hS G.toFunctor G.ι)

AlgebraicGeometry.Space.schematicLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenSubspace.lean, line 41. The attribute's comment: “schematic locus”.

The schematic locus of F: the union of all open subspaces of F which are represented by a scheme over S.

def schematicLocus (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Subfunctor F

AlgebraicGeometry.Space.le_schematicLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenSubspace.lean, line 47. The attribute's comment: “maximality”.

Every open subspace which is represented by a scheme over S is contained in the schematic locus.

theorem le_schematicLocus (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (G : Subfunctor F)
    (hG : IsOpenSubspace B S hS G) (hGrep : G.toFunctor.IsRepresentable) :
    G ≤ schematicLocus B S hS F

Tag 0BAS, a lemma

Tag 0BAS in the Stacks Project.

AlgebraicGeometry.Space.codimensionZero_mem_schematicLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteEtaleSchematicLocus.lean, line 342. The attribute's comment: “codimension-zero points”.

Stacks 0BAS, codimension-zero points. If an algebraic space over S admits a finite, étale, surjective morphism from an object of the site whose underlying scheme is quasi-separated, then every point of codimension zero lies in the schematic locus of Tag 03JH.

theorem codimensionZero_mem_schematicLocus (hF : IsAlgebraicSpace B S hS F)
    (hcover : ∃ (U : BigFppfOver B S hS) (q : yoneda.obj U ⟶ F),
      QuasiSeparatedSpace ((BigFppfOver.toScheme B S hS).obj U) ∧
      IsFinite B S hS q ∧ IsEtale B S hS q ∧ IsSurjective B S hS q)
    (x : points B S hS F) (hx : localRingDimension B S hS x = 0) :
    x ∈ Set.range (pointsMap B S hS (schematicLocus B S hS F).toFunctor
      (schematicLocus B S hS F).ι)

AlgebraicGeometry.Space.denseRange_schematicLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteEtaleSchematicLocus.lean, line 358. The attribute's comment: “density”.

Stacks 0BAS, density. If an algebraic space over S admits a finite, étale, surjective morphism from an object of the site whose underlying scheme is quasi-separated, then the schematic locus of Tag 03JH is dense in its space of points.

theorem denseRange_schematicLocus (hF : IsAlgebraicSpace B S hS F)
    (hcover : ∃ (U : BigFppfOver B S hS) (q : yoneda.obj U ⟶ F),
      QuasiSeparatedSpace ((BigFppfOver.toScheme B S hS).obj U) ∧
      IsFinite B S hS q ∧ IsEtale B S hS q ∧ IsSurjective B S hS q) :
    DenseRange (pointsMap B S hS (schematicLocus B S hS F).toFunctor
      (schematicLocus B S hS F).ι)

Tag 06NH, a proposition

Tag 06NH in the Stacks Project.

AlgebraicGeometry.Space.exists_denseRange_isRepresentable_isOpenSubspace_codimensionZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedCodimensionZero.lean, line 287.

Stacks 06NH. A Zariski locally quasi-separated algebraic space over S — for instance a quasi-separated one — has a dense open subspace which is a scheme, and every point of codimension 0 of the space lies in that subspace. The subspace is the schematic locus of Tag 03JH.

Zariski local quasi-separatedness is the absolute notion of Tag 03BS part (4), as in the source; by Tag 03W7 it is equivalent to the notion over S, which is how the proof uses it. The containment hZ of the terminal scheme in the site is the argument of that absolute notion; it holds in every big fppf site, by AlgebraicGeometry.BigFppfSite.contains_terminal.

theorem exists_denseRange_isRepresentable_isOpenSubspace_codimensionZero
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsAbsolutelyZariskiLocallyQuasiSeparated B S hS hZ F) :
    ∃ G : Subfunctor F, IsOpenSubspace B S hS G ∧ G.toFunctor.IsRepresentable ∧
      DenseRange (pointsMap B S hS G.toFunctor G.ι) ∧
      ∀ x : points B S hS F, localRingDimension B S hS x = 0 →
        x ∈ Set.range (pointsMap B S hS G.toFunctor G.ι)

AlgebraicGeometry.Space.denseRange_schematicLocus_of_isZariskiLocallyQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedSchematicLocus.lean, line 85. The attribute's comment: “density”.

The schematic locus of a Zariski locally quasi-separated algebraic space over S is dense in its space of points; so that space has a dense open subspace which is a scheme.

theorem denseRange_schematicLocus_of_isZariskiLocallyQuasiSeparatedOver
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsZariskiLocallyQuasiSeparatedOver B S hS F) :
    DenseRange (pointsMap B S hS (schematicLocus B S hS F).toFunctor
      (schematicLocus B S hS F).ι)

Sources

Section66.14 Obtaining a scheme #

Section 66.14 of the Stacks Project, Tag 07S5. 3 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07S6, a proposition

Tag 07S6 in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.exists_schemeQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatQuotient/FppfQuotient.lean, line 363. References: SGA 3 V (4.1), “(iv)”.

Stacks 07S6. Let (U, R, s, t, c) be a groupoid scheme over S with s and t finite locally free, with (t, s) an equivalence relation, and such that every nonempty closed subset of U contains a point whose R-equivalence class lies in an affine open. Then there is a scheme M over S, no larger than U, and a finite locally free surjection p : U ⟶ M, whose kernel pair is (t, s) and which represents the fppf quotient sheaf U/R.

The invariant affine opens cover U (Stacks 03JE), the quotient of the restriction of the groupoid to each of them is affine (Stacks 03BM) and is an open subspace of U/R (Stacks 02WU), and those open subspaces jointly cover U/R because U covers it; glueing them (Stacks 01JJ) gives M. Finite local freeness, surjectivity and the size bound transfer from the charts to p because they are local on the target, and the kernel-pair square is the identification of R with the kernel pair of the projection of U onto U/R.

theorem exists_schemeQuotient (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)] (G : GroupoidScheme S)
    [IsFiniteLocallyFree G.source.left] [IsFiniteLocallyFree G.target.left]
    [IsEquivalenceRelation G.target G.source] (hU : B.Contains G.objects.left)
    (h3 : HasAffineOrbitInEveryClosed G) :
    ∃ (M : Over S) (p : G.objects ⟶ M)
      (hp : (groupoidPreRelation G).target ≫ p = (groupoidPreRelation G).source ≫ p)
      (hM : Presheaf.IsSheaf (BigFppfOver.topology B S hS)
        (points (Over.post B.inclusion) M)),
      M.left.size ≤ G.objects.left.size ∧ IsFiniteLocallyFree p.left ∧ Surjective p.left ∧
        IsPullback G.target G.source p p ∧
        IsIso (quotientSheafToPoints (BigFppfOver.topology B S hS) (Over.post B.inclusion)
          (groupoidPreRelation G) p hp hM)

AlgebraicGeometry.Space.isRepresentable_quotientSheaf_of_isInvariantOpen_isAffineOpen_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientCharts.lean, line 229. The attribute's comment: “representability of the quotient sheaf”. References: SGA 3 V (4.1), “(iv), special case”; SGA 3 V (7.1), “(iv), special case”.

The fppf quotient sheaf of a finite locally free groupoid covered by invariant affine opens is representable. For a groupoid scheme over S with finite locally free source and target whose pre-relation is an equivalence relation, and whose object scheme is covered by R-invariant affine opens indexed by a type below the site's cutoff, the quotient sheaf U/R is representable on the big fppf site of S.

theorem isRepresentable_quotientSheaf_of_isInvariantOpen_isAffineOpen_cover {S : Scheme.{u}}
    (G : GroupoidScheme S) [IsFiniteLocallyFree G.source.left]
    [IsFiniteLocallyFree G.target.left] [IsEquivalenceRelation G.target G.source]
    (B : BigFppfSite.{u}) (hS : B.Contains S) (hU : B.Contains G.objects.left)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    {ι : Type u} (hι : #ι < B.cutoff) (V : ι → G.objects.left.Opens)
    (hVinv : ∀ i, IsInvariantOpen G (V i)) (hVaff : ∀ i, IsAffineOpen (V i))
    (hcov : ⨆ i, V i = ⊤) :
    let F : BigFppfOver B S hS ⥤ Over S := Over.post B.inclusion
    let J := BigFppfOver.topology B S hS
    (quotientSheaf J F (groupoidPreRelation G)).obj.IsRepresentable

AlgebraicGeometry.Space.exists_quotientMap_isRepresented_of_isInvariantOpen_isAffineOpen_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientCharts.lean, line 346. The attribute's comment: “the quotient scheme and the three conclusion clauses, on a given site”. References: SGA 3 V (4.1), “invariant affine cover”.

The quotient scheme and the quotient morphism, on a given big fppf site. Under the hypotheses of AlgebraicGeometry.Space.isRepresentable_quotientSheaf_of_isInvariantOpen_isAffineOpen_cover there are a scheme M over S belonging to the big fppf site and a morphism f : U ⟶ M of S-schemes which is finite locally free and surjective, whose kernel pair is the given pair (t, s) — that is R = U ×_M U — and under which the restricted functor of points of M is a sheaf representing the quotient sheaf U/R compatibly with f.

theorem exists_quotientMap_isRepresented_of_isInvariantOpen_isAffineOpen_cover
    {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFiniteLocallyFree G.source.left] [IsFiniteLocallyFree G.target.left]
    [IsEquivalenceRelation G.target G.source]
    (B : BigFppfSite.{u}) (hS : B.Contains S) (hU : B.Contains G.objects.left)
    (hR : B.Contains G.arrows.left)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    {ι : Type u} (hι : #ι < B.cutoff) (V : ι → G.objects.left.Opens)
    (hVinv : ∀ i, IsInvariantOpen G (V i)) (hVaff : ∀ i, IsAffineOpen (V i))
    (hcov : ⨆ i, V i = ⊤) :
    let F : BigFppfOver B S hS ⥤ Over S := Over.post B.inclusion
    let J := BigFppfOver.topology B S hS
    ∃ (M : Over S) (f : G.objects ⟶ M), B.Contains M.left ∧
      IsFiniteLocallyFree f.left ∧ Surjective f.left ∧
      IsPullback G.target G.source f f ∧
      ∃ hM : Presheaf.IsSheaf J (Stacks.Groupoids.points F M),
        ∃ q : quotientSheaf J F (groupoidPreRelation G) ⟶
            (⟨Stacks.Groupoids.points F M, hM⟩ : Sheaf J (Type u)),
          IsIso q ∧ toQuotientSheaf J F (groupoidPreRelation G) ≫ q.hom =
            F.op.whiskerLeft (yoneda.map f)

AlgebraicGeometry.Space.exists_quotientMap_isRepresented_of_affineOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientCharts.lean, line 514. The attribute's comment: “the three conclusion clauses from the affine-orbit condition, on a given site”. References: SGA 3 V (4.1), “(iv)”.

The quotient scheme and the quotient morphism for a groupoid with affine orbits, on a given big fppf site. The same conclusion as AlgebraicGeometry.Space.exists_quotientMap_isRepresented_of_isInvariantOpen_isAffineOpen_cover with the covering by invariant affine opens replaced by the condition that every nonempty closed subset of U contains a point whose R-equivalence class t(s⁻¹({u})) lies in an affine open of U.

theorem exists_quotientMap_isRepresented_of_affineOrbits {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFiniteLocallyFree G.source.left] [IsFiniteLocallyFree G.target.left]
    [IsEquivalenceRelation G.target G.source]
    (B : BigFppfSite.{u}) (hS : B.Contains S) (hU : B.Contains G.objects.left)
    (hR : B.Contains G.arrows.left)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (horbit : ∀ Z : Set G.objects.left, IsClosed Z → Z.Nonempty →
      ∃ u ∈ Z, ∃ W : G.objects.left.Opens, IsAffineOpen W ∧
        G.target.left.base '' (G.source.left.base ⁻¹' {u}) ⊆ (W : Set G.objects.left)) :
    let F : BigFppfOver B S hS ⥤ Over S := Over.post B.inclusion
    let J := BigFppfOver.topology B S hS
    ∃ (M : Over S) (f : G.objects ⟶ M), B.Contains M.left ∧
      IsFiniteLocallyFree f.left ∧ Surjective f.left ∧
      IsPullback G.target G.source f f ∧
      ∃ hM : Presheaf.IsSheaf J (Stacks.Groupoids.points F M),
        ∃ q : quotientSheaf J F (groupoidPreRelation G) ⟶
            (⟨Stacks.Groupoids.points F M, hM⟩ : Sheaf J (Type u)),
          IsIso q ∧ toQuotientSheaf J F (groupoidPreRelation G) ≫ q.hom =
            F.op.whiskerLeft (yoneda.map f)

AlgebraicGeometry.Space.nonempty_finiteFlatQuotient_of_affineOrbits_of_bigFppfSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientCharts.lean, line 551. The attribute's comment: “the finite flat quotient, given a big fppf site containing the groupoid”. References: SGA 3 V (4.1), “more general”.

A finite flat quotient of a groupoid with affine orbits, given a big fppf site. Let (U, R, s, t, c) be a groupoid scheme over S with s and t finite locally free and with (t, s) an equivalence relation, such that every nonempty closed subset of U contains a point whose R-equivalence class lies in an affine open, and suppose given a big fppf site of S containing S, U and R. Then the groupoid has a finite flat quotient in the sense of Stacks.Groupoids.FiniteFlatQuotient.

theorem nonempty_finiteFlatQuotient_of_affineOrbits_of_bigFppfSite {S : Scheme.{u}}
    (G : GroupoidScheme S)
    [IsFiniteLocallyFree G.source.left] [IsFiniteLocallyFree G.target.left]
    [IsEquivalenceRelation G.target G.source]
    (B : BigFppfSite.{u}) (hS : B.Contains S) (hU : B.Contains G.objects.left)
    (hR : B.Contains G.arrows.left)
    (horbit : ∀ Z : Set G.objects.left, IsClosed Z → Z.Nonempty →
      ∃ u ∈ Z, ∃ W : G.objects.left.Opens, IsAffineOpen W ∧
        G.target.left.base '' (G.source.left.base ⁻¹' {u}) ⊆ (W : Set G.objects.left)) :
    Nonempty (FiniteFlatQuotient G)

AlgebraicGeometry.Space.nonempty_finiteFlatQuotient_of_affineOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientCharts.lean, line 581. References: SGA 3 V (4.1), “more general”; SGA 3 V (7.1), “special case”.

Finite flat quotients of groupoids with affine orbits. Let (U, R, s, t, c) be a groupoid scheme over a scheme S such that

s, t : R ⟶ U are finite locally free,

j = (t, s) is an equivalence relation, and

every nonempty closed subset Z of U contains a point u whose R-equivalence class t(s⁻¹({u})) is contained in an affine open of U.

Then there is a finite locally free morphism U ⟶ M of schemes over S with R = U ×_M U and with M representing the quotient sheaf U/R in the fppf topology — that is, the groupoid has a finite flat quotient in the sense of Stacks.Groupoids.FiniteFlatQuotient, which also records that U ⟶ M is surjective.

theorem nonempty_finiteFlatQuotient_of_affineOrbits {S : Scheme.{u}} (G : GroupoidScheme S)
    [IsFiniteLocallyFree G.source.left] [IsFiniteLocallyFree G.target.left]
    [IsEquivalenceRelation G.target G.source]
    (horbit : ∀ Z : Set G.objects.left, IsClosed Z → Z.Nonempty →
      ∃ u ∈ Z, ∃ W : G.objects.left.Opens, IsAffineOpen W ∧
        G.target.left.base '' (G.source.left.base ⁻¹' {u}) ⊆ (W : Set G.objects.left)) :
    Nonempty (FiniteFlatQuotient G)

Tag 07S7, a lemma

Tag 07S7 in the Stacks Project.

AlgebraicGeometry.nonempty_finiteFlatQuotient_actionGroupoid_of_geometry, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FreeGroupSchemeQuotient.lean, line 399. The attribute's comment: “the quotient sheaf is a scheme; all seven alternatives of condition (3)”. References: SGA 3 IX (2.3), “2.3(a)”; SGA 3 V (4.1), “special case”; SGA 3 V (9.0), “partial”; SGA 3 VIB (9.3), “Case 2° of Remark 9.3 b)”; SGA 3 XVI (1.1), “more general”; SGA 3 XXV (4.2), “special case”.

Let S be a scheme, G ⟶ S a group scheme, X ⟶ S a morphism of schemes and a : G ×_S X ⟶ X an action. Assume that G ⟶ S is finite locally free, that the action is free, and that X ⟶ S is affine, or quasi-affine, or projective, or quasi-projective, or X admits an immersion into an affine scheme, or an immersion into Proj A for a graded ring A, or G ⟶ S is radicial. Then the fppf quotient sheaf X/G is a scheme: the action groupoid has a finite flat quotient, so there is a scheme M over S representing X/G on every big fppf site, with X ⟶ M surjective and finite locally free and with kernel pair G ×_S X.

theorem nonempty_finiteFlatQuotient_actionGroupoid_of_geometry [IsFiniteLocallyFree G.hom]
    (hfree : IsFreeAction G X)
    (hgeom : IsAffineHom X.hom ∨ IsQuasiAffineHom X.hom ∨ IsProjective X.hom ∨
      IsQuasiProjective X.hom ∨ HasImmersionToAffine X.left ∨ HasImmersionToProj X.left ∨
      UniversallyInjective G.hom) :
    Nonempty (FiniteFlatQuotient (actionGroupoid (Over.mk (𝟙 S)) G X))

AlgebraicGeometry.isFppfTorsor_quotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FreeGroupSchemeQuotient.lean, line 422. The attribute's comment: “the fppf torsor clause: shear isomorphism and fppf-local sections”.

For a finite flat quotient M = X/G of the action groupoid, the morphism G ×_S X ⟶ X ×_M X sending (g, x) to (g · x, x) is an isomorphism, and X ⟶ M is itself an fppf covering of M over which X ⟶ M has a section, namely the diagonal. These are the two conditions for X ⟶ X/G to be an fppf G-torsor.

theorem isFppfTorsor_quotientMap [IsFiniteLocallyFree G.hom]
    (Q : FiniteFlatQuotient (actionGroupoid (Over.mk (𝟙 S)) G X)) :
    (∃ e : (G ⊗ X).left ≅ pullback Q.quotientMap.left Q.quotientMap.left,
        e.hom ≫ pullback.fst Q.quotientMap.left Q.quotientMap.left = (γ[G, X]).left ∧
          e.hom ≫ pullback.snd Q.quotientMap.left Q.quotientMap.left = (snd G X).left) ∧
      Presieve.singleton Q.quotientMap.left ∈ Scheme.fppfPrecoverage Q.space.left ∧
      ∃ s : X.left ⟶ pullback Q.quotientMap.left Q.quotientMap.left,
        s ≫ pullback.fst Q.quotientMap.left Q.quotientMap.left = 𝟙 X.left

Tag 0BBM, a lemma

Tag 0BBM in the Stacks Project.

Stacks.Groupoids.FiniteFlatQuotient.quasiSeparated_space_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientSeparated.lean, line 84. The attribute's comment: “part (1), quasi-separated over the base”.

If the object scheme of the groupoid is quasi-separated over S, then so is the quotient scheme.

theorem quasiSeparated_space_hom (Q : FiniteFlatQuotient G)
    (hU : QuasiSeparated G.objects.hom) : QuasiSeparated Q.space.hom

Stacks.Groupoids.FiniteFlatQuotient.quasiSeparatedSpace_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientSeparated.lean, line 91. The attribute's comment: “part (2), quasi-separated”.

If the object scheme of the groupoid is quasi-separated, then so is the quotient scheme.

theorem quasiSeparatedSpace_space (Q : FiniteFlatQuotient G)
    (hU : QuasiSeparatedSpace G.objects.left) : QuasiSeparatedSpace Q.space.left

Stacks.Groupoids.FiniteFlatQuotient.isSeparated_space_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientSeparated.lean, line 98. The attribute's comment: “part (3), separated over the base”. References: SGA 1 V (1.6), “partial”.

If the object scheme of the groupoid is separated over S, then so is the quotient scheme.

theorem isSeparated_space_hom (Q : FiniteFlatQuotient G)
    (hU : IsSeparated G.objects.hom) : IsSeparated Q.space.hom

Stacks.Groupoids.FiniteFlatQuotient.isSeparated_space, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFlatQuotientSeparated.lean, line 105. The attribute's comment: “part (4), separated”. References: SGA 1 V (1.6), “partial”.

If the object scheme of the groupoid is separated, then so is the quotient scheme.

theorem isSeparated_space (Q : FiniteFlatQuotient G)
    (hU : Scheme.IsSeparated G.objects.left) : Scheme.IsSeparated Q.space.left

Sources

LeanAlgebraicGeometry.GroupoidScheme.exists_schemeQuotient · AlgebraicGeometry.Space.isRepresentable_quotientSheaf_of_isInvariantOpen_isAffineOpen_cover · AlgebraicGeometry.Space.exists_quotientMap_isRepresented_of_isInvariantOpen_isAffineOpen_cover · AlgebraicGeometry.Space.exists_quotientMap_isRepresented_of_affineOrbits · AlgebraicGeometry.Space.nonempty_finiteFlatQuotient_of_affineOrbits_of_bigFppfSite · AlgebraicGeometry.Space.nonempty_finiteFlatQuotient_of_affineOrbits · AlgebraicGeometry.nonempty_finiteFlatQuotient_actionGroupoid_of_geometry · AlgebraicGeometry.isFppfTorsor_quotientMap

Section66.15 Points on quasi-separated spaces #

Section 66.15 of the Stacks Project, Tag 06NI. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06NJ, a lemma

Tag 06NJ in the Stacks Project.

AlgebraicGeometry.Space.t0Space_points_of_isZariskiLocallyQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedSchematicLocus.lean, line 98. The attribute's comment: “Kolmogorov property”.

Two points of the space of points of a Zariski locally quasi-separated algebraic space over S which are topologically indistinguishable are equal.

theorem t0Space_points_of_isZariskiLocallyQuasiSeparatedOver
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsZariskiLocallyQuasiSeparatedOver B S hS F) :
    T0Space (points B S hS F)

AlgebraicGeometry.Space.quasiSober_points_of_isZariskiLocallyQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedSchematicLocus.lean, line 108. The attribute's comment: “generic points of irreducible closed subsets”.

Every irreducible closed subset of the space of points of a Zariski locally quasi-separated algebraic space over S is the closure of one of its points.

theorem quasiSober_points_of_isZariskiLocallyQuasiSeparatedOver
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsZariskiLocallyQuasiSeparatedOver B S hS F) :
    QuasiSober (points B S hS F)

AlgebraicGeometry.Space.stacksSober_points_of_isZariskiLocallyQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiLocallyQuasiSeparatedSchematicLocus.lean, line 118.

The space of points of a Zariski locally quasi-separated algebraic space over S is sober: every irreducible closed subset of it has a unique generic point.

theorem stacksSober_points_of_isZariskiLocallyQuasiSeparatedOver
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsZariskiLocallyQuasiSeparatedOver B S hS F) :
    StacksSober (points B S hS F)

Tag 0A4G, a lemma

Tag 0A4G in the Stacks Project.

AlgebraicGeometry.Space.spectralSpace_points_of_isQuasiCompactSpace_isAbsolutelyQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpectralPoints.lean, line 213.

Stacks 0A4G. The point space of a quasi-compact quasi-separated algebraic space over S is a spectral space.

theorem spectralSpace_points_of_isQuasiCompactSpace_isAbsolutelyQuasiSeparated
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hqc : IsQuasiCompactSpace B S hS X)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X) :
    SpectralSpace (points B S hS X)

Tag 03DZ, a lemma

Tag 03DZ in the Stacks Project.

AlgebraicGeometry.Space.exists_iso_yoneda_spec_of_surjective_etale_fieldSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFieldAtlas.lean, line 273.

A quasi-separated algebraic space over S admitting a surjective étale morphism from the spectrum of a field k is the spectrum of a field k', and k is a finite separable extension of k'.

theorem exists_iso_yoneda_spec_of_surjective_etale_fieldSpec
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hF : IsAlgebraicSpace B S hS F)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal F)
    (k : Type u) [Field k] {U : BigFppfOver B S hS}
    (eU : (BigFppfOver.toScheme B S hS).obj U ≅ Spec (.of k)) (f : yoneda.obj U ⟶ F)
    (hsurj : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) f)
    (hetale : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) f) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k' k) (_ : Module.Finite k' k)
      (_ : Algebra.IsSeparable k' k) (U' : BigFppfOver B S hS)
      (eU' : (BigFppfOver.toScheme B S hS).obj U' ≅ Spec (.of k'))
      (m : U ⟶ U') (e : F ≅ yoneda.obj U'),
      f ≫ e.hom = yoneda.map m ∧
        eU.inv ≫ (BigFppfOver.toScheme B S hS).map m ≫ eU'.hom =
          Spec.map (CommRingCat.ofHom (algebraMap k' k))

AlgebraicGeometry.Space.exists_field_spectrum_of_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PointLikeSpace.lean, line 643.

Stacks 03DZ. Let S be a scheme, k a field and X an algebraic space over S admitting a surjective étale morphism Spec(k) ⟶ X. If X is quasi-separated — Stacks 03BS part (3), that is, quasi-separated over Spec(ℤ) — then X is isomorphic to Spec(k') for a field k' with k/k' finite separable, the isomorphism carrying the given atlas to the morphism induced by the field extension.

This is AlgebraicGeometry.Space.exists_field_spectrum_of_surjective_etale_of_isQuasiSeparatedOver, which asks only for quasi-separatedness over S and is therefore stronger, together with AlgebraicGeometry.Space.isQuasiSeparatedOver_of_isAbsolutelyQuasiSeparated. Surjectivity is taken in the sense of Stacks 03ME, that the induced map on points is surjective, which is the source's reading; the engine asks instead that every represented base change be a surjective morphism of schemes, and the two agree for a morphism into an algebraic space by AlgebraicGeometry.Space.presheafSurjective_of_isSurjective, whose representability hypothesis is supplied by the representable diagonal of X.

theorem exists_field_spectrum_of_surjective_etale
    (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)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ F)
    (k : Type u) [Field k] (hk : B.Contains (Spec (CommRingCat.of k)))
    (b : Spec (CommRingCat.of k) ⟶ S)
    (f : yoneda.obj (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS)) ⟶ F)
    (hsurj : IsSurjective B S hS f)
    (hetale : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) f) :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k' k)
      (_ : Module.Finite k' k) (_ : Algebra.IsSeparable k' k)
      (hk' : B.Contains (Spec (CommRingCat.of k')))
      (b' : Spec (CommRingCat.of k') ⟶ S),
      ∃ (hbase : Spec.map (CommRingCat.ofHom (algebraMap k' k)) ≫ b' = b)
        (e : F ≅ yoneda.obj (Over.mk (⟨b'⟩ : B.obj hk' ⟶ B.obj hS))),
        f ≫ e.hom = yoneda.map (Over.homMk
          (ObjectProperty.homMk (Spec.map (CommRingCat.ofHom (algebraMap k' k))) :
            B.obj hk ⟶ B.obj hk') (by
              apply ObjectProperty.hom_ext
              exact hbase))

Tag 03E0, a remark

Tag 03E0 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.exists_iso_yoneda_spec_of_isDecentSpace_of_etale_fieldSpec, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/FieldAtlas.lean, line 156 (StacksFrontier): “Stacks 03DZ holds for decent algebraic spaces”.
AlgebraicGeometry.Space.isDecentSpace_of_isAbsolutelyLocallySeparated, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/LocallySeparated.lean, line 1033 (StacksFrontier): “a locally separated algebraic space is decent”.
AlgebraicGeometry.Space.isRepresentable_of_subsingleton_points, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/SinglePointSpace.lean, line 370 (StacksFrontier): “a decent algebraic space with one point is a scheme”.

Sources

LeanAlgebraicGeometry.Space.t0Space_points_of_isZariskiLocallyQuasiSeparatedOver · AlgebraicGeometry.Space.quasiSober_points_of_isZariskiLocallyQuasiSeparatedOver · AlgebraicGeometry.Space.stacksSober_points_of_isZariskiLocallyQuasiSeparatedOver · AlgebraicGeometry.Space.spectralSpace_points_of_isQuasiCompactSpace_isAbsolutelyQuasiSeparated · AlgebraicGeometry.Space.exists_iso_yoneda_spec_of_surjective_etale_fieldSpec · AlgebraicGeometry.Space.exists_field_spectrum_of_surjective_etale · AlgebraicGeometry.Space.exists_iso_yoneda_spec_of_isDecentSpace_of_etale_fieldSpec · AlgebraicGeometry.Space.isDecentSpace_of_isAbsolutelyLocallySeparated

Section66.16 Étale morphisms of algebraic spaces #

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

Tag 03EC, a lemma

Tag 03EC in the Stacks Project.

AlgebraicGeometry.Space.etale_comp_of_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleCharts.lean, line 163. The attribute's comment: “composition”.

Stacks 03EC. An étale morphism of the big fppf site of S followed by an étale chart of an algebraic space is again an étale chart.

theorem etale_comp_of_scheme {U U' : BigFppfOver B S hS}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : U ⟶ U') (g : yoneda.obj U' ⟶ F)
    (hf : AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).map f))
    (hg : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf g) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map f ≫ g)

AlgebraicGeometry.Space.etale_of_etale_charts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleCharts.lean, line 186. The attribute's comment: “morphism_between_charts”.

Stacks 03EC. A morphism of the big fppf site of S between two étale charts of a presheaf is an étale morphism of schemes.

The ambient presheaf need not be an algebraic space, so the statement covers the source one: the second chart is étale and hence relatively representable, which is all that is used. The morphism factors through the fibre product of the two charts, as a section of one projection followed by the other. Both projections are étale by cancellation against the étale charts, and a section of an étale morphism is étale by CategoryTheory.MorphismProperty.of_postcomp, so no descent along an atlas is required.

theorem etale_of_etale_charts {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {U U' : BigFppfOver B S hS}
    (φ : yoneda.obj U ⟶ F) (φ' : yoneda.obj U' ⟶ F)
    (hφ : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf φ)
    (hφ' : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf φ')
    (χ : U ⟶ U') (hχ : yoneda.map χ ≫ φ' = φ) :
    AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).map χ)

AlgebraicGeometry.Space.etale_of_comp_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleCharts.lean, line 220. The attribute's comment: “descent_from_chart”.

Stacks 03EC. Étaleness of a chart of an algebraic space descends along a surjective étale morphism of the big fppf site of S: if χ : U ⟶ U' is surjective étale and yoneda.map χ ≫ φ' is an étale chart, then so is φ'.

theorem etale_of_comp_surjective_etale {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) {U U' : BigFppfOver B S hS} (χ : U ⟶ U')
    [AlgebraicGeometry.Surjective ((BigFppfOver.toScheme B S hS).map χ)]
    [AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).map χ)]
    (φ' : yoneda.obj U' ⟶ X)
    (hφ : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf (yoneda.map χ ≫ φ')) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf φ'

Tag 03FR, a definition

Tag 03FR in the Stacks Project.

AlgebraicGeometry.Space.IsEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 184.

Stacks 03FR. A morphism of algebraic spaces over S is étale when its composite with every étale morphism from a representable presheaf into its source is again étale.

abbrev IsEtale {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

Tag 03FS, a lemma

Tag 03FS in the Stacks Project.

AlgebraicGeometry.Space.isEtale_iff_exists_source_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 113. The attribute's comment: “condition (2)”.

A morphism of algebraic spaces over S is étale exactly when its composite with some surjective étale chart of its source is étale.

theorem isEtale_iff_exists_source_chart {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    IsEtale B S hS f ↔
      ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ F),
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        IsEtale B S hS (p ≫ f)

AlgebraicGeometry.Space.isEtale_iff_exists_target_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 155. The attribute's comment: “condition (3)”.

A morphism of algebraic spaces over S is étale exactly when its base change along some surjective étale chart of its target is étale.

theorem isEtale_iff_exists_target_chart {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    IsEtale B S hS f ↔
      ∃ (V : BigFppfOver B S hS) (q : yoneda.obj V ⟶ G),
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf q ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf q ∧
        IsEtale B S hS (pullback.snd f q)

AlgebraicGeometry.Space.isEtale_iff_exists_etale_chart_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 222. The attribute's comment: “condition (4)”.

A morphism of algebraic spaces over S is étale exactly when it fits in a commuting square of charts, with the chart of the source surjective and étale, the chart of the target étale, and the morphism of schemes between them étale.

theorem isEtale_iff_exists_etale_chart_square {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    IsEtale B S hS f ↔
      ∃ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ F) (q : yoneda.obj V ⟶ G) (α : U ⟶ V),
        p ≫ f = yoneda.map α ≫ q ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf q ∧
        AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).map α)

AlgebraicGeometry.Space.isEtale_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleTargetChartCriterion.lean, line 174.

Stacks 03FS. For a morphism f : F ⟶ G of algebraic spaces over S the following four conditions are equivalent: f is étale; there is a surjective étale scheme chart of F whose composite with f is étale; there is a surjective étale scheme chart of G along which the base change of f is étale; and f fits into a commuting square of étale scheme charts, with the chart of F surjective, whose upper morphism of schemes is étale.

Conditions (1), (2) and (4) are AlgebraicGeometry.Space.isEtale_iff_exists_source_chart and AlgebraicGeometry.Space.isEtale_iff_exists_etale_chart_square; condition (3) is AlgebraicGeometry.Space.isEtale_iff_exists_target_chart.

theorem isEtale_tfae (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    List.TFAE [
      IsEtale B S hS f,
      (∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ F),
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        IsEtale B S hS (p ≫ f)),
      (∃ (V : BigFppfOver B S hS) (ψ : yoneda.obj V ⟶ G),
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf ψ ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf ψ ∧
        IsEtale B S hS (pullback.snd f ψ)),
      (∃ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ F) (q : yoneda.obj V ⟶ G) (α : U ⟶ V),
        p ≫ f = yoneda.map α ≫ q ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf q ∧
        AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).map α))
    ]

Tag 03FT, a lemma

Tag 03FT in the Stacks Project.

AlgebraicGeometry.Space.isEtale_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 75.

The composite of two étale morphisms of presheaves on the big fppf site of S is étale.

theorem isEtale_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G} {g : G ⟶ H}
    (hf : IsEtale B S hS f) (hg : IsEtale B S hS g) : IsEtale B S hS (f ≫ g)

Tag 03FU, a lemma

Tag 03FU in the Stacks Project.

AlgebraicGeometry.Space.isEtale_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 254. References: SGA 1 IX (1.3).

A base change of an étale morphism of algebraic spaces over S is étale.

theorem isEtale_of_isPullback {X' X Z Y : AlgebraicSpaces B S hS}
    (p : X' ⟶ X) (f' : X' ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ Y)
    (h : IsPullback p f' f g) (hf : IsEtale B S hS f.hom) :
    IsEtale B S hS f'.hom

Tag 03FV, a lemma

Tag 03FV in the Stacks Project.

AlgebraicGeometry.Space.isEtale_of_isEtale_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 378.

A morphism between two algebraic spaces which are étale over a common algebraic space is itself étale.

theorem isEtale_of_isEtale_over {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (_hH : IsAlgebraicSpace B S hS H) (f : F ⟶ G) (g : F ⟶ H) (h : G ⟶ H)
    (hg : IsEtale B S hS g) (hh : IsEtale B S hS h) (hfg : f ≫ h = g) :
    IsEtale B S hS f

Tag 03IR, a lemma

Tag 03IR in the Stacks Project.

AlgebraicGeometry.Space.isOpenMap_pointsMap_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleOpenOnPoints.lean, line 75.

Stacks 03IR. An étale morphism f : X ⟶ Y of algebraic spaces over S induces an open map |X| → |Y| on the point sets of Tag 03BU, for the topology of Tag 03BX.

The hypothesis _hG that the target is an algebraic space is retained from the source statement but is not used: only an étale chart of the source enters the argument.

theorem isOpenMap_pointsMap_of_isEtale (f : F ⟶ G) (hF : IsAlgebraicSpace B S hS F)
    (_hG : IsAlgebraicSpace B S hS G) (hf : IsEtale B S hS f) :
    @IsOpenMap _ _ (pointTopology B S hS F) (pointTopology B S hS G)
      (pointsMap B S hS F f)

Tag 03KX, a lemma

Tag 03KX in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_etale_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FiniteFlatAffine/EtaleOverFieldRepresentable.lean, line 305.

Stacks 03KX. An algebraic space over S admitting an étale morphism to an object of the big fppf site over S whose underlying scheme is the spectrum of a field is representable.

theorem isRepresentable_of_etale_over_field
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (k : Type u) [Field k]
    (V : BigFppfOver B S hS)
    (eV : (BigFppfOver.toScheme B S hS).obj V ≅ Spec (.of k))
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (f : F ⟶ yoneda.obj V) (hf : IsEtale B S hS f) :
    F.IsRepresentable

Sources

LeanAlgebraicGeometry.Space.etale_comp_of_scheme · AlgebraicGeometry.Space.etale_of_etale_charts · AlgebraicGeometry.Space.etale_of_comp_surjective_etale · AlgebraicGeometry.Space.IsEtale · AlgebraicGeometry.Space.isEtale_iff_exists_source_chart · AlgebraicGeometry.Space.isEtale_iff_exists_target_chart · AlgebraicGeometry.Space.isEtale_iff_exists_etale_chart_square · AlgebraicGeometry.Space.isEtale_tfae

Section66.17 Spaces and fpqc coverings #

Section 66.17 of the Stacks Project, Tag 03W8. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0APL, a proposition

Tag 0APL in the Stacks Project.

AlgebraicGeometry.IsAlgebraicSpace.isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/IndQuasiAffineFpqcSheaf.lean, line 111.

An algebraic space is a sheaf for the fpqc topology, which is Stacks, Tag 0APL.

theorem isSheaf_fpqc (hF : IsAlgebraicSpace B S hS F) :
    Presheaf.IsSheaf
      ((Scheme.fpqcPrecoverage.comap (BigFppfOver.toScheme B S hS)).toGrothendieck) F

Sources

LeanAlgebraicGeometry.IsAlgebraicSpace.isSheaf_fpqc

Section66.18 The étale site of an algebraic space #

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

Tag 03ED, a definition

Tag 03ED in the Stacks Project.

AlgebraicGeometry.Space.SmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSite.lean, line 119. The attribute's comment: “objects and morphisms”. References: SGA 4½ Arcata (2.1.4), “étale X-schemes”.

Stacks 03ED, parts (1) and (2). The small étale site of a presheaf F on the big fppf site of S, as a category: its objects are the étale charts of F, and its morphisms are the morphisms of the big fppf site of S whose triangle over F commutes.

abbrev SmallEtale

AlgebraicGeometry.Space.SmallEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleSite.lean, line 139. The attribute's comment: “coverings”. References: SGA 4½ Arcata (2.1.4), “étale topology”.

Stacks 03ED, part (3). A family of étale charts of F is a covering family exactly when its family of underlying objects of Sch_κ is a chosen étale covering family of the big étale site carried by B.

abbrev IsCovering (E : Covering (SmallEtale B S hS F)) : Prop

Tag 03G0, a definition

Tag 03G0 in the Stacks Project.

AlgebraicGeometry.Space.essentiallySmall_spacesEtale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleEssentiallySmall.lean, line 243. The attribute's comment: “the set-theoretic condition: the site is essentially small”.

Stacks 03G0. The spaces-étale site of an algebraic space is essentially small at the universe of the schemes, even though its objects live in Type (u + 1).

It is the full subcategory of the slice of the algebraic spaces over X cut out by étaleness of the structure morphism, and that slice is essentially small because the algebraic spaces over S are.

instance essentiallySmall_spacesEtale (X : AlgebraicSpaces B S hS) :
    EssentiallySmall.{u} (SpacesEtale B S hS X)

AlgebraicGeometry.Space.SpacesEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 81. The attribute's comment: “objects and morphisms”.

Stacks 03G0. The spaces-étale site of X: the category of algebraic spaces étale over X, with the commutative triangles over X as morphisms.

abbrev SpacesEtale

AlgebraicGeometry.Space.SpacesEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 118. The attribute's comment: “coverings”.

Stacks 03G0. A family in the spaces-étale site of X covers when every point of its target lifts to a point of some member of the family.

abbrev IsCovering (E : Covering (SpacesEtale B S hS X)) : Prop

AlgebraicGeometry.Space.SpacesEtale.isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 145. The attribute's comment: “site axioms”.

Stacks 03G0. Joint surjectivity on points of families in the spaces-étale site of X satisfies the site axioms.

theorem isSite : IsSite (IsCovering B S hS X)

Tag 03G1, a lemma

Tag 03G1 in the Stacks Project.

AlgebraicGeometry.Space.comparisonFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleComparison.lean, line 154. The attribute's comment: “the functor”.

Stacks 03G1. The canonical inclusion of the small étale site of X into its spaces-étale site: an étale scheme chart of X is an algebraic space étale over X.

def comparisonFunctor : SmallEtale B S hS X.1 ⥤ SpacesEtale B S hS X

AlgebraicGeometry.Space.comparisonFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleComparison.lean, line 162. The attribute's comment: “canonical action on objects”.

Stacks 03G1. The comparison sends a scheme chart to its Yoneda algebraic space over X.

theorem comparisonFunctor_obj (U : SmallEtale B S hS X.1) :
    ((comparisonFunctor B S hS X).obj U).1 = chartOver B S hS X U

AlgebraicGeometry.Space.comparisonFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleComparison.lean, line 167. The attribute's comment: “canonical action on arrows”.

Stacks 03G1. The comparison sends a chart morphism to its Yoneda morphism.

theorem comparisonFunctor_map {U V : SmallEtale B S hS X.1} (f : U ⟶ V) :
    HEq ((comparisonFunctor B S hS X).map f).hom.left.hom
      (yoneda.map ((SmallEtale.toOver B S hS X.1).map f))

AlgebraicGeometry.Space.comparisonFunctor_specialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleComparison.lean, line 634. The attribute's comment: “special cocontinuity”.

Stacks 03G1. The comparison functor is special cocontinuous in the sense of Stacks 03CG.

theorem comparisonFunctor_specialCocontinuous :
    IsSpecialCocontinuous (SmallEtale.topology B S hS X.1) (SpacesEtale.topology B S hS X)
      (comparisonFunctor B S hS X)

AlgebraicGeometry.Space.comparisonFunctor_sheafEquivalence, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleComparison.lean, line 654. The attribute's comment: “equivalence of topoi”.

Stacks 03G1. Restriction along the comparison functor is an equivalence of sheaf categories, for sheaves valued in any category with the limits needed to define the restriction.

instance comparisonFunctor_sheafEquivalence (A : Type w) [Category.{w'} A]
    [∀ Y, HasLimitsOfShape (StructuredArrow Y (comparisonFunctor B S hS X).op) A] :
    ((comparisonFunctor B S hS X).sheafPushforwardContinuous A
      (SmallEtale.topology B S hS X.1)
      (SpacesEtale.topology B S hS X)).IsEquivalence

Tag 03H7, a remark

Tag 03H7 in the Stacks Project.

AlgebraicGeometry.Space.exists_etaleChart_singleton_covering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafConditionOneElement.lean, line 96. The attribute's comment: “the one-element covering by a scheme”.

Let U be an algebraic space étale over X. There is an étale scheme chart V of X and a morphism V → U of the spaces-étale site which is étale and surjective, and the one-element family {V → U} is a covering family of the spaces-étale site of X.

theorem exists_etaleChart_singleton_covering (U : SpacesEtale B S hS X) :
    ∃ (V : SmallEtale B S hS X.1) (f : (comparisonFunctor B S hS X).obj V ⟶ U),
      IsEtale B S hS ((SpacesEtale.toSpaces B S hS X).map f).hom ∧
      IsSurjective B S hS ((SpacesEtale.toSpaces B S hS X).map f).hom ∧
      SpacesEtale.IsCovering B S hS X ⟨U, PreZeroHypercover.singleton.{u + 1} f⟩

AlgebraicGeometry.Space.exists_etaleChart_isPullback_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafConditionOneElement.lean, line 148. The attribute's comment: “the fibre product is a scheme”.

Let U be an algebraic space étale over X, let V be an étale scheme chart of X and let f : V → U be a morphism of the spaces-étale site. Then there is an étale scheme chart W of X and a pair of morphisms p, q : W → V of the small étale site whose images under the comparison functor exhibit W as the fibre product V ×_U V in the spaces-étale site.

theorem exists_etaleChart_isPullback_self (U : SpacesEtale B S hS X)
    (V : SmallEtale B S hS X.1) (f : (comparisonFunctor B S hS X).obj V ⟶ U) :
    ∃ (W : SmallEtale B S hS X.1) (p q : W ⟶ V),
      IsPullback ((comparisonFunctor B S hS X).map p)
        ((comparisonFunctor B S hS X).map q) f f

AlgebraicGeometry.Space.exists_isLimit_fork_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSheafConditionOneElement.lean, line 227. The attribute's comment: “the equalizer diagram”.

Let X be an algebraic space over S, let P be a sheaf on the spaces-étale site of X, and write F = (comparisonFunctor).op ⋙ P for its restriction to the small étale site of X. Then for every algebraic space U étale over X there are an étale scheme chart V of X, a surjective étale morphism f : V → U of the spaces-étale site whose one-element family is a covering, and a second étale scheme chart W with morphisms p, q : W → V of the small étale site exhibiting W as V ×_U V, such that

P(U) → F(V) ⇉ F(W)

is an equalizer diagram, the two parallel arrows being restriction along p and along q.

theorem exists_isLimit_fork_of_isSheaf (P : (SpacesEtale B S hS X)ᵒᵖ ⥤ A)
    (hP : Presheaf.IsSheaf (SpacesEtale.topology B S hS X) P) (U : SpacesEtale B S hS X) :
    ∃ (V : SmallEtale B S hS X.1) (f : (comparisonFunctor B S hS X).obj V ⟶ U)
      (W : SmallEtale B S hS X.1) (p q : W ⟶ V)
      (_ : IsPullback ((comparisonFunctor B S hS X).map p)
        ((comparisonFunctor B S hS X).map q) f f)
      (w : P.map f.op ≫ ((comparisonFunctor B S hS X).op ⋙ P).map p.op =
        P.map f.op ≫
          ((comparisonFunctor B S hS X).op ⋙ P).map q.op),
      IsEtale B S hS ((SpacesEtale.toSpaces B S hS X).map f).hom ∧
      IsSurjective B S hS ((SpacesEtale.toSpaces B S hS X).map f).hom ∧
      SpacesEtale.IsCovering B S hS X ⟨U, PreZeroHypercover.singleton.{u + 1} f⟩ ∧
      Nonempty (IsLimit (Fork.ofι (P.map f.op) w))

AlgebraicGeometry.Space.exists_scheme_chart_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleComparison.lean, line 521. The attribute's comment: “a scheme chart covering the étale space”.

Stacks 03H7. Every algebraic space étale over X is covered, in the spaces-étale site of X, by a single étale scheme chart of X, namely a chosen atlas of it composed with its structure morphism.

theorem exists_scheme_chart_cover (U : SpacesEtale B S hS X) :
    ∃ (V : SmallEtale B S hS X.1) (f : (comparisonFunctor B S hS X).obj V ⟶ U),
      Sieve.generate (Presieve.singleton f) ∈ SpacesEtale.topology B S hS X U

AlgebraicGeometry.Space.exists_smallEtaleDirectImageChartEqualizerEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleDirectImageChartEqualizer.lean, line 341. The attribute's comment: “the equalizer diagram, for the direct image on the small etale sites: the sections of f_{small,*}P over an etale scheme chart V of Y are the equalizer of the sections of P over an etale scheme chart W covering X x_Y V and over a chart W' presenting the self-fibre product of W over X x_Y V”.

Tag 03H7 for the direct image on the small étale sites. Let f : X ⟶ Y be a morphism of algebraic spaces, let P be a sheaf of sets on the small étale site of X, and let V be an étale scheme chart of Y. Then there are étale scheme charts W, W' of X and two morphisms a, b : W' ⟶ W such that

(f_{small,*}P)(V) ⟶ P(W) ⇉ P(W')

is an equalizer: the sections of the direct image over V are in bijection with the sections of P over W on which restriction along a and restriction along b agree.

theorem exists_smallEtaleDirectImageChartEqualizerEquiv (f : X ⟶ Y)
    (P : Sheaf (SmallEtale.topology B S hS X.1) (Type u)) (V : SmallEtale B S hS Y.1) :
    ∃ (W W' : SmallEtale B S hS X.1) (a b : W' ⟶ W),
      Nonempty (((smallEtaleDirectImage B S hS f).obj P).obj.obj (op V) ≃
        {y : P.obj.obj (op W) // P.obj.map a.op y = P.obj.map b.op y})

AlgebraicGeometry.Space.exists_scheme_chart_self_intersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleSchemeChart.lean, line 61. The attribute's comment: “the scheme self-intersection”.

The self-intersection of a scheme chart over an object of the spaces-étale site of X is again an étale scheme chart of X, with its canonical pullback projections.

theorem exists_scheme_chart_self_intersection {U : SpacesEtale B S hS X}
    {V : SmallEtale B S hS X.1} (f : (comparisonFunctor B S hS X).obj V ⟶ U) :
    ∃ (W : SmallEtale B S hS X.1)
      (p q : (comparisonFunctor B S hS X).obj W ⟶ (comparisonFunctor B S hS X).obj V),
      IsPullback p q f f

AlgebraicGeometry.Space.sections_equalizer_of_scheme_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleSchemeChart.lean, line 129. The attribute's comment: “the equalizer diagram”.

The sections of a sheaf on the spaces-étale site of X over an object U are the equalizer of the two restriction maps from a scheme chart covering U to the scheme self-intersection of that chart.

theorem sections_equalizer_of_scheme_chart {U : SpacesEtale B S hS X}
    {V W : SmallEtale B S hS X.1} (f : (comparisonFunctor B S hS X).obj V ⟶ U)
    (p q : (comparisonFunctor B S hS X).obj W ⟶ (comparisonFunctor B S hS X).obj V)
    (hcover : Sieve.generate (Presieve.singleton f) ∈ SpacesEtale.topology B S hS X U)
    (hpullback : IsPullback p q f f)
    (G : Sheaf (SpacesEtale.topology B S hS X) (Type w)) :
    Nonempty (IsLimit (Fork.ofι (G.obj.map f.op) (f := G.obj.map p.op) (g := G.obj.map q.op)
      (by simp [← Functor.map_comp, ← op_comp, hpullback.w])))

Tag 0H01, a definition

Tag 0H01 in the Stacks Project.

AlgebraicGeometry.Space.AffineEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleSite.lean, line 57. The attribute's comment: “objects and morphisms”.

The affine étale site of a presheaf F on the big fppf site of S, as a category: its objects are the étale charts of F with affine source, and its morphisms are the morphisms of schemes whose triangle over F commutes.

abbrev AffineEtale

AlgebraicGeometry.Space.AffineEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleSite.lean, line 85. The attribute's comment: “coverings”.

A family of affine étale charts of F is a covering family exactly when it is a covering family of the small étale site and its index type is finite.

abbrev IsCovering (E : Covering (AffineEtale B S hS F)) : Prop

Tag 04JS, a lemma

Tag 04JS in the Stacks Project.

AlgebraicGeometry.Space.AffineEtale.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleDenseSubsite.lean, line 476.

The inclusion of the affine étale charts of an algebraic space into all its étale charts is a special cocontinuous functor; in particular it is a dense subsite inclusion, and so induces an equivalence between the affine étale topos and the small étale topos.

theorem AffineEtale.inclusion_isSpecialCocontinuous
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (_hF : IsAlgebraicSpace B S hS F) :
    IsSpecialCocontinuous
      (AffineEtale.topology B S hS F)
      (SmallEtale.topology B S hS F)
      (AffineEtale.inclusion B S hS F)

Tag 04JT, a definition

Tag 04JT in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleTopos, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTopos.lean, line 48.

Stacks 04JT. The category of sheaves of sets on the small étale site of a presheaf F on the big fppf site of S; for an algebraic space, its small étale topos.

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

Tag 03G2, a lemma

Tag 03G2 in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_chartDiagram_ofArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineChartDiagramCofinal.lean, line 174. The attribute's comment: “affine chart diagrams are cofinal: covering family”.

Stacks 03G2: the affine chart diagrams over f are cofinal. Every étale scheme chart U of X carries a covering family of affine étale charts of X, each of which is the chart of X of a commuting square of étale scheme charts over f whose chart of Y is affine.

theorem exists_affine_chartDiagram_ofArrows (f : X ⟶ Y) (U : SmallEtale B S hS X.1) :
    ∃ (I : Type u) (W : I → SmallEtale B S hS X.1) (a : ∀ i, W i ⟶ U)
      (d : I → ChartDiagram B S hS X.1 Y.1 f.hom),
      (∀ i, (d i).U = W i) ∧
      (∀ i, IsAffine ((SmallEtale.toOver B S hS X.1 ⋙
        BigFppfOver.toScheme B S hS).obj (W i))) ∧
      (∀ i, IsAffine ((SmallEtale.toOver B S hS Y.1 ⋙
        BigFppfOver.toScheme B S hS).obj (d i).V)) ∧
      Sieve.ofArrows W a ∈ SmallEtale.topology B S hS X.1 U

AlgebraicGeometry.Space.generate_affineChartDiagram_mem_topology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineChartDiagramCofinal.lean, line 257. The attribute's comment: “affine chart diagrams are cofinal: covering sieve”.

Stacks 03G2: the affine chart diagrams over f are cofinal, in sieve form. The affine étale charts of X which are the chart of X of a commuting square of étale scheme charts over f whose chart of Y is affine and satisfies a condition Q holding on all affine charts generate a covering sieve of every étale chart of X.

theorem generate_affineChartDiagram_mem_topology (f : X ⟶ Y)
    (Q : SmallEtale B S hS Y.1 → Prop)
    (hQ : ∀ V : SmallEtale B S hS Y.1,
      IsAffine ((SmallEtale.toOver B S hS Y.1 ⋙ BigFppfOver.toScheme B S hS).obj V) → Q V)
    (U : SmallEtale B S hS X.1) :
    Sieve.generate (fun (Z : SmallEtale B S hS X.1) (_ : Z ⟶ U) =>
      IsAffine ((SmallEtale.toOver B S hS X.1 ⋙ BigFppfOver.toScheme B S hS).obj Z) ∧
      ∃ d : ChartDiagram B S hS X.1 Y.1 f.hom, ∃ _ : d.U = Z,
        IsAffine ((SmallEtale.toOver B S hS Y.1 ⋙ BigFppfOver.toScheme B S hS).obj d.V) ∧
          Q d.V) ∈ SmallEtale.topology B S hS X.1 U

AlgebraicGeometry.Space.smallToposMorphism_comp_abelianInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianInverseImageSquare.lean, line 258. The attribute's comment: “part (3), inverse-image composition at abelian coefficients”.

Stacks 03G2, part (3), inverse-image composition, at abelian coefficients: (f ≫ g)⁻¹ ≅ g⁻¹ ⋙ f⁻¹ for the inverse image of abelian sheaves along the morphisms of small étale topoi.

It is AlgebraicGeometry.Space.smallToposMorphism_comp_inverseImage, the same statement for sheaves of sets, carried over by StacksTag03LR.abelianInverseImageCompIso.

def smallToposMorphism_comp_abelianInverseImage (f : X ⟶ Y) (g : Y ⟶ Z) :
    Sites.abelianInverseImage (smallToposMorphism B S hS (f ≫ g)) ≅
      Sites.abelianInverseImage (smallToposMorphism B S hS g) ⋙
        Sites.abelianInverseImage (smallToposMorphism B S hS f)

AlgebraicGeometry.Space.smallBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 162. The attribute's comment: “part (4), base change on scheme charts”.

For a morphism f whose underlying morphism of presheaves is representable, base change along f of étale scheme charts of Y, as a functor to étale scheme charts of X.

noncomputable def smallBaseChange {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    SmallEtale B S hS Y.1 ⥤ SmallEtale B S hS X.1

AlgebraicGeometry.Space.smallBaseChange_projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 187. The attribute's comment: “part (4), projection of pulled-back scheme charts”.

The cartesian projection from a pulled-back scheme chart to the original chart, viewed as a morphism of algebraic spaces.

noncomputable def smallBaseChange_projection {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    (smallBaseChange B S hS f hf ⋙ comparisonFunctor B S hS X) ⋙
        SpacesEtale.toSpaces B S hS X ⟶
      comparisonFunctor B S hS Y ⋙ SpacesEtale.toSpaces B S hS Y

AlgebraicGeometry.Space.smallBaseChange_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 204. The attribute's comment: “part (4), cartesian scheme-chart base change”.

The base change of an étale scheme chart is cartesian after passage to algebraic spaces.

theorem smallBaseChange_isPullback {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) (V : SmallEtale B S hS Y.1) :
    IsPullback ((smallBaseChange_projection B S hS f hf).app V)
      ((smallBaseChange B S hS f hf ⋙ comparisonFunctor B S hS X).obj V).1.hom
      ((comparisonFunctor B S hS Y).obj V).1.hom f

AlgebraicGeometry.Space.smallBaseChange_comparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 242. The attribute's comment: “part (4), comparison square”.

The square formed by small and spaces-étale base change and the comparison functors commutes up to its canonical natural isomorphism.

noncomputable def smallBaseChange_comparison {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    smallBaseChange B S hS f hf ⋙ comparisonFunctor B S hS X ≅
      comparisonFunctor B S hS Y ⋙ (spacesBaseChange B S hS f).functor

AlgebraicGeometry.Space.smallBaseChange_comparison_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 284. The attribute's comment: “part (4), comparison of cartesian projections”.

The comparison isomorphism AlgebraicGeometry.Space.smallBaseChange_comparison is compatible with the cartesian projections to the original chart.

theorem smallBaseChange_comparison_projection {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) (V : SmallEtale B S hS Y.1) :
    ((smallBaseChange_comparison B S hS f hf).hom.app V).hom.left ≫
        (spacesBaseChange B S hS f).projection.app ((comparisonFunctor B S hS Y).obj V) =
      (smallBaseChange_projection B S hS f hf).app V

AlgebraicGeometry.Space.smallBaseChange_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 344. The attribute's comment: “part (4), small-site morphism”.

Base change of étale scheme charts is a morphism of small étale sites.

theorem smallBaseChange_isMorphismOfSites {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    _root_.IsMorphismOfSites.{u + 1} (smallBaseChange B S hS f hf)
      (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1)

AlgebraicGeometry.Space.smallBaseChange_topos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 364. The attribute's comment: “part (4), induced morphism of topoi”.

The direct image of AlgebraicGeometry.Space.smallToposMorphism is isomorphic to the direct image along the morphism of small étale sites given by base change on scheme charts.

noncomputable def smallBaseChange_topos {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f hf).toIsContinuous
    (smallToposMorphism B S hS f).pushforward ≅
      (smallBaseChange B S hS f hf).sheafPushforwardContinuous (Type (u + 1))
        (SmallEtale.topology B S hS Y.1) (SmallEtale.topology B S hS X.1)

AlgebraicGeometry.Space.smallBaseChange_topos_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 381. The attribute's comment: “part (4), canonical topos comparison coherence”.

The isomorphism AlgebraicGeometry.Space.smallBaseChange_topos, composed with the comparison AlgebraicGeometry.Space.smallBaseChange_pushforward_comparison, is AlgebraicGeometry.Space.smallToposMorphism_comparison.

theorem smallBaseChange_topos_comparison {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom)
    (F : Sheaf (SpacesEtale.topology B S hS X) (Type (u + 1))) :
    letI := (smallBaseChange_isMorphismOfSites B S hS f hf).toIsContinuous
    (smallBaseChange_topos B S hS f hf).hom.app
        (((comparisonFunctor B S hS X).sheafPushforwardContinuous (Type (u + 1))
          (SmallEtale.topology B S hS X.1) (SpacesEtale.topology B S hS X)).obj F) ≫
      (smallBaseChange_pushforward_comparison B S hS f hf).hom.app F =
      (smallToposMorphism_comparison B S hS f).hom.app F

AlgebraicGeometry.Space.smallToposMorphism_comp_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 400. The attribute's comment: “part (3), canonical composition coherence”.

The small-site composition isomorphism AlgebraicGeometry.Space.smallToposMorphism_comp is precisely the transport of the cartesian composition on the spaces-étale site through the comparison equivalences, on every sheaf.

theorem smallToposMorphism_comp_comparison {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) (F : Sheaf (SpacesEtale.topology B S hS X) (Type (u + 1))) :
    (smallToposMorphism B S hS g).pushforward.map
        ((smallToposMorphism_comparison B S hS f).hom.app F) ≫
      (smallToposMorphism_comparison B S hS g).hom.app
        (((spacesBaseChange B S hS f).functor.sheafPushforwardContinuous (Type (u + 1))
          (SpacesEtale.topology B S hS Y) (SpacesEtale.topology B S hS X)).obj F) ≫
      ((comparisonFunctor B S hS Z).sheafPushforwardContinuous (Type (u + 1))
        (SmallEtale.topology B S hS Z.1) (SpacesEtale.topology B S hS Z)).map
          ((spacesBaseChange_pushforward_comp B S hS f g).hom.app F) =
    (smallToposMorphism_comp B S hS f g).hom.app
        (((comparisonFunctor B S hS X).sheafPushforwardContinuous (Type (u + 1))
          (SmallEtale.topology B S hS X.1) (SpacesEtale.topology B S hS X)).obj F) ≫
      (smallToposMorphism_comparison B S hS (f ≫ g)).hom.app F

AlgebraicGeometry.Space.smallToposMorphism_comp_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleBaseChange.lean, line 426. The attribute's comment: “part (3), composition mate coherence”.

The inverse-image composition isomorphism AlgebraicGeometry.Space.smallToposMorphism_comp_inverseImage is the adjoint mate of the direct-image composition isomorphism AlgebraicGeometry.Space.smallToposMorphism_comp.

theorem smallToposMorphism_comp_mate {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (F : Sheaf (SmallEtale.topology B S hS Z.1) (Type (u + 1)))
    (G : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1)))
    (h : ((MorphismOfTopoi.comp (smallToposMorphism B S hS g)
      (smallToposMorphism B S hS f)).inverseImage).obj F ⟶ G) :
    (smallToposMorphism B S hS (f ≫ g)).adj.homEquiv F G
        ((smallToposMorphism_comp_inverseImage B S hS f g).hom.app F ≫ h) =
      (MorphismOfTopoi.comp (smallToposMorphism B S hS g)
          (smallToposMorphism B S hS f)).adj.homEquiv F G h ≫
        (smallToposMorphism_comp B S hS f g).hom.app G

AlgebraicGeometry.Space.spacesBaseChange_comp_inv_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePushforwardAssoc.lean, line 195. The attribute's comment: “part (2), associativity of the composition isomorphism”.

Stacks 03G2, part (2), associativity. The base-change composition isomorphisms of the spaces-étale sites obey the associativity cocycle law. This is the cocycle law for CategoryTheory.Over.pullbackComp, restricted to the objects étale over the base.

theorem spacesBaseChange_comp_inv_assoc (f : V ⟶ W) (g : W ⟶ X) (h : X ⟶ Y)
    (U : SpacesEtale B S hS Y) :
    (spacesBaseChange_comp B S hS (f ≫ g) h).inv.app U ≫
        (spacesBaseChange_comp B S hS f g).inv.app
          ((spacesBaseChange B S hS h).functor.obj U) =
      (spacesBaseChange_comp B S hS f (g ≫ h)).inv.app U ≫
        (spacesBaseChange B S hS f).functor.map
          ((spacesBaseChange_comp B S hS g h).inv.app U)

AlgebraicGeometry.Space.smallToposMorphismTypeU_comp_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePushforwardAssoc.lean, line 235. The attribute's comment: “part (3), associativity of the composition isomorphism”.

Stacks 03G2, part (3), associativity. The composition isomorphisms of the direct images of the small étale topoi obey the associativity cocycle law.

theorem smallToposMorphismTypeU_comp_assoc (f : V ⟶ W) (g : W ⟶ X) (h : X ⟶ Y)
    (M : Sheaf (SmallEtale.topology B S hS V.1) (Type u)) :
    (smallToposMorphismTypeU B S hS h).pushforward.map
          ((smallToposMorphismTypeU_comp B S hS f g).hom.app M) ≫
        (smallToposMorphismTypeU_comp B S hS (f ≫ g) h).hom.app M =
      (smallToposMorphismTypeU_comp B S hS g h).hom.app
          ((smallToposMorphismTypeU B S hS f).pushforward.obj M) ≫
        (smallToposMorphismTypeU_comp B S hS f (g ≫ h)).hom.app M

AlgebraicGeometry.Space.smallToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleToposMorphism.lean, line 107. The attribute's comment: “part (3), morphism of small étale topoi”.

The morphism of small étale topoi induced by a morphism f : X ⟶ Y of algebraic spaces: the morphism of spaces-étale topoi of the base-change morphism of sites, transported along the comparison equivalences AlgebraicGeometry.Space.smallEtaleToposEquiv.

noncomputable def smallToposMorphism {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    MorphismOfTopoi
      (Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1)))
      (Sheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)))

AlgebraicGeometry.Space.smallToposMorphism_comparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleToposMorphism.lean, line 117. The attribute's comment: “part (3), comparison with the spaces-étale topoi”.

The small étale direct image agrees, through the comparison equivalences, with the direct image of the spaces-étale morphism of sites.

noncomputable def smallToposMorphism_comparison {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    ((comparisonFunctor B S hS X).sheafPushforwardContinuous (Type (u + 1))
          (SmallEtale.topology B S hS X.1) (SpacesEtale.topology B S hS X)) ⋙
        (smallToposMorphism B S hS f).pushforward ≅
      ((spacesBaseChange B S hS f).functor.sheafPushforwardContinuous (Type (u + 1))
          (SpacesEtale.topology B S hS Y) (SpacesEtale.topology B S hS X)) ⋙
        (comparisonFunctor B S hS Y).sheafPushforwardContinuous (Type (u + 1))
          (SmallEtale.topology B S hS Y.1) (SpacesEtale.topology B S hS Y)

AlgebraicGeometry.Space.smallToposMorphism_comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleToposMorphism.lean, line 145. The attribute's comment: “part (3), compatibility with composition”.

The small étale direct image is compatible with composition: the composite of the morphisms of topoi of f and g has the same direct image as the morphism of topoi of f ≫ g.

noncomputable def smallToposMorphism_comp {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) :
    (MorphismOfTopoi.comp (smallToposMorphism B S hS g)
        (smallToposMorphism B S hS f)).pushforward ≅
      (smallToposMorphism B S hS (f ≫ g)).pushforward

AlgebraicGeometry.Space.smallToposMorphism_comp_inverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleToposMorphism.lean, line 160. The attribute's comment: “part (3), inverse-image composition”.

The inverse-image composition isomorphism, oriented for pullback of sheaves: (f ≫ g)⁻¹ ≅ g⁻¹ ⋙ f⁻¹. It is the adjoint mate of AlgebraicGeometry.Space.smallToposMorphism_comp.

noncomputable def smallToposMorphism_comp_inverseImage {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    (smallToposMorphism B S hS (f ≫ g)).inverseImage ≅
      (smallToposMorphism B S hS g).inverseImage ⋙
        (smallToposMorphism B S hS f).inverseImage

AlgebraicGeometry.Space.spacesBaseChange_comp_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesBaseChangeAssoc.lean, line 328. The attribute's comment: “part (2), associativity of the composition isomorphism”.

Stacks 03G2, part (2). The composition isomorphism of spaces-étale base change is associative: for f : X ⟶ Y, g : Y ⟶ Z and h : Z ⟶ W the two ways of identifying the threefold iterated base change with base change along f ≫ g ≫ h — first contracting g and h, or first contracting f and g — agree.

This is the coherence that makes AlgebraicGeometry.Space.spacesBaseChange_comp a genuine compatibility of base change with composition, and it is the spaces-étale analogue of CategoryTheory.GrothendieckTopology.overMapPullback_assoc.

theorem spacesBaseChange_comp_assoc {W X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (h : Z ⟶ W) :
    Functor.isoWhiskerRight (spacesBaseChange_comp B S hS g h)
          (spacesBaseChange B S hS f).functor ≪≫ spacesBaseChange_comp B S hS f (g ≫ h) =
      Functor.associator _ _ _ ≪≫
        Functor.isoWhiskerLeft (spacesBaseChange B S hS h).functor
          (spacesBaseChange_comp B S hS f g) ≪≫
        spacesBaseChange_comp B S hS (f ≫ g) h ≪≫
        eqToIso (congrArg (fun k => (spacesBaseChange B S hS k).functor)
          (Category.assoc f g h))

AlgebraicGeometry.Space.smallToposMorphism_comp_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesBaseChangeAssoc.lean, line 427. The attribute's comment: “part (3), associativity of the composition isomorphism”.

Stacks 03G2, part (3). The direct-image composition isomorphism of the morphisms of small étale topoi is associative: for f : X ⟶ Y, g : Y ⟶ Z and h : Z ⟶ W the two ways of identifying the threefold composite of direct images with the direct image of f ≫ g ≫ h agree.

This is the coherence that makes the construction of AlgebraicGeometry.Space.smallToposMorphism "compatible with compositions" in the sense of part (3) of the tag, rather than merely equipped with composition isomorphisms. It is AlgebraicGeometry.Space.spacesBaseChange_pushforward_comp_assoc' transported along the comparison equivalences of Stacks 03G1 by MorphismOfTopoi.transport_comp_pushforward_comp_assoc.

theorem smallToposMorphism_comp_assoc {W X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) (h : Z ⟶ W) :
    Functor.isoWhiskerRight (smallToposMorphism_comp B S hS f g)
          (smallToposMorphism B S hS h).pushforward ≪≫
        smallToposMorphism_comp B S hS (f ≫ g) h ≪≫
        eqToIso (congrArg (fun k => (smallToposMorphism B S hS k).pushforward)
          (Category.assoc f g h)) =
      Functor.associator _ _ _ ≪≫
        Functor.isoWhiskerLeft (smallToposMorphism B S hS f).pushforward
          (smallToposMorphism_comp B S hS g h) ≪≫
        smallToposMorphism_comp B S hS f (g ≫ h)

AlgebraicGeometry.Space.spacesBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleBaseChange.lean, line 152. The attribute's comment: “part (1), the cartesian base-change functor”.

Stacks 03G2, part (1). The canonical base-change datum on the spaces-étale sites: the base change CategoryTheory.Over.pullback f of the slice over Y, restricted to the objects étale over the base, with the first projection of the fibre product.

noncomputable def spacesBaseChange {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    SpacesBaseChange B S hS f

AlgebraicGeometry.Space.spacesBaseChange_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleBaseChange.lean, line 218. The attribute's comment: “part (1), morphism of sites”.

Stacks 03G2, part (1). Base change defines a morphism of sites in the direction X → Y: it is continuous, the spaces-étale site of Y has a terminal object and fibre products, and base change preserves both.

theorem spacesBaseChange_isMorphismOfSites {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    (spacesBaseChange B S hS f).functor.IsMorphismOfSites
      (SpacesEtale.topology B S hS Y) (SpacesEtale.topology B S hS X)

AlgebraicGeometry.Space.spacesBaseChange_comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleBaseChange.lean, line 230. The attribute's comment: “part (2), canonical composition isomorphism”.

Stacks 03G2, part (2). Base change along a composite is canonically isomorphic to the iterated base change, by CategoryTheory.Over.pullbackComp restricted to the objects étale over the base.

noncomputable def spacesBaseChange_comp {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) :
    (spacesBaseChange B S hS g).functor ⋙ (spacesBaseChange B S hS f).functor ≅
      (spacesBaseChange B S hS (f ≫ g)).functor

AlgebraicGeometry.Space.spacesBaseChange_comp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpacesEtaleBaseChange.lean, line 245. The attribute's comment: “part (2), compatibility with cartesian projections”.

Stacks 03G2, part (2). The composition isomorphism is compatible with the cartesian projections to the original object, which pins it down.

theorem spacesBaseChange_comp_projection {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z) (V : SpacesEtale B S hS Z) :
    ((spacesBaseChange_comp B S hS f g).hom.app V).hom.left ≫
        (spacesBaseChange B S hS (f ≫ g)).projection.app V =
      (spacesBaseChange B S hS f).projection.app
          ((spacesBaseChange B S hS g).functor.obj V) ≫
        (spacesBaseChange B S hS g).projection.app V

Tag 03G3, a definition

Tag 03G3 in the Stacks Project.

AlgebraicGeometry.Space.FMap, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRingedToposHom.lean, line 229.

A map of sections along a morphism of algebraic spaces, natural under simultaneous étale restriction of the source and target charts.

structure FMap (P : (SmallEtale B S hS F)ᵒᵖ ⥤ Type v)
    (Q : (SmallEtale B S hS G)ᵒᵖ ⥤ Type w)

Tag 03G4, a lemma

Tag 03G4 in the Stacks Project.

AlgebraicGeometry.Space.chartCorrespondence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartCorrespondence.lean, line 689. The attribute's comment: “f-maps are exactly maps into the direct image”.

The chart correspondence of a morphism f : X ⟶ Y of algebraic spaces: a bijection between the f-maps from a sheaf of sets Q on the small étale site of Y to a sheaf of sets P on the small étale site of X, and the homomorphisms from Q into the direct image of P along AlgebraicGeometry.Space.smallEtaleRingedToposHom, satisfying the sectionwise characterization AlgebraicGeometry.Space.IsChartCorrespondence.

noncomputable def chartCorrespondence (f : X ⟶ Y)
    (P : Sheaf (SmallEtale.topology B S hS X.1) (Type u))
    (Q : Sheaf (SmallEtale.topology B S hS Y.1) (Type u)) :
    { e : FMap B S hS X.1 Y.1 f.hom P.obj Q.obj ≃
        (Q ⟶ (smallEtaleRingedToposHom B S hS f).toToposHom.pushforward.obj P) //
      IsChartCorrespondence B S hS f P Q e }

AlgebraicGeometry.Space.fmapInverseImageEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartCorrespondence.lean, line 701. The attribute's comment: “f-maps are exactly maps out of the inverse image”.

f-maps from Q to P are exactly homomorphisms from the inverse image of Q into P, the inverse image being that of AlgebraicGeometry.Space.smallEtaleRingedToposHom.

noncomputable def fmapInverseImageEquiv (f : X ⟶ Y)
    (P : Sheaf (SmallEtale.topology B S hS X.1) (Type u))
    (Q : Sheaf (SmallEtale.topology B S hS Y.1) (Type u)) :
    FMap B S hS X.1 Y.1 f.hom P.obj Q.obj ≃
      ((smallEtaleRingedToposHom B S hS f).toToposHom.inverseImage.obj Q ⟶ P)

AlgebraicGeometry.Space.fMapEquivPushforwardHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartCorrespondence.lean, line 709. The attribute's comment: “parts (1) and (3)”.

A map on sections over every commutative pair of étale scheme charts over f is equivalently a map of sheaves into the small étale direct image.

noncomputable def fMapEquivPushforwardHom :
    FMap B S hS X.1 Y.1 f.hom F.obj G.obj ≃
      (G ⟶ (smallToposMorphism B S hS f).pushforward.obj F)

AlgebraicGeometry.Space.fMapEquivInverseImageHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartCorrespondence.lean, line 788. The attribute's comment: “parts (2) and (3)”.

A map on sections over every commutative pair of étale scheme charts over f is equivalently a map of sheaves out of the small étale inverse image. The bijection is the composite of AlgebraicGeometry.Space.fMapEquivPushforwardHom with the adjunction bijection of the morphism of small étale topoi.

noncomputable def fMapEquivInverseImageHom :
    FMap B S hS X.1 Y.1 f.hom F.obj G.obj ≃
      ((smallToposMorphism B S hS f).inverseImage.obj G ⟶ F)

AlgebraicGeometry.Space.fMapEquivPushforwardHom_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartCorrespondence.lean, line 803. The attribute's comment: “canonical action on chart sections”.

The bijection AlgebraicGeometry.Space.fMapEquivPushforwardHom is the canonical one. Transport a sheaf F on the small étale site of X through an isomorphism with the restriction of a spaces-étale sheaf H; then on a diagram d of étale scheme charts over f the transported f-map is restriction of the section of the direct image along any arrow from the chart of X into the cartesian base change of the chart of Y whose composite with the cartesian projection is the Yoneda morphism of the vertical morphism of d.

theorem fMapEquivPushforwardHom_chart
    (H : Sheaf (SpacesEtale.topology B S hS X) (Type (u + 1)))
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1)))
    (i : F ≅ (comparisonRestriction B S hS X).obj H)
    (G : Sheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)))
    (ξ : FMap B S hS X.1 Y.1 f.hom F.obj G.obj)
    (d : ChartDiagram B S hS X.1 Y.1 f.hom)
    (h : (comparisonFunctor B S hS X).obj d.U ⟶ chartBaseChange B S hS f d.V)
    (hh : ((SpacesEtale.toSpaces B S hS X).map h ≫
        (spacesBaseChange B S hS f).projection.app
          ((comparisonFunctor B S hS Y).obj d.V)).hom = yoneda.map d.g)
    (s : G.obj.obj (op d.V)) :
    let ψ : G ⟶ (spacesDirectImageRestriction B S hS f).obj H :=
      fMapEquivPushforwardHom B S hS f F G ξ ≫
        (smallToposMorphism B S hS f).pushforward.map i.hom ≫
        (smallToposMorphism_comparison B S hS f).hom.app H
    (((sheafToPresheaf (SmallEtale.topology B S hS X.1)
      (Type (u + 1))).map i.hom).app (op d.U)) (ξ.app d s) =
      H.obj.map h.op
        (((sheafToPresheaf (SmallEtale.topology B S hS Y.1)
          (Type (u + 1))).map ψ).app (op d.V) s)

Tag 03LP, a lemma

Tag 03LP in the Stacks Project.

AlgebraicGeometry.Space.abelianEtaleRestriction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianExtensionByZero.lean, line 61. The attribute's comment: “restriction of abelian sheaves”.

Restriction of abelian étale sheaves along an étale morphism f : X ⟶ Y of algebraic spaces: restriction along postcomposition with f.

abbrev abelianEtaleRestriction (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    Sheaf (SmallEtale.topology B S hS Y.1) AddCommGrpCat.{u} ⥤
      Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u}

AlgebraicGeometry.Space.smallToposMorphism_abelianInverseImage_obj_obj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianRestrictionInverseImage.lean, line 149. The attribute's comment: “the displayed formula for the inverse image, at abelian coefficients”.

Stacks 03LP, the displayed formula for the inverse image, at abelian coefficients. The sections of h_{small}^{-1}G over an étale chart W of U are the sections of G over the composite chart jW, as abelian groups.

This is AlgebraicGeometry.Space.smallToposMorphism_abelianInverseImageIso evaluated at G and at W; on the right-hand side the sections of a restricted sheaf are the asserted ones by definition.

noncomputable def smallToposMorphism_abelianInverseImage_obj_obj (h : U ⟶ V)
    (hh : IsEtale B S hS h.hom)
    (G : Sheaf (SmallEtale.topology B S hS V.1) AddCommGrpCat.{u + 1})
    (W : SmallEtale B S hS U.1) :
    (((Sites.abelianInverseImage (smallToposMorphism B S hS h)).obj G).obj.obj (.op W)) ≅
      G.obj.obj (.op ((smallEtalePostcomp B S hS h hh).obj W))

AlgebraicGeometry.Space.smallEtalePostcomp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePostcomp.lean, line 58. The attribute's comment: “the postcomposition functor”.

Postcomposition of an étale scheme chart with an étale morphism of algebraic spaces, as a functor between the small étale sites. Its underlying scheme and scheme morphisms are unchanged.

def smallEtalePostcomp (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    SmallEtale B S hS X.1 ⥤ SmallEtale B S hS Y.1

AlgebraicGeometry.Space.smallEtalePostcomp_obj_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePostcomp.lean, line 66. The attribute's comment: “action on charts”.

On charts, postcomposition replaces U ⟶ X by its composite with f.

theorem smallEtalePostcomp_obj_hom (f : X ⟶ Y) (hf : IsEtale B S hS f.hom)
    (U : SmallEtale B S hS X.1) :
    ((smallEtalePostcomp B S hS f hf).obj U).1.hom = U.1.hom ≫ f.hom

AlgebraicGeometry.Space.smallEtalePostcomp_map_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePostcomp.lean, line 72. The attribute's comment: “action on chart morphisms”.

On chart morphisms, postcomposition leaves the underlying scheme map unchanged.

theorem smallEtalePostcomp_map_left (f : X ⟶ Y) (hf : IsEtale B S hS f.hom)
    {U V : SmallEtale B S hS X.1} (g : U ⟶ V) :
    ((smallEtalePostcomp B S hS f hf).map g).hom.left = g.hom.left

AlgebraicGeometry.Space.smallEtalePostcomp_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePostcomp.lean, line 111. The attribute's comment: “continuity”.

Postcomposition along an étale morphism of algebraic spaces is continuous for the small étale topologies, so that restriction along it carries sheaves on the small étale site of Y to sheaves on that of X.

instance smallEtalePostcomp_isContinuous (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    (smallEtalePostcomp B S hS f hf).IsContinuous
      (SmallEtale.topology B S hS X.1) (SmallEtale.topology B S hS Y.1)

AlgebraicGeometry.Space.smallEtalePostcomp_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePostcompCocontinuous.lean, line 96. The attribute's comment: “cocontinuity”.

Stacks 03LP. Postcomposition along an étale morphism of algebraic spaces is cocontinuous for the small étale topologies: a covering sieve of the composite chart jU pulls back to a covering sieve of U.

This is AlgebraicGeometry.Space.SmallEtale.smallEtalePostcomp_cover_lift, which in turn comes from the comparison of the slice of the small étale site of X at U with the slice of that of Y at jU — Stacks' remark that a covering of jU in Y_étale is the same thing as a covering of U in X_étale.

instance smallEtalePostcomp_isCocontinuous (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    (smallEtalePostcomp B S hS f hf).IsCocontinuous
      (SmallEtale.topology B S hS X.1) (SmallEtale.topology B S hS Y.1)

AlgebraicGeometry.Space.smallToposMorphism_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestriction.lean, line 129. The attribute's comment: “the associated morphism of topoi”.

For an étale morphism of algebraic spaces the small étale direct image is the direct image attached to the cocontinuous postcomposition functor on charts.

def smallToposMorphism_pushforwardIso (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    (smallToposMorphism B S hS f).pushforward ≅
      (smallEtalePostcomp B S hS f hf).sheafPushforwardCocontinuous (Type (u + 1))
        (SmallEtale.topology B S hS X.1) (SmallEtale.topology B S hS Y.1)

AlgebraicGeometry.Space.smallToposMorphism_inverseImageObjObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestriction.lean, line 140. The attribute's comment: “the formula on sections”.

Sections of the small étale inverse image along an étale morphism over a chart U ⟶ X are the sections of the original sheaf over the composite chart U ⟶ Y.

def smallToposMorphism_inverseImageObjObjIso (f : X ⟶ Y) (hf : IsEtale B S hS f.hom)
    (G : Sheaf (SmallEtale.topology B S hS Y.1) (Type (u + 1)))
    (U : SmallEtale B S hS X.1) :
    ((smallToposMorphism B S hS f).inverseImage.obj G).obj.obj (Opposite.op U) ≅
      G.obj.obj (Opposite.op ((smallEtalePostcomp B S hS f hf).obj U))

AlgebraicGeometry.Space.smallToposMorphism_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestrictionInverseImage.lean, line 215. The attribute's comment: “the morphism of topoi attached to j is f_small”.

Stacks 03LQ, and the remaining assertion of Stacks 03LP: for an étale morphism h : U ⟶ V of algebraic spaces, the inverse image of the morphism of small étale topoi h_{small} of Stacks 03G2, part (3) is restriction along the postcomposition functor j of Stacks 03LP, i.e. G|_{U_étale} = h_{small}^{-1}G.

The small étale morphism of topoi is the transport of the spaces-étale one along the comparison equivalences of Stacks 03G1, so this is AlgebraicGeometry.Space.spacesToposMorphism_inverseImageIso conjugated by those equivalences, the comparison with small étale postcomposition being the identity.

noncomputable def smallToposMorphism_inverseImageIso (h : U ⟶ V) (hh : IsEtale B S hS h.hom) :
    (smallToposMorphism B S hS h).inverseImage ≅
      (smallEtalePostcomp B S hS h hh).sheafPushforwardContinuous (Type (u + 1))
        (SmallEtale.topology B S hS U.1) (SmallEtale.topology B S hS V.1)

AlgebraicGeometry.Space.smallToposMorphism_inverseImage_obj_obj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestrictionInverseImage.lean, line 253. The attribute's comment: “the displayed formula for the inverse image”.

Stacks 03LP, the displayed formula for the inverse image. The sections of h_{small}^{-1}G over an étale chart W of U are the sections of G over the composite chart jW.

This is AlgebraicGeometry.Space.smallToposMorphism_inverseImageIso evaluated at G and at W, the sections of a restricted sheaf being the asserted ones by definition.

noncomputable def smallToposMorphism_inverseImage_obj_obj (h : U ⟶ V)
    (hh : IsEtale B S hS h.hom)
    (G : Sheaf (SmallEtale.topology B S hS V.1) (Type (u + 1)))
    (W : SmallEtale B S hS U.1) :
    (((smallToposMorphism B S hS h).inverseImage.obj G).obj.obj (.op W)) ≅
      G.obj.obj (.op ((smallEtalePostcomp B S hS h hh).obj W))

Tag 03LQ, an equation

Tag 03LQ in the Stacks Project.

AlgebraicGeometry.Space.smallToposMorphism_abelianInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianRestrictionInverseImage.lean, line 126. The attribute's comment: “at abelian coefficients: h_small^{-1} of an abelian sheaf is restriction along j”.

Stacks 03LQ at abelian coefficients. For an étale morphism h : U ⟶ V of algebraic spaces, the inverse image of abelian sheaves along the morphism of small étale topoi h_{small} of Stacks 03G2, part (3) is restriction along the postcomposition functor j of Stacks 03LP, i.e. G|_{U_étale} = h_{small}^{-1}G for G an abelian sheaf.

AlgebraicGeometry.Space.smallToposMorphism_inverseImageIso is the same statement for sheaves of sets, which is the form the source states it in. The right-hand side is AlgebraicGeometry.Space.etaleAbelianRestriction.

Both sides are the conjugate, by the identification of abelian sheaves with commutative group objects of the topos, of CategoryTheory.Functor.mapCommGrp of the corresponding set-level functor: for the inverse image that is the definition of CategoryTheory.Sites.abelianInverseImage, and for restriction along j it is Stacks.Sites.AbelianPullback.abelianSheafPushforwardIso. So the set-level isomorphism is carried across by CategoryTheory.Functor.mapCommGrpNatIso.

noncomputable def smallToposMorphism_abelianInverseImageIso (h : U ⟶ V)
    (hh : IsEtale B S hS h.hom) :
    Sites.abelianInverseImage (smallToposMorphism B S hS h) ≅
      (smallEtalePostcomp B S hS h hh).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S hS U.1) (SmallEtale.topology B S hS V.1)

AlgebraicGeometry.Space.spacesToposMorphism_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestrictionInverseImage.lean, line 180. The attribute's comment: “on the spaces-étale topoi”.

Stacks 03LQ on the spaces-étale topoi. The inverse image of the morphism of spaces-étale topoi attached to an étale morphism h : U ⟶ V is restriction along postcomposition with h.

Its direct image is restriction along base change along h, and AlgebraicGeometry.Space.spacesEtalePostcompSheafAdjunction exhibits restriction along postcomposition as another left adjoint of that functor, so the two agree by uniqueness of left adjoints.

noncomputable def spacesToposMorphism_inverseImageIso (h : U ⟶ V)
    (hh : IsEtale B S hS h.hom) :
    ((spacesBaseChange_isMorphismOfSites B S hS h).morphismOfTopoi).inverseImage ≅
      (spacesEtalePostcomp B S hS h hh).sheafPushforwardContinuous (Type (u + 1))
        (SpacesEtale.topology B S hS U) (SpacesEtale.topology B S hS V)

AlgebraicGeometry.Space.smallToposMorphism_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleRestrictionInverseImage.lean, line 215.

Stacks 03LQ, and the remaining assertion of Stacks 03LP: for an étale morphism h : U ⟶ V of algebraic spaces, the inverse image of the morphism of small étale topoi h_{small} of Stacks 03G2, part (3) is restriction along the postcomposition functor j of Stacks 03LP, i.e. G|_{U_étale} = h_{small}^{-1}G.

The small étale morphism of topoi is the transport of the spaces-étale one along the comparison equivalences of Stacks 03G1, so this is AlgebraicGeometry.Space.spacesToposMorphism_inverseImageIso conjugated by those equivalences, the comparison with small étale postcomposition being the identity.

noncomputable def smallToposMorphism_inverseImageIso (h : U ⟶ V) (hh : IsEtale B S hS h.hom) :
    (smallToposMorphism B S hS h).inverseImage ≅
      (smallEtalePostcomp B S hS h hh).sheafPushforwardContinuous (Type (u + 1))
        (SmallEtale.topology B S hS U.1) (SmallEtale.topology B S hS V.1)

Tag 03LR, a lemma

Tag 03LR in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleAbelianInverseImageSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianInverseImageSquare.lean, line 318. The attribute's comment: “the inverse-image footnote, at abelian coefficients”.

Stacks 03LR's inverse-image footnote, at abelian coefficients. For a cartesian square of algebraic spaces, the inverse image of abelian sheaves on the small étale sites may be taken around the square either way: (f')_{small}^{-1}(G|_{Y'}) = (f_{small}^{-1}G)|_{X'}, naturally in the abelian sheaf G.

As at Type coefficients the hypothesis is only that the square commute, which is AlgebraicGeometry.Space.smallEtaleAbelianInverseImageSquareIsoOfComm; the identity is pure functoriality.

Like AlgebraicGeometry.Space.smallEtaleInverseImageSquareIso, which is the same statement for sheaves of sets, this is the datum of which the inverse of AlgebraicGeometry.Space.smallEtaleAbelianPushforwardBaseChangeIso is expected to be the adjunction mate; that identification is not proved here either.

def smallEtaleAbelianInverseImageSquareIso (sq : IsPullback i f' f g) :
    Sites.abelianInverseImage (smallToposMorphism B S hS g) ⋙
        Sites.abelianInverseImage (smallToposMorphism B S hS f') ≅
      Sites.abelianInverseImage (smallToposMorphism B S hS f) ⋙
        Sites.abelianInverseImage (smallToposMorphism B S hS i)

AlgebraicGeometry.Space.smallEtalePushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePushforwardBaseChange.lean, line 202. The attribute's comment: “part (1), sheaves of sets”.

Stacks 03LR, part (1). For a cartesian square of algebraic spaces whose bottom arrow g is étale, direct image of sheaves of sets on the small étale sites commutes with restriction: f'_{small,*}(F|_{X'}) = (f_{small,*}F)|_{Y'}, naturally in the sheaf F.

Restriction is the inverse image of the small étale morphism of topoi, by Stacks 03LQ. Each of the four functors is the conjugate by the comparison equivalences of Stacks 03G1 of a restriction functor on the spaces-étale sites, where the statement is AlgebraicGeometry.Space.spacesPushforwardBaseChangeIso.

noncomputable def smallEtalePushforwardBaseChangeIso (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom) :
    (smallToposMorphism B S hS i).inverseImage ⋙
        (smallToposMorphism B S hS f').pushforward ≅
      (smallToposMorphism B S hS f).pushforward ⋙
        (smallToposMorphism B S hS g).inverseImage

AlgebraicGeometry.Space.smallEtaleInverseImageSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtalePushforwardBaseChange.lean, line 267. The attribute's comment: “the inverse-image footnote”.

The inverse-image identification around a cartesian square, built from the inverse-image composition isomorphism of Stacks 03G2, part (3) and the commutativity of the square.

It is the datum of which the inverse of smallEtalePushforwardBaseChangeIso is expected to be the adjunction mate; that identification is not proved here.

This is the parenthetical assertion of Stacks 03LR — "Also (f')^\{-1}\_\{small}(G|\_\{Y'}) = (f\_\{small}^\{-1}G)|\_\{X'} because of commutativity of the diagram and (03LQ)" — which is why the hypothesis is only sq and not the étaleness of g: the identity is pure functoriality.

noncomputable def smallEtaleInverseImageSquareIso (sq : IsPullback i f' f g) :
    (smallToposMorphism B S hS g).inverseImage ⋙
        (smallToposMorphism B S hS f').inverseImage ≅
      (smallToposMorphism B S hS f).inverseImage ⋙
        (smallToposMorphism B S hS i).inverseImage

AlgebraicGeometry.Space.isIso_smallEtaleAbelianHigherBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleAbelianBaseChangeMate.lean, line 348. The attribute's comment: “part (2): for every abelian sheaf and every degree n, the canonical comparison (R^n f_{small,} F)|_{Y'} ⟶ R^n f'_{small,}(F|_{X'}) of higher direct images is an isomorphism”.

Étale base change for higher direct images. For a cartesian square of algebraic spaces over S
X' --i--> X
|f'       |f
Y' --g--> Y
with g étale, and for every n, the canonical comparison of higher direct images of abelian sheaves on the small étale sites is an isomorphism: R^n f'_{small,*}(ℱ|_{X'}) and (R^n f_{small,*} ℱ)|_{Y'} are identified by it, naturally in the abelian sheaf ℱ.

theorem isIso_smallEtaleAbelianHigherBaseChangeMap (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom) (n : ℕ) :
    IsIso (smallEtaleAbelianHigherBaseChangeMap B S hS i f' f g sq hg n)

AlgebraicGeometry.Space.smallEtalePushforwardEtaleBaseChange_allParts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleAbelianBaseChangeMate.lean, line 382. The attribute's comment: “the whole statement as one conjunction, in the source's order: part (1), that the canonical base-change 2-cell of sheaves of sets is an isomorphism, i.e. f'_ (F|_X') = (f_ F)|_Y'; its inverse-image footnote, (f')^{-1}(G|_Y') = (f^{-1} G)|_X'; and part (2), that for every degree n the canonical comparison (R^n f_ F)|_Y' -> R^n f'_ (F|_X') of higher direct images of abelian sheaves is an isomorphism”.

Étale base change on the small étale sites. For a cartesian square of algebraic spaces over S
X' --i--> X
|f'       |f
Y' --g--> Y
with g étale, the following three assertions hold. First, the canonical base-change 2-cell f_{small,*} ∘ g_{small}^{-1} ⟶ i_{small}^{-1} ∘ f'_{small,*} of sheaves of sets is invertible, which is f'_{small,*}(ℱ|_{X'}) = (f_{small,*}ℱ)|_{Y'} naturally in ℱ. Second, (f')_{small}^{-1}(𝒢|_{Y'}) = (f_{small}^{-1}𝒢)|_{X'}. Third, in every degree n the canonical comparison (R^n f_{small,*} ℱ)|_{Y'} ⟶ R^n f'_{small,*}(ℱ|_{X'}) of higher direct images of abelian sheaves is invertible.

The second conjunct is stated as Nonempty of an isomorphism of functors; the canonical one is AlgebraicGeometry.Space.smallEtaleInverseImageSquareIso.

theorem smallEtalePushforwardEtaleBaseChange_allParts (sq : IsPullback i f' f g)
    (hg : IsEtale B S hS g.hom) :
    IsIso (properBaseChangeMap B S hS f g f' i sq) ∧
      Nonempty ((smallToposMorphism B S hS g).inverseImage ⋙
            (smallToposMorphism B S hS f').inverseImage ≅
          (smallToposMorphism B S hS f).inverseImage ⋙
            (smallToposMorphism B S hS i).inverseImage) ∧
      ∀ n : ℕ, IsIso (smallEtaleAbelianHigherBaseChangeMap B S hS i f' f g sq hg n)

AlgebraicGeometry.Space.isIso_properBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleBaseChangeMate.lean, line 821. The attribute's comment: “part (1), invertibility of the canonical base-change 2-cell”.

For a cartesian square of algebraic spaces whose bottom arrow g is étale, the base-change 2-cell f_{small,*} ∘ g_{small}^{-1} ⟶ i_{small}^{-1} ∘ f'_{small,*} is an isomorphism.

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

Tag 03LS, a lemma

Tag 03LS in the Stacks Project.

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

The cocycle condition of Stacks 03LS for the restrictions of a sheaf to the étale scheme charts of X: restricting to a chart U, then to a chart V over it, then to a chart W over that, is the same whether the last two steps are taken one at a time or the two morphisms of charts are composed first.

This is AlgebraicGeometry.Space.smallToposMorphism_comp_inverseImage_cocycle at the represented morphisms of the charts, where the three equalities of morphisms of algebraic spaces are AlgebraicGeometry.Space.chartMap_comp_chartToSpace twice and AlgebraicGeometry.Space.chartMap_comp.

theorem chartRestrictionComp_cocycle {W V U : SmallEtale B S hS X.1} (f : V ⟶ U) (g : W ⟶ V) :
    Functor.whiskerRight (chartRestrictionComp B S hS X f).hom
        (chartInverseImage B S hS X g) ≫ (chartRestrictionComp B S hS X g).hom =
    Functor.whiskerLeft (chartRestriction B S hS X U)
        (chartInverseImageComp B S hS X f g).hom ≫
      (chartRestrictionComp B S hS X (g ≫ f)).hom

AlgebraicGeometry.Space.chartGlueingEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartGlueingEquivalence.lean, line 598.

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

The proof is the one the source gives: the chartwise inverse image is restriction along postcomposition (Stacks 03LQ, through Stacks 03LP), so the chartwise data are the slice-indexed data of Stacks 0GWK read through the comparison equivalence of Stacks 04M0 (AlgebraicGeometry.Space.sliceToChartFunctor, an equivalence), and the chartwise description is the slice-indexed one read through it (AlgebraicGeometry.Space.chartGlueingFunctorIso).

def chartGlueingEquivalence :
    Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1)) ≌ ChartGlueingData B S hS X

AlgebraicGeometry.Space.chartInverseImageComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartSheaves.lean, line 112. The attribute's comment: “canonical comparison of inverse images”.

Stacks 03LS. The canonical comparison of successive chartwise inverse images with the inverse image along the composite morphism of charts: it is the adjoint-mate composition isomorphism of Stacks 03G2, part (3), read through the equality chartMap g ≫ chartMap f = chartMap (g ≫ f).

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

AlgebraicGeometry.Space.chartRestrictionComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleChartSheaves.lean, line 132. The attribute's comment: “compatibility of chart restriction with inverse image”.

Stacks 03LS. Restriction to a chart commutes canonically with further restriction 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 chartRestrictionComp {V U : SmallEtale B S hS X.1} (f : V ⟶ U) :
    chartRestriction B S hS X U ⋙ chartInverseImage B S hS X f ≅
      chartRestriction B S hS X V

Tag 05YY, a lemma

Tag 05YY in the Stacks Project.

AlgebraicGeometry.Space.presentationPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtalePresentationCocycle.lean, line 310. The attribute's comment: “the canonical isomorphism and its cocycle condition”.

Stacks 05YY. Let φ : U ⟶ X be a morphism of algebraic spaces with R = U ×_X U and t, s : R ⟶ U the two projections, as for a presentation of X by a surjective étale φ. For a sheaf ℱ on the small étale site of X, the sheaf 𝒢 = φ⁻¹ℱ on the small étale site of U carries a canonical isomorphism

α : t⁻¹𝒢 ⟶ s⁻¹𝒢,

natural in ℱ.

It is the identification of the two iterated inverse images along (t, φ) and along (s, φ), whose composites agree because R is the fibre product of φ with itself.

noncomputable def presentationPullbackIso (φ : U ⟶ X) (s t : R ⟶ U)
    (hR : IsPullback t s φ φ) :
    smallEtaleSheafInverseImage B S hS φ ⋙ smallEtaleSheafInverseImage B S hS t ≅
      smallEtaleSheafInverseImage B S hS φ ⋙ smallEtaleSheafInverseImage B S hS s

AlgebraicGeometry.Space.presentationPullbackIsoApp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtalePresentationCocycle.lean, line 341. The attribute's comment: “the canonical isomorphism and its cocycle condition”.

Stacks 05YY. The isomorphism

α : t⁻¹𝒢 ⟶ s⁻¹𝒢

canonically attached to the sheaf 𝒢 = φ⁻¹ℱ, for φ : U ⟶ X with R = U ×_X U and t, s : R ⟶ U the two projections, as for a presentation of X by a surjective étale φ.

By construction it is the value at ℱ of the natural isomorphism AlgebraicGeometry.Space.presentationPullbackIso.

noncomputable def presentationPullbackIsoApp (φ : U ⟶ X) (s t : R ⟶ U)
    (hR : IsPullback t s φ φ) (F : smallEtaleSheafCat B S hS X) :
    (smallEtaleSheafInverseImage B S hS t).obj
        ((smallEtaleSheafInverseImage B S hS φ).obj F) ≅
      (smallEtaleSheafInverseImage B S hS s).obj
        ((smallEtaleSheafInverseImage B S hS φ).obj F)

AlgebraicGeometry.Space.presentationPullbackIsoApp_cocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtalePresentationCocycle.lean, line 364. The attribute's comment: “the canonical isomorphism and its cocycle condition”.

Stacks 05YY. The cocycle condition on α. Let R₂ = R ×_{s, U, t} R be the fibre product of s and t, with projections pr₀ and pr₁, and let c : R₂ ⟶ R be the composition law of the groupoid, so that c has the target of the first arrow and the source of the second. Then the pentagon

pr₀⁻¹t⁻¹𝒢 → pr₀⁻¹s⁻¹𝒢 = pr₁⁻¹t⁻¹𝒢 → pr₁⁻¹s⁻¹𝒢 = c⁻¹s⁻¹𝒢, pr₀⁻¹t⁻¹𝒢 = c⁻¹t⁻¹𝒢 → c⁻¹s⁻¹𝒢

commutes: its three arrows are pr₀⁻¹α, pr₁⁻¹α and c⁻¹α, and its three equalities are the canonical identifications of iterated inverse images along pairs with the same composite.

This is CategoryTheory.compIsoOfEqApp_cocycle for the small étale inverse images, whose associativity coherence is AlgebraicGeometry.Space.smallToposMorphism_comp_inverseImage_assoc.

theorem presentationPullbackIsoApp_cocycle (φ : U ⟶ X) (s t : R ⟶ U) (hR : IsPullback t s φ φ)
    (pr₀ pr₁ c : R₂ ⟶ R) (hR₂ : IsPullback pr₀ pr₁ s t) (hct : pr₀ ≫ t = c ≫ t)
    (hcs : pr₁ ≫ s = c ≫ s) (F : smallEtaleSheafCat B S hS X) :
    (smallEtaleSheafInverseImage B S hS pr₀).map
          (presentationPullbackIsoApp B S hS φ s t hR F).hom ≫
        (inverseImageCompIsoOfEqApp B S hS pr₀ pr₁ s t hR₂.w
          ((smallEtaleSheafInverseImage B S hS φ).obj F)).hom ≫
        (smallEtaleSheafInverseImage B S hS pr₁).map
          (presentationPullbackIsoApp B S hS φ s t hR F).hom ≫
        (inverseImageCompIsoOfEqApp B S hS pr₁ c s s hcs
          ((smallEtaleSheafInverseImage B S hS φ).obj F)).hom =
      (inverseImageCompIsoOfEqApp B S hS pr₀ c t t hct
          ((smallEtaleSheafInverseImage B S hS φ).obj F)).hom ≫
        (smallEtaleSheafInverseImage B S hS c).map
          (presentationPullbackIsoApp B S hS φ s t hR F).hom

AlgebraicGeometry.Space.SpacesEtale.isEquivalence_toPresentationDescentData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtalePresentationDescent.lean, line 245. The attribute's comment: “the equivalence of categories”.

Let X be an algebraic space over a scheme S, let φ : U ⟶ X be a surjective étale morphism and let (U, R, s, t, c, e, i) be the groupoid of the presentation X = U/R, so that R = U ×_X U with t and s the two projections and c the composition law on R₂ = R ×_{s, U, t} R. Then the functor taking a sheaf ℱ on the small étale site of X to the pair (𝒢, α), where 𝒢 = φ⁻¹ℱ is a sheaf on the small étale site of U and α : t⁻¹𝒢 ⟶ s⁻¹𝒢 is the canonical isomorphism, is an equivalence of categories onto the category of such pairs: pairs of a sheaf on the small étale site of U and an isomorphism t⁻¹𝒢 ⟶ s⁻¹𝒢 whose pentagon over R₂ commutes, with morphisms the maps of sheaves commuting with those isomorphisms.

theorem isEquivalence_toPresentationDescentData
    (hsurj : IsSurjective B S hS Uo.obj.hom.hom) :
    (toPresentationDescentData B S hS t s hR pr₀ pr₁ c hR₂ hct hcs).IsEquivalence

Sources

LeanAlgebraicGeometry.Space.SmallEtale · AlgebraicGeometry.Space.SmallEtale.IsCovering · AlgebraicGeometry.Space.essentiallySmall_spacesEtale · AlgebraicGeometry.Space.SpacesEtale · AlgebraicGeometry.Space.SpacesEtale.IsCovering · AlgebraicGeometry.Space.SpacesEtale.isSite · AlgebraicGeometry.Space.comparisonFunctor · AlgebraicGeometry.Space.comparisonFunctor_obj

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

66.3 Separation axioms to 66.18 The étale site of an…

Section66.3 Separation axioms#

Tag 03BS, a definition

Tag 03DY, a lemma

Tag 0AHR, a lemma

Tag 0AHS, a lemma

Sources

Section66.4 Points of algebraic spaces#

Tag 03BU, a definition

Tag 03BV, a lemma

Tag 03H4, a lemma

Tag 03H5, a lemma

Tag 03BW, a lemma

Tag 03BX, a lemma

Tag 03BY, a definition

Tag 03BZ, a lemma

Tag 03IE, a lemma

Tag 06NF, a lemma

Tag 0H2X, a lemma

Tag 03E1, a lemma

Sources

Section66.5 Quasi-compact spaces#

Tag 03E3, a definition

Tag 03E4, a lemma

Tag 040T, a lemma

Tag 04NN, a lemma

Sources

Section66.6 Special coverings#

Tag 03FX, a lemma

Tag 03FY, a lemma

Tag 03H6, a lemma

Tag 03FZ, a lemma

Tag 07S4, a lemma

Tag 03W7, a lemma

Tag 03IJ, a lemma

Sources

Section66.7 Properties of Spaces defined by properties of schemes#

Tag 03E8, a lemma

Tag 03E6, a definition

Tag 03E7, a remark

Tag 04N2, a lemma

Tag 04RC, a definition

Tag 0BBL, a remark

Sources

Section66.8 Constructible sets#

Tag 0ECT, a lemma

Tag 0ECU, a definition

Sources

Section66.9 Dimension at a point#

Tag 04N5, a definition

Tag 04N6, a definition

Sources

Section66.10 Dimension of local rings#

Tag 0BAM, a lemma

Tag 04NA, a definition

Tag 0BAN, a lemma

Sources

Section66.11 Generic points#

Tag 0BAQ, a lemma

Tag 0BAR, a lemma

Sources

Section66.12 Reduced spaces#

Tag 03IP, the section

Tag 0ABJ, a lemma

Tag 07TW, a lemma

Tag 03IQ, a lemma

Tag 03JJ, a lemma

Tag 047X, a definition

Sources

Section66.13 The schematic locus#

Tag 03JG, the section

Tag 03JH, a lemma

Tag 0BAS, a lemma

Tag 06NH, a proposition

Sources

Section66.14 Obtaining a scheme#

Tag 07S6, a proposition

Tag 07S7, a lemma

Tag 0BBM, a lemma

Sources

Section66.3 Separation axioms #

Section66.4 Points of algebraic spaces #

Section66.5 Quasi-compact spaces #

Section66.6 Special coverings #

Section66.7 Properties of Spaces defined by properties of schemes #

Section66.8 Constructible sets #

Section66.9 Dimension at a point #

Section66.10 Dimension of local rings #

Section66.11 Generic points #

Section66.12 Reduced spaces #

Section66.13 The schematic locus #

Section66.14 Obtaining a scheme #

Section66.15 Points on quasi-separated spaces #

Section66.16 Étale morphisms of algebraic spaces #

Section66.17 Spaces and fpqc coverings #

Section66.18 The étale site of an algebraic space #