67.17 Scheme theoretic closure… to 67.33 Relative dimension

Section67.17 Scheme theoretic closure and density #

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

Tag 0832, a lemma

Tag 0832 in the Stacks Project.

AlgebraicGeometry.isSchemeTheoreticallyDense_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Closure/DensePreimageQuasiFinite.lean, line 322. References: EGA IV (20.5.7), “special case”.

Stacks 0832. The inverse image of a scheme-theoretically dense open subscheme under a morphism of schemes which is flat, locally of finite presentation and locally quasi-finite is scheme-theoretically dense.

public theorem isSchemeTheoreticallyDense_preimage {X S : Scheme.{u}} (f : X ⟶ S)
    [Flat f] [LocallyOfFinitePresentation f] [LocallyQuasiFinite f]
    {W : S.Opens} (hW : Scheme.Opens.IsSchemeTheoreticallyDense W) :
    Scheme.Opens.IsSchemeTheoreticallyDense (f ⁻¹ᵁ W)

Tag 0833, a lemma

Tag 0833 in the Stacks Project.

AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_exists_surjective_etale_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticDensity/ChartCriterion.lean, line 183.

Stacks 0833. Let U be an open subspace of an algebraic space X over a scheme S contained in a big fppf site B. Then U is scheme-theoretically dense in X -- the scheme-theoretic closure of U ×_X V in V is all of V for every étale morphism V ⟶ X of algebraic spaces over S -- if and only if there are a scheme V and a surjective étale morphism φ : V ⟶ X for which that holds over the open subschemes of V alone: the scheme-theoretic closure of U ×_X W in W is all of W for every open subscheme W of V. The second condition says exactly that the open subscheme U ×_X V of V is scheme-theoretically dense in the sense of Stacks 01RB.

The first condition trivially implies the second, since the composite of an open immersion with an étale morphism is étale. For the converse let C be an étale scheme chart of X; by AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_forall_chart it suffices to make the scheme-theoretic closure of U ×_X C in C everything, and the two conditions are compared over T = V ×_X C. The projection T ⟶ V is a base change of the étale chart C, hence étale and so flat, locally of finite presentation and locally quasi-finite, so Stacks 0832 carries scheme-theoretic density of U ×_X V in V to scheme-theoretic density of U ×_X T in T; chartwise this is read through AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_preimage_eq_top_iff, which identifies closures of inverse images with scheme-theoretic dominance of the representing morphisms of schemes. The projection T ⟶ C is a base change of φ, hence surjective étale, and AlgebraicGeometry.Space.subfunctor_eq_top_of_isSurjective_isEtale_preimage descends the closure over T to the closure over C.

Scheme-theoretic density of U ×_X V in V, rather than merely the equality of the scheme-theoretic closure of U ×_X V with V, is what the second condition has to say, and the source's literal reading of it is false. Take for X a scheme and for φ the identity, which is a surjective étale morphism from a scheme: the literal reading of condition (2) is then exactly that the scheme-theoretic closure of U in X is X, whereas condition (1), applied to the open immersions W ⟶ X -- which are étale -- is exactly that U is a scheme-theoretically dense open subscheme of X in the sense of Stacks 01RB. Stacks 01RC exhibits an affine scheme X = Spec(k[x, z₁, z₂, …]/(xⁿzₙ)) and an open U = X ∖ V(z₁, z₂, …) with the former but not the latter: the closure is X because A ⟶ ∏ₙ A_{zₙ} is injective, while U is not even topologically dense in X, hence not scheme-theoretically dense. The literal reading would moreover make the quasi-compactness hypothesis of Stacks 0835 superfluous, and contradict the remark that follows Stacks 0834. By Stacks 01RD the two readings agree exactly when the inclusion is quasi-compact, and it is the density form that Stacks 0832 transports.

The part of the source's argument for (2) implies (1) that does hold for the bare equality is AlgebraicGeometry.Space.schemeTheoreticClosure_eq_top_of_isSurjective_isEtale: a surjective étale chart over which the scheme-theoretic closure of the inverse image is everything already forces the scheme-theoretic closure of U in X to be everything.

theorem isSchemeTheoreticallyDense_iff_exists_surjective_etale_chart
    (hX : IsAlgebraicSpace B S hS X) (U : Subfunctor X) (hU : IsOpenSubspace B S hS U) :
    IsSchemeTheoreticallyDense B S hS U ↔
      ∃ (V : BigFppfOver B S hS) (φ : yoneda.obj V ⟶ X),
        IsSurjective B S hS φ ∧ IsEtale B S hS φ ∧
          ∀ (W : BigFppfOver B S hS) (ψ : W ⟶ V),
            AlgebraicGeometry.IsOpenImmersion ((BigFppfOver.toScheme B S hS).map ψ) →
              schemeTheoreticClosure B S hS (U.preimage (yoneda.map ψ ≫ φ)) = ⊤

Tag 0834, a definition

Tag 0834 in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticClosure, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticDensity/Density.lean, line 38. The attribute's comment: “part (1): the scheme-theoretic closure of an open subspace”.

Stacks 0834, part (1). The scheme-theoretic closure of a subspace U of an algebraic space X over S is the scheme-theoretic image of Stacks 082X of its inclusion.

abbrev schemeTheoreticClosure (U : Subfunctor X) : Subfunctor X

AlgebraicGeometry.Space.IsSchemeTheoreticallyDense, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticDensity/Density.lean, line 49. The attribute's comment: “part (2): scheme-theoretic density of an open subspace”. References: EGA IV (11.10.2), “single open subspace”.

Stacks 0834, part (2). An open subspace U of an algebraic space X over S is scheme-theoretically dense in X when, for every étale morphism φ : V ⟶ X of algebraic spaces over S, the scheme-theoretic closure of U ×_X V in V is all of V.

This is the first of the equivalent conditions of Stacks 0833, and is in general strictly stronger than the scheme-theoretic closure of U itself being all of X.

def IsSchemeTheoreticallyDense (U : Subfunctor X) : Prop

Tag 0835, a lemma

Tag 0835 in the Stacks Project.

AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_schemeTheoreticClosure_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactSchemeTheoreticDensity.lean, line 114.

Let S be a scheme contained in a big fppf site B, let X be an algebraic space over S and let U ⊆ X be an open subspace. If the inclusion U ⟶ X is quasi-compact, then U is scheme-theoretically dense in X if and only if the scheme-theoretic closure of U in X is X.

theorem isSchemeTheoreticallyDense_iff_schemeTheoreticClosure_eq_top
    (hX : IsAlgebraicSpace B S hS X) (U : Subfunctor X) (hU : IsOpenSubspace B S hS U)
    (hqc : IsQuasiCompact B S hS U.ι) :
    IsSchemeTheoreticallyDense B S hS U ↔ schemeTheoreticClosure B S hS U = ⊤

Tag 0836, a lemma

Tag 0836 in the Stacks Project.

AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_mono_fSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticDensity/Density.lean, line 118.

Stacks 0836. Let j : U ⟶ X be an open immersion of algebraic spaces over a scheme S contained in a big fppf site B. Then U is scheme-theoretically dense in X if and only if the canonical homomorphism 𝒪_X ⟶ j_* 𝒪_U of sheaves of commutative rings on the small étale site of X is injective, that is, a monomorphism.

Both sides are tested on the étale scheme charts of X. On the one hand the structure map of the morphism of ringed topoi of Stacks 03G8 is a monomorphism exactly when, over every étale scheme chart V of X, pullback of regular functions along the open immersion of schemes representing U ×_X V is injective; the sections of the direct image over V are a limit over the étale charts of U above U ×_X V, which for a representable morphism is attained at the single chart U ×_X V. On the other hand the scheme-theoretic closure of U ×_X V is all of V exactly when that open immersion of schemes is scheme-theoretically dominant, and -- since the charts of X include every open subscheme of every chart -- dominance over all charts is the same as injectivity on global sections over all charts. Finally density may be tested on the charts alone, by AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_forall_chart.

theorem isSchemeTheoreticallyDense_iff_mono_fSharp (hX : IsAlgebraicSpace B S hS X)
    (U : Subfunctor X) (hU : IsOpenSubspace B S hS U) :
    IsSchemeTheoreticallyDense B S hS U ↔
      Mono (smallEtaleRingedToposHom B S hS
        (ObjectProperty.homMk U.ι :
          (⟨U.toFunctor, hU.1⟩ : AlgebraicSpaces B S hS) ⟶
          (⟨X, hX⟩ : AlgebraicSpaces B S hS))).fSharp

Tag 0837, a lemma

Tag 0837 in the Stacks Project.

AlgebraicGeometry.Space.isSchemeTheoreticallyDense_inf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SchemeTheoreticDensity/Density.lean, line 229.

Stacks 0837. If U and V are scheme-theoretically dense open subspaces of an algebraic space X over a scheme S contained in a big fppf site B, then so is U ∩ V.

Let φ : W ⟶ X be an étale morphism of algebraic spaces over S. The scheme-theoretic closure of (U ∩ V) ×_X W in W is a closed subspace containing the inverse image of U ∩ V, hence is all of W by AlgebraicGeometry.Space.eq_top_of_preimage_inf_le: the density of U along the étale morphism V ×_X W ⟶ X and the density of V along φ are used in turn.

theorem isSchemeTheoreticallyDense_inf (hX : IsAlgebraicSpace B S hS X) (U V : Subfunctor X)
    (hU : IsOpenSubspace B S hS U) (hV : IsOpenSubspace B S hS V)
    (hUdense : IsSchemeTheoreticallyDense B S hS U)
    (hVdense : IsSchemeTheoreticallyDense B S hS V) :
    IsOpenSubspace B S hS (U ⊓ V) ∧ IsSchemeTheoreticallyDense B S hS (U ⊓ V)

Tag 088G, a lemma

Tag 088G in the Stacks Project.

AlgebraicGeometry.Space.isOpenImmersion_and_dense_toSchemeTheoreticImage_of_qc_or_reduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionDenseOpenInSchemeTheoreticImage.lean, line 74.

Stacks 088G. Let S be a scheme and let h : Z ⟶ X be an immersion of algebraic spaces over S. Assume either that h is quasi-compact or that Z is reduced, and let Z̄ ⊆ X be the scheme-theoretic image of h. Then the morphism Z ⟶ Z̄ is an open immersion which identifies Z with a scheme-theoretically dense open subspace of Z̄; moreover Z is topologically dense in Z̄.

Spelled out, the five assertions are: the morphism onto the scheme-theoretic image is an open immersion; it is an isomorphism onto its range, which is the identification of Z with a subspace of Z̄; that range is an open subspace of Z̄; it is scheme-theoretically dense in Z̄; and the induced map on points has dense range.

Each is proved separately in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ImmersionSchemeTheoreticallyDenseOpen.lean, the identification being the only one not stated there: it is CategoryTheory.Subfunctor.toRange of the morphism onto the image, which is an isomorphism because that morphism is an open immersion and hence a monomorphism.

theorem isOpenImmersion_and_dense_toSchemeTheoreticImage_of_qc_or_reduced
    {Z X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hZ : IsAlgebraicSpace B S hS Z)
    (hX : IsAlgebraicSpace B S hS X) (h : Z ⟶ X) (hh : IsImmersion B S hS h)
    (hq_or_hr : IsQuasiCompact B S hS h ∨
      HasEtaleLocalProperty B S hS Z (fun W : Scheme.{u} => IsReduced W)) :
    IsOpenImmersion B S hS (toSchemeTheoreticImage B S hS h) ∧
      IsIso (Subfunctor.toRange (toSchemeTheoreticImage B S hS h)) ∧
      IsOpenSubspace B S hS (Subfunctor.range (toSchemeTheoreticImage B S hS h)) ∧
      IsSchemeTheoreticallyDense B S hS (Subfunctor.range (toSchemeTheoreticImage B S hS h)) ∧
      DenseRange (pointsMap B S hS Z (toSchemeTheoreticImage B S hS h))

Tag 084N, a lemma

Tag 084N in the Stacks Project.

AlgebraicGeometry.Space.eq_of_eq_on_of_schemeTheoreticImageSubfunctor_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SeparatedEqualizer.lean, line 161.

Stacks 084N. Let X and Y be algebraic spaces over an algebraic space T with structure morphisms p : X ⟶ T and q : Y ⟶ T, and let f, g : X ⟶ Y be morphisms over T. Let U ⊆ X be an open subspace with f and g agreeing on U. If the scheme-theoretic closure of U in X, that is the scheme-theoretic image of U ⟶ X, is all of X and q is separated, then f = g.

The agreement locus of f and g is a closed subspace of X containing U, so minimality of the scheme-theoretic image of U ⟶ X puts that image inside the agreement locus, which is therefore all of X. Openness of U, and indeed algebraicity of U, are not used.

theorem eq_of_eq_on_of_schemeTheoreticImageSubfunctor_eq_top (hT : IsAlgebraicSpace B S hS T)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (p : X ⟶ T) (q : Y ⟶ T)
    (f g : X ⟶ Y) (hf : f ≫ q = p) (hg : g ≫ q = p) (U : Subfunctor X)
    (_hU : IsOpenSubspace B S hS U) (hfg : U.ι ≫ f = U.ι ≫ g)
    (hclosure : schemeTheoreticImageSubfunctor B S hS U.ι = ⊤) (hq : IsSeparated B S hS q) :
    f = g

Sources

LeanAlgebraicGeometry.isSchemeTheoreticallyDense_preimage · AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_exists_surjective_etale_chart · AlgebraicGeometry.Space.schemeTheoreticClosure · AlgebraicGeometry.Space.IsSchemeTheoreticallyDense · AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_schemeTheoreticClosure_eq_top · AlgebraicGeometry.Space.isSchemeTheoreticallyDense_iff_mono_fSharp · AlgebraicGeometry.Space.isSchemeTheoreticallyDense_inf · AlgebraicGeometry.Space.isOpenImmersion_and_dense_toSchemeTheoreticImage_of_qc_or_reduced

Section67.18 Dominant morphisms #

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

Tag 0ABL, a definition

Tag 0ABL in the Stacks Project.

AlgebraicGeometry.Space.IsDominant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RationalMaps.lean, line 85. References: EGA I (2.2.6), “dominant”.

A morphism of algebraic spaces over S is dominant when the image of its map on points is dense in the point space of the target.

abbrev IsDominant (f : F ⟶ G) : Prop

Sources

LeanAlgebraicGeometry.Space.IsDominant

Section67.19 Universally injective morphisms #

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

Tag 03MU, a lemma

Tag 03MU in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_iff_injective_on_field_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/Basic.lean, line 197.

Stacks 03MU. A representable transformation is universally injective if and only if its maps on field-valued points are injective.

theorem universallyInjective_iff_injective_on_field_points
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G) (ha : yoneda.relativelyRepresentable a) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@AlgebraicGeometry.UniversallyInjective : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)) a ↔
      ∀ (K : Type u) [Field K] (T : BigFppfOver B S hS),
        ((BigFppfOver.toScheme B S hS).obj T ≅ Spec (.of K)) →
      Function.Injective (a.app (Opposite.op T)))

Tag 040X, a lemma

Tag 040X in the Stacks Project.

AlgebraicGeometry.Space.injectiveOnFieldPoints_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyInjectiveFieldPoints.lean, line 291.

Stacks 040X. For a morphism f : X ⟶ Y from an algebraic space over S the following are equivalent:

the map X(K) → Y(K) is injective for every field K over S,

for every morphism Y' ⟶ Y of algebraic spaces over S the induced map |Y' ×_Y X| → |Y'| is injective, and

the diagonal morphism X ⟶ X ×_Y X is surjective.

theorem injectiveOnFieldPoints_tfae (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    List.TFAE [InjectiveOnFieldPoints B S hS f, UniversallyInjective B S hS f,
      IsSurjective B S hS (pullback.diagonal f)]

Tag 03MV, a definition

Tag 03MV in the Stacks Project.

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

Stacks 03MV. A morphism is universally injective if every base change along an algebraic space induces an injective map on points.

abbrev UniversallyInjective {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) : Prop

Tag 05VS, a remark

Tag 05VS in the Stacks Project.

AlgebraicGeometry.AffineLineInvolution.not_isSeparated_squaringMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineLineInvolutionSquaringMap.lean, line 500. The attribute's comment: “part (5): the squaring morphism is not separated”.

Stacks 05VS, part (5), which is also the last assertion of the example of Stacks 05Z6: the squaring map X ⟶ 𝐀¹_k on the involution quotient is not separated. Its relative diagonal has the relation of Stacks 02Z1 as a represented base change, and that relation is not a closed immersion.

theorem not_isSeparated_squaringMap (hchar : (2 : k) ≠ 0) :
    ¬ Space.IsSeparated B (Spec (.of k)) hk (squaringMap k B hk)

AlgebraicGeometry.AffineLineInvolution.squaringMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/SquaringMap.lean, line 111. The attribute's comment: “part (1): the morphism X ⟶ 𝐀¹_k squaring the coordinate”.

Stacks 05VS, part (1). The canonical morphism from the involution quotient to the affine line, descended from squaring the coordinate: the point with coordinate x is sent to the point with coordinate x ^ 2. This is the morphism X ⟶ 𝐀¹_k of the remark.

noncomputable def squaringMap (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    (involutionQuotient k B hk).obj ⟶
      Stacks.Groupoids.points (Over.post (X := B.obj hk) B.inclusion) (affineLine k)

AlgebraicGeometry.AffineLineInvolution.isIso_squaringMap_pullback_puncturedAffineLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/SquaringMapProperties.lean, line 362. The attribute's comment: “part (2): an isomorphism away from the origin”.

Stacks 05VS, part (2). Over a field in which 2 is invertible, the squaring map from the involution quotient to the affine line is an isomorphism away from the origin: its base change along the inclusion of the punctured affine line is an isomorphism.

theorem isIso_squaringMap_pullback_puncturedAffineLine (hchar : (2 : k) ≠ 0)
    (B : BigFppfSite.{u}) (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    IsIso (pullback.snd (squaringMap k B hk)
      ((Over.post (X := B.obj hk) B.inclusion).op.whiskerLeft
        (yoneda.map (puncturedAffineLineInclusion k))))

AlgebraicGeometry.AffineLineInvolution.existsUnique_pointsMap_squaringMap_eq_originPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/SquaringMapProperties.lean, line 540. The attribute's comment: “part (3): exactly one point above the origin”.

Stacks 05VS, part (3). Exactly one point of the involution quotient lies over the origin of the affine line under the morphism descended from squaring the coordinate.

The quotient projection is locally surjective, hence surjective on the points of Stacks 03BU, so every point of the quotient over the origin comes from a point of the affine line whose square is the origin; such a point is the origin by AlgebraicGeometry.AffineLineInvolution.eq_affineLineZero_of_square_eq, and the image of the origin is the point sought. No assumption on the characteristic is needed: in characteristic two the relation is the diagonal and the statement is that squaring is injective on field-valued points.

theorem existsUnique_pointsMap_squaringMap_eq_originPoint (B : BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    ∃! x : Space.points B (Spec (.of k)) hk (involutionQuotient k B hk).obj,
      Space.pointsMap B (Spec (.of k)) hk _ (squaringMap k B hk) x = originPoint k B hk

AlgebraicGeometry.AffineLineInvolution.universallyInjective_squaringMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/SquaringMapProperties.lean, line 594. The attribute's comment: “part (4): universally injective”.

Stacks 05VS, part (4). Away from characteristic two the morphism descended from squaring the coordinate is universally injective.

Universal injectivity is tested on field-valued points by AlgebraicGeometry.Space.universallyInjective_of_fieldPoints, so it suffices to make two sections of the quotient over the spectrum of a field with the same square agree over a further field spectrum. The quotient projection is locally surjective, so after two successive restrictions both sections are classes of points t₁, t₂ of the affine line with the same square. Over a field the coordinate of t₁ is zero or a unit: in the first case the common square is the origin and both points are the origin, the test object being reduced; in the second the common square lies in the punctured line, and AlgebraicGeometry.AffineLineInvolution.quotient_eq_of_square_eq identifies the two classes.

theorem universallyInjective_squaringMap (hchar : (2 : k) ≠ 0) (B : BigFppfSite.{u})
    (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    Space.UniversallyInjective B (Spec (.of k)) hk (squaringMap k B hk)

Tag 03MW, a lemma

Tag 03MW in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/Basic.lean, line 248. References: EGA IV (11.9.14), “base change stability”.

Stacks 03MW. A base change of a universally injective morphism of algebraic spaces over S is universally injective.

Nothing is needed beyond unwinding the definition: a base change of Z ×_Y X ⟶ Z along k : W ⟶ Z is a base change of X ⟶ Y along k ≫ g.

theorem universallyInjective_pullback (f : X ⟶ Y) (g : Z ⟶ Y)
    (hf : UniversallyInjective B S hS f) :
    UniversallyInjective B S hS (pullback.fst g f)

AlgebraicGeometry.Space.universallyInjective_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/Basic.lean, line 302. References: EGA IV (11.9.14), “base change stability”.

Stacks 03MW for an arbitrary cartesian square: if IsPullback a b g f and f is universally injective, then so is a.

This is AlgebraicGeometry.Space.universallyInjective_pullback composed with the identification of the given square with the canonical fibre product.

theorem universallyInjective_of_isPullback (hC : IsAlgebraicSpace B S hS C)
    (hZ : IsAlgebraicSpace B S hS Z) (hT : IsAlgebraicSpace B S hS T) (f : C ⟶ T) (g : Z ⟶ T)
    (hf : UniversallyInjective B S hS f) {a : A ⟶ Z} {b : A ⟶ C}
    (hpb : IsPullback a b g f) : UniversallyInjective B S hS a

Tag 03MX, a lemma

Tag 03MX in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjectiveSchemeTests.lean, line 362.

Stacks 03MX. For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following are equivalent: f is universally injective; the base change Z ×_Y X ⟶ Z of f along every morphism from a scheme over S is universally injective; the same for every morphism from an affine scheme over S; the same for one morphism from a scheme over S which is surjective; and the base change of f along each member of some Zariski covering of Y is universally injective.

theorem universallyInjective_tfae {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [UniversallyInjective B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          UniversallyInjective B S hS (pullback.snd f g),
        ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
            UniversallyInjective B S hS (pullback.snd f g),
        ∃ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsSurjective B S hS g ∧ UniversallyInjective B S hS (pullback.snd f g),
        ∃ (I : Type u) (U : I → Subfunctor Y), IsZariskiCover B S hS I U ∧
          ∀ i, UniversallyInjective B S hS (pullback.snd f (U i).ι)]

Tag 03MY, a lemma

Tag 03MY in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversallyInjective/Basic.lean, line 277.

Stacks 03MY. A composition of universally injective morphisms of algebraic spaces over S is universally injective.

The base change W ×_Z X ⟶ W of the composite along k : W ⟶ Z is identified by the pasting isomorphism W ×_Z X ≅ (W ×_Z Y) ×_Y X with the composition of a base change of X ⟶ Y and a base change of Y ⟶ Z.

theorem universallyInjective_comp (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : UniversallyInjective B S hS f) (hg : UniversallyInjective B S hS g) :
    UniversallyInjective B S hS (f ≫ g)

Sources

LeanAlgebraicGeometry.Space.universallyInjective_iff_injective_on_field_points · AlgebraicGeometry.Space.injectiveOnFieldPoints_tfae · AlgebraicGeometry.Space.UniversallyInjective · AlgebraicGeometry.AffineLineInvolution.not_isSeparated_squaringMap · AlgebraicGeometry.AffineLineInvolution.squaringMap · AlgebraicGeometry.AffineLineInvolution.isIso_squaringMap_pullback_puncturedAffineLine · AlgebraicGeometry.AffineLineInvolution.existsUnique_pointsMap_squaringMap_eq_originPoint · AlgebraicGeometry.AffineLineInvolution.universallyInjective_squaringMap

Section67.20 Affine morphisms #

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

Tag 03WE, a lemma

Tag 03WE in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_tfae_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineHomEtaleDescent.lean, line 71. The attribute's comment: “items (1) and (2): affine as a representable morphism iff every base change to”.

Stacks 03WG. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is representable and affine as a morphism of presheaves; f is affine in the sense of Stacks 03WF; for every affine object of the site étale over Y the base change of f is represented by an affine object of the site; there is a surjective étale scheme chart of Y along which the base change of f is affine; and there is a Zariski covering of Y over whose members the base changes of f are affine.

This is AlgebraicGeometry.Space.isAffineHom_tfae with its descent hypothesis discharged by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isAffineHom.

theorem isAffineHom_tfae_of_isAlgebraicSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    List.TFAE [
      (yoneda.relativelyRepresentable f ∧
        (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.IsAffineHom.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f),
      IsAffineHom B S hS f,
      (∀ (V : BigAffineFppf B S hS)
        (g : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj V) ⟶ Y),
        IsEtale B S hS g →
          ∃ (W : BigAffineFppf B S hS)
            (p : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj W) ⟶ X)
            (q : (BigAffineFppf.inclusion B S hS).obj W ⟶
              (BigAffineFppf.inclusion B S hS).obj V),
            IsPullback p (yoneda.map q) f g),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧
        IsEtale B S hS g ∧
        IsAffineHom B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsAffineHom B S hS (pullback.snd f (U i).ι))]

AlgebraicGeometry.Space.presheaf_isAffineHom_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineHomEtaleDescent.lean, line 116.

Stacks 03WE. Let f : X ⟶ Y be a representable morphism of algebraic spaces over a scheme S. Then f is affine in the sense of Stacks 03HA — every represented base change of f is an affine morphism of schemes — if and only if for every affine object Z of the site and every morphism yoneda.obj Z ⟶ Y the fibre product X ×_Y Z is represented by an affine object of the site.

The right-hand side is AlgebraicGeometry.Space.IsAffineHom, Stacks 03WF, with its abbreviation unfolded, so that the quantifier over the test object stands in the statement: it ranges over all morphisms from an affine object of the site, not over the étale ones alone. That is what separates it from condition (3) of AlgebraicGeometry.Space.isAffineHom_tfae_of_isAlgebraicSpace, which is the same condition restricted to the étale test morphisms.

The equivalence is the one between conditions (1) and (2) of that theorem, whose condition (1) conjoins representability to the Stacks 03HA condition; representability is the hypothesis hf of the source here, and MorphismProperty.presheaf carries it on the left anyway.

theorem presheaf_isAffineHom_iff
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : yoneda.relativelyRepresentable f) :
    (MorphismProperty.inverseImage
        (@_root_.AlgebraicGeometry.IsAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      ∀ (Z : BigAffineFppf B S hS)
        (g : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj Z) ⟶ Y),
        ∃ (W : BigAffineFppf B S hS)
          (p : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj W) ⟶ X)
          (q : (BigAffineFppf.inclusion B S hS).obj W ⟶
            (BigAffineFppf.inclusion B S hS).obj Z),
          IsPullback p (yoneda.map q) f g

Tag 03WF, a definition

Tag 03WF in the Stacks Project.

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

A morphism of algebraic spaces is affine if each base change to an affine scheme is represented by an affine scheme.

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

Tag 03WG, a lemma

Tag 03WG in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_tfae_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineHomEtaleDescent.lean, line 71.

Stacks 03WG. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is representable and affine as a morphism of presheaves; f is affine in the sense of Stacks 03WF; for every affine object of the site étale over Y the base change of f is represented by an affine object of the site; there is a surjective étale scheme chart of Y along which the base change of f is affine; and there is a Zariski covering of Y over whose members the base changes of f are affine.

This is AlgebraicGeometry.Space.isAffineHom_tfae with its descent hypothesis discharged by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isAffineHom.

theorem isAffineHom_tfae_of_isAlgebraicSpace
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    List.TFAE [
      (yoneda.relativelyRepresentable f ∧
        (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.IsAffineHom.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f),
      IsAffineHom B S hS f,
      (∀ (V : BigAffineFppf B S hS)
        (g : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj V) ⟶ Y),
        IsEtale B S hS g →
          ∃ (W : BigAffineFppf B S hS)
            (p : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj W) ⟶ X)
            (q : (BigAffineFppf.inclusion B S hS).obj W ⟶
              (BigAffineFppf.inclusion B S hS).obj V),
            IsPullback p (yoneda.map q) f g),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧
        IsEtale B S hS g ∧
        IsAffineHom B S hS (pullback.snd f g)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsAffineHom B S hS (pullback.snd f (U i).ι))]

Tag 03WH, a lemma

Tag 03WH in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Affine.lean, line 50.

The composition of affine morphisms is affine.

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

Tag 03WI, a lemma

Tag 03WI in the Stacks Project.

AlgebraicGeometry.Space.IsAffineHom.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineHomTfae.lean, line 76.

Affineness of a morphism of algebraic spaces over S is stable under base change: if f' sits in a Cartesian square over f, then f' is affine as soon as f is.

theorem IsAffineHom.of_isPullback {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : X ⟶ Y} {g : Y' ⟶ Y} {k : X' ⟶ X} {f' : X' ⟶ Y'} (sq : IsPullback k f' f g)
    (hf : IsAffineHom B S hS f) : IsAffineHom B S hS f'

Tag 07U2, a lemma

Tag 07U2 in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 91. References: EGA II (1.2.2).

A closed immersion of algebraic spaces is affine.

theorem isAffineHom_of_isClosedImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G)
    (hf : IsClosedImmersion B S hS f) :
    IsAffineHom B S hS f

Tag 081V, a lemma

Tag 081V in the Stacks Project.

AlgebraicGeometry.Space.affineOverBaseChangeAlgebraHom_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineOverBaseChangeAlgebraNaturality.lean, line 482. The attribute's comment: “naturality in Z of the base-change comparison g^(f_ 𝒪_Z) ⟶ f'_* 𝒪_{Y ×_X Z}”.

The base-change comparison of 𝒪_Y-algebras is natural in the algebraic space affine over X. For a morphism φ : Z₁ ⟶ Z₂ of algebraic spaces affine over X, the square
g^* (f₂_* 𝒪_{Z₂}) ⟶ (f₂')_* 𝒪_{Y ×_X Z₂}
       ↓                       ↓
g^* (f₁_* 𝒪_{Z₁}) ⟶ (f₁')_* 𝒪_{Y ×_X Z₁}
of 𝒪_Y-algebras commutes, the vertical maps being the pullback of the direct-image map of φ and the direct-image map of its base change.

theorem affineOverBaseChangeAlgebraHom_naturality (g : Y ⟶ X) {Z₁ Z₂ : AffineOver B S hS X}
    (φ : Z₁ ⟶ Z₂) :
    (algebraPullback B S hS g).map (pushforwardAlgebraMap B S hS φ.hom) ≫
        affineOverBaseChangeAlgebraHom B S hS g Z₁ =
      affineOverBaseChangeAlgebraHom B S hS g Z₂ ≫
        pushforwardAlgebraMap B S hS (affineOverBaseChangeMap B S hS g φ).hom

AlgebraicGeometry.Space.affineOverBaseChangeMap_comp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineOverBaseChangeFunctor.lean, line 149. The attribute's comment: “naturality of the projections of the geometric base change Y ×_X Z ⟶ Z in Z; the anti-equivalence of the tag and its compatibility with base change are not proved”.

The projections of the geometric base change are natural in the affine algebraic space being base-changed.

This has exactly the type of the affineBaseChange_projection_naturality field of AlgebraicGeometry.Space.BaseChangeCompatibility, and is proved with no anti-equivalence and no base-change compatibility: it is the defining property of AlgebraicGeometry.Space.affineOverBaseChangeMap.

theorem affineOverBaseChangeMap_comp_projection (g : Y ⟶ X) {Z Z' : AffineOver B S hS X}
    (φ : Z ⟶ Z') :
    (affineOverBaseChangeMap B S hS g φ).hom.left ≫
        affineOverBaseChangeProjection B S hS g Z' =
      affineOverBaseChangeProjection B S hS g Z ≫ φ.hom.left

AlgebraicGeometry.Space.affineOverBaseChangeFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineOverBaseChangeFunctor.lean, line 166. The attribute's comment: “base change of the algebraic spaces affine over X as a functor; the anti-equivalence of the tag and its compatibility with base change are not proved”.

Base change of the algebraic spaces affine over X, as a functor AffineOver X ⥤ AffineOver Y.

On objects it is AlgebraicGeometry.Space.affineOverBaseChange and on morphisms AlgebraicGeometry.Space.affineOverBaseChangeMap. This has exactly the type of the affineBaseChange field of AlgebraicGeometry.Space.BaseChangeCompatibility, of which StacksFrontier.AlgebraicGeometry.Spaces.BoundedDirectImageAlgebraFactorization constructs only the action on objects.

def affineOverBaseChangeFunctor (g : Y ⟶ X) :
    AffineOver B S hS X ⥤ AffineOver B S hS Y

AlgebraicGeometry.Space.faithful_affinePushforwardAlgebraFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffinePushforwardAlgebraFunctorFullyFaithful.lean, line 56. The attribute's comment: “faithfulness of the direct image functor f ↦ f_* 𝒪_Y from the algebraic spaces affine over X; the corrected anti-equivalence and the base-change compatibility as a whole are affineAlgebraAntiEquivalence_bounded”.

The direct-image functor f ↦ f_* 𝒪_Y of Stacks 081V is faithful.

This is the faithfulness half of the anti-equivalence clause of the tag, and no more: the functor is not shown full by this statement — that is AlgebraicGeometry.Space.full_affinePushforwardAlgebraFunctor below — nor essentially surjective, and nothing is proved about the tag's compatibility with base change. AlgebraicGeometry.Space.eq_of_pushforwardRingMap_eq is the content; AlgebraicGeometry.Space.faithful_affinePushforwardAlgebraFunctor_iff is what strips the two full subcategories and the opposite category off it.

Restricting the target to the bounded quasi-coherent algebras changes nothing, by AlgebraicGeometry.Space.faithful_boundedPushforwardAlgebraFunctor_iff.

theorem faithful_affinePushforwardAlgebraFunctor (X : AlgebraicSpaces B S hS) :
    (quasicoherentPushforwardAlgebraFunctor B S hS X).Faithful

AlgebraicGeometry.Space.full_affinePushforwardAlgebraFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffinePushforwardAlgebraFunctorFullyFaithful.lean, line 77. The attribute's comment: “fullness of the direct image functor f ↦ f_* 𝒪_Y from the algebraic spaces affine over X; the corrected anti-equivalence and the base-change compatibility as a whole are affineAlgebraAntiEquivalence_bounded”.

The direct-image functor f ↦ f_* 𝒪_Y of Stacks 081V is full.

This is the fullness half of the anti-equivalence clause of the tag, and no more: nothing is proved here about the functor's essential surjectivity, which would need the relative spectrum of a quasi-coherent algebra, nor about the tag's compatibility with base change. AlgebraicGeometry.Space.exists_pushforwardAlgebraMap_eq is the content; AlgebraicGeometry.Space.full_affinePushforwardAlgebraFunctor_iff is what strips the two full subcategories and the opposite category off it.

Faithfulness is AlgebraicGeometry.Space.faithful_affinePushforwardAlgebraFunctor, so the two together make the functor fully faithful, and clause (a) of AlgebraicGeometry.Space.isEquivalence_boundedPushforwardAlgebraFunctor_iff_bijective — that f ↦ f_* be bijective — is delivered.

theorem full_affinePushforwardAlgebraFunctor (X : AlgebraicSpaces B S hS) :
    (quasicoherentPushforwardAlgebraFunctor B S hS X).Full

AlgebraicGeometry.Space.algebraPullback_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlgebraPullbackQuasicoherent.lean, line 166. The attribute's comment: “the algebraPullback_isQuasicoherent clause”.

The pullback of a quasi-coherent algebra sheaf along a morphism of algebraic spaces is quasi-coherent.

This is the algebraPullback_isQuasicoherent field of AlgebraicGeometry.Space.BaseChangeCompatibility, at AlgebraicGeometry.Space.algebraPullback.

theorem algebraPullback_isQuasicoherent (g : Y ⟶ X)
    (A : AlgebraSheaf.{u, u} B S hS X.1 X.2) (hA : A.IsQuasicoherent) :
    ((algebraPullback B S hS g).obj A).IsQuasicoherent

AlgebraicGeometry.Space.boundedPushforwardAlgebraFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BoundedAffineAlgebraAntiEquivalence.lean, line 176. The attribute's comment: “the direct image functor f ↦ f_* 𝒪_Y from the algebraic spaces affine over X, in the corrected form with the target restricted to the quasi-coherent 𝒪_X-algebras whose sections at every étale chart of X number fewer than the big fppf site's cutoff — the bound the direct image of an affine morphism satisfies by construction, and which the tag's unrestricted target fails (not_essSurj_affinePushforwardAlgebraFunctor_of_cutoff_le_mk_sections). This registration is the functor itself; its faithfulness, fullness and essential surjectivity are faithful_affinePushforwardAlgebraFunctor, full_affinePushforwardAlgebraFunctor and essSurj_boundedPushforwardAlgebraFunctor (via boundedRelativeSpec, Stacks 081W), and the base-change compatibility is the subject of the other 081V registrations”. References: SGA 3 III (0.1.7), “more general”.

The contravariant functor f ↦ f_* 𝒪_Y from the algebraic spaces affine over X to the quasi-coherent sheaves of commutative 𝒪_X-algebras whose sections at every étale chart of X are fewer than the cutoff of the ambient big fppf site.

def boundedPushforwardAlgebraFunctor (X : AlgebraicSpaces B S hS) :
    (AffineOver B S hS X)ᵒᵖ ⥤ BoundedQuasicoherentAlgebra B S hS X

AlgebraicGeometry.Space.affineAlgebraAntiEquivalence_bounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BoundedAffineAlgebraAntiEquivalenceProof.lean, line 107. The attribute's comment: “corrected form: f ↦ f_* 𝒪_Y is an anti-equivalence from the algebraic spaces affine over X onto the quasi-coherent 𝒪_X-algebras with fewer than the big fppf site's cutoff many sections over every étale chart (the unrestricted target is refuted by not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart, and the bounded algebras are exactly the essential image by essImage_boundedPushforwardAlgebraFunctor_iff), and it commutes with arbitrary base change g : Y ⟶ X, naturally in the affine space”.

For every algebraic space X, the direct image f ↦ f_* 𝒪_Y is an anti-equivalence from the algebraic spaces affine over X onto the quasi-coherent 𝒪_X-algebras with fewer than the big fppf site's cutoff many sections over every étale chart; and for every morphism g : Y ⟶ X of algebraic spaces the direct image commutes with base change along g, naturally in the affine space.

theorem affineAlgebraAntiEquivalence_bounded :
    (∀ X : AlgebraicSpaces B S hS, (boundedPushforwardAlgebraFunctor B S hS X).IsEquivalence) ∧
      ∀ {X Y : AlgebraicSpaces B S hS} (g : Y ⟶ X),
        Nonempty (quasicoherentPushforwardAlgebraFunctor B S hS X ⋙
            quasicoherentAlgebraPullback B S hS g ≅
          (affineOverBaseChangeFunctor B S hS g).op ⋙
            quasicoherentPushforwardAlgebraFunctor B S hS Y)

AlgebraicGeometry.Space.pushforwardAlgebraMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraMorphism.lean, line 626. The attribute's comment: “the direct image f ↦ f_* 𝒪_Y on morphisms, as a map of 𝒪_X-algebras”.

The contravariant action of f ↦ f_* 𝒪_Y on morphisms, as a morphism of 𝒪_X-algebras. A morphism f : Y ⟶ Z of algebraic spaces over X induces f_* : Z.hom_* 𝒪_Z ⟶ Y.hom_* 𝒪_Y, and that map of sheaves of commutative rings carries the structure-algebra map of the first to the structure-algebra map of the second.

This is one piece of Stacks 081V: the functor of the anti-equivalence on morphisms. It is functorial, by AlgebraicGeometry.Space.pushforwardAlgebraMap_id and AlgebraicGeometry.Space.pushforwardAlgebraMap_comp, and AlgebraicGeometry.Space.pushforwardAlgebraFunctor is the functor they assemble; the anti-equivalence itself is not constructed, see the implementation notes of this file.

def pushforwardAlgebraMap (f : Y ⟶ Z) :
    pushforwardAlgebra B S hS Z ⟶ pushforwardAlgebra B S hS Y

AlgebraicGeometry.Space.pushforwardAlgebraFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraMorphism.lean, line 780. The attribute's comment: “the direct image functor f ↦ f_* 𝒪_Y”.

The direct-image functor of Stacks 081V. The contravariant functor from the algebraic spaces over X to the sheaves of commutative 𝒪_X-algebras which sends f : Y ⟶ X to f_* 𝒪_Y and a morphism over X to the map it induces on direct images.

This is the functor of Stacks 081V on the whole over-category rather than on AlgebraicGeometry.Space.AffineOver X, and with values in all algebra sheaves rather than in AlgebraicGeometry.Space.QuasicoherentAlgebra X: quasi-coherence of f_* 𝒪_Y for a quasi-compact, quasi-separated f is Stacks 03M9, which is stated nowhere in this development, so restricting the codomain is not available. It is not shown to be an anti-equivalence; see the implementation notes of this file.

noncomputable def pushforwardAlgebraFunctor :
    (Over X)ᵒᵖ ⥤ AlgebraSheaf.{u, u} B S hS X.1 X.2

Declarations registered for the tag:

AlgebraicGeometry.Space.affineQuasicoherentPushforwardAlgebraFunctor, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffinePushforwardQuasicoherentAlgebra.lean, line 87 (StacksFrontier): “the direct image functor f ↦ f_* 𝒪_Y on the algebraic spaces affine over X, with values in the quasi-coherent 𝒪_X-algebras”.

Tag 081W, a definition

Tag 081W in the Stacks Project.

AlgebraicGeometry.Space.boundedRelativeSpec, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeSpecBounded.lean, line 99. The attribute's comment: “the bounded case only: the relative spectrum of a quasi-coherent O_X-algebra A with fewer than the big fppf site's cutoff many sections at every etale chart, built inside the site of X from its functor of points relativeSpecPoints A, with pushforwardAlgebraBoundedRelativeSpecIso and nonempty_iso_boundedRelativeSpec identifying it as the object corresponding to A under 081V. The tag for an arbitrary quasi-coherent algebra is relativeSpectrum (RelativeSpectrum), which applies this construction over an enlarged site”.

Stacks 081W, the bounded case. The relative spectrum \underline{Spec}_X(𝒜) of a quasi-coherent 𝒪_X-algebra 𝒜 with fewer than B.cutoff sections over every étale chart, as an algebraic space affine over X in the big fppf site of X: the object whose direct image π_* 𝒪 is 𝒜 (AlgebraicGeometry.Space.pushforwardAlgebraBoundedRelativeSpecIso), unique up to isomorphism over X (AlgebraicGeometry.Space.nonempty_iso_boundedRelativeSpec).

The size condition is the bound that every direct image of an affine morphism in the same site satisfies: an algebra violating it is the direct image of no algebraic space of the site affine over X (AlgebraicGeometry.Space.not_essSurj_affinePushforwardAlgebraFunctor_of_cutoff_le_mk_sections). The relative spectrum of an arbitrary quasi-coherent algebra is AlgebraicGeometry.Space.relativeSpectrum, which carries the full registration of the tag and is this construction applied over an enlargement of the site.

The construction is the functor of points AlgebraicGeometry.Space.relativeSpecPoints 𝒜; that it is an algebraic space affine over X is AlgebraicGeometry.Space.isAlgebraicSpace_and_presheaf_isAffineHom_relativeSpecPoints.

def boundedRelativeSpec (A : QuasicoherentAlgebra B S hS X)
    (hA : AlgebraSheaf.SectionsBelowCutoff B S hS A.obj) : AffineOver B S hS X

AlgebraicGeometry.Space.relativeSpec, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeSpecDirectImage.lean, line 102. The attribute's comment: “the relative spectrum, for a given anti-equivalence of Stacks 081V”.

The relative spectrum \underline{Spec}_X(A) of a quasi-coherent 𝒪_X-algebra on an algebraic space X, as an algebraic space affine over X: the value on A of the inverse of the anti-equivalence E.

def relativeSpec {X : AlgebraicSpaces B S hS} (A : QuasicoherentAlgebra B S hS X) :
    AffineOver B S hS X

AlgebraicGeometry.Space.relativeSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeSpectrum.lean, line 230. The attribute's comment: “the relative spectrum Spec_X(A) of an arbitrary quasi-coherent O_X-algebra A on an algebraic space X, with no further hypothesis: the algebraic space affine over X corresponding to A under 081V. It lives on an enlargement relativeSpectrumSite A of the big fppf site of X (Stacks 03FO; necessary, since an algebra with at least B.cutoff sections over a chart is the direct image of no space affine over X in the same site: not_essSurj_affinePushforwardAlgebraFunctor_of_cutoff_le_mk_sections), over X read there by 03FP; its direct image is A read there (pushforwardAlgebraRelativeSpectrumIso, relativeSpectrumRestrictIso) and it is unique up to unique isomorphism with that property (existsUnique_iso_relativeSpectrum)”.

Stacks 081W. The relative spectrum \underline{Spec}_X(𝒜) of an arbitrary quasi-coherent sheaf of 𝒪_X-algebras 𝒜 on an algebraic space X: the algebraic space affine over X corresponding to 𝒜 under the anti-equivalence of Stacks 081V.

Where it lives. It is an algebraic space of the big fppf site AlgebraicGeometry.Space.relativeSpectrumSite 𝒜, a big fppf site containing the site B of X, and it is affine over AlgebraicGeometry.Space.relativeSpectrumBase 𝒜, which is X read in that site (Stacks 03FP, AlgebraicGeometry.changeBigSite). It cannot in general live in B itself: an algebra with at least B.cutoff sections over an étale chart is the direct image of no algebraic space of B affine over X (AlgebraicGeometry.Space.not_essSurj_affinePushforwardAlgebraFunctor_of_cutoff_le_mk_sections, AlgebraicGeometry.Space.exists_quasicoherentAlgebra_cutoff_le_mk_sections), so the site is enlarged, as Stacks 03FO allows, past the cardinality of the sections of 𝒜.

What it is. It is the object of Stacks 081V over the enlarged site corresponding to AlgebraicGeometry.Space.relativeSpectrumAlgebra 𝒜, which is 𝒜 read on the small étale site of X enlarged (its sections over the charts of X are those of 𝒜, AlgebraicGeometry.Space.relativeSpectrumRestrictIso): its direct image is that algebra (AlgebraicGeometry.Space.pushforwardAlgebraRelativeSpectrumIso) and it is unique up to unique isomorphism with that property (AlgebraicGeometry.Space.existsUnique_iso_relativeSpectrum). When 𝒜 is bounded it is the relative spectrum AlgebraicGeometry.Space.boundedRelativeSpec built inside the site of X, read in the enlarged site (AlgebraicGeometry.Space.nonempty_iso_changeBigSite_boundedRelativeSpec).

No hypothesis is placed on 𝒜 beyond quasi-coherence.

def relativeSpectrum (A : QuasicoherentAlgebra B S hS X) :
    AffineOver (relativeSpectrumSite A) S (contains_relativeSpectrumSite A)
      (relativeSpectrumBase A)

Tag 081X, a remark

Tag 081X in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherent_pushforwardAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraFactorization.lean, line 141. The attribute's comment: “quasi-coherence of the pushforward algebra”.

The direct image of the structure sheaf along a quasi-compact, quasi-separated morphism of algebraic spaces is a quasi-coherent algebra. The hypothesis h03M9 is Stacks 03M9, that such a direct image preserves quasi-coherence of modules.

theorem isQuasicoherent_pushforwardAlgebra (f : Y ⟶ X)
    (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (h03M9 : IsQuasiCompact B S hS f.hom → IsQuasiSeparated B S hS f.hom →
      ∀ F : Modules.{u, u} B S hS Y.1 Y.2, F.IsQuasicoherentOnSite →
        ((modulePushforward B S hS f).obj F).IsQuasicoherentOnSite) :
    (pushforwardAlgebra B S hS (Over.mk f)).IsQuasicoherent

AlgebraicGeometry.Space.directImageFactorizationMap_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraFactorization.lean, line 165. The attribute's comment: “the canonical factorization”.

The canonical factorization Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) ⟶ X. The canonical morphism composed with the structure morphism of the relative spectrum of f_* 𝒪_Y is f.

theorem directImageFactorizationMap_factorization (f : Y ⟶ X)
    (hqc : (pushforwardAlgebra B S hS (Over.mk f)).IsQuasicoherent) :
    (directImageFactorizationMap B S hS E C f hqc).left ≫
        (relativeSpecDirectImage B S hS E f hqc).obj.hom = f

AlgebraicGeometry.Space.qcqsDirectImageFactorizationMap_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraFactorization.lean, line 202. The attribute's comment: “the canonical factorization of a quasi-compact quasi-separated morphism”.

Stacks 081X. A quasi-compact, quasi-separated morphism f : Y ⟶ X of algebraic spaces factors canonically as Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) ⟶ X.

theorem qcqsDirectImageFactorizationMap_factorization :
    (qcqsDirectImageFactorizationMap B S hS E C f hfqc hfqs h03M9).left ≫
        (qcqsRelativeSpecDirectImage B S hS E f hfqc hfqs h03M9).obj.hom = f

AlgebraicGeometry.Space.directImageSpec_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageSpecFactorization.lean, line 101. The attribute's comment: “corrected (bounded) form: quasi-coherence of f_ 𝒪_Y, the factorization Y → Spec_X(f_ 𝒪_Y) → X, and its canonicity”. References: SGA 3 VIB (11.1), “partial”.

The canonical factorization through the relative spectrum of f_* 𝒪_Y. Let f : Y ⟶ X be a quasi-compact, quasi-separated morphism of algebraic spaces. Then f_* 𝒪_Y is a quasi-coherent 𝒪_X-algebra, and f factors as Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) ⟶ X through the canonical morphism AlgebraicGeometry.Space.toDirectImageSpec, which is the unique morphism over X whose direct-image map is the identification \underline{Spec}_X(f_* 𝒪_Y)_* 𝒪 ≅ f_* 𝒪_Y.

The relative spectrum is the bounded one of AlgebraicGeometry.Space.boundedRelativeSpec: the unbounded form of Stacks 081V is refuted here by AlgebraicGeometry.Space.not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart, and the size condition it needs is proved for f_* 𝒪_Y by AlgebraicGeometry.Space.sectionsBelowCutoff_pushforwardAlgebra.

theorem directImageSpec_factorization :
    (pushforwardAlgebra B S hS (Over.mk f)).IsQuasicoherent ∧
      (toDirectImageSpec B S hS f hfqc hfqs).left ≫ (directImageSpec B S hS f hfqc hfqs).obj.hom =
        f ∧
      ∀ g : Over.mk f ⟶ (directImageSpec B S hS f hfqc hfqs).obj,
        g = toDirectImageSpec B S hS f hfqc hfqs ↔
          pushforwardAlgebraMap B S hS g = (directImageSpecIso B S hS f hfqc hfqs).hom

AlgebraicGeometry.Space.isQuasicoherent_pushforwardAlgebra_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QcqsDirectImageAlgebraFactorization.lean, line 78. The attribute's comment: “quasi-coherence of the pushforward algebra”. References: EGA IV (21.12.1), “more general”.

The direct image of the structure sheaf along a quasi-compact, quasi-separated morphism of algebraic spaces is a quasi-coherent algebra, with nothing assumed, stated for an algebraic space T over X. The module underlying the algebra is the direct image of 𝒪_T, which is quasi-coherent by Stacks 03M9 (AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePushforward_of_qcqs).

This is AlgebraicGeometry.Space.isQuasicoherent_pushforwardAlgebra with its Stacks 03M9 hypothesis supplied, read at an object of Over X rather than at Over.mk f. The form at a morphism f : Y ⟶ X is AlgebraicGeometry.Space.isQuasicoherent_pushforwardAlgebra_of_qcqs of StacksFrontier.AlgebraicGeometry.Spaces.PushforwardAlgebraQcqs.

theorem isQuasicoherent_pushforwardAlgebra_unconditional (T : Over X)
    (hfqc : IsQuasiCompact B S hS T.hom.hom) (hfqs : IsQuasiSeparated B S hS T.hom.hom) :
    (pushforwardAlgebra B S hS T).IsQuasicoherent

AlgebraicGeometry.Space.qcqsDirectImageFactorizationMap_factorization_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QcqsDirectImageAlgebraFactorization.lean, line 132. The attribute's comment: “the canonical factorization of a quasi-compact quasi-separated morphism — but presupposing an inhabitant of AffineAlgebraAntiEquivalence, which not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart shows is uninhabited over any algebraic space with one affine chart carrying a nonzero ring of functions, so the statement is vacuous there; the factorization against the bounded anti-equivalence, which that argument does not refute, is boundedQcqsDirectImageFactorizationMap_factorization”.

Stacks 081X. A quasi-compact, quasi-separated morphism f : Y ⟶ X of algebraic spaces factors canonically as Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) ⟶ X, with nothing assumed beyond the anti-equivalence of Stacks 081V and its base-change compatibility.

This is AlgebraicGeometry.Space.qcqsDirectImageFactorizationMap_factorization with its Stacks 03M9 hypothesis supplied.

This statement is vacuous, for the reason recorded at AlgebraicGeometry.Space.directImageFactorizationMap_factorization: the anti-equivalence E it presupposes is an inhabitant of AlgebraicGeometry.Space.AffineAlgebraAntiEquivalence, which AlgebraicGeometry.Space.not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart empties. The same factorization against the bounded anti-equivalence is AlgebraicGeometry.Space.boundedQcqsDirectImageFactorizationMap_factorization of StacksFrontier.AlgebraicGeometry.Spaces.BoundedDirectImageAlgebraFactorization. Stacks 081X is delivered unconditionally by AlgebraicGeometry.Space.directImageSpec_factorization of StacksFrontier.AlgebraicGeometry.Spaces.DirectImageSpecFactorization.

theorem qcqsDirectImageFactorizationMap_factorization_unconditional :
    (qcqsDirectImageFactorizationMap_unconditional B S hS E C f hfqc hfqs).left ≫
        (qcqsRelativeSpecDirectImage_unconditional B S hS E f hfqc hfqs).obj.hom = f

Declarations registered for the tag:

AlgebraicGeometry.Space.isQuasicoherent_pushforwardAlgebra_of_qcqs, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/PushforwardAlgebraQuasicoherentQcqs.lean, line 25 (StacksFrontier): “quasi-coherence of the pushforward algebra”.

Tag 08AI, a lemma

Tag 08AI in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_affineQuasicoherentDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineDirectImageEquivalence.lean, line 514. The attribute's comment: “the functor F ↦ f_F from quasi-coherent 𝒪_Y-modules to quasi-coherent f_𝒪_Y-modules is an equivalence of categories, for an affine morphism”.

Stacks 08AI, first assertion. Let f : Y ⟶ X be an affine morphism of algebraic spaces over S and 𝒜 = f_*𝒪_Y. The functor ℱ ↦ f_*ℱ from quasi-coherent 𝒪_Y-modules to quasi-coherent 𝒜-modules is an equivalence of categories.

The functor is AlgebraicGeometry.Space.affineQuasicoherentDirectImage, which is the direct image of Stacks 03D1 on the nose (AlgebraicGeometry.Space.affineQuasicoherentDirectImage_comp_ι); its quasi-inverse is 𝒢 ↦ 𝒪_Y ⊗_{f⁻¹𝒜} f⁻¹𝒢. The second assertion of the tag is AlgebraicGeometry.Space.isQuasicoherentOnSite_restrictScalars_structureSharp_iff.

theorem isEquivalence_affineQuasicoherentDirectImage (hf : IsAffineHom B S hS f.hom) :
    (affineQuasicoherentDirectImage B S hS f hf).IsEquivalence

AlgebraicGeometry.Space.isQuasicoherentOnSite_restrictScalars_structureSharp_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageAlgebraQuasicoherenceCriterion.lean, line 87. The attribute's comment: “an 𝒜-module is quasi-coherent as an 𝒪_X-module if and only if it is quasi-coherent as an 𝒜-module”.

Stacks 08AI, second assertion. Let f : Y ⟶ X be an affine morphism of algebraic spaces over S and let 𝒜 = f_*𝒪_Y. An 𝒜-module is quasi-coherent as an 𝒪_X-module — that is, after restriction of scalars along the structure map f♯ : 𝒪_X ⟶ 𝒜 of Stacks 03G8 — if and only if it is quasi-coherent as an 𝒜-module.

This is AlgebraicGeometry.Space.isQuasicoherentOnSite_restrictScalars_iff at A = f_*𝒪_Y, whose quasi-coherence as an 𝒪_X-module is AlgebraicGeometry.Space.isQuasicoherentOnSite_restrictScalars_structureRingSheafDirectImage, the first assertion of Stacks 07U8 at the structure sheaf.

theorem isQuasicoherentOnSite_restrictScalars_structureSharp_iff (f : Y ⟶ X)
    (hf : IsAffineHom B S hS f.hom)
    (M : SheafOfModules.{u} (structureRingSheafDirectImage B S hS f)) :
    ((SheafOfModules.restrictScalars.{u} (structureSharp B S hS f)).obj
        M).IsQuasicoherentOnSite ↔ M.IsQuasicoherentOnSite

AlgebraicGeometry.Space.quasicoherentDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasicoherentDirectImageAffine.lean, line 102. The attribute's comment: “the functor F ↦ f_*F on quasi-coherent modules”.

Stacks 08AI, the functor. Direct image as a functor QCoh(𝒪_Y) ⥤ QCoh(A), granted that it preserves quasi-coherence. This is the functor F ↦ f_*F whose invertibility is the first sentence of the tag.

noncomputable def quasicoherentDirectImage (f : Y ⟶ X)
    (hqc : DirectImagePreservesQuasicoherence B S hS f) :
    QuasicoherentSheaves.{u, u} B S hS Y.1 Y.2 ⥤
      (SheafOfModules.isQuasicoherentOnSite (affineDirectImageAlgebra B S hS f)).FullSubcategory

Tag 08GB, a lemma

Tag 08GB in the Stacks Project.

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

Let X ⟶ Y ⟶ T be morphisms of presheaves on the big fppf site of S. If the composite X ⟶ T is affine and the relative diagonal of Y ⟶ T is affine, then X ⟶ Y is affine.

theorem isAffineHom_of_isAffineHom_comp_of_isAffineHom_diagonal
    {X Y T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (g : Y ⟶ T)
    (hfg : IsAffineHom B S hS (f ≫ g))
    (hΔ : IsAffineHom B S hS (pullback.diagonal g)) :
    IsAffineHom B S hS f

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

Let X ⟶ Y ⟶ T be morphisms of presheaves on the big fppf site of S. If the composite X ⟶ T is affine and Y ⟶ T is separated, then X ⟶ Y is affine.

theorem isAffineHom_of_isAffineHom_comp_of_isSeparated
    {X Y T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (g : Y ⟶ T)
    (hfg : IsAffineHom B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    IsAffineHom B S hS f

AlgebraicGeometry.Space.isAffineHom_of_affine_source_of_isAffineHom_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/AffineDiagonal.lean, line 222. The attribute's comment: “part (3)”. References: EGA II (1.6.3).

A morphism from an affine object of the big fppf site of S to a presheaf whose absolute diagonal, in the sense of Stacks 03BS, is affine is affine.

theorem isAffineHom_of_affine_source_of_isAffineHom_diag
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (X : BigAffineFppf B S hS)
    (f : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj X) ⟶ Y)
    (hΔ : IsAffineHom B (⊤_ Scheme.{u}) hZ (diag (viewOverIntegers B S hS hZ Y))) :
    IsAffineHom B S hS f

AlgebraicGeometry.Space.isAffineHom_of_affine_source_of_isAbsolutelySeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/AffineDiagonal.lean, line 266. The attribute's comment: “part (4)”. References: EGA II (1.6.3).

A morphism from an affine object of the big fppf site of S to a separated algebraic space, in the absolute sense of Stacks 03BS, is affine: its absolute diagonal is a closed immersion, hence affine by Stacks 07U2.

theorem isAffineHom_of_affine_source_of_isAbsolutelySeparated
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (X : BigAffineFppf B S hS)
    (f : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj X) ⟶ Y)
    (hsep : IsAbsolutelySeparated B S hS hZ Y) :
    IsAffineHom B S hS f

Tag 09TF, a lemma

Tag 09TF in the Stacks Project.

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

Stacks 09TF. A morphism from the spectrum of an Artinian ring to a quasi-separated algebraic space is affine.

Following the source: for an étale morphism from an affine scheme V ⟶ X, the fibre product Spec(A) ×_X V is quasi-compact because X is quasi-separated, and étale over Spec(A), whose topology is discrete; so it is a scheme with finite discrete underlying space, hence affine.

theorem isAffineHom_of_isArtinianRing
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u}))
    (F : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : AlgebraicGeometry.IsAlgebraicSpace B S hS F)
    (hqs : AlgebraicGeometry.Space.IsAbsolutelyQuasiSeparated B S hS hZ F)
    (A : CommRingCat.{u}) [IsArtinianRing A]
    (hA : B.Contains (Spec A)) (p : B.obj hA ⟶ B.obj hS)
    (f : yoneda.obj (Over.mk p) ⟶ F) :
    AlgebraicGeometry.Space.IsAffineHom B S hS f

Sources

LeanAlgebraicGeometry.Space.isAffineHom_tfae_of_isAlgebraicSpace · AlgebraicGeometry.Space.presheaf_isAffineHom_iff · AlgebraicGeometry.Space.IsAffineHom · AlgebraicGeometry.Space.isAffineHom_comp · AlgebraicGeometry.Space.IsAffineHom.of_isPullback · AlgebraicGeometry.Space.isAffineHom_of_isClosedImmersion · AlgebraicGeometry.Space.affineOverBaseChangeAlgebraHom_naturality · AlgebraicGeometry.Space.affineOverBaseChangeMap_comp_projection

Section67.21 Quasi-affine morphisms #

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

Tag 03WK, a lemma

Tag 03WK in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.presheaf_isQuasiAffineHom_iff, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineComposition.lean, line 52 (StacksFrontier): “representable case: 03HA-quasi-affine iff affine base changes are quasi-affine”.

Tag 03WL, a definition

Tag 03WL in the Stacks Project.

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

A morphism of algebraic spaces is quasi-affine if each of its base changes to an affine scheme is represented by a quasi-affine scheme.

abbrev IsQuasiAffineHom (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) : Prop

Tag 03WM, a lemma

Tag 03WM in the Stacks Project.

AlgebraicGeometry.Space.isQuasiAffineHom_tfae_etaleChart_of_isAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineTfaeComplete.lean, line 104.

For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following four conditions are equivalent: f is relatively representable and all of its represented base changes are quasi-affine morphisms of schemes; f is quasi-affine in the sense of Stacks 03WL; the base change of f along some surjective étale scheme chart of Y is quasi-affine; and there is a Zariski covering of Y over whose members f is quasi-affine.

theorem isQuasiAffineHom_tfae_etaleChart_of_isAlgebraicSpace
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@_root_.AlgebraicGeometry.IsQuasiAffineHom.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f,
      IsQuasiAffineHom B S hS f,
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) g ∧
        IsQuasiAffineHom B S hS (pullback.fst g f)),
      (∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, IsQuasiAffineHom B S hS (pullback.fst (U i).ι f))
    ]

Tag 03WN, a lemma

Tag 03WN in the Stacks Project.

AlgebraicGeometry.Space.IsQuasiAffineHom.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineComposition.lean, line 38.

The composite of two quasi-affine morphisms of algebraic spaces over a scheme S is quasi-affine.

theorem IsQuasiAffineHom.comp {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z) {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : IsQuasiAffineHom B S hS f) (hg : IsQuasiAffineHom B S hS g) :
    IsQuasiAffineHom B S hS (f ≫ g)

Tag 03WO, a lemma

Tag 03WO in the Stacks Project.

AlgebraicGeometry.Space.IsQuasiAffineHom.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineTfae.lean, line 102.

Quasi-affineness of a morphism of algebraic spaces over S is stable under base change: if f' sits in a Cartesian square over f, then f' is quasi-affine as soon as f is.

theorem IsQuasiAffineHom.of_isPullback {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : X ⟶ Y} {g : Y' ⟶ Y} {k : X' ⟶ X} {f' : X' ⟶ Y'} (sq : IsPullback k f' f g)
    (hf : IsQuasiAffineHom B S hS f) : IsQuasiAffineHom B S hS f'

Tag 086S, a lemma

Tag 086S in the Stacks Project.

AlgebraicGeometry.Space.isQuasiAffineHom_iff_isOpenImmersion_overHomOfPushforwardAlgebraIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineCanonicalFactorization.lean, line 71. The attribute's comment: “for every algebraic space P affine over X with an identification e of its direct-image algebra with f_ O_Y, i.e. every relative spectrum of f_ O_Y: a quasi-compact f is quasi-affine iff the canonical morphism Y ⟶ P over X of 081X attached to e is an open immersion; quasi-separatedness of f is not needed once P and e are given”.

Stacks 086S. Let f : Y ⟶ X be a quasi-compact morphism of algebraic spaces over S, let P be an algebraic space affine over X, and let e : P_* 𝒪_P ≅ f_* 𝒪_Y identify its direct-image algebra with that of f, so that P is the relative spectrum \underline{Spec}_X(f_* 𝒪_Y). Then f is quasi-affine if and only if the canonical morphism Y ⟶ P over X of Stacks 081X attached to e is an open immersion.

theorem isQuasiAffineHom_iff_isOpenImmersion_overHomOfPushforwardAlgebraIso
    {X Y : AlgebraicSpaces B S hS} (f : Y ⟶ X) (hfqc : IsQuasiCompact B S hS f.hom)
    (P : AffineOver B S hS X)
    (e : pushforwardAlgebra B S hS P.obj ≅ pushforwardAlgebra B S hS (Over.mk f)) :
    IsQuasiAffineHom B S hS f.hom ↔
      IsOpenImmersion B S hS (overHomOfPushforwardAlgebraIso B S hS e).left.hom

AlgebraicGeometry.Space.isQuasiAffineHom_iff_isOpenImmersion_toDirectImageSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineCanonicalFactorization.lean, line 96. The attribute's comment: “corrected (bounded) form: Spec_X(f_ O_Y) is directImageSpec f, the relative spectrum of 081W in its bounded form (the unbounded 081V is refuted by not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart), whose size condition on f_ O_Y is proved; the morphism is toDirectImageSpec f, the canonical factorization of 081X; hypotheses exactly f quasi-compact and quasi-separated”.

Stacks 086S, in the corrected (bounded) form. A quasi-compact, quasi-separated morphism f : Y ⟶ X of algebraic spaces over S is quasi-affine if and only if its canonical factorization Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) of Stacks 081X is an open immersion.

The relative spectrum is AlgebraicGeometry.Space.directImageSpec, Stacks 081W in its corrected form: the relative spectrum of a quasi-coherent algebra whose sections over every chart number fewer than the cutoff of the site. The unbounded form of 081V that the source's \underline{Spec}_X presupposes is refuted in this development by AlgebraicGeometry.Space.not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart. The size condition on f_* 𝒪_Y is proved, not assumed (AlgebraicGeometry.Space.sectionsBelowCutoff_pushforwardAlgebra), so the hypotheses are exactly those of the source.

theorem isQuasiAffineHom_iff_isOpenImmersion_toDirectImageSpec {X Y : AlgebraicSpaces B S hS}
    (f : Y ⟶ X) (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom) :
    IsQuasiAffineHom B S hS f.hom ↔
      IsOpenImmersion B S hS (toDirectImageSpec B S hS f hfqc hfqs).left.hom

AlgebraicGeometry.Space.isQuasiAffineHom_of_isOpenImmersion_qcqsDirectImageFactorizationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineDirectImageFactorization.lean, line 113. The attribute's comment: “proves only: the factorization is an open immersion implies f is quasi-affine”.

A quasi-compact, quasi-separated morphism f : Y ⟶ X of algebraic spaces over S whose canonical morphism Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) is an open immersion is quasi-affine.

theorem isQuasiAffineHom_of_isOpenImmersion_qcqsDirectImageFactorizationMap (f : Y ⟶ X)
    (hfqc : IsQuasiCompact B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (hoi : IsOpenImmersion B S hS
      (qcqsDirectImageFactorizationMap B S hS E C f hfqc hfqs
        fun hqc hqs => isQuasicoherentOnSite_modulePushforward_of_qcqs B S hS f hqc hqs).left.hom) :
    IsQuasiAffineHom B S hS f.hom

AlgebraicGeometry.Space.isQuasiAffineHom_iff_isOpenImmersion_affineOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineOpenImmersionAffineOver.lean, line 430. The attribute's comment: “both directions, for every P affine over X by p and every g : Y ⟶ P over X whose map on direct-image algebras p_ O_P ⟶ f_ O_Y is an isomorphism: a quasi-compact f is quasi-affine iff g is an open immersion; this is the general form, and the canonical morphism of 081X is one such g”.

Let f : Y ⟶ X be a quasi-compact morphism of algebraic spaces over S, let P be an algebraic space affine over X by p, and let g : Y ⟶ P be a morphism over X whose map on direct-image algebras p_* 𝒪_P ⟶ f_* 𝒪_Y is an isomorphism. Then f is quasi-affine if and only if g is an open immersion.

theorem isQuasiAffineHom_iff_isOpenImmersion_affineOver {X Y : AlgebraicSpaces B S hS} (f : Y ⟶ X)
    (hfqc : IsQuasiCompact B S hS f.hom) (P : AffineOver B S hS X) (g : Over.mk f ⟶ P.obj)
    (hring : IsIso (pushforwardRingMap B S hS g)) :
    IsQuasiAffineHom B S hS f.hom ↔ IsOpenImmersion B S hS g.left.hom

AlgebraicGeometry.Space.isQuasiAffineHom_of_isOpenImmersion_qcqsDirectImageFactorizationMap_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiAffineOpenImmersionAffineOver.lean, line 454. The attribute's comment: “proves only: the factorization is an open immersion implies f is quasi-affine — and presupposes AffineAlgebraAntiEquivalence, which this development proves uninhabited (not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart), so the statement is vacuous; the non-vacuous form is isQuasiAffineHom_of_isOpenImmersion_boundedRelativeSpecDirectImage”.

A quasi-compact, quasi-separated morphism f : Y ⟶ X of algebraic spaces over S whose canonical morphism Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) of Stacks 081X is an open immersion is quasi-affine.

The hypothesis E is an inhabitant of AlgebraicGeometry.Space.AffineAlgebraAntiEquivalence, which AlgebraicGeometry.Space.not_nonempty_affineAlgebraAntiEquivalence_of_hasNonzeroAffineChart proves uninhabited, so the statement is vacuous.

theorem isQuasiAffineHom_of_isOpenImmersion_qcqsDirectImageFactorizationMap_unconditional
    (f : Y ⟶ X) (hfqc : IsQuasiCompact B S hS f.hom)
    (hfqs : IsQuasiSeparated B S hS f.hom)
    (hoi : IsOpenImmersion B S hS
      (qcqsDirectImageFactorizationMap_unconditional B S hS E C f hfqc hfqs).left.hom) :
    IsQuasiAffineHom B S hS f.hom

Sources

Section67.22 Types of morphisms étale local on source-and-target #

Section 67.22 of the Stacks Project, Tag 03MI. 7 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03MJ, a lemma

Tag 03MJ in the Stacks Project.

AlgebraicGeometry.Space.presheafImpliesHoldsOnEveryEtaleChart_of_etale_precomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartBridge.lean, line 114. The attribute's comment: “condition (1) from the represented base changes”.

Stacks 03MJ, condition (1) from the represented base changes. A property P of scheme morphisms which survives composition with an étale morphism in front of it holds on every étale chart of a morphism of presheaves all of whose represented base changes have P.

theorem presheafImpliesHoldsOnEveryEtaleChart_of_etale_precomp (P : MorphismProperty Scheme.{u})
    (hP : ∀ {X Y Z : Scheme.{u}} (i : X ⟶ Y) (p : Y ⟶ Z), Etale i → P p → P (i ≫ p)) :
    PresheafImpliesHoldsOnEveryEtaleChart B S hS P

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

Stacks 03MJ, the equivalence of conditions (1) and (2). A property of morphisms of schemes which is étale local on the source and target holds on every commuting square of étale charts of a morphism of algebraic spaces exactly when it holds on one such square whose chart of the source is surjective.

theorem holdsOnEveryEtaleChart_iff_surjectiveChart
    (hP : IsEtaleLocalOnSourceAndTarget P)
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) :
    HoldsOnEveryEtaleChart B S hS P f ↔ HoldsOnSurjectiveEtaleChart B S hS P f

AlgebraicGeometry.Space.holdsOnEveryEtaleChart_iff_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartLocality.lean, line 142. The attribute's comment: “representable source and target”.

Stacks 03MJ for a morphism of representable presheaves: a property of morphisms of schemes which is étale local on the source and target holds on every commuting square of étale charts of the morphism exactly when it holds of the morphism of schemes read off the canonical representations of source and target.

theorem holdsOnEveryEtaleChart_iff_representable
    (hP : IsEtaleLocalOnSourceAndTarget P)
    [F.IsRepresentable] [G.IsRepresentable] (f : F ⟶ G) :
    HoldsOnEveryEtaleChart B S hS P f ↔
      P ((BigFppfOver.toScheme B S hS).map
        (yoneda.preimage (F.reprW.hom ≫ f ≫ G.reprW.inv)))

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

Stacks 03MJ for a representable morphism of algebraic spaces: when P is in addition stable under base change and local on the base for the fppf topology, the every-chart condition is exactly the relative morphism property of the inverse image of P, that is, P holds of every represented base change of the morphism.

theorem holdsOnEveryEtaleChart_iff_relative
    (hP : IsEtaleLocalOnSourceAndTarget P)
    [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (f : F ⟶ G) (hf : yoneda.relativelyRepresentable f) :
    HoldsOnEveryEtaleChart B S hS P f ↔
      (P.inverseImage (BigFppfOver.toScheme B S hS)).presheaf f

Tag 04RD, a definition

Tag 04RD in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.HoldsOnEveryEtaleChart, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation.lean, line 122 (StacksFrontier).

Tag 0AML, a remark

Tag 0AML in the Stacks Project.

AlgebraicGeometry.Space.holdsOnEveryEtaleChart_isStableUnderComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartComposition.lean, line 143.

Stacks 0AML. A property of morphisms of schemes which is étale local on the source and target and stable under composition induces a composition stable property of morphisms of algebraic spaces over S, namely the condition that it hold on every commuting square of étale charts.

theorem holdsOnEveryEtaleChart_isStableUnderComposition
    (P : MorphismProperty Scheme.{u})
    (hP : IsEtaleLocalOnSourceAndTarget P)
    [P.IsStableUnderComposition] :
    MorphismProperty.IsStableUnderComposition
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        HoldsOnEveryEtaleChart B S hS P f.hom)

Tag 0AMM, a remark

Tag 0AMM in the Stacks Project.

AlgebraicGeometry.Space.holdsOnEveryEtaleChart_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartBaseChange.lean, line 249.

A property of morphisms of schemes which is étale local on the source and target and stable under base change induces a base-change stable property of morphisms of algebraic spaces over S, namely the condition that it hold on every commuting square of etale charts.

theorem holdsOnEveryEtaleChart_isStableUnderBaseChange
    (P : MorphismProperty Scheme.{u})
    (hP : IsEtaleLocalOnSourceAndTarget P)
    [P.IsStableUnderBaseChange] :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        HoldsOnEveryEtaleChart B S hS P f.hom)

Tag 04NC, a lemma

Tag 04NC in the Stacks Project.

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

Stacks 04NC, equivalence of conditions (1) and (2). An étale-local property of germ morphisms holds in every pointed chart if and only if it holds in one pointed chart.

theorem holdsOnEveryEtaleChartAtPoint_iff_some
    (Q : ∀ {X Y : GermOfScheme.{u}}, MorphismOfGerms X Y → Prop)
    (hQ : MorphismOfGerms.IsEtaleLocalOnSourceAndTarget Q)
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (f : F ⟶ G) (x : points B S hS F) :
    HoldsOnEveryEtaleChartAtPoint B S hS Q f x ↔
      HoldsOnSomeEtaleChartAtPoint B S hS Q f x

AlgebraicGeometry.Space.holdsOnEveryEtaleChartAtPoint_iff_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartAtPoint.lean, line 431. The attribute's comment: “representable source and target”.

Stacks 04NC, representable source and target. For representable algebraic spaces the chart condition is the property of the induced morphism of scheme germs at the corresponding scheme point.

theorem holdsOnEveryEtaleChartAtPoint_iff_representable
    (Q : ∀ {X Y : GermOfScheme.{u}}, MorphismOfGerms X Y → Prop)
    (hQ : MorphismOfGerms.IsEtaleLocalOnSourceAndTarget Q)
    [F.IsRepresentable] [G.IsRepresentable] (f : F ⟶ G) (x : points B S hS F)
    (p : FieldValuedPoint B S hS (yoneda.obj F.reprX)) (t : Spec (.of p.carrier))
    (hx : pointsMap B S hS (yoneda.obj F.reprX) F.reprW.hom
      (p.class B S hS (yoneda.obj F.reprX)) = x) :
    HoldsOnEveryEtaleChartAtPoint B S hS Q f x ↔
      Q (MorphismOfGerms.ofSchemeHom
        ((BigFppfOver.toScheme B S hS).map
          (yoneda.preimage (F.reprW.hom ≫ f ≫ G.reprW.inv)))
        (((BigFppfOver.toScheme B S hS).map p.value) t))

Tag 04RE, a definition

Tag 04RE in the Stacks Project.

AlgebraicGeometry.Space.HoldsOnEveryEtaleChartAtPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartAtPoint.lean, line 129.

Stacks 04RE. The property holds in every pair of étale charts at the point. For a property of morphisms of germs of schemes which is étale local on the source-and-target this is the definition of a morphism of algebraic spaces having that property at a point: by AlgebraicGeometry.Space.holdsOnEveryEtaleChartAtPoint_iff_some it is equivalent to the some-chart condition, which is the equivalence the definition invokes.

abbrev HoldsOnEveryEtaleChartAtPoint
    (Q : ∀ {X Y : GermOfScheme.{u}}, MorphismOfGerms X Y → Prop)
    (f : F ⟶ G) (x : points B S hS F) : Prop

Tag 04RF, a lemma

Tag 04RF in the Stacks Project.

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

A morphism has the germ property at a point exactly when it has the corresponding scheme-morphism property on an open neighbourhood of that point.

theorem holdsOnEveryEtaleChartAtPoint_iff_exists_open
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty Scheme.{u})
    (hP : AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget P)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (x : points B S hS X) :
    HoldsOnEveryEtaleChartAtPoint B S hS
      (MorphismOfGerms.HasRepresentativeWithProperty P) f x ↔
      ∃ (U : Subfunctor X), IsOpenSubspace B S hS U ∧
        x ∈ Set.range (pointsMap B S hS U.toFunctor U.ι) ∧
          HoldsOnEveryEtaleChart B S hS P (U.ι ≫ f)

AlgebraicGeometry.Space.holdsOnEveryEtaleChart_iff_forall_atPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartAtPointOpen.lean, line 658. The attribute's comment: “part (3)”.

A morphism of algebraic spaces has an étale-local property if and only if its germ has the associated property at every source point.

theorem holdsOnEveryEtaleChart_iff_forall_atPoint
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty Scheme.{u})
    (hP : AlgebraicGeometry.IsEtaleLocalOnSourceAndTarget P)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    HoldsOnEveryEtaleChart B S hS P f ↔
      ∀ x : points B S hS X,
        HoldsOnEveryEtaleChartAtPoint B S hS
          (MorphismOfGerms.HasRepresentativeWithProperty P) f x

Declarations registered for the tag:

MorphismOfGerms.hasRepresentativeWithProperty_isEtaleLocalOnSourceAndTarget registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartAtPointOpen.lean, line 485 (StacksFrontier).

Sources

LeanAlgebraicGeometry.Space.presheafImpliesHoldsOnEveryEtaleChart_of_etale_precomp · AlgebraicGeometry.Space.holdsOnEveryEtaleChart_iff_surjectiveChart · AlgebraicGeometry.Space.holdsOnEveryEtaleChart_iff_representable · AlgebraicGeometry.Space.holdsOnEveryEtaleChart_iff_relative · AlgebraicGeometry.Space.HoldsOnEveryEtaleChart · AlgebraicGeometry.Space.holdsOnEveryEtaleChart_isStableUnderComposition · AlgebraicGeometry.Space.holdsOnEveryEtaleChart_isStableUnderBaseChange · AlgebraicGeometry.Space.holdsOnEveryEtaleChartAtPoint_iff_some

Section67.23 Morphisms of finite type #

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

Tag 03XF, a definition

Tag 03XF in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyOfFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteType.lean, line 83. The attribute's comment: “part (1): locally of finite type”. References: EGA I (6.6.2).

Stacks 03XF, part (1). A morphism of algebraic spaces over S is locally of finite type when every commuting square of étale scheme charts induces a scheme morphism which is locally of finite type.

abbrev IsLocallyOfFiniteType (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteType.lean, line 90. The attribute's comment: “part (3): finite type”.

Stacks 03XF, part (3). A morphism of algebraic spaces over S is of finite type when it is locally of finite type and quasi-compact.

abbrev IsFiniteType (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsFiniteTypeAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteType.lean, line 114. The attribute's comment: “part (2): finite type at a point”.

Stacks 03XF, part (2). A morphism of algebraic spaces over S is of finite type at a point x of its source when some open subspace of the source containing x is locally of finite type over the target.

abbrev IsFiniteTypeAt (f : X ⟶ Y) (x : points B S hS X) : Prop

Tag 03XG, a lemma

Tag 03XG in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_comp', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypePermanence.lean, line 55. The attribute's comment: “locally of finite type”.

The composite f ≫ g of two morphisms locally of finite type is locally of finite type, as soon as the intermediate and final presheaves G and H are algebraic spaces over S.

theorem isLocallyOfFiniteType_comp' (f : F ⟶ G) (g : G ⟶ H)
    (hG : IsAlgebraicSpace B S hS G) (hH : IsAlgebraicSpace B S hS H)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) :
    IsLocallyOfFiniteType B S hS (f ≫ g)

AlgebraicGeometry.Space.isLocallyOfFiniteType_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeProperties.lean, line 138. The attribute's comment: “locally of finite type”.

Stacks 03XG, the case of being locally of finite type: the composite of two morphisms of algebraic spaces over S which are locally of finite type is locally of finite type.

Being locally of finite type is étale local on the source and target (Stacks 04R3) and stable under composition (Stacks 01T3), so this is an instance of Stacks 0AML.

theorem isLocallyOfFiniteType_comp
    {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 : G ⟶ H)
    (hf : IsLocallyOfFiniteType B S hS f)
    (hg : IsLocallyOfFiniteType B S hS g) :
    IsLocallyOfFiniteType B S hS (f ≫ g)

AlgebraicGeometry.Space.isFiniteType_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Proper.lean, line 92. The attribute's comment: “finite type”.

Stacks 03XG, finite type. The composite of two morphisms of algebraic spaces over S which are of finite type is of finite type: it is locally of finite type by Stacks 03XG and quasi-compact by Stacks 03HG.

theorem isFiniteType_comp (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsFiniteType B S hS f) (hg : IsFiniteType B S hS g) :
    IsFiniteType B S hS (f ≫ g)

AlgebraicGeometry.Space.isFiniteType_comp', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperPermanence.lean, line 65. The attribute's comment: “finite type”.

Stacks 03XG, finite type. The composite of two morphisms of algebraic spaces over S which are of finite type is of finite type.

Algebraicity of the source is not needed and is not assumed, which is what distinguishes this from AlgebraicGeometry.Space.isFiniteType_comp.

theorem isFiniteType_comp' (f : X ⟶ Y) (g : Y ⟶ Z)
    (hY : IsAlgebraicSpace B S hS Y) (hZ : IsAlgebraicSpace B S hS Z)
    (hf : IsFiniteType B S hS f) (hg : IsFiniteType B S hS g) :
    IsFiniteType B S hS (f ≫ g)

Tag 03XH, a lemma

Tag 03XH in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeProperties.lean, line 156. The attribute's comment: “locally of finite type”.

Stacks 03XH, the case of being locally of finite type: being locally of finite type is stable under base change.

Being locally of finite type is étale local on the source and target (Stacks 04R3) and stable under base change (Stacks 01T4), so this is an instance of Stacks 0AMM.

theorem isLocallyOfFiniteType_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        IsLocallyOfFiniteType B S hS f.hom)

AlgebraicGeometry.Space.isFiniteType_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperBaseChange.lean, line 66. The attribute's comment: “finite type”.

Being of finite type is stable under base change for morphisms of algebraic spaces over S.

instance isFiniteType_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsFiniteType B S hS f.hom)

AlgebraicGeometry.Space.IsLocallyOfFiniteType.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteBaseChange.lean, line 285. The attribute's comment: “locally of finite type”.

The base change of a morphism of algebraic spaces over S which is locally of finite type along an arbitrary morphism of algebraic spaces is locally of finite type.

The square is the one with p over f, so p : W ⟶ Z is the base change of f : X ⟶ Y.

theorem IsLocallyOfFiniteType.of_isPullback
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFiniteType B S hS p

AlgebraicGeometry.Space.IsFiniteType.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteBaseChange.lean, line 303. The attribute's comment: “finite type”.

The base change of a morphism of algebraic spaces over S which is of finite type along an arbitrary morphism of algebraic spaces is of finite type.

theorem IsFiniteType.of_isPullback
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsFiniteType B S hS f) :
    IsFiniteType B S hS p

Tag 040Y, a lemma

Tag 040Y in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_iff_holdsOnEveryEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeTfae.lean, line 161. The attribute's comment: “conditions (1) and (7)”.

Stacks 040Y, conditions (1) and (7). A morphism of algebraic spaces over S is locally of finite type exactly when the scheme morphism induced in every commuting square of étale charts of it is locally of finite type. This is AlgebraicGeometry.Space.IsLocallyOfFiniteType unfolded.

theorem isLocallyOfFiniteType_iff_holdsOnEveryEtaleChart (f : X ⟶ Y) :
    IsLocallyOfFiniteType B S hS f ↔
      HoldsOnEveryEtaleChart B S hS
        (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) f

AlgebraicGeometry.Space.isLocallyOfFiniteType_iff_holdsOnSurjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeTfae.lean, line 228. The attribute's comment: “conditions (1) and (8)”.

Stacks 040Y, conditions (1) and (8). A morphism of algebraic spaces over S is locally of finite type exactly when it is locally of finite type on one commuting square of étale charts whose chart of the source is surjective.

theorem isLocallyOfFiniteType_iff_holdsOnSurjectiveEtaleChart
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsLocallyOfFiniteType B S hS f ↔
      HoldsOnSurjectiveEtaleChart B S hS
        (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) f

AlgebraicGeometry.Space.isLocallyOfFiniteType_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeTfae.lean, line 242. The attribute's comment: “condition (1) implies condition (3)”.

Stacks 040Y, condition (1) implies condition (3). The base change of a morphism of algebraic spaces over S which is locally of finite type to any scheme over its target is locally of finite type. This is Stacks 03XH for the cartesian square of the base change.

theorem isLocallyOfFiniteType_pullback_fst
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocallyOfFiniteType B S hS f) (V : BigFppfOver B S hS)
    (g : yoneda.obj V ⟶ Y) :
    IsLocallyOfFiniteType B S hS (pullback.fst g f)

AlgebraicGeometry.Space.isLocallyOfFiniteType_iff_exists_etale_atlas_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeTfae.lean, line 299. The attribute's comment: “conditions (1) and (5)”.

Stacks 040Y, conditions (1) and (5). A morphism of algebraic spaces over S is locally of finite type exactly when its base change to some surjective étale scheme over its target is locally of finite type.

theorem isLocallyOfFiniteType_iff_exists_etale_atlas_pullback
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsLocallyOfFiniteType B S hS f ↔
      ∃ (V : BigFppfOver B S hS) (b : yoneda.obj V ⟶ Y),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) b ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) b ∧
        IsLocallyOfFiniteType B S hS (pullback.fst b f)

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

Stacks 040Y, conditions (1) and (3). A morphism of algebraic spaces over S is locally of finite type exactly when its base change to every scheme over its target is locally of finite type.

theorem isLocallyOfFiniteType_iff_forall_pullback_fst
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsLocallyOfFiniteType B S hS f ↔
      ∀ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsLocallyOfFiniteType B S hS (pullback.fst g f)

AlgebraicGeometry.Space.isLocallyOfFiniteType_iff_exists_surjective_etale_source_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeTfae.lean, line 374. The attribute's comment: “conditions (1) and (6)”.

Stacks 040Y, conditions (1) and (6). A morphism of algebraic spaces over S is locally of finite type exactly when its composite with some surjective étale chart of its source is locally of finite type.

For the forward direction an atlas of the source is étale, hence locally of finite type by Stacks 06LT, and local finite type is stable under composition by Stacks 03XG.

theorem isLocallyOfFiniteType_iff_exists_surjective_etale_source_chart
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsLocallyOfFiniteType B S hS f ↔
      ∃ (U₀ : BigFppfOver B S hS) (φ : yoneda.obj U₀ ⟶ X),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) φ ∧
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) φ ∧
        IsLocallyOfFiniteType B S hS (φ ≫ f)

AlgebraicGeometry.Space.isLocallyOfFiniteType_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FiniteType.lean, line 697.

Stacks 040Y. For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following nine conditions are equivalent: f is locally of finite type; f is of finite type at every point of X; the base change of f along every morphism from a scheme over S is locally of finite type; the same for every morphism from an affine scheme over S; the base change of f along some surjective étale chart of Y is locally of finite type; the composite of f with some surjective étale chart of X is locally of finite type; every commuting square of étale charts of f induces a scheme morphism which is locally of finite type; some such square whose chart of X is surjective does; and there are Zariski coverings of Y and of the inverse images in X of its members over which f is locally of finite type.

theorem isLocallyOfFiniteType_tfae (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [IsLocallyOfFiniteType B S hS f,
       (∀ x : points B S hS X, IsFiniteTypeAt B S hS f x),
       (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsLocallyOfFiniteType B S hS (pullback.fst g f)),
       (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
          IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
            IsLocallyOfFiniteType B S hS (pullback.fst g f)),
       (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y), IsSurjective B S hS g ∧
          IsEtale B S hS g ∧ IsLocallyOfFiniteType B S hS (pullback.fst g f)),
       (∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ X), IsSurjective B S hS g ∧
          IsEtale B S hS g ∧ IsLocallyOfFiniteType B S hS (g ≫ f)),
       HoldsOnEveryEtaleChart B S hS
         (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) f,
       HoldsOnSurjectiveEtaleChart B S hS
         (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) f,
       (∃ (I : Type u) (Yᵢ : I → Subfunctor Y), IsZariskiCover B S hS I Yᵢ ∧
          ∀ i, ∃ (J : Type u) (Xᵢⱼ : J → Subfunctor ((Yᵢ i).preimage f).toFunctor),
            IsZariskiCover B S hS J Xᵢⱼ ∧
              ∀ j, IsLocallyOfFiniteType B S hS
                ((Xᵢⱼ j).ι ≫ (Yᵢ i).fromPreimage f))]

AlgebraicGeometry.Space.isFiniteTypeAt_of_isLocallyOfFiniteType', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteAtPoint.lean, line 179. The attribute's comment: “condition (1) implies condition (2)”.

Stacks 040Y, condition (1) implies condition (2). A morphism locally of finite type is of finite type at every point of its source.

Only the source has to be an algebraic space, which is what distinguishes this from AlgebraicGeometry.Space.isFiniteTypeAt_of_isLocallyOfFiniteType: that form goes through the permanence of local finite type under composition and so carries an algebraicity hypothesis on the target as well.

theorem isFiniteTypeAt_of_isLocallyOfFiniteType' (hX : IsAlgebraicSpace B S hS X)
    {f : X ⟶ Y} (hf : IsLocallyOfFiniteType B S hS f) (x : points B S hS X) :
    IsFiniteTypeAt B S hS f x

Tag 04ZK, a lemma

Tag 04ZK in the Stacks Project.

AlgebraicGeometry.Space.isLocallyNoetherian_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyNoetherianFiniteType.lean, line 40. References: EGA IV (1.3.3); EGA I (6.3.7), “locally Noetherian”.

A morphism of algebraic spaces over S which is locally of finite type and whose target is locally Noetherian has locally Noetherian source.

theorem isLocallyNoetherian_of_isLocallyOfFiniteType
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (hN : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T)

Tag 0462, a lemma

Tag 0462 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeProperties.lean, line 206. References: EGA I (6.6.6), “(v)”; EGA IV (1.3.4), “(v)”.

Stacks 0462. If a composite of morphisms of algebraic spaces over S is locally of finite type, then so is its first factor.

This is also the locally-of-finite-type clause of part (1) of Stacks 0AGC, whose other clauses are in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean.

theorem isLocallyOfFiniteType_of_comp
    {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 : G ⟶ H)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g)) :
    IsLocallyOfFiniteType B S hS f

Tag 06ED, a lemma

Tag 06ED in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FiniteType.lean, line 146.

Stacks 06ED. An immersion of algebraic spaces over S is locally of finite type. Each of its represented base changes is an immersion of schemes, hence locally of finite type, and being locally of finite type passes from the represented base changes to the étale charts by the implication of Stacks 03MJ.

theorem isLocallyOfFiniteType_of_isImmersion (f : X ⟶ Y) (hf : IsImmersion B S hS f) :
    IsLocallyOfFiniteType B S hS f

Sources

LeanAlgebraicGeometry.Space.IsLocallyOfFiniteType · AlgebraicGeometry.Space.IsFiniteType · AlgebraicGeometry.Space.IsFiniteTypeAt · AlgebraicGeometry.Space.isLocallyOfFiniteType_comp' · AlgebraicGeometry.Space.isLocallyOfFiniteType_comp · AlgebraicGeometry.Space.isFiniteType_comp · AlgebraicGeometry.Space.isFiniteType_comp' · AlgebraicGeometry.Space.isLocallyOfFiniteType_isStableUnderBaseChange

Section67.24 Points and geometric points #

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

Tag 0487, a lemma

Tag 0487 in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_iff_surjective_app_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 610. References: EGA IV (1.3.7), “more general”; EGA I (6.3.10), “more general”.

Stacks 0487. A morphism of algebraic spaces over S which is locally of finite type is surjective exactly when, for every algebraically closed field k of the working universe whose spectrum lies in the chosen site and every structure morphism Spec k ⟶ S, the induced map X(k) ⟶ Y(k) is surjective.

theorem isSurjective_iff_surjective_app_isAlgClosed
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) :
    IsSurjective B S hS f ↔
      ∀ (k : Type u) [Field k] [IsAlgClosed k] (hk : B.Contains (Spec (.of k)))
        (b : Spec (.of k) ⟶ S),
        Function.Surjective
          (f.app (Opposite.op (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS))))

Tag 0488, a lemma

Tag 0488 in the Stacks Project.

AlgebraicGeometry.Space.geometricPoints_large_enough, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeEnoughFields.lean, line 76.

Stacks 0488. Let S be a scheme and let X, Y be algebraic spaces over S.

As k ranges over all algebraically closed fields over S the geometric points ȳ ∈ Y(k) cover all of |Y|.

As k ranges over all algebraically closed fields over S with |k| ≥ λ(Y) and |k| > λ(X) the geometric points ȳ ∈ Y(k) cover all of |Y|.

For any geometric point s̄ : Spec k → S where k has cardinality > λ(X) the map X(k) → |X_s| is surjective.

For a morphism X → Y and any geometric point s̄ : Spec k → S where k has cardinality > λ(X), the map X(k) → |X| ×_{|Y|} Y(k) is surjective.

A morphism X → Y is surjective if and only if X(k) → Y(k) is surjective for all algebraically closed fields k over S with |k| > λ(X) and |k| ≥ λ(Y).

Following the source, λ(X) and λ(Y) are the cardinals AlgebraicGeometry.Scheme.lambdaCard of schemes carrying a surjective étale morphism onto X and onto Y; the clauses quantify over all such atlases.

theorem geometricPoints_large_enough
    (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) :
    -- (1) geometric points cover the point set
    (∀ y : points B S hS Y, ∃ p : GeometricPoint B S hS Y, p.image = y) ∧
    -- (2) geometric points over large enough fields cover the point set
    (∀ (UX UY : BigFppfOver B S hS) (fX : yoneda.obj UX ⟶ X) (fY : yoneda.obj UY ⟶ Y),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fX →
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fX →
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fY →
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fY →
      ∀ y : points B S hS Y, ∃ p : GeometricPoint B S hS Y, p.LiesOver y ∧
        ((BigFppfOver.toScheme B S hS).obj UY).lambdaCard ≤ Cardinal.mk p.val.carrier ∧
        ((BigFppfOver.toScheme B S hS).obj UX).lambdaCard < Cardinal.mk p.val.carrier) ∧
    -- (3) `X(k) → |X_s|` is surjective
    (∀ (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ X),
      (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 →
      ∀ (k : Type u) [Field k] [IsAlgClosed k] (hk : B.Contains (Spec (.of k)))
        (b : Spec (.of k) ⟶ S),
        ((BigFppfOver.toScheme B S hS).obj U).lambdaCard < Cardinal.mk k →
      ∀ (s : S) (hs : ∀ t, b t = s) (Xs : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
        (pr : Xs ⟶ X) (pr' : Xs ⟶ yoneda.obj (residueSiteObject B S hS s))
        (hpb : IsPullback pr pr' (toBaseSiteMap B S hS X)
          (yoneda.map (toBaseSiteObject B S hS (residueSiteObject B S hS s)))),
        Function.Surjective (fibrePointOfFieldPoint B S hS hk b s hs pr pr' hpb)) ∧
    -- (4) `X(k) → |X| ×_{|Y|} Y(k)` is surjective
    (∀ (a : X ⟶ Y) (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ X),
      (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 →
      ∀ (k : Type u) [Field k] [IsAlgClosed k] (hk : B.Contains (Spec (.of k)))
        (b : Spec (.of k) ⟶ S),
        ((BigFppfOver.toScheme B S hS).obj U).lambdaCard < Cardinal.mk k →
      ∀ (x : points B S hS X)
        (y : Y.obj (Opposite.op (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS)))),
        pointsMap B S hS X a x =
            (⟨k, hk, b, y⟩ : FieldValuedPoint B S hS Y).class B S hS Y →
        ∃ z : X.obj (Opposite.op (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS))),
          a.app (Opposite.op (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS))) z = y ∧
          (⟨k, hk, b, z⟩ : FieldValuedPoint B S hS X).class B S hS X = x) ∧
    -- (5) surjectivity is tested on the field-valued points over large enough fields
    (∀ (a : X ⟶ Y) (UX UY : BigFppfOver B S hS)
        (fX : yoneda.obj UX ⟶ X) (fY : yoneda.obj UY ⟶ Y),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fX →
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fX →
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fY →
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) fY →
      (IsSurjective B S hS a ↔
        ∀ (k : Type u) [Field k] [IsAlgClosed k] (hk : B.Contains (Spec (.of k)))
          (b : Spec (.of k) ⟶ S),
          ((BigFppfOver.toScheme B S hS).obj UX).lambdaCard < Cardinal.mk k →
          ((BigFppfOver.toScheme B S hS).obj UY).lambdaCard ≤ Cardinal.mk k →
          Function.Surjective
            (a.app (Opposite.op (Over.mk (⟨b⟩ : B.obj hk ⟶ B.obj hS))))))

Sources

LeanAlgebraicGeometry.Space.isSurjective_iff_surjective_app_isAlgClosed · AlgebraicGeometry.Space.geometricPoints_large_enough

Section67.25 Points of finite type #

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

Tag 06EF, a lemma

Tag 06EF in the Stacks Project.

AlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_isClosed_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 396.

Stacks 06EF, and the assertion of Stacks 06EH for arbitrary scheme charts. A point of an algebraic space over S is a finite type point exactly when it is the image of a closed point of a scheme étale over the space.

theorem isFiniteTypePoint_iff_exists_isClosed_etaleChart
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (x : points B S hS X) :
    IsFiniteTypePoint B S hS X x ↔
      ∃ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
        (p : FieldValuedPoint B S hS (yoneda.obj U)),
        IsEtale B S hS φ ∧
          IsClosed ({schemePoint B S hS U p} : Set ((BigFppfOver.toScheme B S hS).obj U)) ∧
          pointsMap B S hS (yoneda.obj U) φ (p.class B S hS (yoneda.obj U)) = x

Tag 06EG, a definition

Tag 06EG in the Stacks Project.

AlgebraicGeometry.Space.IsFiniteTypePoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 190. The attribute's comment: “finite type point”.

Stacks 06EG. A point of an algebraic space over S is a finite type point when some field-valued point representing it has a morphism to the space which is locally of finite type.

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

AlgebraicGeometry.Space.finiteTypePoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 197. The attribute's comment: “set of finite type points”.

Stacks 06EG. The set X_{ft-pts} of finite type points of an algebraic space over S.

abbrev finiteTypePoints (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Set (points B S hS X)

Tag 06EH, a lemma

Tag 06EH in the Stacks Project.

AlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_isClosed_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 396. The attribute's comment: “all scheme charts”.

Stacks 06EF, and the assertion of Stacks 06EH for arbitrary scheme charts. A point of an algebraic space over S is a finite type point exactly when it is the image of a closed point of a scheme étale over the space.

theorem isFiniteTypePoint_iff_exists_isClosed_etaleChart
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (x : points B S hS X) :
    IsFiniteTypePoint B S hS X x ↔
      ∃ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
        (p : FieldValuedPoint B S hS (yoneda.obj U)),
        IsEtale B S hS φ ∧
          IsClosed ({schemePoint B S hS U p} : Set ((BigFppfOver.toScheme B S hS).obj U)) ∧
          pointsMap B S hS (yoneda.obj U) φ (p.class B S hS (yoneda.obj U)) = x

AlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_isAffine_isClosed_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 416. The attribute's comment: “affine scheme charts”.

Stacks 06EH, the assertion for affine scheme charts. A point of an algebraic space over S is a finite type point exactly when it is the image of a closed point of an affine scheme étale over the space.

theorem isFiniteTypePoint_iff_exists_isAffine_isClosed_etaleChart
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (x : points B S hS X) :
    IsFiniteTypePoint B S hS X x ↔
      ∃ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
        (p : FieldValuedPoint B S hS (yoneda.obj U)),
        IsAffine ((BigFppfOver.toScheme B S hS).obj U) ∧ IsEtale B S hS φ ∧
          IsClosed ({schemePoint B S hS U p} : Set ((BigFppfOver.toScheme B S hS).obj U)) ∧
          pointsMap B S hS (yoneda.obj U) φ (p.class B S hS (yoneda.obj U)) = x

Tag 06EI, a lemma

Tag 06EI in the Stacks Project.

AlgebraicGeometry.Space.mapsTo_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 283.

A locally finite type morphism of algebraic spaces over S carries finite type points to finite type points. This is the algebraic-space counterpart of Stacks 02J3, and is the easy inclusion of AlgebraicGeometry.Space.image_finiteTypePoints_eq.

theorem mapsTo_finiteTypePoints {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    Set.MapsTo (pointsMap B S hS X f) (finiteTypePoints B S hS X)
      (finiteTypePoints B S hS Y)

Tag 06EJ, a lemma

Tag 06EJ in the Stacks Project.

AlgebraicGeometry.Space.image_finiteTypePoints_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 494.

Stacks 06EJ. A surjective morphism of algebraic spaces over S which is locally of finite type maps the finite type points of its source onto the finite type points of its target.

One inclusion is AlgebraicGeometry.Space.mapsTo_finiteTypePoints. For the other, a finite type point of the target is represented by a locally finite type morphism from a field spectrum; the fibre product of the source with that field spectrum over the target is a nonempty algebraic space locally of finite type over the source, so it has a finite type point by Stacks 06EK, whose image in the source is the required point.

theorem image_finiteTypePoints_eq {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hsurj : IsSurjective B S hS f) :
    pointsMap B S hS X f '' finiteTypePoints B S hS X = finiteTypePoints B S hS Y

Tag 06EK, a lemma

Tag 06EK in the Stacks Project.

AlgebraicGeometry.Space.inter_finiteTypePoints_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 443. The attribute's comment: “locally closed subsets”.

Stacks 06EK, locally closed subsets. A nonempty locally closed set of points of an algebraic space over S contains a finite type point.

The set is pulled back to a surjective étale scheme chart, where it is again nonempty and locally closed because the map on points is continuous and surjective and the point topology of a represented presheaf is the topology of the representing scheme; Stacks 02J4 produces a finite type point there and its image in |X| is a finite type point by Stacks 02J3.

theorem inter_finiteTypePoints_nonempty (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) {T : Set (points B S hS X)}
    (hT : IsLocallyClosed T) (hne : T.Nonempty) :
    (T ∩ finiteTypePoints B S hS X).Nonempty

AlgebraicGeometry.Space.closure_inter_finiteTypePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PointsOfFiniteType.lean, line 472. The attribute's comment: “closed subsets”.

Stacks 06EK, closed subsets. The finite type points lying in a closed set of points of an algebraic space over S are dense in it.

theorem closure_inter_finiteTypePoints (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) {T : Set (points B S hS X)} (hT : IsClosed T) :
    closure (T ∩ finiteTypePoints B S hS X) = T

Tag 06EL, a lemma

Tag 06EL in the Stacks Project.

AlgebraicGeometry.Space.isFiniteTypePoint_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypePointTfae.lean, line 78.

Let S be a scheme, let X be an algebraic space over S and let x be a point of X. The following are equivalent:

x is a finite type point;

there is an algebraic space Z whose space of points is a singleton and a morphism f : Z ⟶ X which is locally of finite type with {x} the image of |f|;

there is an algebraic space Z and a morphism f : Z ⟶ X such that Z carries a surjective étale morphism from the spectrum of a field, f is locally of finite type, f is a monomorphism, and x is the image under |f| of the point of that field spectrum.

Conditions (1) and (2) are equivalent by AlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_singleton_space; condition (1) implies condition (3) by AlgebraicGeometry.Space.exists_mono_isLocallyOfFiniteType_etale_fieldPoint_of_isFiniteTypePoint, and condition (3) implies condition (1) by AlgebraicGeometry.Space.isFiniteTypePoint_pointsMap_of_isSurjective_fieldPoint.

theorem isFiniteTypePoint_tfae (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) (x : points B S hS X) :
    [IsFiniteTypePoint B S hS X x,
      ∃ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z) (f : Z ⟶ X),
        Nonempty (points B S hS Z) ∧ Subsingleton (points B S hS Z) ∧
          IsLocallyOfFiniteType B S hS f ∧ Set.range (pointsMap B S hS Z f) = {x},
      ∃ (Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z) (f : Z ⟶ X)
          (z : FieldValuedPoint B S hS Z),
        IsSurjective B S hS (yonedaEquiv.symm z.value) ∧
          IsEtale B S hS (yonedaEquiv.symm z.value) ∧
          IsLocallyOfFiniteType B S hS f ∧ Mono f ∧
          x = pointsMap B S hS Z f (z.class B S hS Z)].TFAE

Sources

LeanAlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_isClosed_etaleChart · AlgebraicGeometry.Space.IsFiniteTypePoint · AlgebraicGeometry.Space.finiteTypePoints · AlgebraicGeometry.Space.isFiniteTypePoint_iff_exists_isAffine_isClosed_etaleChart · AlgebraicGeometry.Space.mapsTo_finiteTypePoints · AlgebraicGeometry.Space.image_finiteTypePoints_eq · AlgebraicGeometry.Space.inter_finiteTypePoints_nonempty · AlgebraicGeometry.Space.closure_inter_finiteTypePoints

Section67.26 Nagata spaces #

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

Tag 0BAU, a lemma

Tag 0BAU in the Stacks Project.

AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 306.

Stacks 0BAU. A morphism of algebraic spaces over S which is locally of finite type and whose target is Nagata has Nagata source.

A surjective étale chart q : h_V ⟶ Y witnessing that the target is Nagata lifts, by Stacks 02X1, to a surjective étale chart p : h_U ⟶ X of the source and a morphism α : U ⟶ V of the site making the square commute. Local finite type of the morphism tests exactly such squares, so the scheme morphism underlying α is locally of finite type with Nagata target, whence U is Nagata by Stacks 035A and p is the required chart.

theorem isNagata_of_isLocallyOfFiniteType
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (hN : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsNagataScheme T)) :
    HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsNagataScheme T)

Tag 0BAV, a lemma

Tag 0BAV in the Stacks Project.

AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_nagataScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 333. The attribute's comment: “part (1): over a Nagata scheme”.

Stacks 0BAV, part (1). An algebraic space over S locally of finite type over a Nagata scheme is Nagata.

theorem isNagata_of_isLocallyOfFiniteType_over_nagataScheme (hX : IsAlgebraicSpace B S hS X)
    (T : BigFppfOver B S hS) (hT : IsNagataScheme ((BigFppfOver.toScheme B S hS).obj T))
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    HasEtaleLocalProperty B S hS X (fun Z : Scheme.{u} => IsNagataScheme Z)

AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 345. The attribute's comment: “part (2): over a field”.

Stacks 0BAV, part (2). An algebraic space over S locally of finite type over a field is Nagata.

theorem isNagata_of_isLocallyOfFiniteType_over_field (hX : IsAlgebraicSpace B S hS X)
    (k : Type u) [Field k] (T : BigFppfOver B S hS)
    (e : (BigFppfOver.toScheme B S hS).obj T ≅ Spec (.of k))
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    HasEtaleLocalProperty B S hS X (fun Z : Scheme.{u} => IsNagataScheme Z)

AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_completeLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 358. The attribute's comment: “part (3): over a Noetherian complete local ring”.

Stacks 0BAV, part (3). An algebraic space over S locally of finite type over a Noetherian complete local ring is Nagata. Completeness is IsPrecomplete (IsLocalRing.maximalIdeal R) R, as in Stacks 032W.

theorem isNagata_of_isLocallyOfFiniteType_over_completeLocalRing (hX : IsAlgebraicSpace B S hS X)
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) R] (T : BigFppfOver B S hS)
    (e : (BigFppfOver.toScheme B S hS).obj T ≅ Spec (.of R))
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    HasEtaleLocalProperty B S hS X (fun Z : Scheme.{u} => IsNagataScheme Z)

AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_int, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 372. The attribute's comment: “part (4): over the integers”.

Stacks 0BAV, part (4). An algebraic space over S locally of finite type over the integers is Nagata. "Over the integers" is read as "over the terminal scheme of the ambient universe", which is the spectrum of ULift ℤ.

theorem isNagata_of_isLocallyOfFiniteType_over_int (hX : IsAlgebraicSpace B S hS X)
    (T : BigFppfOver B S hS) (hT : IsTerminal ((BigFppfOver.toScheme B S hS).obj T))
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    HasEtaleLocalProperty B S hS X (fun Z : Scheme.{u} => IsNagataScheme Z)

AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_dedekindDomain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 385. The attribute's comment: “part (5): over a Dedekind domain of characteristic zero”.

Stacks 0BAV, part (5). An algebraic space over S locally of finite type over a Dedekind domain of characteristic zero is Nagata.

theorem isNagata_of_isLocallyOfFiniteType_over_dedekindDomain (hX : IsAlgebraicSpace B S hS X)
    (R : Type u) [CommRing R] [IsDedekindDomain R] [CharZero R] (T : BigFppfOver B S hS)
    (e : (BigFppfOver.toScheme B S hS).obj T ≅ Spec (.of R))
    (f : X ⟶ yoneda.obj T) (hf : IsLocallyOfFiniteType B S hS f) :
    HasEtaleLocalProperty B S hS X (fun Z : Scheme.{u} => IsNagataScheme Z)

Sources

LeanAlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType · AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_nagataScheme · AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_field · AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_completeLocalRing · AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_int · AlgebraicGeometry.Space.isNagata_of_isLocallyOfFiniteType_over_dedekindDomain

Section67.27 Quasi-finite morphisms #

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

Tag 03XJ, a definition

Tag 03XJ in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyQuasiFinite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteType.lean, line 97. The attribute's comment: “part (1): locally quasi-finite morphisms”.

Stacks 03XJ, part (1). A morphism of algebraic spaces over S is locally quasi-finite when every commuting square of étale scheme charts induces a scheme morphism which is locally of finite type and locally quasi-finite.

abbrev IsLocallyQuasiFinite (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsQuasiFinite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteType.lean, line 105. The attribute's comment: “part (3): quasi-finite morphisms”.

Stacks 03XJ, part (3). A morphism of algebraic spaces over S is quasi-finite when it is locally quasi-finite and quasi-compact.

abbrev IsQuasiFinite (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsQuasiFiniteAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteType.lean, line 124. The attribute's comment: “part (2): quasi-finite at a point”.

Stacks 03XJ, part (2). A morphism of algebraic spaces over S is quasi-finite at a point x of its source when some open subspace of the source containing x is locally quasi-finite over the target.

abbrev IsQuasiFiniteAt (f : X ⟶ Y) (x : points B S hS X) : Prop

Tag 0ABM, a lemma

Tag 0ABM in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyQuasiFinite.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteBaseChange.lean, line 321. The attribute's comment: “part (3): locally quasi-finite”.

The base change of a locally quasi-finite morphism of algebraic spaces over S along an arbitrary morphism of algebraic spaces is locally quasi-finite.

The square is the one with p over f, so p : W ⟶ Z is the base change of f : X ⟶ Y.

theorem IsLocallyQuasiFinite.of_isPullback
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyQuasiFinite B S hS f) :
    IsLocallyQuasiFinite B S hS p

AlgebraicGeometry.Space.IsQuasiFinite.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteBaseChange.lean, line 338. The attribute's comment: “part (4): quasi-finite”.

The base change of a quasi-finite morphism of algebraic spaces over S along an arbitrary morphism of algebraic spaces is quasi-finite.

theorem IsQuasiFinite.of_isPullback
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsQuasiFinite B S hS f) :
    IsQuasiFinite B S hS p

AlgebraicGeometry.Space.isOpen_setOf_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteLocus.lean, line 195. The attribute's comment: “part (1): the quasi-finite locus is open”.

Stacks 0ABM, part (1). The set of points at which a morphism of algebraic spaces over S is quasi-finite is open in the point space of Tag 03BU. Applied to a base change f' of f this is the second clause of part (1), that the quasi-finite locus of f' is open.

The source assumes f locally of finite type; that is not needed.

theorem isOpen_setOf_isQuasiFiniteAt (f : X ⟶ Y) :
    IsOpen {x | IsQuasiFiniteAt B S hS f x}

AlgebraicGeometry.Space.setOf_isQuasiFiniteAt_eq_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteLocus.lean, line 238. The attribute's comment: “part (2): the locus commutes with base change”. References: SGA 3 V (7.4), “more general”.

Stacks 0ABM, part (2). For a morphism of algebraic spaces over S which is locally of finite type, the locus of quasi-finiteness of a base change is the inverse image of the locus of quasi-finiteness of the morphism.

Compatible surjective étale charts of the cartesian square (AlgebraicGeometry.Space.exists_compatible_etale_charts) give a chart V of the target, a chart U ⟶ V of f, a chart V' ⟶ V of g and the induced chart U' = U ×_V V' ⟶ V' of the base change, with U' an atlas of the fibre product. A field-valued point of U' lying over the given point of |X'| turns the two squares into pointed étale charts of f' at that point and of f at its image, whose selected scheme points correspond under U' ⟶ U. Local quasi-finiteness of morphisms of schemes being étale local on the source and target (Stacks 04R3), quasi-finiteness at a point is the induced germ condition read in any one pointed chart (Stacks 04NC), so each side becomes quasi-finiteness of a morphism of schemes at corresponding points of a cartesian square of schemes, which is Stacks 01TM.

theorem setOf_isQuasiFiniteAt_eq_preimage_of_isPullback
    {X₁ X₀ Y₁ Y₀ : AlgebraicSpaces B S hS} {g' : X₁ ⟶ X₀} {f' : X₁ ⟶ Y₁} {f : X₀ ⟶ Y₀}
    {g : Y₁ ⟶ Y₀} (sq : IsPullback g' f' f g)
    (hf : IsLocallyOfFiniteType B S hS f.hom) :
    {x' | IsQuasiFiniteAt B S hS f'.hom x'} =
      pointsMap B S hS X₁.1 g'.hom ⁻¹' {x | IsQuasiFiniteAt B S hS f.hom x}

AlgebraicGeometry.Space.setOf_isQuasiFiniteAt_eq_preimage_of_isPullback', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteLocusBaseChange.lean, line 111. The attribute's comment: “part (2): the quasi-finite locus commutes with base change”.

In a cartesian square of presheaves over S whose corners X, Y and Z are algebraic spaces, with f locally of finite type, the locus in the source of the base change of f where that base change is quasi-finite is the preimage, under the projection on points, of the locus in the source of f where f is quasi-finite.

The square is the one with p over f and q over g, so p : W ⟶ Z is the base change of f : X ⟶ Y and q : W ⟶ X is the projection.

theorem setOf_isQuasiFiniteAt_eq_preimage_of_isPullback'
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (hf : IsLocallyOfFiniteType B S hS f) :
    {x' | IsQuasiFiniteAt B S hS p x'} =
      pointsMap B S hS W q ⁻¹' {x | IsQuasiFiniteAt B S hS f x}

Tag 03XK, a lemma

Tag 03XK in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteMorphismProperty.lean, line 76. The attribute's comment: “locally quasi-finite”.

Stacks 03XK, the locally quasi-finite case: the composite of two locally quasi-finite morphisms of algebraic spaces over S is locally quasi-finite.

Local quasi-finiteness of morphisms of schemes is étale local on the source and target (Stacks 04R3) and stable under composition, each conjunct being, so this is an instance of Stacks 0AML.

theorem isLocallyQuasiFinite_comp {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 : G ⟶ H)
    (hf : IsLocallyQuasiFinite B S hS f) (hg : IsLocallyQuasiFinite B S hS g) :
    IsLocallyQuasiFinite B S hS (f ≫ g)

AlgebraicGeometry.Space.isQuasiFinite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteMorphismProperty.lean, line 94. The attribute's comment: “quasi-finite”.

Stacks 03XK, the quasi-finite case: the composite of two quasi-finite morphisms of algebraic spaces over S is quasi-finite.

Quasi-finiteness is local quasi-finiteness together with quasi-compactness, and the latter is stable under composition by Stacks 03HG.

theorem isQuasiFinite_comp {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 : G ⟶ H)
    (hf : IsQuasiFinite B S hS f) (hg : IsQuasiFinite B S hS g) :
    IsQuasiFinite B S hS (f ≫ g)

Tag 03XL, a lemma

Tag 03XL in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyQuasiFinite.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteBaseChange.lean, line 321. The attribute's comment: “locally quasi-finite”.

The base change of a locally quasi-finite morphism of algebraic spaces over S along an arbitrary morphism of algebraic spaces is locally quasi-finite.

The square is the one with p over f, so p : W ⟶ Z is the base change of f : X ⟶ Y.

theorem IsLocallyQuasiFinite.of_isPullback
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyQuasiFinite B S hS f) :
    IsLocallyQuasiFinite B S hS p

AlgebraicGeometry.Space.IsQuasiFinite.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteBaseChange.lean, line 338. The attribute's comment: “quasi-finite”.

The base change of a quasi-finite morphism of algebraic spaces over S along an arbitrary morphism of algebraic spaces is quasi-finite.

theorem IsQuasiFinite.of_isPullback
    {W X Z 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)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsQuasiFinite B S hS f) :
    IsQuasiFinite B S hS p

AlgebraicGeometry.Space.isLocallyQuasiFinite_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteMorphismProperty.lean, line 109. The attribute's comment: “locally quasi-finite”.

Stacks 03XL, the locally quasi-finite case: being locally quasi-finite is stable under base change.

Local quasi-finiteness of morphisms of schemes is étale local on the source and target (Stacks 04R3) and stable under base change, each conjunct being, so this is an instance of Stacks 0AMM.

instance isLocallyQuasiFinite_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        IsLocallyQuasiFinite B S hS f.hom)

AlgebraicGeometry.Space.isQuasiFinite_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteMorphismProperty.lean, line 125. The attribute's comment: “quasi-finite”.

Stacks 03XL, the quasi-finite case: being quasi-finite is stable under base change.

Quasi-finiteness is local quasi-finiteness together with quasi-compactness, and the latter is stable under base change by Stacks 03HF.

instance isQuasiFinite_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsQuasiFinite B S hS f.hom)

Tag 06RW, a lemma

Tag 06RW in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_forall_discreteTopology_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiFinite.lean, line 1426.

Stacks 06RW. A morphism of algebraic spaces over S which is locally of finite type is locally quasi-finite exactly when, for every field-valued point of its target, the point space of the fibre over that point is discrete.

For the forward implication the fibre over a field-valued point is locally quasi-finite over the field spectrum by Stacks 03XL, so its étale charts are discrete schemes; an étale chart is open and surjective on points, hence the point space of the fibre is discrete.

For the converse a commuting square of étale charts of f is compared with the fibre product of the chart of the target along f, and each point of the chart of the target is handled through its canonical residue-field representative: the fibre of the morphism of the site over that point is a chart of the corresponding fibre of f, which is discrete, so the morphism of the site has no nontrivial specialization in that fibre and is therefore locally quasi-finite by [Stacks Project, Tag 01TH].

theorem isLocallyQuasiFinite_iff_forall_discreteTopology_fibre
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hft : IsLocallyOfFiniteType B S hS f) :
    IsLocallyQuasiFinite B S hS f ↔
      ∀ p : FieldValuedPoint B S hS Y,
        DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f))

Tag 040Z, a lemma

Tag 040Z in the Stacks Project.

AlgebraicGeometry.Space.locallyQuasiFinite_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiFinite.lean, line 781.

Stacks 040Z. Nine criteria for a morphism of algebraic spaces over S to be locally quasi-finite: pointwise quasi-finiteness, local quasi-finiteness of every base change to a scheme or to an affine scheme or to one surjective étale chart of the target, local quasi-finiteness of the composite with one surjective étale chart of the source, and local quasi-finiteness of the morphism of schemes in every — or in one surjective — commuting square of étale charts, or over a pair of Zariski coverings.

theorem locallyQuasiFinite_tfae {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [
      IsLocallyQuasiFinite B S hS f,
      ∀ x : points B S hS X, IsQuasiFiniteAt B S hS f x,
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsLocallyQuasiFinite B S hS (pullback.fst g f),
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          IsLocallyQuasiFinite B S hS (pullback.fst g f),
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧ IsEtale B S hS g ∧
          IsLocallyQuasiFinite B S hS (pullback.fst g f),
      ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X),
        IsSurjective B S hS p ∧ IsEtale B S hS p ∧ IsLocallyQuasiFinite B S hS (p ≫ f),
      ∀ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p → IsEtale B S hS q → p ≫ f = yoneda.map a ≫ q →
          IsLocallyQuasiFinite B S hS (yoneda.map a),
      ∃ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p ∧ IsEtale B S hS q ∧ IsSurjective B S hS p ∧
          p ≫ f = yoneda.map a ≫ q ∧ IsLocallyQuasiFinite B S hS (yoneda.map a),
      ∃ (I : Type u) (Yopen : I → Subfunctor Y) (J : I → Type u)
        (Xopen : ∀ i, J i → Subfunctor (pullback f (Yopen i).ι)),
        IsZariskiCover B S hS I Yopen ∧ (∀ i, IsZariskiCover B S hS (J i) (Xopen i)) ∧
          ∀ i j, IsLocallyQuasiFinite B S hS ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 03XM, a lemma

Tag 03XM in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiFinite.lean, line 498.

Stacks 03XM. An immersion of algebraic spaces over S is locally quasi-finite.

Neither the source nor the target has to be an algebraic space: the immersion property is a condition on the represented base changes of the morphism, and so is what the proof uses.

theorem isLocallyQuasiFinite_of_isImmersion {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (hf : IsImmersion B S hS f) :
    IsLocallyQuasiFinite B S hS f

Tag 03XN, a lemma

Tag 03XN in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiFinite.lean, line 417.

Stacks 03XN. If a composite of morphisms of algebraic spaces over S is locally quasi-finite, then so is its first factor.

Local quasi-finiteness of morphisms of schemes is étale local on the source and target (Stacks 04R3) and is inherited by the first factor of a composite that has it, local finite type by Stacks 01T8 and the fibre condition by AlgebraicGeometry.LocallyQuasiFinite.of_comp, so this is an instance of the cancellation form of Stacks 03MJ.

This is also the locally-quasi-finite clause of part (1) of Stacks 0AGC, whose other clauses are in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Immersions.lean.

theorem isLocallyQuasiFinite_of_comp {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 : G ⟶ H)
    (hfg : IsLocallyQuasiFinite B S hS (f ≫ g)) :
    IsLocallyQuasiFinite B S hS f

Tag 0ABN, a lemma

Tag 0ABN in the Stacks Project.

AlgebraicGeometry.Space.finite_setOf_mapsTo_and_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteLocus.lean, line 399.

Stacks 0ABN. For a morphism of algebraic spaces over S of finite type, only finitely many points of the source lying over a fixed point of the target are points at which the morphism is quasi-finite.

Represent the point of the target by a field-valued point Spec k ⟶ Y and base change twice: once along it, and once more along the identity of Spec k. The second base change is a finite-type morphism out of an algebraic space with quasi-compact source, so it has an affine surjective étale chart U (Stacks 03H6), and the morphism of schemes U ⟶ Spec k it induces is of finite type with compact source, hence quasi-compact: Stacks 0AAY bounds the set of its quasi-finite points over the closed point of Spec k, and that is all of U because Spec k is a one-point space.

A point of |X| over the given point at which f is quasi-finite lifts through both cartesian squares (Stacks 03H4), and quasi-finiteness travels with it because forming the quasi-finite locus commutes with base change (AlgebraicGeometry.Space.setOf_isQuasiFiniteAt_eq_preimage_of_isPullback). A field-valued representative of the lift on the chart then exhibits the point as the image of a member of that finite set.

theorem finite_setOf_mapsTo_and_isQuasiFiniteAt
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsFiniteType B S hS f) (y : points B S hS Y) :
    {x : points B S hS X |
      pointsMap B S hS X f x = y ∧ IsQuasiFiniteAt B S hS f x}.Finite

Tag 0463, a lemma

Tag 0463 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiFinite.lean, line 550. The attribute's comment: “local quasi-finiteness”.

Stacks 0463, the local quasi-finiteness clause: a monomorphism of algebraic spaces over S which is locally of finite type is locally quasi-finite.

The relative diagonal of a monomorphism is an isomorphism, hence an open immersion after every represented base change, so part (2) of [Stacks Project, Tag 05W1] makes the morphism unramified and [Stacks Project, Tag 05W0] makes it locally quasi-finite.

The separatedness clause of the tag is AlgebraicGeometry.Space.isSeparated_of_mono, which is [Stacks Project, Tag 042N] and needs no finite-type hypothesis.

theorem isLocallyQuasiFinite_of_mono {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hmono : Mono f) (hft : IsLocallyOfFiniteType B S hS f) :
    IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Space.isSeparated_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedQuasiFiniteEtaleDescent.lean, line 218. The attribute's comment: “separatedness”.

Stacks 042N. A monomorphism of presheaves on the big fppf site of S is a separated morphism of algebraic spaces over S: its relative diagonal is an isomorphism, and an isomorphism is a closed immersion. The statement is made for an arbitrary morphism of presheaves on the big fppf site of S; no algebraic-space hypothesis is used.

This strictly generalises AlgebraicGeometry.Space.isSeparated_of_isIso, which is the same statement for an isomorphism.

theorem isSeparated_of_mono {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (m : F ⟶ G) (hm : Mono m) :
    IsSeparated B S hS m

AlgebraicGeometry.Space.isSeparated_isLocallyQuasiFinite_of_isLocallyOfFiniteType_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedMonoCriteria.lean, line 243.

Stacks 0463. A monomorphism of algebraic spaces over S which is locally of finite type is separated and locally quasi-finite.

Separatedness is [Stacks Project, Tag 042N], already available as AlgebraicGeometry.Space.isSeparated_of_mono; local quasi-finiteness goes through unramifiedness, which a monomorphism locally of finite type has by AlgebraicGeometry.Space.isUnramified_of_isLocallyOfFiniteType_of_mono.

These are two of the three assertions of the "moreover" clause of [Stacks Project, Tag 05W6], reached from its condition (3); the equivalence of conditions (1) and (3) carries them over to condition (1), and the two unconditional equivalences below carry them over to conditions (2) and (4).

theorem isSeparated_isLocallyQuasiFinite_of_isLocallyOfFiniteType_mono (f : X ⟶ Y)
    (h : IsLocallyOfFiniteType B S hS f ∧ Mono f) :
    IsSeparated B S hS f ∧ IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Space.isSeparated_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RelativeDiagonalMonomorphism.lean, line 148. The attribute's comment: “separatedness”.

Stacks 042N. A monomorphism of algebraic spaces over S is separated: its relative diagonal is an isomorphism, and an isomorphism is a closed immersion.

The statement is made for an arbitrary morphism of presheaves on the big fppf site of S; no algebraic-space hypothesis is used.

theorem isSeparated_of_mono {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : F ⟶ G) (hg : Mono g) :
    IsSeparated B S hS g

Sources

LeanAlgebraicGeometry.Space.IsLocallyQuasiFinite · AlgebraicGeometry.Space.IsQuasiFinite · AlgebraicGeometry.Space.IsQuasiFiniteAt · AlgebraicGeometry.Space.IsLocallyQuasiFinite.of_isPullback · AlgebraicGeometry.Space.IsQuasiFinite.of_isPullback · AlgebraicGeometry.Space.isOpen_setOf_isQuasiFiniteAt · AlgebraicGeometry.Space.setOf_isQuasiFiniteAt_eq_preimage_of_isPullback · AlgebraicGeometry.Space.setOf_isQuasiFiniteAt_eq_preimage_of_isPullback'

Section67.28 Morphisms of finite presentation #

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

Tag 03XP, a definition

Tag 03XP in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyOfFinitePresentation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation.lean, line 91. The attribute's comment: “part (1): locally of finite presentation”.

Stacks 03XP, part (1). A morphism of algebraic spaces over S is locally of finite presentation when every commuting square of étale scheme charts induces a scheme morphism which is locally of finite presentation.

abbrev IsLocallyOfFinitePresentation (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsFinitePresentationAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation.lean, line 105. The attribute's comment: “part (2): finite presentation at a point”.

Stacks 03XP, part (2). A morphism of algebraic spaces over S is of finite presentation at a point x of its source when it is locally of finite presentation on an open subspace of the source containing x.

Ten predicates of this library share this signature, among them AlgebraicGeometry.Space.IsFiniteTypeAt and AlgebraicGeometry.Space.IsSmoothAt: each applies the same "holds on an open subspace through x" schema to a different property of morphisms of schemes, and each is a different part of a different tag of the source. The shape is shared, the content is not.

abbrev IsFinitePresentationAt (f : X ⟶ Y) (x : points B S hS X) : Prop

AlgebraicGeometry.Space.IsFinitePresentation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentation.lean, line 115. The attribute's comment: “part (3): finite presentation”.

Stacks 03XP, part (3). A morphism of algebraic spaces over S is of finite presentation when it is locally of finite presentation, quasi-compact and quasi-separated.

abbrev IsFinitePresentation (f : X ⟶ Y) : Prop

Tag 03XQ, a lemma

Tag 03XQ in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleChartComposition.lean, line 161. The attribute's comment: “locally of finite presentation”.

Stacks 03XQ, the case of being locally of finite presentation: the composite of two morphisms of algebraic spaces over S which are locally of finite presentation is locally of finite presentation.

Being locally of finite presentation is étale local on the source and target (Stacks 04R3) and stable under composition (Stacks 01TR), so this is an instance of Stacks 0AML.

theorem isLocallyOfFinitePresentation_comp
    {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 : G ⟶ H)
    (hf : IsLocallyOfFinitePresentation B S hS f)
    (hg : IsLocallyOfFinitePresentation B S hS g) :
    IsLocallyOfFinitePresentation B S hS (f ≫ g)

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

Stacks 03XQ, the case of being of finite presentation: the composite of two morphisms of algebraic spaces over S which are of finite presentation is of finite presentation.

Finite presentation is local finite presentation together with quasi-compactness and quasi-separatedness, and each of the three is stable under composition.

theorem isFinitePresentation_comp
    {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 : G ⟶ H)
    (hf : IsFinitePresentation B S hS f)
    (hg : IsFinitePresentation B S hS g) :
    IsFinitePresentation B S hS (f ≫ g)

Tag 03XR, a lemma

Tag 03XR in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparison.lean, line 118. The attribute's comment: “locally of finite presentation”.

Stacks 03XR, the case of being locally of finite presentation: that property of morphisms of algebraic spaces over S is stable under base change.

Being locally of finite presentation is étale local on the source and target (Stacks 04R3) and stable under base change, so this is the instance of Stacks 0AMM at that property.

theorem isLocallyOfFinitePresentation_isStableUnderBaseChange
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        IsLocallyOfFinitePresentation B S hS f.hom)

AlgebraicGeometry.Space.isFinitePresentation_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationBaseChange.lean, line 83. The attribute's comment: “finite presentation”. References: SGA 1 VIII (3.6), “more general”.

Being of finite presentation is a property of morphisms of algebraic spaces over S that is stable under base change.

instance isFinitePresentation_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsFinitePresentation B S hS f.hom)

Tag 0410, a lemma

Tag 0410 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 342.

Stacks 0410. Nine criteria for a morphism of algebraic spaces over S to be locally of finite presentation: pointwise finite presentation, local finite presentation of every base change to a scheme or to an affine scheme or to one surjective étale chart of the target, local finite presentation of the composite with one surjective étale chart of the source, local finite presentation of the morphism of schemes in every — or in one surjective — commuting square of étale charts, or over a pair of Zariski coverings.

Local finite presentation of morphisms of schemes is étale local on the source and target (Stacks 04R3), stable under composition and base change, and implied by étaleness, so this is the instance of AlgebraicGeometry.Space.holdsOnEveryEtaleChart_tfae at that property.

theorem isLocallyOfFinitePresentation_tfae
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [
      IsLocallyOfFinitePresentation B S hS f,
      ∀ x : points B S hS X, IsFinitePresentationAt B S hS f x,
      ∀ (W : BigFppfOver B S hS) (g : yoneda.obj W ⟶ Y),
        IsLocallyOfFinitePresentation B S hS (pullback.fst g f),
      ∀ (W : BigFppfOver B S hS) (g : yoneda.obj W ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj W) →
          IsLocallyOfFinitePresentation B S hS (pullback.fst g f),
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧ IsEtale B S hS g ∧
          IsLocallyOfFinitePresentation B S hS (pullback.fst g f),
      ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X),
        IsSurjective B S hS p ∧ IsEtale B S hS p ∧
          IsLocallyOfFinitePresentation B S hS (p ≫ f),
      ∀ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p → IsEtale B S hS q → p ≫ f = yoneda.map a ≫ q →
          IsLocallyOfFinitePresentation B S hS (yoneda.map a),
      ∃ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p ∧ IsEtale B S hS q ∧ IsSurjective B S hS p ∧
          p ≫ f = yoneda.map a ≫ q ∧ IsLocallyOfFinitePresentation B S hS (yoneda.map a),
      ∃ (I : Type u) (Yopen : I → Subfunctor Y) (J : I → Type u)
        (Xopen : ∀ i, J i → Subfunctor (pullback f (Yopen i).ι)),
        IsZariskiCover B S hS I Yopen ∧ (∀ i, IsZariskiCover B S hS (J i) (Xopen i)) ∧
          ∀ i j, IsLocallyOfFinitePresentation B S hS
            ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 0464, a lemma

Tag 0464 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeProperties.lean, line 105.

Stacks 0464, first assertion. A morphism of algebraic spaces over S which is locally of finite presentation is locally of finite type.

theorem isLocallyOfFiniteType_of_isLocallyOfFinitePresentation
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G}
    (hf : IsLocallyOfFinitePresentation B S hS f) :
    IsLocallyOfFiniteType B S hS f

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

Stacks 0464, second assertion. A morphism of algebraic spaces over S of finite presentation is of finite type.

theorem isFiniteType_of_isFinitePresentation
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G}
    (hf : IsFinitePresentation B S hS f) :
    IsFiniteType B S hS f

Tag 04ZL, a lemma

Tag 04ZL in the Stacks Project.

AlgebraicGeometry.Space.isNoetherian_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 206.

Stacks 04ZL. A morphism of algebraic spaces over S of finite presentation whose target is Noetherian has Noetherian source.

Noetherianity of an algebraic space (Stacks 03EA) is quasi-compactness, quasi-separatedness and local Noetherianity. The first two of the three are exactly Stacks 06G5 applied to the quasi-compact and quasi-separated target, and local Noetherianity of the source comes from Stacks 04ZK, the morphism being locally of finite type by Stacks 0464.

theorem isNoetherian_of_isFinitePresentation (hZ : B.Contains (⊤_ Scheme.{u})) (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsFinitePresentation B S hS f) (hYnoeth : IsNoetherian B S hS hZ Y) :
    IsNoetherian B S hS hZ X

Tag 06G4, a lemma

Tag 06G4 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 245. The attribute's comment: “part (1)”. References: SGA 3 VIA (2.5.4), “more general”.

Stacks 06G4, part (1). A morphism of algebraic spaces over S which is locally of finite type and whose target is locally Noetherian is locally of finite presentation.

The surjective étale atlas of the target witnessing its local Noetherianity lifts, by Stacks 02X1, to a surjective étale chart of the source together with a morphism of the site making the square commute. Local finite type of the morphism tests exactly such squares, so the underlying scheme morphism is locally of finite type with locally Noetherian target and hence locally of finite presentation; one surjective chart square suffices by Stacks 03MJ.

theorem isLocallyOfFinitePresentation_of_isLocallyOfFiniteType
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hN : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFinitePresentation B S hS f

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

Stacks 06G4, part (2). A morphism of algebraic spaces over S which is of finite type and quasi-separated and whose target is locally Noetherian is of finite presentation.

Finite presentation is local finite presentation, quasi-compactness and quasi-separatedness (Stacks 03XP, part (3)) and finite type is local finite type together with quasi-compactness (Stacks 03XF, part (3)), so only the first conjunct has content and that is part (1).

theorem isFinitePresentation_of_isFiniteType
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hN : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hf : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    IsFinitePresentation B S hS f

Tag 06G5, a lemma

Tag 06G5 in the Stacks Project.

AlgebraicGeometry.Space.qcqs_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 187.

Stacks 06G5. If Y is a quasi-compact and quasi-separated algebraic space over S and X is of finite presentation over Y, then X is quasi-compact and quasi-separated.

The two conclusions are independent of each other and each comes from one conjunct of finite presentation (Stacks 03XP, part (3)): quasi-compactness of X from quasi-compactness of f, and quasi-separatedness of X from quasi-separatedness of f. As everywhere in this development, a quasi-compact and quasi-separated algebraic space is one which is quasi-compact in the sense of Stacks 03E3 and quasi-separated in the absolute sense of Stacks 03BS, part (3), that is, quasi-separated over the terminal scheme.

theorem qcqs_of_isFinitePresentation (hZ : B.Contains (⊤_ Scheme.{u})) {f : X ⟶ Y}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y)
    (hf : IsFinitePresentation B S hS f) :
    IsQuasiCompactSpace B S hS X ∧ IsAbsolutelyQuasiSeparated B S hS hZ X

Tag 05WT, a lemma

Tag 05WT in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationCancellation.lean, line 127.

Stacks 05WT. If a composite of morphisms of algebraic spaces over S is locally of finite presentation and its second factor is locally of finite type, then its first factor is locally of finite presentation.

Being locally of finite presentation is étale local on the source and target by Stacks 04R3 and cancels against being locally of finite type at the level of schemes by Stacks 02FV, part (1), so this is the two-property cancellation of the chart condition at those two properties.

theorem isLocallyOfFinitePresentation_of_comp
    {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 : G ⟶ H)
    (hfg : IsLocallyOfFinitePresentation B S hS (f ≫ g))
    (hg : IsLocallyOfFiniteType B S hS g) :
    IsLocallyOfFinitePresentation B S hS f

Tag 084P, a lemma

Tag 084P in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 300. The attribute's comment: “the local assertion”. References: EGA IV (1.4.3.1), “more general”; EGA IV (17.4.1.2), “more general”.

Stacks 084P, the local assertion. The relative diagonal of a morphism of algebraic spaces over S which is locally of finite type is locally of finite presentation.

The diagonal is the first factor of a factorisation of the identity of the source through the fibre square. The identity is locally of finite presentation because it is étale (Stacks 0468), and the second projection is locally of finite type by base change, so Stacks 05WT applies.

theorem isLocallyOfFinitePresentation_pullbackDiagonal (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyOfFinitePresentation B S hS (pullback.diagonal f)

AlgebraicGeometry.Space.isFinitePresentation_pullbackDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 318. The attribute's comment: “the global assertion”.

Stacks 084P, the global assertion. The relative diagonal of a quasi-separated morphism of algebraic spaces over S which is locally of finite type is of finite presentation.

Quasi-compactness of the diagonal is quasi-separatedness of the morphism (Stacks 03HL, part (3)). Quasi-separatedness of the diagonal follows from its separatedness by Stacks 03KK, and the diagonal is separated because it is so after every represented base change (Stacks 03HK, part (4)) and the two readings agree for a representable morphism (Stacks 03KY), the diagonal being representable by Stacks 03HK, part (1).

theorem isFinitePresentation_pullbackDiagonal (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    IsFinitePresentation B S hS (pullback.diagonal f)

Tag 06CN, a lemma

Tag 06CN in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentation.lean, line 225.

Stacks 06CN. An open immersion of algebraic spaces over S is locally of finite presentation.

An open immersion is relatively étale, so in a commuting square of étale charts the composite of the chart of the source with the immersion is an étale chart of the target and Stacks 03EC makes the morphism of the site étale; an étale morphism of schemes is locally of finite presentation. Neither the source nor the target has to be an algebraic space.

theorem isLocallyOfFinitePresentation_of_isOpenImmersion {f : X ⟶ Y}
    (hf : IsOpenImmersion B S hS f) : IsLocallyOfFinitePresentation B S hS f

Tag 084Q, a lemma

Tag 084Q in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentation_iff_isFiniteTypeOnSite_kernelIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersionFinitePresentation.lean, line 282. The attribute's comment: “finite type of the ideal sheaf on the small étale site of the target”. References: EGA IV (1.4.5), “closed immersion case”; EGA IV (8.6.1), “more general”; SGA 3 XI (6.4), “more general”.

Stacks 084Q. A closed immersion i : Z ⟶ X of algebraic spaces over S is of finite presentation if and only if the associated quasi-coherent sheaf of ideals 𝓘 = Ker(𝒪_X ⟶ i_*𝒪_Z) is of finite type as an 𝒪_X-module, that is, of finite type on the small étale site of X in the sense of Stacks 03DL (5), which is how Properties of Spaces, Section 66.30 reads the condition.

Both implications go through the affine étale charts of X. On such a chart C the sections of 𝓘 are the ideal cut out by the cartesian projection Z ×_X C ⟶ C (AlgebraicGeometry.Space.ker_structureSharp_app_eq_ker_appTop, Stacks 03G8 part (2)), and finite type of 𝓘 is finite generation of those ideals (AlgebraicGeometry.Space.isFiniteTypeOnSite_kernelIdealSheaf_iff_forall_affine_fg_ker); on the other side, finite generation of that ideal over an affine chart is local finite presentation of the projection, by the case of schemes (Stacks 01TV) together with AlgebraicGeometry.Scheme.IdealSheafData.isFiniteType_of_fg_ideal_top. Local finite presentation on all affine charts is local finite presentation of i, and the two remaining conjuncts of finite presentation hold for every closed immersion.

theorem isFinitePresentation_iff_isFiniteTypeOnSite_kernelIdealSheaf (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom) :
    IsFinitePresentation B S hS i.hom ↔
      SheafOfModules.IsFiniteTypeOnSite (kernelIdealSheaf B S hS i).toSheafOfModules

Sources

Section67.29 Constructible sets #

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

Tag 0ECW, a lemma

Tag 0ECW in the Stacks Project.

AlgebraicGeometry.Space.isEtaleLocallyConstructible_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 176.

Stacks 0ECW. The inverse image of an étale-locally constructible subset of the points of an algebraic space over S under a morphism of algebraic spaces is étale locally constructible.

A surjective étale chart q : h_V ⟶ Y of the target lifts by Stacks 02X1 to a surjective étale chart p : h_U ⟶ X of the source together with a morphism α : U ⟶ V of the site over f. Read through the homeomorphisms of Stacks 03BX, the inverse image of E on U is the inverse image along the scheme morphism underlying α of the inverse image of E on V, so it is locally constructible by Stacks 054I; one surjective chart suffices by Stacks 0ECT.

theorem isEtaleLocallyConstructible_preimage
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (E : Set (points B S hS Y)) (hE : IsEtaleLocallyConstructible B S hS Y E) :
    IsEtaleLocallyConstructible B S hS X (pointsMap B S hS X f ⁻¹' E)

Tag 0ECX, a theorem

Tag 0ECX in the Stacks Project.

AlgebraicGeometry.Space.isEtaleLocallyConstructible_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 217. References: EGA IV (1.8.4); EGA IV (1.8.4.1); EGA IV (9.5.1); SGA 1 IV (6.2).

Stacks 0ECX, Chevalley's theorem for algebraic spaces. The image of an étale-locally constructible subset of the points of an algebraic space over S under a quasi-compact morphism locally of finite presentation is étale locally constructible.

By Stacks 0ECT it is enough to test the image on an affine étale chart g : h_V ⟶ Y. The base change h_V ×_Y X is a quasi-compact algebraic space because g has quasi-compact source and f is quasi-compact, so it has an affine surjective étale chart t : h\_T ⟶ h\_V ×\_Y X by Stacks 03H6. The chart T sits over V by a morphism q of the site and over X by an étale chart, so the inverse image of E on T is constructible, and q is a morphism of affine schemes which is locally of finite presentation because f is; Chevalley's theorem for schemes therefore makes its image constructible. That image is the inverse image of the image of E under g, which is where Stacks 03H4 and surjectivity of t on points are used.

theorem isEtaleLocallyConstructible_image
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsQuasiCompact B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f)
    (E : Set (points B S hS X)) (hE : IsEtaleLocallyConstructible B S hS X E) :
    IsEtaleLocallyConstructible B S hS Y (pointsMap B S hS X f '' E)

Sources

LeanAlgebraicGeometry.Space.isEtaleLocallyConstructible_preimage · AlgebraicGeometry.Space.isEtaleLocallyConstructible_image

Section67.30 Flat morphisms #

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

Tag 03MK, the section

Tag 03MK in the Stacks Project.

RingHom.Flat.faithfullyFlat_of_isLocalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FaithfullyFlatLocalHom.lean, line 47. The attribute's comment: “section tag: a flat local homomorphism of local rings is faithfully flat”. References: EGA 0 (6.6.1), “(e) ⇒ (a), special case”; EGA 0 (6.6.2), “partial, special case”; SGA 1 IV (2.2), “special case”; SGA 1 IV (2.6), “(i), special case”.

A flat local homomorphism of local rings is faithfully flat.

theorem faithfullyFlat_of_isLocalHom {R S : Type*} [CommRing R] [CommRing S] [IsLocalRing R]
    [IsLocalRing S] {f : R →+* S} (hf : f.Flat) [IsLocalHom f] : f.FaithfullyFlat

AlgebraicGeometry.Space.faithfullyFlat_etaleLocalRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FaithfullyFlatLocalHom.lean, line 64. The attribute's comment: “section tag: the étale local ring map of a flat morphism is faithfully flat”.

The canonical homomorphism of étale local rings 𝒪_{G, f ∘ x} ⟶ 𝒪_{F, x} induced by a flat morphism f : F ⟶ G of algebraic spaces at a geometric point x of its source is faithfully flat.

theorem faithfullyFlat_etaleLocalRingMap {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G)
    (hf : IsFlat B S hS f) (x : GeometricPoint B S hS F) :
    (etaleLocalRingMap hF f x).FaithfullyFlat

Tag 03ML, a definition

Tag 03ML in the Stacks Project.

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

A morphism of algebraic spaces over S is flat when the morphism of schemes underlying every commuting square of étale scheme charts of it is flat.

abbrev IsFlat (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.IsFlatAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/AtAPoint.lean, line 54. The attribute's comment: “part (2)”.

Stacks 03ML, part (2). A morphism of algebraic spaces over S is flat at a point x of its source when the morphism of germs it induces in every pointed étale scheme chart at x is flat on local rings.

abbrev IsFlatAt (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) (x : points B S hS F) : Prop

Tag 08EW, a lemma

Tag 08EW in the Stacks Project.

AlgebraicGeometry.Space.isFlat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Flat.lean, line 723. The attribute's comment: “the equivalence of (1) and (2): flat iff flat at every point of |X|”.

Nine criteria for a morphism of algebraic spaces over S to be flat: pointwise flatness, flatness of every base change to a scheme or to an affine scheme or to one surjective étale chart of the target, flatness of the composite with one surjective étale chart of the source, flatness of the morphism of schemes in every — or in one surjective — commuting square of étale charts, or over a pair of Zariski coverings.

theorem isFlat_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      IsFlat B S hS f,
      ∀ x : points B S hS X, IsFlatAt B S hS f x,
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsFlat B S hS (pullback.fst g f),
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) → IsFlat B S hS (pullback.fst g f),
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧ IsEtale B S hS g ∧ IsFlat B S hS (pullback.fst g f),
      ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X),
        IsSurjective B S hS p ∧ IsEtale B S hS p ∧ IsFlat B S hS (p ≫ f),
      ∀ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p → IsEtale B S hS q → p ≫ f = yoneda.map a ≫ q →
          IsFlat B S hS (yoneda.map a),
      ∃ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p ∧ IsEtale B S hS q ∧ IsSurjective B S hS p ∧
          p ≫ f = yoneda.map a ≫ q ∧ IsFlat B S hS (yoneda.map a),
      ∃ (I : Type u) (Yopen : I → Subfunctor Y) (J : I → Type u)
        (Xopen : ∀ i, J i → Subfunctor (pullback f (Yopen i).ι)),
        IsZariskiCover B S hS I Yopen ∧ (∀ i, IsZariskiCover B S hS (J i) (Xopen i)) ∧
          ∀ i j, IsFlat B S hS ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 03MN, a lemma

Tag 03MN in the Stacks Project.

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

Stacks 03MN. A composition of flat morphisms of algebraic spaces over S is flat.

theorem isFlat_comp
    {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 : G ⟶ H)
    (hf : IsFlat B S hS f) (hg : IsFlat B S hS g) :
    IsFlat B S hS (f ≫ g)

Tag 03MO, a lemma

Tag 03MO in the Stacks Project.

AlgebraicGeometry.Space.isFlat_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/FlatLocalAtSource.lean, line 104.

Stacks Project, Tag 03MO. Flatness of morphisms of algebraic spaces over S is stable under base change.

theorem isFlat_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsFlat B S hS f.hom)

Tag 03MM, a lemma

Tag 03MM in the Stacks Project.

AlgebraicGeometry.Space.isFlat_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Flat.lean, line 723.

Nine criteria for a morphism of algebraic spaces over S to be flat: pointwise flatness, flatness of every base change to a scheme or to an affine scheme or to one surjective étale chart of the target, flatness of the composite with one surjective étale chart of the source, flatness of the morphism of schemes in every — or in one surjective — commuting square of étale charts, or over a pair of Zariski coverings.

theorem isFlat_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      IsFlat B S hS f,
      ∀ x : points B S hS X, IsFlatAt B S hS f x,
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsFlat B S hS (pullback.fst g f),
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsAffine ((BigFppfOver.toScheme B S hS).obj Z) → IsFlat B S hS (pullback.fst g f),
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧ IsEtale B S hS g ∧ IsFlat B S hS (pullback.fst g f),
      ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X),
        IsSurjective B S hS p ∧ IsEtale B S hS p ∧ IsFlat B S hS (p ≫ f),
      ∀ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p → IsEtale B S hS q → p ≫ f = yoneda.map a ≫ q →
          IsFlat B S hS (yoneda.map a),
      ∃ (U V : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X) (q : yoneda.obj V ⟶ Y) (a : U ⟶ V),
        IsEtale B S hS p ∧ IsEtale B S hS q ∧ IsSurjective B S hS p ∧
          p ≫ f = yoneda.map a ≫ q ∧ IsFlat B S hS (yoneda.map a),
      ∃ (I : Type u) (Yopen : I → Subfunctor Y) (J : I → Type u)
        (Xopen : ∀ i, J i → Subfunctor (pullback f (Yopen i).ι)),
        IsZariskiCover B S hS I Yopen ∧ (∀ i, IsZariskiCover B S hS (J i) (Xopen i)) ∧
          ∀ i j, IsFlat B S hS ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 042S, a lemma

Tag 042S in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_of_isFlat_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Flat.lean, line 772. References: EGA IV (2.4.6), “in particular clause”; EGA IV (15.2.1), “flat+lfp ⇒ univ open”; SGA 3 XVI (2.1), “more general”.

A flat morphism of algebraic spaces over S which is locally of finite presentation is universally open in the sense of Stacks 03Z2.

theorem universallyOpen_of_isFlat_of_isLocallyOfFinitePresentation
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f) :
    UniversallyOpen B S hS f

Tag 0413, a lemma

Tag 0413 in the Stacks Project.

AlgebraicGeometry.Space.isOpen_iff_isOpen_preimage_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 370. The attribute's comment: “open subsets”. References: EGA IV (2.3.12), “open case”; SGA 1 VIII (4.3), “open subsets”; SGA 1 IX (2.2), “flat qc case, open”.

Stacks 0413, open subsets. A subset of the points of the target of a flat, quasi-compact, surjective morphism of algebraic spaces over S is open exactly when its inverse image on points is open.

Openness in the point topology is tested on the presheaves represented by the objects of the site, and openness there is openness in the representing scheme, hence local on its affine opens; those affine opens are objects of the site with affine underlying scheme, so AlgebraicGeometry.Space.isOpen_preimage_pointsMap_of_isAffine applies to each.

theorem isOpen_iff_isOpen_preimage_pointsMap
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hqc : IsQuasiCompact B S hS f) (hsurj : IsSurjective B S hS f)
    (T : Set (points B S hS Y)) :
    IsOpen T ↔ IsOpen (pointsMap B S hS X f ⁻¹' T)

AlgebraicGeometry.Space.isClosed_iff_isClosed_preimage_pointsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 412. The attribute's comment: “closed subsets”. References: EGA IV (2.3.12), “closed case”; SGA 1 VIII (4.3), “closed subsets”; SGA 1 IX (2.2), “flat qc case, closed”.

Stacks 0413, closed subsets. A subset of the points of the target of a flat, quasi-compact, surjective morphism of algebraic spaces over S is closed exactly when its inverse image on points is closed. This is AlgebraicGeometry.Space.isOpen_iff_isOpen_preimage_pointsMap at the complement.

theorem isClosed_iff_isClosed_preimage_pointsMap
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hqc : IsQuasiCompact B S hS f) (hsurj : IsSurjective B S hS f)
    (T : Set (points B S hS Y)) :
    IsClosed T ↔ IsClosed (pointsMap B S hS X f ⁻¹' T)

AlgebraicGeometry.Space.isSubmersive_of_isFlat_of_isQuasiCompact_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 428. The attribute's comment: “submersive”. References: EGA IV (15.7.8), “fppf ⇒ submersive”; EGA IV (2.3.12); SGA 1 VIII (4.3); SGA 1 IX (2.2), “flat qc submersive”.

Stacks 0413, submersiveness. A flat, quasi-compact, surjective morphism of algebraic spaces over S is submersive: it is surjective on points, and openness of a subset of the points of its target is openness of the inverse image.

theorem isSubmersive_of_isFlat_of_isQuasiCompact_of_isSurjective
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hqc : IsQuasiCompact B S hS f) (hsurj : IsSurjective B S hS f) :
    IsSubmersive B S hS f

AlgebraicGeometry.Space.universallySubmersive_of_isFlat_of_isQuasiCompact_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Submersive.lean, line 440. The attribute's comment: “universally submersive”.

Stacks 0413, universal submersiveness. A flat, quasi-compact, surjective morphism of algebraic spaces over S is universally submersive: each of the three hypotheses is stable under base change, by Stacks 03MO, Stacks 03HF and Stacks 03MH.

theorem universallySubmersive_of_isFlat_of_isQuasiCompact_of_isSurjective
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hqc : IsQuasiCompact B S hS f) (hsurj : IsSurjective B S hS f) :
    UniversallySubmersive B S hS f

Tag 04NG, a lemma

Tag 04NG in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_etaleLocalRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatEtaleLocalRing.lean, line 406. The attribute's comment: “the canonical homomorphism of étale local rings”.

Stacks 04NG. A morphism f of algebraic spaces over S induces at a geometric point x of its source a unique homomorphism of étale local rings 𝒪_{G, f ∘ x} ⟶ 𝒪_{F, x} compatible with the germ maps in every commuting diagram of pointed étale scheme charts over f.

theorem existsUnique_etaleLocalRingMap (hF : IsAlgebraicSpace B S hS F) (f : F ⟶ G)
    (x : GeometricPoint B S hS F) :
    ∃! φ : etaleLocalRing B S hS G (geometricPointMap f x) →+* etaleLocalRing B S hS F x,
      IsEtaleLocalRingMap f x φ

AlgebraicGeometry.Space.isFlatAt_iff_etaleLocalRingMap_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatEtaleLocalRing.lean, line 581. The attribute's comment: “the flatness criterion”.

Stacks 04NG. A morphism f of algebraic spaces over S is flat at the image of a geometric point x of its source exactly when the canonical homomorphism of étale local rings 𝒪_{G, f ∘ x} ⟶ 𝒪_{F, x} is flat.

For a point x₀ of F with x.LiesOver x₀ the statement for x₀ follows by rewriting along that equality.

theorem isFlatAt_iff_etaleLocalRingMap_flat (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (x : GeometricPoint B S hS F) :
    IsFlatAt B S hS f x.image ↔ (etaleLocalRingMap hF f x).Flat

Tag 073C, a lemma

Tag 073C in the Stacks Project.

AlgebraicGeometry.Space.isFlat_iff_smallEtaleRingedToposHom_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleFlatTopos.lean, line 596.

Stacks 073C. A morphism of algebraic spaces over S is flat if and only if the morphism of small étale ringed topoi (f_small, f♯) : (X_étale, 𝒪_X) ⟶ (Y_étale, 𝒪_Y) associated to it is flat.

theorem isFlat_iff_smallEtaleRingedToposHom_isFlat :
    IsFlat B S hS f.hom ↔
      RingedToposHom.IsFlat (smallEtaleRingedToposHom B S hS f)

Tag 089C, a lemma

Tag 089C in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticSupport_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SchemeTheoreticSupportFlatPullback.lean, line 245. The attribute's comment: “flatness of the morphism, quasi-coherence of the module and finiteness of its type are the hypotheses of the tag and are all consumed; the affine-chart description of the pullback of modules, Descent Proposition 03DX(2) read across the morphism, is proved, not carried”.

[Stacks, Tag 089C]. Let f : Y ⟶ X be a flat morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module of finite type with scheme-theoretic support Z ⊆ X. Then the inverse image f⁻¹(Z) is the scheme-theoretic support of f^*F.

theorem schemeTheoreticSupport_modulePullback {f : Y ⟶ X} (hf : IsFlat B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hft : PresheafOfModules.IsFiniteType (smallEtaleRingedSite B S hS X.1 X.2).J F.val) :
    schemeTheoreticSupport B S hS Y ((modulePullback B S hS f).obj F) =
      (schemeTheoreticSupport B S hS X F).preimage f.hom

Tag 089D, a lemma

Tag 089D in the Stacks Project.

AlgebraicGeometry.Space.isSchemeTheoreticallyDense_preimage_of_isFlat_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactSchemeTheoreticDensity.lean, line 149.

Let S be a scheme contained in a big fppf site B, let f : X ⟶ Y be a flat morphism of algebraic spaces over S and let V ⊆ Y be an open subspace whose inclusion is quasi-compact. If V is scheme-theoretically dense in Y, then f⁻¹V is scheme-theoretically dense in X.

theorem isSchemeTheoreticallyDense_preimage_of_isFlat_of_isQuasiCompact
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsFlat B S hS f) (V : Subfunctor Y) (hV : IsOpenSubspace B S hS V)
    (hqc : IsQuasiCompact B S hS V.ι)
    (hdense : IsSchemeTheoreticallyDense B S hS V) :
    IsSchemeTheoreticallyDense B S hS (V.preimage f)

Tag 089E, a lemma

Tag 089E in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_pullback_snd_of_isFlat_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/QuasiCompactImageFlatBaseChange.lean, line 642. References: EGA IV (2.3.2).

The scheme-theoretic image of a quasi-compact morphism g : V ⟶ Y of algebraic spaces over S commutes with flat base change: for a flat f : X ⟶ Y, the scheme-theoretic image of V ×_Y X ⟶ X is the inverse image along f of the scheme-theoretic image of g.

theorem schemeTheoreticImageSubfunctor_pullback_snd_of_isFlat_of_isQuasiCompact
    {X Y V : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : V ⟶ Y)
    (hf : IsFlat B S hS f.hom) (hg : IsQuasiCompact B S hS g.hom) :
    schemeTheoreticImageSubfunctor B S hS (pullback.snd g.hom f.hom) =
      (schemeTheoreticImageSubfunctor B S hS g.hom).preimage f.hom

Sources

LeanRingHom.Flat.faithfullyFlat_of_isLocalHom · AlgebraicGeometry.Space.faithfullyFlat_etaleLocalRingMap · AlgebraicGeometry.Space.IsFlat · AlgebraicGeometry.Space.IsFlatAt · AlgebraicGeometry.Space.isFlat_tfae · AlgebraicGeometry.Space.isFlat_comp · AlgebraicGeometry.Space.isFlat_isStableUnderBaseChange · AlgebraicGeometry.Space.universallyOpen_of_isFlat_of_isLocallyOfFinitePresentation

Section67.31 Flat modules #

Section 67.31 of the Stacks Project, Tag 05VT. 6 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05VU, a lemma

Tag 05VU in the Stacks Project.

AlgebraicGeometry.Space.isFlatOverAt_exists_chartDiagram_iff_isFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleAtGeometricPointEquiv.lean, line 276.

Stacks 05VU. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and let x̄ be a geometric point of X. The following are equivalent:

there is a commuting square of étale scheme charts U ⟶ V over f and a point u of U above the image of x̄ in |X| at which the restriction of F to U is flat over V;

the geometric stalk F_{x̄} is flat over the étale local ring 𝒪_{Y, ȳ}, where ȳ = f ∘ x̄.

Condition (1) is AlgebraicGeometry.Space.IsFlatOverAtOnChartDiagram, the ringed-space predicate of Stacks 08KT on the square, the condition "above x" being AlgebraicGeometry.Space.ChartPoint; condition (2) is AlgebraicGeometry.Space.IsFlatOverAtGeometricPoint. Condition (2) mentions no chart, so the equivalence also says that condition (1) does not depend on the chosen square or point.

theorem isFlatOverAt_exists_chartDiagram_iff_isFlatOverAtGeometricPoint
    {Xs Ys : AlgebraicSpaces B S hS} (f : Xs ⟶ Ys)
    (F : Modules.{u, u} B S hS Xs.1 Xs.2) [F.IsQuasicoherentOnSite]
    (xbar : GeometricPoint B S hS Xs.1) :
    (∃ (d : ChartDiagram B S hS Xs.1 Ys.1 f.hom) (u : chartScheme d.U),
        ChartPoint B S hS d.U.obj.left d.U.obj.hom u xbar.image ∧
        IsFlatOverAtOnChartDiagram B S hS Xs.2 F d u) ↔
      IsFlatOverAtGeometricPoint B S hS f F xbar

Tag 05VV, a definition

Tag 05VV in the Stacks Project.

AlgebraicGeometry.Space.IsFlatOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModule.lean, line 101. The attribute's comment: “flatness over the target”.

Stacks 05VV. An 𝒪_X-module is flat over Y along f : X ⟶ Y when, on every commuting square of étale scheme charts of f, its restriction to the chart of X is flat over the chart of Y.

noncomputable abbrev IsFlatOver (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X hX) : Prop

AlgebraicGeometry.Space.IsFlatOverAtPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModule.lean, line 131. The attribute's comment: “flatness over the target at a point of |X|”.

Stacks 05VV at a point of |X|. An 𝒪_X-module is flat over Y at a point x of |X| when, on some commuting square of étale scheme charts of f and at some point of the chart of X lying over x, the restriction of F to that chart is flat over the chart of Y at that point, in the stalkwise sense of Stacks 08KT part (1) for ringed spaces.

Quantifying existentially over the charts is what the source does: this is condition (1) of Stacks 05VU, which that lemma identifies with the geometric-stalk condition (2) at x. That lemma is not unavailable in this development — it is registered, for a quasi-coherent module, as AlgebraicGeometry.Space.isFlatOverAt_exists_chartDiagram_iff_isFlatOverAtGeometricPoint of StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleAtGeometricPointEquiv.lean, which is downstream of this file; so the identification, and with it the independence of the chosen square, is made there and not here. The consequence this definition's consumers want is AlgebraicGeometry.Space.isFlatOverAtPoint_iff_isFlatOverAtOnChartDiagram of StacksFrontier/AlgebraicGeometry/Spaces/FlatModulePointChartIndependence.lean: the condition may be read on any one square through the point.

This is the pointwise form of AlgebraicGeometry.Space.IsFlatOver, which asks the same ringed-space condition at every point of every chart square; the global predicate restricts to this one at every chart point, which is AlgebraicGeometry.Space.isFlatOverAtPoint_of_isFlatOver; that the global predicate is exactly the conjunction of this one over all x of |X| is AlgebraicGeometry.Space.isFlatOver_iff_forall_isFlatOverAtPoint of StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleAllPoints.lean, again downstream of this file because the converse direction rests on the chart independence.

noncomputable def IsFlatOverAtPoint (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X hX) (x : points B S hS X) : Prop

AlgebraicGeometry.Space.isFlatOver_iff_forall_isFlatOverAtPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleAllPoints.lean, line 89. The attribute's comment: “the all-x characterisation, for a quasi-coherent module”.

Stacks 05VV, the all-x characterisation. For a quasi-coherent 𝒪_X-module F, flatness of F over Y in the every-chart sense of AlgebraicGeometry.Space.IsFlatOver holds exactly when F is flat over Y at every point of |X| in the pointwise sense of AlgebraicGeometry.Space.IsFlatOverAtPoint, which is condition (1) of Stacks 05VU at that point. This is the form in which the source states the definition: F is flat over Y when the equivalent conditions of Stacks 05VU hold at every point of |X|.

The forward direction holds for an arbitrary 𝒪_X-module; quasi-coherence is what makes the pointwise condition chart-independent and so is needed only for the converse.

theorem isFlatOver_iff_forall_isFlatOverAtPoint {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    IsFlatOver B S hS X.2 f.hom F ↔
      ∀ x : points B S hS X.1, IsFlatOverAtPoint B S hS X.2 f.hom F x

Tag 05VW, a lemma

Tag 05VW in the Stacks Project.

AlgebraicGeometry.Space.isFlatOver_modulePullback_of_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CoherentStackFinitePresentationStability.lean, line 104. The attribute's comment: “the final assertion for a module of finite presentation”.

Stacks 05VW, the final assertion, for a module of finite presentation. In a cartesian square of algebraic spaces
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
the inverse image of an 𝒪_X-module of finite presentation flat over Y is flat over Y'.

This is AlgebraicGeometry.Space.isFlatOver_modulePullback, whose two quasi-coherence instances finite presentation supplies: the module is quasi-coherent because it is of finite presentation, and its inverse image is of finite presentation by AlgebraicGeometry.Space.isFinitePresentationOnSite_modulePullback, hence quasi-coherent for the same reason.

theorem isFlatOver_modulePullback_of_isFinitePresentationOnSite
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : SheafOfModules.IsFinitePresentationOnSite F)
    (hflat : IsFlatOver B S hS X.2 f.hom F) :
    IsFlatOver B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F)

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleBaseChange.lean, line 125. The attribute's comment: “part (1): the pullback of a module flat over the target at a point is flat over the new target at every point above it”.

Stacks 05VW, part (1). In a cartesian square of algebraic spaces
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
let x̄' be a geometric point of X' and let F be an 𝒪_X-module flat over Y at the image x̄ of x̄'. Then the pullback (g')^* F is flat over Y' at x̄'.

At the geometric stalks this is base change of flatness over a pushout of rings: the stalk of (g')^* F at x̄' is 𝒪_{X', x̄'} ⊗_{𝒪_{X, x̄}} F_{x̄} by Stacks 05VQ, and 𝒪_{X', x̄'} is flat over 𝒪_{X, x̄} ⊗_{𝒪_{Y, ȳ}} 𝒪_{Y', ȳ'}, so flatness of F_{x̄} over 𝒪_{Y, ȳ} passes to flatness of the base change over 𝒪_{Y', ȳ'}.

theorem isFlatOverAtGeometricPoint_modulePullback
    {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    (x' : GeometricPoint B S hS X'.1)
    (hF : IsFlatOverAtGeometricPoint B S hS f F (geometricPointMap g'.hom x')) :
    IsFlatOverAtGeometricPoint B S hS f' ((modulePullback B S hS g').obj F) x'

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_of_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleBaseChange.lean, line 212. The attribute's comment: “part (2): relative flatness of a module at a point descends along a base change flat at the image point”.

Stacks 05VW, part (2). In a cartesian square of algebraic spaces
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
let x̄' be a geometric point of X', let F be an 𝒪_X-module and suppose that g is flat at the image ȳ' of x̄' in Y'. If the pullback (g')^* F is flat over Y' at x̄', then F is flat over Y at the image x̄ of x̄'.

Flatness of g at ȳ' makes (g')^* F flat over Y at x̄' by Stacks 05VX, part (1); over the étale local rings that reads as flatness of 𝒪_{X', x̄'} ⊗_{𝒪_{X, x̄}} F_{x̄} over 𝒪_{Y, ȳ} through Stacks 05VQ. The same flatness of g makes 𝒪_{X, x̄} → 𝒪_{X', x̄'} flat, and it is a local homomorphism of local rings, hence faithfully flat; so flatness of F_{x̄} over 𝒪_{Y, ȳ} follows by Stacks 0584 (2).

theorem isFlatOverAtGeometricPoint_of_modulePullback
    {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y}
    (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    (x' : GeometricPoint B S hS X'.1)
    (hg : IsFlatAt B S hS g.hom (geometricPointMap f'.hom x').image)
    (hF : IsFlatOverAtGeometricPoint B S hS f' ((modulePullback B S hS g').obj F) x') :
    IsFlatOverAtGeometricPoint B S hS f F (geometricPointMap g'.hom x')

AlgebraicGeometry.Space.isFlatOver_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleBaseChange.lean, line 309. The attribute's comment: “the final assertion: the pullback of a quasi-coherent module flat over the target is flat over the new target”.

Stacks 05VW, the final assertion. In a cartesian square of algebraic spaces
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
the pullback of a quasi-coherent 𝒪_X-module flat over Y is flat over Y'.

Chartwise flatness of Stacks 05VV is flatness of the geometric stalks over the étale local rings of the base at every geometric point, by Stacks 05VU, and that pointwise condition is carried by the base change at each geometric point of X'.

theorem isFlatOver_modulePullback {X Y X' Y' : AlgebraicSpaces B S hS} {g' : X' ⟶ X}
    {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (hpb : IsPullback g' f' f g)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    [((modulePullback B S hS g').obj F).IsQuasicoherentOnSite]
    (hF : IsFlatOver B S hS X.2 f.hom F) :
    IsFlatOver B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F)

AlgebraicGeometry.Space.mem_flatLocus_modulePullback_of_mem_flatLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleBaseChangePoint.lean, line 109. The attribute's comment: “part (1) read at a point of the point space of Stacks 03BU, flatness at a point being membership of the relative flat locus of Stacks 0DLR”.

Stacks 05VW, part (1), at a point of the point space. In a cartesian square of algebraic spaces
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
let F be a quasi-coherent 𝒪_X-module and let x' be a point of |X'|. If F is flat over Y at the image of x' in |X|, then the inverse image (g')^*F is flat over Y' at x', flatness at a point being membership of the relative flat locus of Stacks 0DLR.

A geometric point of X' above x' exists by Stacks 04XE, flatness at a point is flatness of the geometric stalk there by AlgebraicGeometry.Space.mem_flatLocus_iff_isFlatOverAtGeometricPoint, and the implication between the two geometric-stalk conditions is part (1) of Stacks 05VW, AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_modulePullback. The inverse image is quasi-coherent by Stacks 03GA.

theorem mem_flatLocus_modulePullback_of_mem_flatLocus {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y}
    {g : Y' ⟶ Y} (sq : IsPullback g'.hom f'.hom f.hom g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x' : points B S hS X'.1)
    (hx : pointsMap B S hS X'.1 g'.hom x' ∈ flatLocus B S hS X.2 f.hom F) :
    x' ∈ flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F)

AlgebraicGeometry.Space.mem_flatLocus_of_mem_flatLocus_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleBaseChangePoint.lean, line 148. The attribute's comment: “part (2) read at a point of the point space of Stacks 03BU, flatness at a point being membership of the relative flat locus of Stacks 0DLR”.

Stacks 05VW, part (2), at a point of the point space. In a cartesian square of algebraic spaces
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
let F be a quasi-coherent 𝒪_X-module, let x' be a point of |X'| and suppose that g is flat at the image of x' in |Y'|. If the inverse image (g')^*F is flat over Y' at x', then F is flat over Y at the image of x' in |X|, flatness at a point being membership of the relative flat locus of Stacks 0DLR.

The proof is that of part (1) read in the opposite direction: a geometric point of X' above x' exists by Stacks 04XE, flatness at a point is flatness of the geometric stalk there by AlgebraicGeometry.Space.mem_flatLocus_iff_isFlatOverAtGeometricPoint, and the implication between the two geometric-stalk conditions is part (2) of Stacks 05VW, AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_of_modulePullback. The inverse image is quasi-coherent by Stacks 03GA.

theorem mem_flatLocus_of_mem_flatLocus_modulePullback {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y}
    {g : Y' ⟶ Y} (sq : IsPullback g'.hom f'.hom f.hom g.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x' : points B S hS X'.1)
    (hg : IsFlatAt B S hS g.hom (pointsMap B S hS X'.1 f'.hom x'))
    (hx : x' ∈ flatLocus B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F)) :
    pointsMap B S hS X'.1 g'.hom x' ∈ flatLocus B S hS X.2 f.hom F

AlgebraicGeometry.Space.isFlatOverAtPoint_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleBaseChangePoint.lean, line 199. The attribute's comment: “parts (1) and (2) at a point of |X'|, flatness at a point being Stacks 05VV (1), and the final assertion, for a quasi-coherent module”.

Stacks 05VW. Let
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
be a cartesian square of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and write F' = (g')^*F. For every point x' of |X'| with image x in |X|:

if F is flat over Y at x, then F' is flat over Y' at x';

if g is flat at the image f'(x') of x' in |Y'| and F' is flat over Y' at x', then F is flat over Y at x;

and in particular, if F is flat over Y, then F' is flat over Y'.

Flatness of a module over the target at a point of the point space is AlgebraicGeometry.Space.IsFlatOverAtPoint of Stacks 05VV, flatness over the target is AlgebraicGeometry.Space.IsFlatOver of Stacks 05VV, and flatness of g at a point is AlgebraicGeometry.Space.IsFlatAt of Stacks 03ML part (2).

At a point, a geometric point of X' above x' exists by Stacks 0488 part (1), flatness at a point is flatness of the geometric stalk there by Stacks 05VU, AlgebraicGeometry.Space.mem_flatLocus_iff_isFlatOverAtGeometricPoint, and the two parts are then AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_modulePullback and AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_of_modulePullback. The final assertion is AlgebraicGeometry.Space.isFlatOver_modulePullback, the quasi-coherence of F' it asks for being Stacks 03GA, AlgebraicGeometry.Space.isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite, so that nothing beyond quasi-coherence of F is assumed.

theorem isFlatOverAtPoint_baseChange {g' : X' ⟶ X} {f' : X' ⟶ Y'}
    {f : X ⟶ Y} {g : Y' ⟶ Y} (hpb : IsPullback g' f' f g) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] :
    (∀ x' : points B S hS X'.1,
        IsFlatOverAtPoint B S hS X.2 f.hom F (pointsMap B S hS X'.1 g'.hom x') →
          IsFlatOverAtPoint B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) x') ∧
      (∀ x' : points B S hS X'.1, IsFlatAt B S hS g.hom (pointsMap B S hS X'.1 f'.hom x') →
        IsFlatOverAtPoint B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F) x' →
          IsFlatOverAtPoint B S hS X.2 f.hom F (pointsMap B S hS X'.1 g'.hom x')) ∧
      (IsFlatOver B S hS X.2 f.hom F →
        IsFlatOver B S hS X'.2 f'.hom ((modulePullback B S hS g').obj F))

Tag 05VX, a lemma

Tag 05VX in the Stacks Project.

AlgebraicGeometry.Space.isFlatOverAtGeometricPoint_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleComposition.lean, line 119. The attribute's comment: “part (1): flatness of a module at a point composes with flatness of the base”.

If an 𝒪_X-module F is flat at a geometric point x̄ of X over Y and Y is flat over Z at the image ȳ of x̄, then F is flat at x̄ over Z.

Over the étale local rings this is transitivity of flatness: F_{x̄} is flat over 𝒪_{Y, ȳ} and 𝒪_{Y, ȳ} is flat over 𝒪_{Z, z̄}.

theorem isFlatOverAtGeometricPoint_comp {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) (F : Modules.{u, m} B S hS X.1 X.2)
    (xbar : GeometricPoint B S hS X.1)
    (hF : IsFlatOverAtGeometricPoint B S hS f F xbar)
    (hg : IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image) :
    IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar

AlgebraicGeometry.Space.isFlatAt_of_isFaithfullyFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleComposition.lean, line 137. The attribute's comment: “part (3): flatness of the base at a point descends from a faithfully flat geometric stalk”.

If the geometric stalk F_{x̄} of an 𝒪_X-module at a geometric point x̄ of X is a faithfully flat module over the étale local ring 𝒪_{Y, ȳ} of the image ȳ of x̄, and F is flat at x̄ over Z, then Y is flat over Z at ȳ.

Over the étale local rings this is flat permanence (Stacks 039V): F_{x̄} is flat over 𝒪_{Z, z̄} and faithfully flat over 𝒪_{Y, ȳ}, hence 𝒪_{Y, ȳ} is flat over 𝒪_{Z, z̄}.

theorem isFlatAt_of_isFaithfullyFlatOverAtGeometricPoint {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) (F : Modules.{u, m} B S hS X.1 X.2)
    (xbar : GeometricPoint B S hS X.1)
    (hff : IsFaithfullyFlatOverAtGeometricPoint B S hS f F xbar)
    (hfg : IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar) :
    IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image

AlgebraicGeometry.Space.isFlatAt_of_nontrivial_fibre_of_isFlatOverAtGeometricPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleComposition.lean, line 159. The attribute's comment: “part (2): flatness of the base at a point descends from a module flat over both and with nonzero fibre at a representative of the point”.

Let F be an 𝒪_X-module and let x̄ be a geometric point of X with image ȳ in Y. If F is flat at x̄ over Y, the fibre of F at x̄ is nonzero and F is flat at x̄ over Z, then Y is flat over Z at ȳ.

The fibre of F at x̄ is the quotient F_{x̄} ⧸ 𝔪_{x̄} F_{x̄} of the geometric stalk by the maximal ideal of 𝒪_{X, x̄}; it is the pullback x̄^* F of F along x̄, regarded as a representative of its image point with values in an algebraically closed field. Since 𝒪_{Y, ȳ} → 𝒪_{X, x̄} is a local homomorphism, nonvanishing of that fibre forces the fibre of F_{x̄} over 𝒪_{Y, ȳ} to be nonzero as well, so that F_{x̄} is a faithfully flat 𝒪_{Y, ȳ}-module (Stacks 00HP) and part (3) applies.

theorem isFlatAt_of_nontrivial_fibre_of_isFlatOverAtGeometricPoint
    {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z) (F : Modules.{u, m} B S hS X.1 X.2)
    (xbar : GeometricPoint B S hS X.1)
    (hf : IsFlatOverAtGeometricPoint B S hS f F xbar)
    (hfibre :
      letI := isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
      Nontrivial ((geometricModuleStalk B S hS X xbar F) ⧸
        (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar)) •
          (⊤ : Submodule (etaleLocalRing B S hS X.1 xbar)
            (geometricModuleStalk B S hS X xbar F))))
    (hfg : IsFlatOverAtGeometricPoint B S hS (f ≫ g) F xbar) :
    IsFlatAt B S hS g.hom (geometricPointMap f.hom xbar).image

Tag 05VY, a lemma

Tag 05VY in the Stacks Project.

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

Stacks 05VY. Let S be a scheme contained in the big fppf site B, let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over S, let G be a quasi-coherent 𝒪_Y-module and let x be a point of |X|, with image y in |Y|. Then:

if f is flat at x, then G is flat over Z at y if and only if f^*G is flat over Z at x;

in particular, if f is surjective and flat, then G is flat over Z if and only if f^*G is flat over Z.

A geometric point above x turns each side of (1) into the geometric-stalk condition (2) of Stacks 05VU; there the stalk of f^*G is 𝒪_{X, x̄} ⊗_{𝒪_{Y, ȳ}} G_ȳ by Stacks 05VQ and 𝒪_{Y, ȳ} ⟶ 𝒪_{X, x̄} is faithfully flat, so the equivalence is Stacks 0584 (2). For (2) the morphism f is flat at every point, and surjectivity of |X| → |Y| puts a point of |X| above every point of |Y|.

theorem relativeFlatnessPermanence_modulePullback (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y Z : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (G : Modules.{u, u} B S hS Y.1 Y.2) [G.IsQuasicoherentOnSite] (x : points B S hS X.1) :
    (IsFlatAt B S hS f.hom x →
        (IsFlatOverAtPoint B S hS Y.2 g.hom G (pointsMap B S hS X.1 f.hom x) ↔
          IsFlatOverAtPoint B S hS X.2 (f ≫ g).hom ((modulePullback B S hS f).obj G) x)) ∧
      (IsSurjective B S hS f.hom → IsFlat B S hS f.hom →
        (IsFlatOver B S hS Y.2 g.hom G ↔
          IsFlatOver B S hS X.2 (f ≫ g).hom ((modulePullback B S hS f).obj G)))

Tag 0CVU, a lemma

Tag 0CVU in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_of_isFlatOver_of_fullSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatModuleUniversallyOpen.lean, line 122. References: EGA IV (11.3.1), “f|U open”; EGA IV (2.4.6); EGA IV (15.2.1), “more general”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite presentation and let 𝓕 be an 𝒪_X-module which, on charts, is quasi-coherent, of finite type, of full support and flat over Y. Then f is universally open.

theorem universallyOpen_of_isFlatOver_of_fullSupport
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X hX)
    (hf : IsLocallyOfFinitePresentation B S hS f)
    (hqc : IsQuasicoherentOnCharts B S hS hX F) (hft : IsFiniteTypeOnCharts B S hS hX F)
    (hsupp : HasFullSupportOnCharts B S hS hX F) (hflat : IsFlatOver B S hS hX f F) :
    UniversallyOpen B S hS f

Sources

Section67.32 Generic flatness #

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

Tag 06QS, a proposition

Tag 06QS in the Stacks Project.

AlgebraicGeometry.Space.exists_dense_open_genericFlatness_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/GenericFlatness.lean, line 179. The attribute's comment: “the one-chart core of the proof: Tag 052B read on a commuting square of affine étale charts”.

Stacks 06QS, the one-chart core. On a commuting square of étale charts of f whose source and target charts are affine and whose target chart is reduced, the chart morphism becomes flat and locally of finite presentation over a dense open of the target chart, over which the module becomes flat over the target and of finite presentation.

theorem exists_dense_open_genericFlatness_chart
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X hX)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hft : IsFiniteTypeOnCharts B S hS hX F)
    {U V : BigFppfOver B S hS}
    [IsAffine ((BigFppfOver.toScheme B S hS).obj U)]
    [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    [IsReduced ((BigFppfOver.toScheme B S hS).obj V)]
    {p : yoneda.obj U ⟶ X} {b : yoneda.obj V ⟶ Y} (a : U ⟶ V)
    (hpE : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf p)
    (hbE : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf b)
    (hcomm : p ≫ f = yoneda.map a ≫ b)
    (hLFT : AlgebraicGeometry.LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map a)) :
    ∃ W : ((BigFppfOver.toScheme B S hS).obj V).Opens,
      Dense (W : Set ((BigFppfOver.toScheme B S hS).obj V)) ∧
      AlgebraicGeometry.Flat (((BigFppfOver.toScheme B S hS).map a) ∣_ W) ∧
      AlgebraicGeometry.LocallyOfFinitePresentation
        (((BigFppfOver.toScheme B S hS).map a) ∣_ W) ∧
      ∀ u : (BigFppfOver.toScheme B S hS).obj U,
        ((BigFppfOver.toScheme B S hS).map a) u ∈ W →
          pointOfEtaleChart B S hS ⟨CostructuredArrow.mk p, hpE⟩ u ∈
              flatLocus B S hS hX f F ∧
            pointOfEtaleChart B S hS ⟨CostructuredArrow.mk p, hpE⟩ u ∈
              finitePresentationLocus B S hS hX F

AlgebraicGeometry.Space.exists_dense_open_genericFlatness_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/GenericFlatness.lean, line 415. The attribute's comment: “step 3 of the proof: the case of a reduced affine base”.

Stacks 06QS for a reduced affine base, step 3 of the source. A finite-type morphism of algebraic spaces to a reduced affine scheme of the site, together with a module which is quasi-coherent of finite type on charts, becomes flat, locally of finite presentation and quasi-compact, and the module flat over the base and of finite presentation, over a dense open of the base.

theorem exists_dense_open_genericFlatness_of_isAffine
    (hX : IsAlgebraicSpace B S hS X) (Z : BigFppfOver B S hS)
    [IsAffine ((BigFppfOver.toScheme B S hS).obj Z)]
    [IsReduced ((BigFppfOver.toScheme B S hS).obj Z)]
    (f : X ⟶ yoneda.obj Z) (hf : IsFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hft : IsFiniteTypeOnCharts B S hS hX F) :
    ∃ W : ((BigFppfOver.toScheme B S hS).obj Z).Opens,
      Dense (W : Set ((BigFppfOver.toScheme B S hS).obj Z)) ∧
      IsFlat B S hS (pullback.snd f (yoneda.map (openSiteObjectHom B S hS Z W))) ∧
      IsLocallyOfFinitePresentation B S hS
        (pullback.snd f (yoneda.map (openSiteObjectHom B S hS Z W))) ∧
      IsQuasiCompact B S hS (pullback.snd f (yoneda.map (openSiteObjectHom B S hS Z W))) ∧
      ∀ x : points B S hS X,
        pointsEquivScheme B S hS Z (pointsMap B S hS X f x) ∈ W →
          x ∈ flatLocus B S hS hX f F ∧ x ∈ finitePresentationLocus B S hS hX F

AlgebraicGeometry.Space.exists_dense_open_genericFlatness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/GenericFlatness.lean, line 689.

Stacks 06QS. Let f : X ⟶ Y be a morphism of algebraic spaces over S of finite type with Y reduced, and let F be an 𝒪_X-module which is quasi-coherent of finite type on charts. Then there is a dense open subspace W of Y such that the base change of f over W is flat, locally of finite presentation and quasi-compact, and such that F is flat over Y and of finite presentation at every point of X lying over W.

theorem exists_dense_open_genericFlatness
    (hX : IsAlgebraicSpace B S hS X) {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hY : IsAlgebraicSpace B S hS Y)
    (hYred : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T))
    (f : X ⟶ Y) (hf : IsFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hft : IsFiniteTypeOnCharts B S hS hX F) :
    ∃ W : Subfunctor Y, IsDenseOpenSubspace B S hS hY W ∧
      IsFlat B S hS (pullback.snd f W.ι) ∧
      IsLocallyOfFinitePresentation B S hS (pullback.snd f W.ι) ∧
      IsQuasiCompact B S hS (pullback.snd f W.ι) ∧
      ∀ x : points B S hS X,
        pointsMap B S hS X f x ∈ Set.range (pointsMap B S hS W.toFunctor W.ι) →
          x ∈ flatLocus B S hS hX f F ∧
            x ∈ finitePresentationLocus B S hS hX F

AlgebraicGeometry.Space.exists_dense_open_genericFlatness_of_isScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/GenericFlatness.lean, line 736. The attribute's comment: “step 2 of the proof: the case of a reduced scheme base”.

Stacks 06QS for a reduced scheme base, step 2 of the source. This is the general statement for a base which is represented by an object of the site, where the identity may be taken as the surjective étale chart witnessing reducedness.

theorem exists_dense_open_genericFlatness_of_isScheme
    (hX : IsAlgebraicSpace B S hS X) (Z : BigFppfOver B S hS)
    [IsReduced ((BigFppfOver.toScheme B S hS).obj Z)]
    (f : X ⟶ yoneda.obj Z) (hf : IsFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hft : IsFiniteTypeOnCharts B S hS hX F) :
    ∃ W : Subfunctor (yoneda.obj Z),
      IsDenseOpenSubspace B S hS (isAlgebraicSpace_yoneda B S hS Z) W ∧
      IsFlat B S hS (pullback.snd f W.ι) ∧
      IsLocallyOfFinitePresentation B S hS (pullback.snd f W.ι) ∧
      IsQuasiCompact B S hS (pullback.snd f W.ι) ∧
      ∀ x : points B S hS X,
        pointsMap B S hS X f x ∈ Set.range (pointsMap B S hS W.toFunctor W.ι) →
          x ∈ flatLocus B S hS hX f F ∧
            x ∈ finitePresentationLocus B S hS hX F

Tag 06QT, a proposition

Tag 06QT in the Stacks Project.

AlgebraicGeometry.Space.exists_dense_open_genericFlatness_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/GenericFlatnessFinitePresentation.lean, line 107.

Stacks 06QT. Let f : X ⟶ Y be a quasi-separated morphism of algebraic spaces over S of finite type with Y reduced, and let F be an 𝒪_X-module which is quasi-coherent of finite type on charts. Then there is a dense open subspace W of Y such that the base change of f over W is flat and of finite presentation, and such that F is flat over Y and of finite presentation at every point of X lying over W.

This is Stacks 06QS refined by the quasi-separatedness hypothesis: that proposition gives flatness, local finite presentation and quasi-compactness of the base change, and a base change of a quasi-separated morphism is quasi-separated.

theorem exists_dense_open_genericFlatness_isFinitePresentation
    (hX : IsAlgebraicSpace B S hS X) {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hY : IsAlgebraicSpace B S hS Y)
    (hYred : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T))
    (f : X ⟶ Y) (hqs : IsQuasiSeparated B S hS f) (hf : IsFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hft : IsFiniteTypeOnCharts B S hS hX F) :
    ∃ W : Subfunctor Y, IsDenseOpenSubspace B S hS hY W ∧
      IsFlat B S hS (pullback.snd f W.ι) ∧
      IsFinitePresentation B S hS (pullback.snd f W.ι) ∧
      ∀ x : points B S hS X,
        pointsMap B S hS X f x ∈ Set.range (pointsMap B S hS W.toFunctor W.ι) →
          x ∈ flatLocus B S hS hX f F ∧
            x ∈ finitePresentationLocus B S hS hX F

AlgebraicGeometry.Space.exists_dense_open_genericFlatness_isFinitePresentation_of_isScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/GenericFlatnessFinitePresentation.lean, line 131. The attribute's comment: “the case of a base represented by an object of the site”.

Stacks 06QT for a base represented by an object of the site. This is the statement of the tag for a reduced scheme base, where the identity may be taken as the surjective étale chart witnessing reducedness.

theorem exists_dense_open_genericFlatness_isFinitePresentation_of_isScheme
    (hX : IsAlgebraicSpace B S hS X) (Z : BigFppfOver B S hS)
    [IsReduced ((BigFppfOver.toScheme B S hS).obj Z)]
    (f : X ⟶ yoneda.obj Z) (hqs : IsQuasiSeparated B S hS f) (hf : IsFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX)
    (hqc : IsQuasicoherentOnCharts B S hS hX F)
    (hft : IsFiniteTypeOnCharts B S hS hX F) :
    ∃ W : Subfunctor (yoneda.obj Z),
      IsDenseOpenSubspace B S hS (isAlgebraicSpace_yoneda B S hS Z) W ∧
      IsFlat B S hS (pullback.snd f W.ι) ∧
      IsFinitePresentation B S hS (pullback.snd f W.ι) ∧
      ∀ x : points B S hS X,
        pointsMap B S hS X f x ∈ Set.range (pointsMap B S hS W.toFunctor W.ι) →
          x ∈ flatLocus B S hS hX f F ∧
            x ∈ finitePresentationLocus B S hS hX F

Sources

LeanAlgebraicGeometry.Space.exists_dense_open_genericFlatness_chart · AlgebraicGeometry.Space.exists_dense_open_genericFlatness_of_isAffine · AlgebraicGeometry.Space.exists_dense_open_genericFlatness · AlgebraicGeometry.Space.exists_dense_open_genericFlatness_of_isScheme · AlgebraicGeometry.Space.exists_dense_open_genericFlatness_isFinitePresentation · AlgebraicGeometry.Space.exists_dense_open_genericFlatness_isFinitePresentation_of_isScheme

Section67.33 Relative dimension #

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

Tag 04NM, a definition

Tag 04NM in the Stacks Project.

AlgebraicGeometry.Space.HasFiberLocalRingDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionAtPoint.lean, line 81. The attribute's comment: “local_ring_fibre_dimension”.

Stacks 04NM, dimension of the local ring of a fibre. The local ring of the fibre of f has dimension d at x, tested on every étale chart at x.

abbrev HasFiberLocalRingDimension (d : ℕ∞) (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hF : IsAlgebraicSpace B S hS F) (_hG : IsAlgebraicSpace B S hS G)
    (f : F ⟶ G) (x : points B S hS F) : Prop

AlgebraicGeometry.Space.HasRelativeDimensionAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionAtPoint.lean, line 92. The attribute's comment: “relative_dimension_at_point”.

Stacks 04NM, relative dimension at a point. A morphism of algebraic spaces has relative dimension d at x if its fibre has dimension d at the corresponding point in every étale chart.

abbrev HasRelativeDimensionAt (d : ℕ∞) (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ G) (x : points B S hS F) : Prop

AlgebraicGeometry.Space.HasTranscendenceDegreeAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionAtPoint.lean, line 101. The attribute's comment: “transcendence_degree”.

Stacks 04NM, transcendence degree at a point. The transcendence degree of x over its image under f is r. For algebraic spaces this is equivalently tested on one or every étale scheme chart at x.

abbrev HasTranscendenceDegreeAt (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) (x : points B S hS F) (r : ℕ∞) :
    Prop

Tag 06LR, a definition

Tag 06LR in the Stacks Project.

AlgebraicGeometry.Space.HasRelativeDimensionLE, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeDimension.lean, line 150. The attribute's comment: “part (1): relative dimension at most d”.

Stacks 06LR, part (1). A morphism of algebraic spaces has relative dimension ≤ d if it has relative dimension ≤ d at every point of its source.

abbrev HasRelativeDimensionLE (d : ℕ) (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.HasRelativeDimension, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeDimension.lean, line 157. The attribute's comment: “part (2): relative dimension d”.

Stacks 06LR, part (2). A morphism of algebraic spaces has relative dimension d if it has relative dimension d at every point of its source.

abbrev HasRelativeDimension (d : ℕ) (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

Tag 06RX, a lemma

Tag 06RX in the Stacks Project.

AlgebraicGeometry.Space.hasTranscendenceDegreeAt_comp_iff_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeDimension.lean, line 363.

Stacks 06RX. Let X ⟶ Y ⟶ Z be morphisms of algebraic spaces over S with X ⟶ Y locally quasi-finite, and let x be a point of X. The transcendence degree of x over its image in Z is the transcendence degree of the image of x in Y over that same point: on compatible étale charts the first morphism becomes a locally quasi-finite morphism of schemes, which contributes a finite residue-field extension and so no transcendence degree.

theorem hasTranscendenceDegreeAt_comp_iff_of_isLocallyQuasiFinite
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsLocallyQuasiFinite B S hS f) (x : points B S hS X) (r : ℕ∞) :
    HasTranscendenceDegreeAt B S hS (f ≫ g) x r ↔
      HasTranscendenceDegreeAt B S hS g (pointsMap B S hS X f x) r

Tag 0ECY, a lemma

Tag 0ECY in the Stacks Project.

AlgebraicGeometry.Space.hasTranscendenceDegreeAt_zero_of_isFiniteTypePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeDimension.lean, line 409.

Stacks 0ECY. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, with Y Jacobson. Then the transcendence degree of a finite type point x of X over its image is zero.

The Jacobson hypothesis is the étale-local property of Tag 03E6 for JacobsonSpace, written out as one surjective étale atlas by a Jacobson scheme.

theorem hasTranscendenceDegreeAt_zero_of_isFiniteTypePoint
    (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)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (hJac : ∃ (V : BigFppfOver B S hS) (b : yoneda.obj V ⟶ Y),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Surjective.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) b ∧
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS))) b ∧
      JacobsonSpace ((BigFppfOver.toScheme B S hS).obj V))
    (x : points B S hS X) (hx : IsFiniteTypePoint B S hS X x) :
    HasTranscendenceDegreeAt B S hS f x 0

Tag 0AFH, a lemma

Tag 0AFH in the Stacks Project.

AlgebraicGeometry.Space.dimensionAtPoint_eq_add_of_hasRelativeDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeDimension.lean, line 500.

Stacks 0AFH. Let f : X ⟶ Y be a morphism of locally Noetherian algebraic spaces over S which is flat, locally of finite type and of relative dimension d. Then for every point x of X with image y in Y we have dim_x(X) = dim_y(Y) + d.

Local Noetherianity of an algebraic space is the étale-local property of Tag 03E6 for AlgebraicGeometry.IsLocallyNoetherian, as in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianSpaces.lean. The source is assumed locally Noetherian, as in the statement of the tag, but the hypothesis is not used: by Tag 04ZK it follows from local Noetherianity of the target and local finite type of f, which is how the chart of the source is seen to be locally Noetherian below.

The proof reduces everything to one commuting square of surjective étale charts α : U ⟶ V over f, obtained by Tag 02X1 from the locally Noetherian atlas of the target. The induced morphism of schemes is flat and locally of finite type, being the chart morphism of a flat morphism locally of finite type, and its source is locally Noetherian because its target is. It has relative dimension d in the scheme sense of part (3) of Tag 02NJ: the pointed chart built from the canonical field-valued representative of a point w of U reads the relative dimension of f above w as the local dimension of the fibre of the chart morphism through w, so that local dimension is d at every point of U, and constant local fibre dimension over a field gives equidimensional fibres of dimension d. The dimension formula for the chart morphism is then Tag 0AFE, and its two sides are the dimensions of the two algebraic spaces at the corresponding points, by the chart independence of Tag 04N5.

theorem dimensionAtPoint_eq_add_of_hasRelativeDimension
    (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)
    (_hNX : HasEtaleLocalProperty B S hS X (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (hNY : HasEtaleLocalProperty B S hS Y (fun Z : Scheme.{u} => IsLocallyNoetherian Z))
    (f : X ⟶ Y) (hflat : IsFlat B S hS f) (hft : IsLocallyOfFiniteType B S hS f)
    {d : ℕ} (hdim : HasRelativeDimension d B S hS f) (x : points B S hS X) :
    dimensionAtPoint B S hS X hX x =
      dimensionAtPoint B S hS Y hY (pointsMap B S hS X f x) + (d : WithBot ℕ∞)

Sources

LeanAlgebraicGeometry.Space.HasFiberLocalRingDimension · AlgebraicGeometry.Space.HasRelativeDimensionAt · AlgebraicGeometry.Space.HasTranscendenceDegreeAt · AlgebraicGeometry.Space.HasRelativeDimensionLE · AlgebraicGeometry.Space.HasRelativeDimension · AlgebraicGeometry.Space.hasTranscendenceDegreeAt_comp_iff_of_isLocallyQuasiFinite · AlgebraicGeometry.Space.hasTranscendenceDegreeAt_zero_of_isFiniteTypePoint · AlgebraicGeometry.Space.dimensionAtPoint_eq_add_of_hasRelativeDimension

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

67.17 Scheme theoretic closure… to 67.33 Relative dimension

Section67.17 Scheme theoretic closure and density#

Tag 0832, a lemma

Tag 0833, a lemma

Tag 0834, a definition

Tag 0835, a lemma

Tag 0836, a lemma

Tag 0837, a lemma

Tag 088G, a lemma

Tag 084N, a lemma

Sources

Section67.18 Dominant morphisms#

Tag 0ABL, a definition

Sources

Section67.19 Universally injective morphisms#

Tag 03MU, a lemma

Tag 040X, a lemma

Tag 03MV, a definition

Tag 05VS, a remark

Tag 03MW, a lemma

Tag 03MX, a lemma

Tag 03MY, a lemma

Sources

Section67.20 Affine morphisms#

Tag 03WE, a lemma

Tag 03WF, a definition

Tag 03WG, a lemma

Tag 03WH, a lemma

Tag 03WI, a lemma

Tag 07U2, a lemma

Tag 081V, a lemma

Tag 081W, a definition

Tag 081X, a remark

Tag 08AI, a lemma

Tag 08GB, a lemma

Tag 09TF, a lemma

Sources

Section67.21 Quasi-affine morphisms#

Tag 03WK, a lemma

Tag 03WL, a definition

Tag 03WM, a lemma

Tag 03WN, a lemma

Tag 03WO, a lemma

Tag 086S, a lemma

Sources

Section67.22 Types of morphisms étale local on source-and-target#

Tag 03MJ, a lemma

Tag 04RD, a definition

Tag 0AML, a remark

Tag 0AMM, a remark

Tag 04NC, a lemma

Tag 04RE, a definition

Tag 04RF, a lemma

Sources

Section67.23 Morphisms of finite type#

Tag 03XF, a definition

Tag 03XG, a lemma

Tag 03XH, a lemma

Tag 040Y, a lemma

Tag 04ZK, a lemma

Tag 0462, a lemma

Tag 06ED, a lemma

Sources

Section67.24 Points and geometric points#

Tag 0487, a lemma

Tag 0488, a lemma

Sources

Section67.25 Points of finite type#

Tag 06EF, a lemma

Tag 06EG, a definition

Tag 06EH, a lemma

Tag 06EI, a lemma

Tag 06EJ, a lemma

Tag 06EK, a lemma

Tag 06EL, a lemma

Sources

Section67.26 Nagata spaces#

Tag 0BAU, a lemma

Tag 0BAV, a lemma

Sources

Section67.17 Scheme theoretic closure and density #

Section67.18 Dominant morphisms #

Section67.19 Universally injective morphisms #

Section67.20 Affine morphisms #

Section67.21 Quasi-affine morphisms #

Section67.22 Types of morphisms étale local on source-and-target #

Section67.23 Morphisms of finite type #

Section67.24 Points and geometric points #

Section67.25 Points of finite type #

Section67.26 Nagata spaces #

Section67.27 Quasi-finite morphisms #

Section67.28 Morphisms of finite presentation #

Section67.29 Constructible sets #

Section67.30 Flat morphisms #

Section67.31 Flat modules #

Section67.32 Generic flatness #

Section67.33 Relative dimension #