67.34 Morphisms and dimensions… to 67.48 Relative normalization of…

Section67.34 Morphisms and dimensions of fibres#

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

Tag 04NQ, a lemma

Tag 04NQ in the Stacks Project.

AlgebraicGeometry.Space.relativeDimensionAt_eq_fiberLocalRingDimension_add_transcendenceDegreeAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 313.

Stacks 04NQ. For a morphism of algebraic spaces over S which is locally of finite type, the relative dimension at a point is the dimension of the local ring of the fibre there plus the transcendence degree of the point over its image.

The three invariants of Stacks 04NM are chart conditions, so all three are read off one pointed étale chart at the point (Stacks 04NC); on the resulting morphism of schemes the identity is the dimension formula of Stacks 02FX.

theorem relativeDimensionAt_eq_fiberLocalRingDimension_add_transcendenceDegreeAt
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (f : F ⟶ G) (x : points B S hS F) (hf : IsLocallyOfFiniteType B S hS f)
    (d e r : ℕ∞) (hd : HasRelativeDimensionAt d B S hS f x)
    (he : HasFiberLocalRingDimension e B S hS hF hG f x)
    (hr : HasTranscendenceDegreeAt B S hS f x r) : d = e + r

Tag 04NR, a lemma

Tag 04NR in the Stacks Project.

AlgebraicGeometry.Space.hasTranscendenceDegreeAt_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 354. The attribute's comment: “part (3): additivity of the transcendence degree”.

Additivity of the transcendence degree at a point, part (3) of Stacks 04NR. For composable morphisms f : X ⟶ Y and g : Y ⟶ Z of algebraic spaces over S and a point x of X, the transcendence degree of x over its image under f ≫ g is the sum of the transcendence degree of x over f x and of f x over g (f x).

Compatible étale charts for the composite (AlgebraicGeometry.Space.exists_compatible_etale_charts_comp) read all three transcendence degrees on a single commuting pair of chart morphisms α and β of the site; on the resulting morphisms of schemes the three residue fields form a tower and the transcendence degree of a tower is additive.

The source assumes f and g locally of finite type; that is not needed, neither for the chart comparison nor for the tower identity.

theorem hasTranscendenceDegreeAt_comp {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) (x : points B S hS X)
    (r s : ℕ∞) (hr : HasTranscendenceDegreeAt B S hS f x r)
    (hs : HasTranscendenceDegreeAt B S hS g (pointsMap B S hS X f x) s) :
    HasTranscendenceDegreeAt B S hS (f ≫ g) x (r + s)

AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_le_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 477. The attribute's comment: “part (1): the relative dimension of a composite is at most the sum”.

Stacks 04NR, part (1). For composable morphisms of algebraic spaces over S which are locally of finite type, the relative dimension of the composite at a point is at most the sum of the relative dimension of the first morphism there and of the second morphism at the image point.

Compatible étale charts for the composite read all three relative dimensions as fibre dimensions of a pair of composable morphisms of schemes at one point, where the inequality is part of Stacks 02JS.

theorem hasRelativeDimensionAt_comp_le_add {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) (x : points B S hS X)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) (d e n : ℕ∞)
    (hd : HasRelativeDimensionAt d B S hS f x)
    (he : HasRelativeDimensionAt e B S hS g (pointsMap B S hS X f x))
    (hn : HasRelativeDimensionAt n B S hS (f ≫ g) x) : n ≤ d + e

AlgebraicGeometry.Space.exists_hasRelativeDimensionAt_comp_le_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 500. The attribute's comment: “part (1): the relative dimension of a composite is at most the sum”.

Stacks 04NR, part (1). The composite of two morphisms of algebraic spaces over S which are locally of finite type has a relative dimension at every point of its source, and that dimension is at most the sum of the relative dimensions of the two factors.

theorem exists_hasRelativeDimensionAt_comp_le_add {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) (x : points B S hS X)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) (d e : ℕ∞)
    (hd : HasRelativeDimensionAt d B S hS f x)
    (he : HasRelativeDimensionAt e B S hS g (pointsMap B S hS X f x)) :
    ∃ n : ℕ∞, HasRelativeDimensionAt n B S hS (f ≫ g) x ∧ n ≤ d + e

AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 517. The attribute's comment: “part (2): equality when the first morphism is flat at the point”.

Stacks 04NR, part (2), special case. The inequality of part (1) is an equality as soon as the first morphism is flat at the point.

On compatible étale charts for the composite this is the corresponding part of Stacks 02JS, flatness of f at x becoming flatness of the first chart morphism at the selected scheme point.

theorem hasRelativeDimensionAt_comp_of_isFlatAt {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) (x : points B S hS X)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) (d e : ℕ∞)
    (hd : HasRelativeDimensionAt d B S hS f x)
    (he : HasRelativeDimensionAt e B S hS g (pointsMap B S hS X f x))
    (hflat : IsFlatAt B S hS f x) :
    HasRelativeDimensionAt (d + e) B S hS (f ≫ g) x

AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_of_isFlatAt_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1057. The attribute's comment: “part (2): equality when the morphism of field-valued fibres is flat”.

Stacks 04NR, part (2). The inequality of part (1) is an equality as soon as the morphism of field-valued fibres over the image point is flat at a point above x: here Xk and Yk are the fibres of X and Y over a field-valued representative p of the image of x in Z, presented by the two cartesian squares, x' is a point of Xk above x, and Xk ⟶ Yk is flat at x'.

Relative dimension is invariant under base change (part (1) of Stacks 04NS), so all three relative dimensions may be read on the fibres over p, where the first morphism is flat at the chosen point and AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_of_isFlatAt applies. The fibres are algebraic because they are fibre products of algebraic spaces (Stacks 02X2), and the two morphisms between them are locally of finite type because being so is stable under base change (Stacks 03XH).

No chosen fibre-product objects are imposed: the two squares are cartesian squares of arbitrary presheaves, which is why neither fibre is assumed algebraic.

theorem hasRelativeDimensionAt_comp_of_isFlatAt_fibre
    {X Y Z Xk Yk : (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) (x : points B S hS X)
    (hf : IsLocallyOfFiniteType B S hS f) (hg : IsLocallyOfFiniteType B S hS g) (d e : ℕ∞)
    (hd : HasRelativeDimensionAt d B S hS f x)
    (he : HasRelativeDimensionAt e B S hS g (pointsMap B S hS X f x))
    (p : FieldValuedPoint B S hS Z) (px : Xk ⟶ X) (py : Yk ⟶ Y)
    (qy : Yk ⟶ yoneda.obj (p.siteObject B S hS Z)) (fk : Xk ⟶ Yk) (x' : points B S hS Xk)
    (hpx : IsPullback px fk f py)
    (hpy : IsPullback py qy g (yonedaEquiv.symm p.value))
    (hx : pointsMap B S hS Xk px x' = x) (hflat : IsFlatAt B S hS fk x') :
    HasRelativeDimensionAt (d + e) B S hS (f ≫ g) x

Tag 04NS, a lemma

Tag 04NS in the Stacks Project.

AlgebraicGeometry.Space.hasRelativeDimensionAt_iff_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 686. The attribute's comment: “part (1): invariance of the relative dimension under base change”.

Invariance of relative dimension under base change, part (1) of Stacks 04NS. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, the relative dimension of the base change f' at a point x' of its source is the relative dimension of f at the image of x'.

Read on the compatible pointed charts of AlgebraicGeometry.Space.exists_etaleChartAtPoint_pair_of_isPullback, each side is the dimension of the fibre of a morphism of schemes at corresponding points of a cartesian square, which is part (1) of Stacks 02FY.

The source assumes all four corners of the square algebraic; the fourth corner X' need not be, because the two chart conditions are compared on charts supplied as data rather than on charts produced from an atlas.

theorem hasRelativeDimensionAt_iff_of_isPullback {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX : IsAlgebraicSpace B S hS X) (hY' : IsAlgebraicSpace B S hS Y')
    (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (x' : points B S hS X') (d : ℕ∞) :
    HasRelativeDimensionAt d B S hS f (pointsMap B S hS X' g' x') ↔
      HasRelativeDimensionAt d B S hS f' x'

AlgebraicGeometry.Space.exists_fiberLocalRingDimension_add_eq_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 784. The attribute's comment: “part (2): the gain in the dimension of the local ring of the fibre is the loss in transcendence degree”.

Part (2) of Stacks 04NS. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, the dimension gained by the local ring of the fibre at a point x' of the source of the base change, over its value for f at the image of x', is the transcendence degree lost there; in particular the common difference is nonnegative, which is why it is recorded as a summand n rather than as a difference.

The transcendence degrees are compared on the compatible pointed charts of AlgebraicGeometry.Space.exists_etaleChartAtPoint_pair_of_isPullback, where the drop is part (2) of Stacks 02FY for the resulting cartesian square of schemes; the sum of the two invariants is the relative dimension (Stacks 04NQ) and so agrees on the two sides by part (1) of Stacks 04NS, which turns that drop into the gain of the other invariant. The transcendence degree at x' is finite, so it cancels.

theorem exists_fiberLocalRingDimension_add_eq_of_isPullback
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (x' : points B S hS X') (e r e' r' : ℕ∞)
    (he : HasFiberLocalRingDimension e B S hS hX hY f (pointsMap B S hS X' g' x'))
    (hr : HasTranscendenceDegreeAt B S hS f (pointsMap B S hS X' g' x') r)
    (he' : HasFiberLocalRingDimension e' B S hS hX' hY' f' x')
    (hr' : HasTranscendenceDegreeAt B S hS f' x' r') :
    ∃ n : ℕ∞, e + n = e' ∧ r' + n = r

AlgebraicGeometry.Space.fiberLocalRingDimension_le_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 832. The attribute's comment: “part (2): the dimension of the local ring of the fibre does not decrease”.

Part (2) of Stacks 04NS. Base change does not decrease the dimension of the local ring of the fibre at a point.

theorem fiberLocalRingDimension_le_of_isPullback
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (x' : points B S hS X') (e r e' r' : ℕ∞)
    (he : HasFiberLocalRingDimension e B S hS hX hY f (pointsMap B S hS X' g' x'))
    (hr : HasTranscendenceDegreeAt B S hS f (pointsMap B S hS X' g' x') r)
    (he' : HasFiberLocalRingDimension e' B S hS hX' hY' f' x')
    (hr' : HasTranscendenceDegreeAt B S hS f' x' r') : e ≤ e'

AlgebraicGeometry.Space.transcendenceDegreeAt_le_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 850. The attribute's comment: “part (2): the transcendence degree does not increase”.

Part (2) of Stacks 04NS. Base change does not increase the transcendence degree of a point over its image.

theorem transcendenceDegreeAt_le_of_isPullback
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (x' : points B S hS X') (e r e' r' : ℕ∞)
    (he : HasFiberLocalRingDimension e B S hS hX hY f (pointsMap B S hS X' g' x'))
    (hr : HasTranscendenceDegreeAt B S hS f (pointsMap B S hS X' g' x') r)
    (he' : HasFiberLocalRingDimension e' B S hS hX' hY' f' x')
    (hr' : HasTranscendenceDegreeAt B S hS f' x' r') : r' ≤ r

AlgebraicGeometry.Space.exists_point_preserving_fiberLocalRingDimension_and_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 890. The attribute's comment: “part (3): a common lift at which both invariants are preserved”.

Part (3) of Stacks 04NS. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, a point x of X and a point y' of Y' with the same image in Y have a common lift x' to X' at which the dimension of the local ring of the fibre and the transcendence degree both take the value they take at x — that is, at which the common difference of part (2) vanishes.

Some common lift exists because the point set of a fibre product surjects onto the fibre product of the point sets (Stacks 03H4). On the compatible pointed charts at such a lift (AlgebraicGeometry.Space.exists_etaleChartAtPoint_pair_of_isPullback) part (3) of Stacks 02FY replaces the scheme point selected by the chart of the base change by one lying over the same two points at which both invariants are preserved; the same chart with that point as its representative is a pointed chart at its image in X', and that image is the required lift, because the two source charts commute with the horizontal arrow of the square.

theorem exists_point_preserving_fiberLocalRingDimension_and_trdeg
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (x : points B S hS X) (y' : points B S hS Y')
    (hxy : pointsMap B S hS X f x = pointsMap B S hS Y' g y') :
    ∃ x' : points B S hS X', pointsMap B S hS X' g' x' = x ∧
      pointsMap B S hS X' f' x' = y' ∧
      (∀ d : ℕ∞, HasFiberLocalRingDimension d B S hS hX hY f x ↔
        HasFiberLocalRingDimension d B S hS hX' hY' f' x') ∧
      (∀ r : ℕ∞, HasTranscendenceDegreeAt B S hS f x r ↔
        HasTranscendenceDegreeAt B S hS f' x' r)

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

In a cartesian square of algebraic spaces over S with f locally of finite type, the relative dimension of the base change of f at a point of its source is the relative dimension of f at the image of that point.

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. Only X, Y and Z are assumed to be algebraic spaces.

theorem hasRelativeDimensionAt_iff_of_isPullback' (d : ℕ∞)
    {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' : points B S hS W) :
    HasRelativeDimensionAt d B S hS p x' ↔
      HasRelativeDimensionAt d B S hS f (pointsMap B S hS W q x')

Tag 04NT, a lemma

Tag 04NT in the Stacks Project.

AlgebraicGeometry.Space.isOpen_setOf_hasRelativeDimensionAt_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionOpenness.lean, line 55.

For a morphism of algebraic spaces over S which is locally of finite type, the set of points of the source at which the relative dimension is at most n is open.

theorem isOpen_setOf_hasRelativeDimensionAt_le (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f)
    (n : ℕ) :
    IsOpen {x : points B S hS F |
      ∃ d : ℕ∞, d ≤ (n : ℕ∞) ∧ HasRelativeDimensionAt d B S hS f x}

Tag 04NU, a lemma

Tag 04NU in the Stacks Project.

AlgebraicGeometry.Space.isRetrocompact_setOf_exists_hasRelativeDimensionAt_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1170.

Stacks 04NU. For a morphism of algebraic spaces over S which is locally of finite presentation and a natural number n, the open set of Stacks 04NT — the points of the source at which the relative dimension is at most n — is retrocompact in the point space of Tag 03BU.

As for Stacks 04NT, a surjective étale chart a of the source lifted from an atlas of the target reads the locus, point by point, as the bounded-fibre-dimension locus Wₙ of the induced morphism of schemes, which is retrocompact by Stacks 02G0. Points of a represented presheaf are homeomorphic to points of the representing scheme (Tag 03BX), so the preimage of the locus under |a| is retrocompact; transporting that to the locus itself uses that |a| is a continuous open surjection: a compact open K of the target is covered by the images of the preimages of finitely many affine opens of the chart contained in the open |a| ⁻¹' K, and on each of them the intersection with the locus is the image of a compact set.

theorem isRetrocompact_setOf_exists_hasRelativeDimensionAt_le (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G)
    (hf : IsLocallyOfFinitePresentation B S hS f) (n : ℕ) :
    IsRetrocompact {x : points B S hS F |
      ∃ d : ℕ∞, d ≤ (n : ℕ∞) ∧ HasRelativeDimensionAt d B S hS f x}

Tag 04NV, a lemma

Tag 04NV in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_forall_hasRelativeDimensionAt_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionQuasiFinite.lean, line 60.

A morphism f : F ⟶ G of presheaves over S on the big fppf site which is locally of finite type is locally quasi-finite exactly when it has relative dimension 0 at every point of its source. In particular this holds for a morphism of algebraic spaces over S.

theorem isLocallyQuasiFinite_iff_forall_hasRelativeDimensionAt_zero (f : F ⟶ G)
    (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyQuasiFinite B S hS f ↔
      ∀ x : points B S hS F, HasRelativeDimensionAt 0 B S hS f x

Tag 04NW, a lemma

Tag 04NW in the Stacks Project.

AlgebraicGeometry.Space.locallyQuasiFinitePart, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1275. The attribute's comment: “the canonical open subspace”.

Stacks 04NW, the canonical open subspace. The open subspace of the source of a morphism of algebraic spaces over S which is locally of finite type cut out by the points of relative dimension 0; it is an open subspace by Stacks 04NT and Stacks 03BZ.

noncomputable def locallyQuasiFinitePart (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f) :
    {U : Subfunctor F // IsOpenSubspace B S hS U}

AlgebraicGeometry.Space.mem_range_pointsMap_locallyQuasiFinitePart_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1286. The attribute's comment: “the points of the canonical open subspace”.

Stacks 04NW, the points of the canonical open subspace. A point of the source lies in the point set of AlgebraicGeometry.Space.locallyQuasiFinitePart exactly when the relative dimension there is 0.

theorem mem_range_pointsMap_locallyQuasiFinitePart_iff (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f)
    (x : points B S hS F) :
    x ∈ Set.range (pointsMap B S hS (locallyQuasiFinitePart B S hS hF hG f hf).1.toFunctor
        (locallyQuasiFinitePart B S hS hF hG f hf).1.ι) ↔
      HasRelativeDimensionAt 0 B S hS f x

AlgebraicGeometry.Space.isLocallyQuasiFinite_locallyQuasiFinitePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1310. The attribute's comment: “local quasi-finiteness of the restriction”.

Stacks 04NW, local quasi-finiteness of the restriction. The restriction of the morphism to AlgebraicGeometry.Space.locallyQuasiFinitePart is locally quasi-finite.

Every point of the open subspace has relative dimension 0 for the restricted morphism, because relative dimension is unchanged by restricting the source to an open subspace, so this is Stacks 04NV for the restriction.

theorem isLocallyQuasiFinite_locallyQuasiFinitePart (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyQuasiFinite B S hS ((locallyQuasiFinitePart B S hS hF hG f hf).1.ι ≫ f)

AlgebraicGeometry.Space.exists_one_le_hasRelativeDimensionAt_of_not_mem_locallyQuasiFinitePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1327. The attribute's comment: “positive relative dimension outside the canonical open subspace”.

Stacks 04NW, positive relative dimension outside the canonical open subspace. At a point of the source which is not in the point set of AlgebraicGeometry.Space.locallyQuasiFinitePart the relative dimension is at least 1: a relative dimension exists there, and were it 0 the point would lie in that point set.

theorem exists_one_le_hasRelativeDimensionAt_of_not_mem_locallyQuasiFinitePart
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G)
    (hf : IsLocallyOfFiniteType B S hS f) (x : points B S hS F)
    (hx : x ∉ Set.range (pointsMap B S hS
      (locallyQuasiFinitePart B S hS hF hG f hf).1.toFunctor
      (locallyQuasiFinitePart B S hS hF hG f hf).1.ι)) :
    ∃ d : ℕ∞, 1 ≤ d ∧ HasRelativeDimensionAt d B S hS f x

AlgebraicGeometry.Space.le_locallyQuasiFinitePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1344. The attribute's comment: “maximality of the canonical open subspace”.

Stacks 04NW, maximality. Every open subspace of the source over which the morphism is locally quasi-finite is contained in AlgebraicGeometry.Space.locallyQuasiFinitePart; together with AlgebraicGeometry.Space.isLocallyQuasiFinite_locallyQuasiFinitePart this is what makes it canonical.

theorem le_locallyQuasiFinitePart (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f)
    (U : {U : Subfunctor F // IsOpenSubspace B S hS U})
    (hU : IsLocallyQuasiFinite B S hS (U.1.ι ≫ f)) :
    U ≤ locallyQuasiFinitePart B S hS hF hG f hf

AlgebraicGeometry.Space.locallyQuasiFinitePart_preimage_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1371. The attribute's comment: “compatibility with arbitrary base change”. References: SGA 3 V (7.4), “more general”.

Stacks 04NW, compatibility with arbitrary base change. In a cartesian square of algebraic spaces over S whose right vertical arrow is locally of finite type, the base change is locally of finite type and its locally quasi-finite part is the inverse image of the locally quasi-finite part of the morphism.

On points both sides are the relative-dimension-zero locus, and relative dimension at a point is invariant under base change by part (1) of Stacks 04NS.

theorem locallyQuasiFinitePart_preimage_of_isPullback
    {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) :
    ∃ hf' : IsLocallyOfFiniteType B S hS f',
      (locallyQuasiFinitePart B S hS hX' hY' f' hf').1 =
        (locallyQuasiFinitePart B S hS hX hY f hf).1.preimage g'

AlgebraicGeometry.Space.isOpenSubspace_relativeDimensionZeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionZeroLocus.lean, line 110. The attribute's comment: “the canonical open subspace”.

For a morphism of algebraic spaces over S which is locally of finite type, the locus where the relative dimension is zero is an open subspace of the source.

theorem isOpenSubspace_relativeDimensionZeroLocus (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f) :
    IsOpenSubspace B S hS (relativeDimensionZeroLocus B S hS f)

AlgebraicGeometry.Space.isLocallyQuasiFinite_relativeDimensionZeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionZeroLocus.lean, line 128. The attribute's comment: “local quasi-finiteness of the restriction”. References: EGA III (4.4.12), “partial”.

A morphism of algebraic spaces over S which is locally of finite type is locally quasi-finite on the open subspace of its source where its relative dimension is zero.

theorem isLocallyQuasiFinite_relativeDimensionZeroLocus (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f) :
    IsLocallyQuasiFinite B S hS ((relativeDimensionZeroLocus B S hS f).ι ≫ f)

AlgebraicGeometry.Space.one_le_of_hasRelativeDimensionAt_of_notMem_relativeDimensionZeroLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDimensionZeroLocus.lean, line 143. The attribute's comment: “relative dimension at least one outside the subspace”.

At a point of the source which is not in the relative-dimension-zero locus, every value of the relative dimension of the morphism is at least 1.

theorem one_le_of_hasRelativeDimensionAt_of_notMem_relativeDimensionZeroLocus (f : F ⟶ G)
    (x : points B S hS F)
    (hx : x ∉ Set.range (pointsMap B S hS (relativeDimensionZeroLocus B S hS f).toFunctor
      (relativeDimensionZeroLocus B S hS f).ι))
    (d : ℕ∞) (hd : HasRelativeDimensionAt d B S hS f x) : 1 ≤ d

Tag 06LS, a lemma

Tag 06LS in the Stacks Project.

AlgebraicGeometry.Space.isQuasiFiniteAt_of_dimensionAtPoint_fiber_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FibreDimension.lean, line 1470.

Stacks 06LS. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, let p be a field-valued point of Y — a morphism Spec k ⟶ Y from the spectrum of a field over S — and let z be a point of the fibre X ×_Y Spec k at which that fibre has dimension 0 in the sense of Stacks 04N5. Then f is quasi-finite at the image of z: after replacing X by an open subspace containing that image, f is locally quasi-finite.

theorem isQuasiFiniteAt_of_dimensionAtPoint_fiber_eq_zero (hX : IsAlgebraicSpace B S hS F)
    (hY : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (hf : IsLocallyOfFiniteType B S hS f)
    (p : FieldValuedPoint B S hS G)
    (z : points B S hS (pullback f (yonedaEquiv.symm p.value)))
    (hz : dimensionAtPoint B S hS (pullback f (yonedaEquiv.symm p.value))
      (isAlgebraicSpace_pullback B S hS f (yonedaEquiv.symm p.value) hX
        (isAlgebraicSpace_yoneda B S hS (p.siteObject B S hS G)) hY) z = 0) :
    IsQuasiFiniteAt B S hS f
      (pointsMap B S hS (pullback f (yonedaEquiv.symm p.value))
        (pullback.fst f (yonedaEquiv.symm p.value)) z)

Sources

• Section 67.34, Tag 04NP
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.relativeDimensionAt_eq_fiberLocalRingDimension_add_transcendenceDegreeAt · AlgebraicGeometry.Space.hasTranscendenceDegreeAt_comp · AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_le_add · AlgebraicGeometry.Space.exists_hasRelativeDimensionAt_comp_le_add · AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_of_isFlatAt · AlgebraicGeometry.Space.hasRelativeDimensionAt_comp_of_isFlatAt_fibre · AlgebraicGeometry.Space.hasRelativeDimensionAt_iff_of_isPullback · AlgebraicGeometry.Space.exists_fiberLocalRingDimension_add_eq_of_isPullback

Section67.35 The dimension formula#

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

Tag 0BAX, a lemma

Tag 0BAX in the Stacks Project.

AlgebraicGeometry.Space.finite_zeroDimensionalSpecializations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 463. The attribute's comment: “finiteness of the family entering the maximum”. References: EGA IV (13.2.6), “more general”.

Stacks 0BAX, finiteness of the family entering the maximum. Under the hypotheses of the dimension formula only finitely many codimension-zero points of the source specialize to a given point.

The source is locally Noetherian by Stacks 04ZK, hence has locally finite irreducible components by Stacks 0GMB, so every quasi-compact algebraic space étale over it has finitely many codimension-zero points by Stacks 0BB1. An affine étale chart through the point is such a space, its image on points is open by Stacks 03BX and therefore contains every point specializing to the given one, and codimension zero is étale-invariant by Stacks 0A4H.

theorem finite_zeroDimensionalSpecializations (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hf : IsLocallyOfFiniteType B S hS f) (x : points B S hS X) :
    {ξ : points B S hS X | x ∈ closure {ξ} ∧ localRingDimension B S hS ξ = 0}.Finite

AlgebraicGeometry.Space.exists_genericResidueFieldTranscendenceDegreeAt_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 520. The attribute's comment: “attainment of the maximum”.

Stacks 0BAX, attainment of the maximum. Under the hypotheses of the dimension formula the supremum defining the correction term is attained, so it is a maximum.

The family is finite by AlgebraicGeometry.Space.finite_zeroDimensionalSpecializations, and it is nonempty because the generic point of an irreducible component of an étale chart through the chosen point maps to a codimension-zero point specializing to it (Stacks 0BAQ).

theorem exists_genericResidueFieldTranscendenceDegreeAt_eq (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hf : IsLocallyOfFiniteType B S hS f) (x : points B S hS X) :
    ∃ ξ : {ξ : points B S hS X // x ∈ closure {ξ} ∧ localRingDimension B S hS ξ = 0},
      genericResidueFieldTranscendenceDegreeAt B S hS f x =
        residueFieldTranscendenceDegreeAt B S hS f ξ.1

AlgebraicGeometry.Space.localRingDimension_add_residueFieldTranscendenceDegree_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ConstructibleSets.lean, line 594. The attribute's comment: “dimension inequality”. References: EGA IV (5.6.5), “more general”.

Stacks 0BAX, the dimension inequality. For a morphism of algebraic spaces over S locally of finite type with locally Noetherian target, the dimension of the local ring at a point plus the residue-field transcendence degree there is at most the dimension of the local ring at the image point plus the largest residue-field transcendence degree at a codimension-zero point specializing to the given one.

Everything is read on one pointed étale chart of Stacks 04NC: the two local dimensions are the Krull dimensions of the two chart stalks by Stacks 0BAM, the two residue-field degrees are those of the morphism of charts by Stacks 04NK, and the inequality between them is the dimension formula for schemes, Stacks 0BAE. The chart's own maximum is bounded by the one in the statement because each generic point of the chart through the chart point maps to a codimension-zero point of the source specializing to the given one, by Stacks 0BAQ and Stacks 0A4H.

theorem localRingDimension_add_residueFieldTranscendenceDegree_le (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hf : IsLocallyOfFiniteType B S hS f) (x : points B S hS X) :
    (localRingDimension B S hS x : WithBot ℕ∞) +
        (residueFieldTranscendenceDegreeAt B S hS f x : WithBot ℕ∞) ≤
      (localRingDimension B S hS (pointsMap B S hS X f x) : WithBot ℕ∞) +
        (genericResidueFieldTranscendenceDegreeAt B S hS f x : WithBot ℕ∞)

Tag 0BAY, a lemma

Tag 0BAY in the Stacks Project.

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

Stacks 0BAY. For a morphism of algebraic spaces over S locally of finite type with locally Noetherian target, the dimension of the source is at most the dimension of the target plus the supremum of the residue-field transcendence degrees at the codimension-zero points of the source.

Both dimensions are suprema of local-ring dimensions by Stacks 0BAN, and at each point the pointwise inequality is Stacks 0BAX, whose correction term is attained at a codimension-zero point and so is bounded by the supremum over all of them.

theorem dimension_le_add_iSup_residueFieldTranscendenceDegree (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hf : IsLocallyOfFiniteType B S hS f) :
    dimension B S hS X hX ≤ dimension B S hS Y hY +
      ((⨆ ξ : {ξ : points B S hS X // localRingDimension B S hS ξ = 0},
        residueFieldTranscendenceDegreeAt B S hS f ξ.1 : ℕ∞) : WithBot ℕ∞)

Sources

• Section 67.35, Tag 0BAW
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.finite_zeroDimensionalSpecializations · AlgebraicGeometry.Space.exists_genericResidueFieldTranscendenceDegreeAt_eq · AlgebraicGeometry.Space.localRingDimension_add_residueFieldTranscendenceDegree_le · AlgebraicGeometry.Space.dimension_le_add_iSup_residueFieldTranscendenceDegree

Section67.36 Syntomic morphisms#

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

Tag 03Z7, a definition

Tag 03Z7 in the Stacks Project.

AlgebraicGeometry.Space.IsSyntomic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Syntomic.lean, line 59. The attribute's comment: “part (1): syntomic morphisms”.

Stacks 03Z7, part (1). A morphism of algebraic spaces over S is syntomic when the scheme morphism underlying every commuting square of étale scheme charts of it is syntomic.

abbrev IsSyntomic (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsSyntomicAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Syntomic.lean, line 67. The attribute's comment: “part (2): syntomic at a point”.

Stacks 03Z7, part (2). A morphism of algebraic spaces over S is syntomic at a point x of its source when it is syntomic on some open subspace of the source having a point over x.

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

Tag 03Z8, a lemma

Tag 03Z8 in the Stacks Project.

AlgebraicGeometry.Space.isSyntomic_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Syntomic.lean, line 162.

Stacks 03Z8. The composite of two syntomic morphisms of algebraic spaces over S is syntomic.

Syntomicity of scheme morphisms is stable under composition ([Stacks Project, Tag 01UH]) and is étale local on the source and target (Tag 04R3), so this is the instance of [Stacks Project, Tag 0AML] at that property.

theorem isSyntomic_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 : IsSyntomic B S hS f) (hg : IsSyntomic B S hS g) :
    IsSyntomic B S hS (f ≫ g)

Tag 03Z9, a lemma

Tag 03Z9 in the Stacks Project.

AlgebraicGeometry.Space.isSyntomic_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Syntomic.lean, line 178.

Stacks 03Z9. Syntomic morphisms of algebraic spaces over S are stable under base change.

Syntomicity of scheme morphisms is stable under base change ([Stacks Project, Tag 01UI]) and is étale local on the source and target (Tag 04R3), so this is the instance of [Stacks Project, Tag 0AMM] at that property.

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

Tag 03ZA, a lemma

Tag 03ZA in the Stacks Project.

AlgebraicGeometry.Space.isSyntomic_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SyntomicTfae.lean, line 92.

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

Syntomicity of morphisms of schemes is étale local on the source and target (Tag 04R3), stable under composition ([Stacks Project, Tag 01UH]) and under base change ([Stacks Project, Tag 01UI]), and implied by étaleness ([Stacks Project, Tag 01VD]), so this is the instance of AlgebraicGeometry.Space.holdsOnEveryEtaleChart_tfae — Tag 03MM for an arbitrary such property — at that property. Condition (2) is AlgebraicGeometry.Space.IsSyntomicAt, which is by definition condition (2) of that theorem.

theorem isSyntomic_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      IsSyntomic B S hS f,
      ∀ x : points B S hS X, IsSyntomicAt B S hS f x,
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsSyntomic 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) → IsSyntomic 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 ∧ IsSyntomic 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 ∧ IsSyntomic 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 →
          IsSyntomic 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 ∧ IsSyntomic 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, IsSyntomic B S hS ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 0DEY, a lemma

Tag 0DEY in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isSyntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Syntomic.lean, line 128.

Stacks 0DEY. A syntomic morphism of algebraic spaces over S is locally of finite presentation.

Both properties are the condition of Tag 03MJ on every commuting square of étale charts, so the statement is the scheme-level implication of [Stacks Project, Tag 01UK] quantified over the charts.

theorem isLocallyOfFinitePresentation_of_isSyntomic {f : X ⟶ Y}
    (hf : IsSyntomic B S hS f) : IsLocallyOfFinitePresentation B S hS f

Tag 0DEZ, a lemma

Tag 0DEZ in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_isSyntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Syntomic.lean, line 139.

Stacks 0DEZ. A syntomic morphism of algebraic spaces over S is flat.

Both properties are the condition of Tag 03MJ on every commuting square of étale charts, so the statement is the scheme-level implication of [Stacks Project, Tag 01UL] quantified over the charts.

theorem isFlat_of_isSyntomic {f : X ⟶ Y} (hf : IsSyntomic B S hS f) : IsFlat B S hS f

Tag 0DF0, a lemma

Tag 0DF0 in the Stacks Project.

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

A syntomic morphism of algebraic spaces over S is universally open in the sense of Stacks 03Z2.

theorem universallyOpen_of_isSyntomic
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsSyntomic B S hS f) : UniversallyOpen B S hS f

Sources

• Section 67.36, Tag 03Z6
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsSyntomic · AlgebraicGeometry.Space.IsSyntomicAt · AlgebraicGeometry.Space.isSyntomic_comp · AlgebraicGeometry.Space.isSyntomic_isStableUnderBaseChange · AlgebraicGeometry.Space.isSyntomic_tfae · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isSyntomic · AlgebraicGeometry.Space.isFlat_of_isSyntomic · AlgebraicGeometry.Space.universallyOpen_of_isSyntomic

Section67.37 Smooth morphisms#

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

Tag 03ZC, a definition

Tag 03ZC in the Stacks Project.

AlgebraicGeometry.Space.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Smooth.lean, line 43. The attribute's comment: “part (1): smooth morphisms”.

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

abbrev IsSmooth (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsSmoothAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Smooth.lean, line 50. The attribute's comment: “part (2): smooth at a point”.

A morphism of algebraic spaces over S is smooth at a point x of its source when it is smooth on some open subspace of the source having a point over x.

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

Tag 03ZD, a lemma

Tag 03ZD in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothMorphismProperty.lean, line 72. References: EGA IV (17.3.3), “more general”; EGA IV (6.8.3), “more general”.

Stacks 03ZD. The composite of two smooth morphisms of algebraic spaces over S is smooth: this is Stacks 0AML applied to the smooth property of morphisms of schemes, which is étale local on the source and target and stable under composition.

theorem isSmooth_comp {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 : IsSmooth B S hS f) (hg : IsSmooth B S hS g) :
    IsSmooth B S hS (f ≫ g)

Tag 03ZE, a lemma

Tag 03ZE in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/SmoothLocalAtSource.lean, line 119. References: SGA 1 II (1.3), “(ii)”.

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

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

Tag 03ZF, a lemma

Tag 03ZF in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothTfae.lean, line 479.

The pointwise, scheme-local, étale-local, and Zariski-local criteria for smoothness of a morphism of algebraic spaces.

theorem isSmooth_tfae
    (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) :
    List.TFAE [
      IsSmooth B S hS f,
      (∀ x : points B S hS X, IsSmoothAt B S hS f x),
      (∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsSmooth 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) →
          IsSmooth B S hS (pullback.snd f g)),
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        IsSmooth B S hS (pullback.snd f g)),
      (∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X),
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf p ∧
        IsSmooth B S hS (p ≫ f)),
      HoldsOnEveryEtaleChart B S hS
        (@Smooth.{u} : MorphismProperty Scheme.{u}) f,
      HoldsOnSurjectiveEtaleChart B S hS
        (@Smooth.{u} : MorphismProperty Scheme.{u}) f,
      (∃ (I : Type u) (V : I → Subfunctor Y),
        IsZariskiCover B S hS I V ∧
        ∀ i, ∃ (J : Type u)
          (U : J → Subfunctor (pullback f (V i).ι)),
          IsZariskiCover B S hS J U ∧
          ∀ j, IsSmooth B S hS
            ((U j).ι ≫ pullback.snd f (V i).ι))
    ]

Tag 04AJ, a lemma

Tag 04AJ in the Stacks Project.

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

Stacks 04AJ. A smooth morphism of algebraic spaces over S is locally of finite presentation.

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

Tag 06MH, a lemma

Tag 06MH in the Stacks Project.

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

Stacks 06MH. A smooth morphism of algebraic spaces over S is locally of finite type.

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

Tag 04TA, a lemma

Tag 04TA in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothFlat.lean, line 48.

Stacks 04TA. A smooth morphism of algebraic spaces over S is flat: on each commuting square of étale scheme charts the underlying scheme morphism is smooth, hence flat.

theorem isFlat_of_isSmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (hf : IsSmooth B S hS f) :
    IsFlat B S hS f

Tag 06CP, a lemma

Tag 06CP in the Stacks Project.

AlgebraicGeometry.Space.isSyntomic_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Syntomic.lean, line 190.

Stacks 06CP. A smooth morphism of algebraic spaces over S is syntomic.

On each commuting square of étale charts the underlying morphism of schemes is smooth, hence syntomic by AlgebraicGeometry.syntomic_of_smooth, which is Stacks 01VD.

theorem isSyntomic_of_isSmooth (f : X ⟶ Y) (hf : IsSmooth B S hS f) :
    IsSyntomic B S hS f

Tag 0DZI, a lemma

Tag 0DZI in the Stacks Project.

AlgebraicGeometry.Space.le_maximalSmoothOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Smooth.lean, line 271. The attribute's comment: “maximality of the smooth locus”.

Stacks 0DZI, maximality. Every open subspace on which f is smooth is contained in the smooth locus: it is a member of the family the smooth locus is the supremum of.

theorem le_maximalSmoothOpen (f : X ⟶ Y) {U : Subfunctor X}
    (hU : IsOpenSubspace B S hS U) (hUf : IsSmooth B S hS (U.ι ≫ f)) :
    U ≤ maximalSmoothOpen B S hS f

AlgebraicGeometry.Space.isOpenSubspace_maximalSmoothOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Smooth.lean, line 411. The attribute's comment: “the smooth locus is an open subspace”.

Stacks 0DZI, openness. The smooth locus of a morphism of algebraic spaces over S is an open subspace.

theorem isOpenSubspace_maximalSmoothOpen (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsOpenSubspace B S hS (maximalSmoothOpen B S hS f)

AlgebraicGeometry.Space.isSmooth_maximalSmoothOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Smooth.lean, line 419. The attribute's comment: “the morphism is smooth on its smooth locus”.

Stacks 0DZI, smoothness on the open. A morphism of algebraic spaces over S is smooth on its smooth locus.

theorem isSmooth_maximalSmoothOpen (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsSmooth B S hS ((maximalSmoothOpen B S hS f).ι ≫ f)

AlgebraicGeometry.Space.maximalSmoothOpen_eq_preimage_of_isFlat_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Smooth.lean, line 738. The attribute's comment: “part (1): base change by a flat morphism locally of finite presentation”. References: EGA IV (17.7.4), “more general”.

Stacks 0DZI, part (1). Formation of the smooth locus commutes with base change by a morphism which is flat and locally of finite presentation.

theorem maximalSmoothOpen_eq_preimage_of_isFlat_isLocallyOfFinitePresentation
    (sq : IsPullback g' f' f g) (hgflat : IsFlat B S hS g.hom)
    (hglfp : IsLocallyOfFinitePresentation B S hS g.hom) :
    maximalSmoothOpen B S hS f'.hom = (maximalSmoothOpen B S hS f.hom).preimage g'.hom

AlgebraicGeometry.Space.maximalSmoothOpen_eq_preimage_of_isLocallyOfFinitePresentation_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Smooth.lean, line 749. The attribute's comment: “part (2): flat base change of a morphism locally of finite presentation”. References: EGA IV (17.7.4), “(v), special case”.

Stacks 0DZI, part (2). For a morphism locally of finite presentation, formation of the smooth locus commutes with every flat base change.

theorem maximalSmoothOpen_eq_preimage_of_isLocallyOfFinitePresentation_isFlat
    (sq : IsPullback g' f' f g) (hflfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (hgflat : IsFlat B S hS g.hom) :
    maximalSmoothOpen B S hS f'.hom = (maximalSmoothOpen B S hS f.hom).preimage g'.hom

Tag 0AFI, a lemma

Tag 0AFI in the Stacks Project.

AlgebraicGeometry.Space.dimensionAtPoint_eq_add_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SmoothDimensionFormula.lean, line 70.

Stacks 0AFI. Let f : X ⟶ Y be a smooth morphism of locally Noetherian algebraic spaces over S. For every point x of X with image y in Y we have dim_x(X) = dim_y(Y) + dim_x(X_y), where dim_x(X_y) is the relative dimension d of f at x in the sense of Tag 04NM.

public theorem dimensionAtPoint_eq_add_of_isSmooth
    (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) (hf : IsSmooth B S hS f) {d : ℕ∞} (x : points B S hS X)
    (hd : HasRelativeDimensionAt d B S hS f x) :
    dimensionAtPoint B S hS X hX x =
      dimensionAtPoint B S hS Y hY (pointsMap B S hS X f x) + (d : WithBot ℕ∞)

Sources

• Section 67.37, Tag 03ZB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsSmooth · AlgebraicGeometry.Space.IsSmoothAt · AlgebraicGeometry.Space.isSmooth_comp · AlgebraicGeometry.Space.isSmooth_isStableUnderBaseChange · AlgebraicGeometry.Space.isSmooth_tfae · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isSmooth · AlgebraicGeometry.Space.isLocallyOfFiniteType_of_isSmooth · AlgebraicGeometry.Space.isFlat_of_isSmooth

Section67.38 Unramified morphisms#

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

Tag 03ZH, a definition

Tag 03ZH in the Stacks Project.

AlgebraicGeometry.Space.IsUnramified, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unramified.lean, line 124. The attribute's comment: “part (1): unramified morphisms”.

Stacks 03ZH, part (1). A morphism of algebraic spaces over S is unramified when the scheme morphism in every commuting square of étale scheme charts is unramified.

abbrev IsUnramified (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsGUnramified, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unramified.lean, line 131. The attribute's comment: “part (3): G-unramified morphisms”.

Stacks 03ZH, part (3). A morphism of algebraic spaces over S is G-unramified when the scheme morphism in every commuting square of étale scheme charts is G-unramified.

abbrev IsGUnramified (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsUnramifiedAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unramified.lean, line 139. The attribute's comment: “part (2): unramified at a point”.

Stacks 03ZH, part (2). A morphism of algebraic spaces over S is unramified at a point x of its source when it is unramified on some open subspace of the source having a point over x.

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

AlgebraicGeometry.Space.IsGUnramifiedAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unramified.lean, line 148. The attribute's comment: “part (4): G-unramified at a point”.

Stacks 03ZH, part (4). A morphism of algebraic spaces over S is G-unramified at a point x of its source when it is G-unramified on some open subspace of the source having a point over x.

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

Tag 04G1, a lemma

Tag 04G1 in the Stacks Project.

AlgebraicGeometry.Space.isGUnramified_iff_isUnramified_and_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 274.

Stacks 04G1. A morphism of algebraic spaces over S is G-unramified exactly when it is unramified and locally of finite presentation.

All three properties are conditions on every commuting square of étale charts, so the statement is the scheme-level equivalence AlgebraicGeometry.gUnramified_iff_unramified_and_locallyOfFinitePresentation quantified over the charts, together with the distribution of a universal quantifier over a conjunction.

theorem isGUnramified_iff_isUnramified_and_isLocallyOfFinitePresentation (f : X ⟶ Y) :
    IsGUnramified B S hS f ↔
      (IsUnramified B S hS f ∧ IsLocallyOfFinitePresentation B S hS f)

Tag 03ZI, a lemma

Tag 03ZI in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 165.

Stacks 03ZI. The composite of two unramified morphisms of algebraic spaces over S is unramified.

Unramifiedness of scheme morphisms is étale local on the source and target and stable under composition, so this is the instance of [Stacks Project, Tag 0AML] at that property.

theorem isUnramified_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 : IsUnramified B S hS f) (hg : IsUnramified B S hS g) :
    IsUnramified B S hS (f ≫ g)

Tag 03ZJ, a lemma

Tag 03ZJ in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 188. References: SGA 1 I (3.5), “(iii)”.

Stacks 03ZJ. Unramified morphisms of algebraic spaces over S are stable under base change.

Unramifiedness of scheme morphisms is étale local on the source and target and stable under base change, so this is the instance of [Stacks Project, Tag 0AMM] at that property.

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

Tag 03ZK, a lemma

Tag 03ZK in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 578.

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

Unramifiedness of morphisms of schemes is étale local on the source and target ([Stacks Project, Tag 04R3]), stable under composition ([Stacks Project, Tag 02G9]) and under base change ([Stacks Project, Tag 02GA]), and implied by étaleness, so this is the instance of AlgebraicGeometry.Space.holdsOnEveryEtaleChart_tfae — Stacks 03MM for an arbitrary such property — at that property. Condition (2) is AlgebraicGeometry.Space.IsUnramifiedAt, which is by definition condition (2) of that theorem.

theorem isUnramified_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      IsUnramified B S hS f,
      ∀ x : points B S hS X, IsUnramifiedAt B S hS f x,
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsUnramified 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) → IsUnramified 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 ∧ IsUnramified 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 ∧ IsUnramified 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 →
          IsUnramified 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 ∧ IsUnramified 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, IsUnramified B S hS ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 05VZ, a lemma

Tag 05VZ in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Unramified.lean, line 194.

Stacks 05VZ. An unramified morphism of algebraic spaces is locally of finite type. In every étale chart the underlying scheme morphism is unramified, hence locally of finite type by AlgebraicGeometry.locallyOfFiniteType_of_unramified.

This is also the local-finite-type half of the implication (1) ⇒ (3) of [Stacks Project, Tag 05W6].

theorem isLocallyOfFiniteType_of_isUnramified {f : X ⟶ Y} (hf : IsUnramified B S hS f) :
    IsLocallyOfFiniteType B S hS f

Tag 05W0, a lemma

Tag 05W0 in the Stacks Project.

AlgebraicGeometry.Space.isQuasiFiniteAt_of_isUnramifiedAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 295. The attribute's comment: “pointwise statement”.

Stacks 05W0, the pointwise statement: a morphism of algebraic spaces over S which is unramified at a point of its source is quasi-finite at that point.

The open subspace witnessing unramifiedness at the point witnesses quasi-finiteness there, by the global statement applied to the restriction of the morphism.

theorem isQuasiFiniteAt_of_isUnramifiedAt {f : X ⟶ Y} {x : points B S hS X}
    (hf : IsUnramifiedAt B S hS f x) : IsQuasiFiniteAt B S hS f x

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedQuasiFinite.lean, line 67. The attribute's comment: “global consequence”. References: EGA IV (17.4.3).

Stacks 05W0, the global consequence. An unramified morphism of algebraic spaces over S is locally quasi-finite: on every commuting square of étale scheme charts the induced scheme morphism is unramified, hence locally of finite type and locally quasi-finite.

theorem isLocallyQuasiFinite_of_isUnramified {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (h : IsUnramified B S hS f) :
    IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Space.isLocallyQuasiFinite_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedQuasiFinite.lean, line 67. The attribute's comment: “an unramified morphism is locally quasi-finite”. References: EGA IV (17.4.3).

Stacks 05W0, the global consequence. An unramified morphism of algebraic spaces over S is locally quasi-finite: on every commuting square of étale scheme charts the induced scheme morphism is unramified, hence locally of finite type and locally quasi-finite.

theorem isLocallyQuasiFinite_of_isUnramified {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (h : IsUnramified B S hS f) :
    IsLocallyQuasiFinite B S hS f

Tag 06CQ, a lemma

Tag 06CQ in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 232.

Stacks 06CQ. An immersion of algebraic spaces over S is unramified.

An immersion is representable, so an atlas b of the target pulls back to a surjective étale chart a of the source over an immersion α of schemes; α is unramified, and that one surjective étale square suffices by [Stacks Project, Tag 03MJ].

theorem isUnramified_of_isImmersion (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y} (hf : IsImmersion B S hS f) :
    IsUnramified B S hS f

Tag 05W1, a lemma

Tag 05W1 in the Stacks Project.

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

Stacks 05W1, part (2). A morphism of algebraic spaces over S which is locally of finite type and whose relative diagonal is an open immersion is unramified.

On a commuting square of surjective étale charts the relative diagonal of the morphism α of the site sits over the relative diagonal of f, which is étale after every represented base change because it is an open immersion after every such base change. Both legs of that square are therefore étale, so the relative diagonal of α is étale by [Stacks Project, Tag 03FV]; it is also a split monomorphism, hence universally injective, so it is an open immersion by [Stacks Project, Tag 02LC]. Now α is unramified by [Stacks Project, Tag 02GE], and one surjective étale square suffices by [Stacks Project, Tag 03MJ].

theorem isUnramified_of_isOpenImmersion_pullbackDiagonal (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hft : IsLocallyOfFiniteType B S hS f)
    (hdiag : IsOpenImmersion B S hS (pullback.diagonal f)) :
    IsUnramified B S hS f

AlgebraicGeometry.Space.isOpenImmersion_diagonal_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedDiagonal.lean, line 487. The attribute's comment: “part (1)”. References: EGA IV (17.4.2), “a) ⇒ b)”; SGA 1 I (3.4), “diagonal case (g = id)”; SGA 3 XI (1.3), “more general”.

Stacks 05W1, part (1). The relative diagonal of an unramified morphism of algebraic spaces over S is an open immersion.

Each represented base change of the relative diagonal is a monomorphism of schemes, because the relative diagonal is a base change of the absolute diagonal of the source (AlgebraicGeometry.isPullback_pullbackDiagonal_diag) and the absolute diagonal of an algebraic space is a monomorphism after every represented base change (AlgebraicGeometry.Space.monomorphisms_diag_of_representable, part (2) of [Stacks Project, Tag 02X4]). It is moreover étale, which is AlgebraicGeometry.Space.presheaf_etale_diagonal_of_isUnramified. A morphism of schemes which is étale and universally injective — in particular one which is étale and a monomorphism — is an open immersion by [Stacks Project, Tag 025G].

theorem isOpenImmersion_diagonal_of_isUnramified
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsUnramified B S hS f) :
    IsOpenImmersion B S hS (pullback.diagonal f)

AlgebraicGeometry.Space.isUnramified_of_isOpenImmersion_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedDiagonal.lean, line 524. The attribute's comment: “part (2)”. References: EGA IV (17.4.2), “b) ⇒ a)”; SGA 3 XI (1.3), “more general”.

Stacks 05W1, part (2). A morphism of algebraic spaces over S which is locally of finite type and whose relative diagonal is an open immersion is unramified.

Let a : h_U ⟶ X, b : h_V ⟶ Y be étale charts over h : U ⟶ V, and let p : h_U ⟶ X ×_Y h_V be the induced morphism. The morphism p is representable, because p composed with the base change X ×_Y h_V ⟶ X of b is the representable a and representability cancels (CategoryTheory.Functor.relativelyRepresentable.hasOfPostcompProperty, [Stacks Project, Tag 05L9]). Its kernel pair R is, by CategoryTheory.Limits.isPullback_kernelPair_diagonal, a base change of the relative diagonal of f, so R ⟶ U ×_V U is an open immersion by hypothesis.

The relative diagonal U ⟶ U ×_V U factors through R by a section σ of its first projection, and it remains to see that σ is an open immersion. The relative diagonal d : U ⟶ R_a of p over the kernel pair R_a of a is one: it is a section of the étale first projection of R_a, hence étale by AlgebraicGeometry.Etale.of_comp, and a split monomorphism, hence an open immersion by [Stacks Project, Tag 025G]. The comparison e : R ⟶ R_a is a monomorphism because the two projections of R are jointly monic, and σ is the base change of d along e — the square 𝟙, σ, d, e is cartesian because e is a monomorphism. Composing the two open immersions and transporting along the comparison of the fibre product of h with itself in the site and in schemes gives that the diagonal of the scheme morphism is an open immersion, and part (2) of [Stacks Project, Tag 02GE] concludes.

theorem isUnramified_of_isOpenImmersion_diagonal (f : X ⟶ Y)
    (hft : IsLocallyOfFiniteType B S hS f)
    (hoi : IsOpenImmersion B S hS (pullback.diagonal f)) :
    IsUnramified B S hS f

Tag 05W2, a lemma

Tag 05W2 in the Stacks Project.

AlgebraicGeometry.Space.unramifiedLocus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 644. The attribute's comment: “part (1): the open unramified locus”.

Stacks 05W2, part (1). The open subspace of the source of a morphism of algebraic spaces over S cut out by the points at which the morphism is unramified.

Openness of that set of points is AlgebraicGeometry.Space.isOpen_setOf_isUnramifiedAt, and the open subspace realizing it is produced by the correspondence of part (1) of [Stacks Project, Tag 03BZ] between the open subspaces of an algebraic space and the open subsets of its point space. No finiteness hypothesis is needed, because unramifiedness at a point is stated as the existence of an open subspace on which the morphism is unramified; the source's local-finite-type assumption is only used for its part (2).

noncomputable def unramifiedLocus (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    {U : Subfunctor X // IsOpenSubspace B S hS U}

AlgebraicGeometry.Space.range_pointsMap_unramifiedLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 652. The attribute's comment: “part (1): the points of the open unramified locus”.

Stacks 05W2, part (1). The points of AlgebraicGeometry.Space.unramifiedLocus are exactly the points at which the morphism is unramified.

theorem range_pointsMap_unramifiedLocus (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    Set.range (pointsMap B S hS (unramifiedLocus B S hS hX f).1.toFunctor
        (unramifiedLocus B S hS hX f).1.ι) =
      {x : points B S hS X | IsUnramifiedAt B S hS f x}

AlgebraicGeometry.Space.isUnramifiedAt_iff_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UnramifiedLocusOnBase.lean, line 212. The attribute's comment: “part (2): base-change invariance of the unramified locus, pointwise”.

Part (2) of Stacks 05W2, read at a point. In a cartesian square of algebraic spaces over S whose right vertical arrow f is locally of finite type, the base change f' is unramified at a point x' of its source exactly when f is unramified at the image of x'; that is, forming the unramified locus commutes with base change.

Read on the compatible pointed charts of AlgebraicGeometry.Space.exists_etaleChartAtPoint_pair_of_isPullback, each side is unramifiedness of a morphism of schemes at corresponding points of a cartesian square of schemes whose right vertical arrow is locally of finite type.

The source assumes all four corners of the square algebraic; only the three producing the charts and the source of the base change are needed, the latter merely to read unramifiedness at a point of it off a single chart.

theorem isUnramifiedAt_iff_of_isPullback {X' X Y' Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    (hX' : IsAlgebraicSpace B S hS X') (hX : IsAlgebraicSpace B S hS X)
    (hY' : IsAlgebraicSpace B S hS Y') (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsLocallyOfFiniteType B S hS f) (x' : points B S hS X') :
    IsUnramifiedAt B S hS f (pointsMap B S hS X' g' x') ↔ IsUnramifiedAt B S hS f' x'

Tag 06G6, a lemma

Tag 06G6 in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Unramified.lean, line 203.

Stacks 06G6. If a composite of morphisms of algebraic spaces over S is unramified, then so is its first factor.

Lift a surjective étale atlas of Z through g and the resulting chart of Y through f, by [Stacks Project, Tag 02X1]. The scheme morphism on top of the outer square is unramified by hypothesis, hence so is its first factor by [Stacks Project, Tag 02GG]; that is one surjective étale square for f, which suffices by [Stacks Project, Tag 03MJ].

theorem isUnramified_of_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)
    (hfg : IsUnramified B S hS (f ≫ g)) : IsUnramified B S hS f

Sources

• Section 67.38, Tag 03ZG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsUnramified · AlgebraicGeometry.Space.IsGUnramified · AlgebraicGeometry.Space.IsUnramifiedAt · AlgebraicGeometry.Space.IsGUnramifiedAt · AlgebraicGeometry.Space.isGUnramified_iff_isUnramified_and_isLocallyOfFinitePresentation · AlgebraicGeometry.Space.isUnramified_comp · AlgebraicGeometry.Space.isUnramified_isStableUnderBaseChange · AlgebraicGeometry.Space.isUnramified_tfae

Section67.39 Étale morphisms#

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

Tag 04RH, a definition

Tag 04RH in the Stacks Project.

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

A morphism of algebraic spaces is étale at a point if it is étale on an open subspace containing that point.

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

Tag 03XT, a lemma

Tag 03XT in the Stacks Project.

AlgebraicGeometry.Space.isEtale_local_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocalTfae.lean, line 128.

Stacks 03XT. Nine equivalent criteria for a morphism f : X ⟶ Y of algebraic spaces over S to be étale: f is étale; f is étale at every point of |X|; the base change of f to every scheme is étale; the base change of f to every affine scheme is étale; the base change of f to one surjective étale scheme chart of Y is étale; the composite of f with one surjective étale scheme chart of X is étale; in every commuting square of étale scheme charts of f the morphism of schemes between the charts is étale; there is one such square with surjective chart of the source; and there are Zariski coverings Y = ⋃ Yᵢ and f⁻¹(Yᵢ) = ⋃ Xᵢⱼ with every Xᵢⱼ ⟶ Yᵢ étale.

theorem isEtale_local_tfae
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE [
      IsEtale B S hS f,
      ∀ x : points B S hS X, IsEtaleAt B S hS f x,
      ∀ (Z : BigFppfOver B S hS) (g : yoneda.obj Z ⟶ Y),
        IsEtale 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) →
          IsEtale B S hS (pullback.snd f g),
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        IsSurjective B S hS g ∧ IsEtale B S hS g ∧ IsEtale B S hS (pullback.snd f g),
      ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ X),
        IsSurjective B S hS p ∧ IsEtale B S hS p ∧ IsEtale 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 →
          AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).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 ∧
            AlgebraicGeometry.Etale ((BigFppfOver.toScheme B S hS).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, IsEtale B S hS ((Xopen i j).ι ≫ pullback.snd f (Yopen i).ι)
    ]

Tag 0465, a lemma

Tag 0465 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 75. The attribute's comment: “the composition of two etale morphisms of algebraic spaces is etale”.

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

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

Tag 0466, a lemma

Tag 0466 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 254. The attribute's comment: “the base change of an étale morphism of algebraic spaces is étale”. References: SGA 1 IX (1.3).

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

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

Tag 03XU, a lemma

Tag 03XU in the Stacks Project.

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

Stacks 03XU. An étale morphism of algebraic spaces over S is locally quasi-finite: an étale morphism of schemes is locally of finite type and locally quasi-finite (Stacks 03II).

Only the target has to be an algebraic space, where the source requires both.

theorem isLocallyQuasiFinite_of_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hY : IsAlgebraicSpace B S hS Y)
    {f : X ⟶ Y} (hf : IsEtale B S hS f) :
    IsLocallyQuasiFinite B S hS f

Tag 04XX, a lemma

Tag 04XX in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtlas.lean, line 124.

Stacks 04XX. An étale morphism of algebraic spaces over S is smooth: an étale morphism of schemes is smooth.

theorem isSmooth_of_isEtale
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hG : IsAlgebraicSpace B S hS G)
    {f : F ⟶ G} (hf : IsEtale B S hS f) :
    IsSmooth B S hS f

Tag 0467, a lemma

Tag 0467 in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtlas.lean, line 139.

Stacks 0467. An étale morphism of algebraic spaces over S is flat: in every commuting square of étale charts the chart morphism of schemes is étale, by cancellation (AlgebraicGeometry.Space.etale_of_comp_etale_chart), and an étale morphism of schemes is flat.

Nothing is asked of the target.

theorem isFlat_of_isEtale {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : F ⟶ G}
    (hf : IsEtale B S hS f) : IsFlat B S hS f

Tag 0468, a lemma

Tag 0468 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothAtlas.lean, line 152.

Stacks 0468. An étale morphism of algebraic spaces over S is locally of finite presentation: the chart morphism of schemes in every commuting square of étale charts is étale, hence locally of finite presentation.

Nothing is asked of the target.

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

Tag 06LT, a lemma

Tag 06LT in the Stacks Project.

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

An étale morphism of presheaves on the big fppf site of S is locally of finite type; neither the source nor the target has to be an algebraic space.

theorem isLocallyOfFiniteType_of_isEtale' (f : F ⟶ G) (hf : IsEtale B S hS f) :
    IsLocallyOfFiniteType B S hS f

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

Stacks 06LT. An étale morphism of algebraic spaces over S is locally of finite type: an étale morphism of schemes is.

Only the target has to be an algebraic space, where the source requires both.

theorem isLocallyOfFiniteType_of_isEtale
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hY : IsAlgebraicSpace B S hS Y)
    {f : X ⟶ Y} (hf : IsEtale B S hS f) :
    IsLocallyOfFiniteType B S hS f

Tag 06CR, a lemma

Tag 06CR in the Stacks Project.

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

Stacks 06CR. An étale morphism of algebraic spaces over S is unramified.

In a commuting square of étale charts of f the morphism of schemes on top is étale, hence formally unramified and locally of finite type, hence unramified by [Stacks Project, Tag 02HE]. Nothing is asked of the target.

theorem isUnramified_of_isEtale {f : X ⟶ Y} (hf : IsEtale B S hS f) :
    IsUnramified B S hS f

Tag 05W3, a lemma

Tag 05W3 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_of_isEtale_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleMorphisms.lean, line 378. The attribute's comment: “a morphism over Z between algebraic spaces étale over Z is étale”.

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

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

Tag 06LU, a lemma

Tag 06LU in the Stacks Project.

AlgebraicGeometry.Space.isEtale_of_isFlat_of_isUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Etale.lean, line 106.

Stacks 06LU. A morphism of algebraic spaces over S which is locally of finite presentation, flat and unramified is étale.

Lift an atlas q of the target through f by [Stacks Project, Tag 02X1] to a surjective étale chart p of the source over a morphism α of the site. The three hypotheses, read on that one square, say that the scheme morphism underlying α is locally of finite presentation, flat and unramified, hence formally unramified by [Stacks Project, Tag 02HE] and therefore étale. One such square suffices by condition (4) of [Stacks Project, Tag 03FS].

theorem isEtale_of_isFlat_of_isUnramified (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hlfp : IsLocallyOfFinitePresentation B S hS f) (hflat : IsFlat B S hS f)
    (hunr : IsUnramified B S hS f) :
    IsEtale B S hS f

Sources

• Section 67.39, Tag 03XS
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsEtaleAt · AlgebraicGeometry.Space.isEtale_local_tfae · AlgebraicGeometry.Space.isEtale_comp · AlgebraicGeometry.Space.isEtale_of_isPullback · AlgebraicGeometry.Space.isLocallyQuasiFinite_of_isEtale · AlgebraicGeometry.Space.isSmooth_of_isEtale · AlgebraicGeometry.Space.isFlat_of_isEtale · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isEtale

Section67.40 Proper morphisms#

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

Tag 03ZM, a definition

Tag 03ZM in the Stacks Project.

AlgebraicGeometry.Space.isProperULift_whiskerRight_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedProperTransfer.lean, line 134. The attribute's comment: “for a universe lift”.

Stacks 03ZM for a universe lift. The universe lift of a morphism of presheaves of Type u on the big fppf site of S is proper — separated, of finite type and universally closed — exactly when the morphism is.

Each conjunct transfers separately: separatedness by AlgebraicGeometry.Space.isSeparatedULift_whiskerRight_iff, being of finite type by AlgebraicGeometry.Space.isFiniteTypeULift_whiskerRight_iff and universal closedness by AlgebraicGeometry.Space.universallyClosedULift_whiskerRight_iff.

theorem isProperULift_whiskerRight_iff {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (q : F ⟶ G) :
    IsProperULift.{w} B S hS (Functor.whiskerRight q uliftFunctor.{w}) ↔
      IsProper B S hS q

AlgebraicGeometry.Space.IsProper, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosed.lean, line 132.

A morphism of algebraic spaces over S is proper when it is separated, of finite type and universally closed.

abbrev IsProper (f : F ⟶ G) : Prop

Tag 083R, a lemma

Tag 083R in the Stacks Project.

AlgebraicGeometry.Space.isProper_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ProperCriteria.lean, line 162.

Stacks 083R. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is proper; the base change of f along every morphism to Y from a presheaf represented by an object of the site is proper; the same for the objects with affine underlying scheme; the base change of f along some surjective étale morphism to Y from a represented presheaf is proper; and there is a Zariski covering of Y along each member of which the base change of f is proper.

theorem isProper_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [IsProper B S hS f,
        ∀ (W : BigFppfOver B S hS) (g : yoneda.obj W ⟶ Y),
          IsProper 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) →
            IsProper 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 ∧
            IsProper B S hS (pullback.fst g f),
        ∃ (I : Type u) (U : I → Subfunctor Y) (_ : IsZariskiCover B S hS I U),
          ∀ i, IsProper B S hS (pullback.fst (U i).ι f)]

Tag 04WP, a lemma

Tag 04WP in the Stacks Project.

AlgebraicGeometry.Space.isProper_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperBaseChange.lean, line 164.

Properness of morphisms of algebraic spaces over S is stable under base change.

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

Tag 04XY, a lemma

Tag 04XY in the Stacks Project.

AlgebraicGeometry.Space.isProper_comp', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperPermanence.lean, line 81.

Stacks 04XY. The composite of two proper morphisms of algebraic spaces over S is proper: each of the three conjuncts of properness is stable under composition.

Algebraicity of the source is not needed and is not assumed, which is what distinguishes this from AlgebraicGeometry.Space.isProper_comp. None of the three conjuncts asks for it: separatedness is a condition on a relative diagonal, and the quantifiers of AlgebraicGeometry.Space.IsQuasiCompact and AlgebraicGeometry.Space.UniversallyClosed reach only the intermediate and final spaces.

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

Tag 04XZ, a lemma

Tag 04XZ in the Stacks Project.

AlgebraicGeometry.Space.isProper_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperClosedImmersion.lean, line 202.

Stacks 04XZ. A closed immersion of algebraic spaces over S is proper.

theorem isProper_of_isClosedImmersion
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsClosedImmersion B S hS f) :
    IsProper B S hS f

Tag 04NX, a lemma

Tag 04NX in the Stacks Project.

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

Stacks 04NX, part (2). If a composite of morphisms of algebraic spaces over S is proper and its second factor is separated, then its first factor is proper.

Properness is separatedness, finite type and universal closedness (Stacks 03ZM). The first cancels by Stacks 03KR and the universal closedness by part (1) of Stacks 04NX; finite type is local finite type, which cancels by Stacks 0462, together with quasi-compactness, which cancels by Stacks 03KS against a quasi-separated second factor — and the second factor is quasi-separated, being separated (Stacks 03KK).

theorem isProper_of_comp_of_isSeparated {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)
    (hfg : IsProper B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    IsProper B S hS f

AlgebraicGeometry.Space.universallyClosed_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosedPermanence.lean, line 67. The attribute's comment: “part (1): universal closedness”. References: EGA II (5.4.9), “5.4.3 univ. closed”.

Stacks 04NX, part (1). Let X ⟶ Y ⟶ Z be morphisms of algebraic spaces over S. If the composite X ⟶ Z is universally closed and Y ⟶ Z is separated, then X ⟶ Y is universally closed.

theorem universallyClosed_of_comp_of_isSeparated {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)
    (hfg : UniversallyClosed B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Space.isClosed_range_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosedPermanence.lean, line 91. The attribute's comment: “part (1): closed image”.

Stacks 04NX, part (1). Under the hypotheses of AlgebraicGeometry.Space.universallyClosed_of_comp_of_isSeparated, the image of |X| in |Y| is closed.

theorem isClosed_range_of_comp_of_isSeparated {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)
    (hfg : UniversallyClosed B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    _root_.IsClosed (Set.range (pointsMap B S hS X f))

Tag 08AJ, a lemma

Tag 08AJ in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_of_isSurjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Proper.lean, line 120. The attribute's comment: “universally closed image”.

Stacks 08AJ, universally closed image. Let X ⟶ Y ⟶ T be morphisms of algebraic spaces over S. If X is universally closed over T and X ⟶ Y is surjective, then Y is universally closed over T.

theorem universallyClosed_of_isSurjective_comp
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hT : IsAlgebraicSpace B S hS T) (f : X ⟶ Y) (q : Y ⟶ T)
    (hfq : UniversallyClosed B S hS (f ≫ q)) (hf : IsSurjective B S hS f) :
    UniversallyClosed B S hS q

AlgebraicGeometry.Space.isProper_of_isSurjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Proper.lean, line 160. The attribute's comment: “properness of the image”.

Stacks 08AJ, properness of the image. Let X ⟶ Y ⟶ T be morphisms of algebraic spaces over S. If X is universally closed over T, the morphism X ⟶ Y is surjective and Y is separated and of finite type over T, then Y is proper over T.

theorem isProper_of_isSurjective_comp
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hT : IsAlgebraicSpace B S hS T) (f : X ⟶ Y) (q : Y ⟶ T)
    (hfq : UniversallyClosed B S hS (f ≫ q)) (hf : IsSurjective B S hS f)
    (hsep : IsSeparated B S hS q) (hft : IsFiniteType B S hS q) :
    IsProper B S hS q

AlgebraicGeometry.Space.universallyClosed_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosedImage.lean, line 105. The attribute's comment: “first assertion: universal closedness”.

Stacks 08AJ, first assertion. Let p : X ⟶ Z and q : Y ⟶ Z be morphisms of algebraic spaces over S and let f : X ⟶ Y be a morphism over Z. If p is universally closed and f is surjective, then q is universally closed.

A base change T ×_Z Y ⟶ T of q is, after the pasting isomorphism (T ×_Z Y) ×_Y X ≅ T ×_Z X, preceded by the base change of f, which is surjective on points by Stacks 03MH; the composite is the base change T ×_Z X ⟶ T of p, closed by hypothesis.

theorem universallyClosed_of_isSurjective {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) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : f ≫ q = p) (hf : IsSurjective B S hS f)
    (hp : UniversallyClosed B S hS p) :
    UniversallyClosed B S hS q

AlgebraicGeometry.Space.isProper_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosedImage.lean, line 124. The attribute's comment: “second assertion: properness”.

Stacks 08AJ, second assertion. In the situation of AlgebraicGeometry.Space.universallyClosed_of_isSurjective, if moreover q is separated and of finite type, then q is proper.

theorem isProper_of_isSurjective {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) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : f ≫ q = p) (hf : IsSurjective B S hS f)
    (hp : UniversallyClosed B S hS p)
    (hsep : IsSeparated B S hS q) (hft : IsFiniteType B S hS q) :
    IsProper B S hS q

Tag 0AGD, a lemma

Tag 0AGD in the Stacks Project.

AlgebraicGeometry.Space.isSurjective_toSchemeTheoreticImage_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ProperSchemeTheoreticImage.lean, line 106. The attribute's comment: “second assertion: surjectivity onto the scheme-theoretic image”.

Stacks 0AGD, second assertion. Let h : X ⟶ Y, f : X ⟶ T and g : Y ⟶ T be morphisms of algebraic spaces over S with h ≫ g = f. If f is proper and g is separated, then the morphism from X to the scheme-theoretic image of h is surjective.

The image of |X| in |Z| is dense, by part (4) of Stacks 082Z, h being quasi-compact by Stacks 03KS; and it is closed, being the preimage along the continuous injection |Z| → |Y| of the image of |X| in |Y|, which is closed by part (1) of Stacks 04NX.

theorem isSurjective_toSchemeTheoreticImage_of_isProper
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hT : IsAlgebraicSpace B S hS T) (h : X ⟶ Y) (f : X ⟶ T) (g : Y ⟶ T)
    (hcomm : h ≫ g = f) (hf : IsProper B S hS f) (hg : IsSeparated B S hS g) :
    IsSurjective B S hS (toSchemeTheoreticImage B S hS h)

AlgebraicGeometry.Space.isProper_schemeTheoreticImageSubfunctor_inclusion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ProperSchemeTheoreticImage.lean, line 149. The attribute's comment: “first assertion: the scheme-theoretic image is proper over the base”.

Stacks 0AGD, first assertion. Let h : X ⟶ Y, f : X ⟶ T and g : Y ⟶ T be morphisms of algebraic spaces over S with h ≫ g = f. If f is proper and g is separated and locally of finite type, then the scheme-theoretic image of h is proper over T.

The scheme-theoretic image is a closed subspace of Y (Stacks 082X), so its structure morphism over T is separated by Stacks 04CH and Stacks 03KQ, and locally of finite type by Stacks 03XG; it is quasi-compact by part (2) of Stacks 040W, X ⟶ T being quasi-compact and X surjecting onto the image by AlgebraicGeometry.Space.isSurjective_toSchemeTheoreticImage_of_isProper. Properness is then the second assertion of Stacks 08AJ, f being universally closed.

theorem isProper_schemeTheoreticImageSubfunctor_inclusion_comp
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hT : IsAlgebraicSpace B S hS T) (h : X ⟶ Y) (f : X ⟶ T) (g : Y ⟶ T)
    (hcomm : h ≫ g = f) (hf : IsProper B S hS f) (hg : IsSeparated B S hS g)
    (hgft : IsLocallyOfFiniteType B S hS g) :
    IsProper B S hS ((schemeTheoreticImageSubfunctor B S hS h).ι ≫ g)

Tag 04Y0, a lemma

Tag 04Y0 in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_tfae_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DiagonalProperTFAE.lean, line 49.

For a morphism of algebraic spaces over S the following are equivalent: it is separated; its relative diagonal is universally closed; its relative diagonal is proper.

theorem isSeparated_tfae_diagonal (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) :
    List.TFAE [IsSeparated B S hS f,
      UniversallyClosed B S hS (pullback.diagonal f),
      IsProper B S hS (pullback.diagonal f)]

Sources

• Section 67.40, Tag 03ZL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isProperULift_whiskerRight_iff · AlgebraicGeometry.Space.IsProper · AlgebraicGeometry.Space.isProper_tfae · AlgebraicGeometry.Space.isProper_isStableUnderBaseChange · AlgebraicGeometry.Space.isProper_comp' · AlgebraicGeometry.Space.isProper_of_isClosedImmersion · AlgebraicGeometry.Space.isProper_of_comp_of_isSeparated · AlgebraicGeometry.Space.universallyClosed_of_comp_of_isSeparated

Section67.41 Valuative criteria#

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

Tag 03IX, a definition

Tag 03IX in the Stacks Project.

AlgebraicGeometry.Space.ValuativeCriterion.Uniqueness, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Criterion.lean, line 173. The attribute's comment: “uniqueness”.

There is at most one extension of a compatible generic point to any valuation ring.

public def Uniqueness (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.ValuativeCriterion.Existence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Criterion.lean, line 178. The attribute's comment: “existence”.

A compatible generic point extends after a field extension and passage to a dominating valuation ring.

public def Existence (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.ValuativeCriterion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Criterion.lean, line 192. The attribute's comment: “both parts”.

A morphism satisfies both parts of the valuative criterion.

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

Tag 03K8, a lemma

Tag 03K8 in the Stacks Project.

AlgebraicGeometry.Space.valuativeCriterion_existence_iff_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Representable.lean, line 255.

For a representable morphism, a lift after a dominating extension exists exactly when every valuative square has a lift before extension.

public theorem valuativeCriterion_existence_iff_lift
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) (hf : yoneda.relativelyRepresentable f) :
    ValuativeCriterion.Existence f ↔
      (∀ q : ValuativeSquare f, Nonempty q.Lift)

Tag 03KH, a lemma

Tag 03KH in the Stacks Project.

AlgebraicGeometry.Space.valuativeCriterion_existence_iff_finiteSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/FiniteSeparable.lean, line 614.

Allowing arbitrary field extensions in the existence valuative criterion is equivalent to allowing only finite separable ones.

public theorem valuativeCriterion_existence_iff_finiteSeparable
    (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) :
    ValuativeCriterion.Existence f ↔ ExistenceFiniteSeparable f

Tag 0ARH, a lemma

Tag 0ARH in the Stacks Project.

AlgebraicGeometry.Space.exists_lift_of_dominatingExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/PushDownSolution.lean, line 319.

A lift of a dominating extension of a valuative square for a separated morphism of algebraic spaces descends to a lift of the square itself. The extension K'/K of fraction fields is arbitrary: no finiteness or separability condition is imposed on it.

The descent step needs the sheaf condition for the single faithfully flat covering Spec A' ⟶ Spec A; it is supplied by the fpqc sheaf condition AlgebraicGeometry.IsAlgebraicSpace.isSheaf_fpqc for X, which is Stacks 0APL.

public theorem exists_lift_of_dominatingExtension
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y)
    (hf : AlgebraicGeometry.Space.IsSeparated B S hS f)
    (q : ValuativeSquare f) (e : q.DominatingExtension)
    (he : Nonempty e.square.Lift) :
    Nonempty q.Lift

Tag 0A3W, a lemma

Tag 0A3W in the Stacks Project.

AlgebraicGeometry.Space.valuativeCriterion_existence_iff_lift_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/PushDownSolution.lean, line 761.

For a separated morphism of algebraic spaces, allowing a dominating extension of the valuation ring does not change the existence half of the valuative criterion: the criterion holds exactly when every valuative square already has a lift over the original valuation ring.

public theorem valuativeCriterion_existence_iff_lift_of_isSeparated
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y)
    (hf : AlgebraicGeometry.Space.IsSeparated B S hS f) :
    ValuativeCriterion.Existence f ↔ ∀ q : ValuativeSquare f, Nonempty q.Lift

Tag 03KI, an example

Tag 03KI in the Stacks Project.

AlgebraicGeometry.TwistedDoubledOrigin.universallyClosed_surjective_specMap_algebraMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 124. The attribute's comment: “Spec(k') → Spec(k) is universally closed and surjective”.

Stacks 03KI, the morphism Spec k' ⟶ Spec k. For a finite extension k'/k of fields, the morphism Spec k' ⟶ Spec k is universally closed, being finite, and surjective, its target being a single point.

theorem universallyClosed_surjective_specMap_algebraMap [FiniteDimensional k K] :
    UniversallyClosed (Spec.map (CommRingCat.ofHom (algebraMap k K))) ∧
      Surjective (Spec.map (CommRingCat.ofHom (algebraMap k K)))

AlgebraicGeometry.TwistedDoubledOrigin.isQuasiCompact_quotientBaseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 218. The attribute's comment: “π is quasi-compact”.

Stacks 03KI, the quasi-compactness clause. The structure morphism π : X ⟶ S = 𝔸¹_k of the Galois twist of the affine line with zero doubled is quasi-compact.

The quotient is a quasi-compact algebraic space, its chart being the affine line over k', and the base is quasi-separated, being affine; so part (1) of Stacks 073B applies.

theorem isQuasiCompact_quotientBaseMap :
    Space.IsQuasiCompact B (base k) hS (quotientBaseMap k K hdegree σ hσ B hS)

AlgebraicGeometry.TwistedDoubledOrigin.universallyClosed_quotientBaseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 289. The attribute's comment: “π is universally closed”.

Stacks 03KI, the universal closedness clause. The structure morphism π : X ⟶ S = 𝔸¹_k of the Galois twist of the affine line with zero doubled is universally closed.

The chart U = Spec k'[x] ⟶ X is surjective and U ⟶ S is universally closed, being finite, so Stacks 08AJ pushes universal closedness down to π.

theorem universallyClosed_quotientBaseMap :
    Space.UniversallyClosed B (base k) hS (quotientBaseMap k K hdegree σ hσ B hS)

AlgebraicGeometry.TwistedDoubledOrigin.universallyClosed_doubledProjOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 314. The attribute's comment: “the affine line with zero doubled is universally closed over the affine line”.

Stacks 03KI, the affine line with zero doubled. The affine line over k' with zero doubled is universally closed over the affine line over k'.

The two copies of the affine line cover it, and their union maps to the affine line by the codiagonal, which is finite; so Mathlib's descent of universal closedness along a surjection applies.

theorem universallyClosed_doubledProjOver : UniversallyClosed (doubledProjOver k K).left

AlgebraicGeometry.TwistedDoubledOrigin.exists_isIso_baseChangePresheaf_comp_doubledProjOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 346. The attribute's comment: “after base change by Spec(k') → Spec(k), π is the affine line with zero doubled over the affine line”.

Stacks 03KI, the base change to k'. After base change along U = S ×_{Spec k} Spec k' = 𝔸¹_{k'} ⟶ S, the structure morphism π is identified with the morphism from the affine line over k' with zero doubled to the affine line over k': the base change U ×_S X is isomorphic to the functor of points of the glued scheme, compatibly with the projections to U.

The isomorphism is the one of part (6) of Stacks 03FN; both it and the projections are determined on the self-product U ×_S U, where both projections are the first one.

theorem exists_isIso_baseChangePresheaf_comp_doubledProjOver :
    ∃ χ : baseChangePresheaf k K B hS hdegree σ hσ ⟶
        (pointsFunctor k B hS).obj (doubledOverBase k K),
      IsIso χ ∧ χ ≫ (pointsFunctor k B hS).map (doubledProjOver k K) =
        pullback.fst (pointsCoverToBase k K B hS) (quotientBaseMap k K hdegree σ hσ B hS)

AlgebraicGeometry.TwistedDoubledOrigin.exists_mono_isPullback_zeroFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 443. The attribute's comment: “the point of X above 0 corresponds to a monomorphism Spec(k') → X”.

Stacks 03KI, the point above the origin. The point of X above 0 ∈ 𝔸¹_k is a monomorphism Spec k' ⟶ X: there is a monomorphism from the functor of points of Spec k' into X whose square over the origin Spec k ⟶ 𝔸¹_k is Cartesian, so Spec k' is the whole fibre of π over the origin.

The fibre is computed in AlgebraicGeometry.TwistedDoubledOrigin.twistedRelationQuotient_zeroFibre; its map to X is a monomorphism because the origin is a monomorphism into the base.

theorem exists_mono_isPullback_zeroFibre :
    ∃ m : (pointsFunctor k B hS).obj (zeroCoverOverBase k K) ⟶
        (quadraticGaloisTwistedDoubledOrigin k K hdegree σ hσ B hS).obj,
      Mono m ∧ IsPullback m ((pointsFunctor k B hS).map (zeroCoverToZeroBase k K))
        (quotientBaseMap k K hdegree σ hσ B hS)
        ((pointsFunctor k B hS).map (zeroBaseToBase k))

AlgebraicGeometry.TwistedDoubledOrigin.formalDiskValuativeSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 538. The attribute's comment: “the solid square of the displayed diagram, over the valuation ring k⟦x⟧”.

Stacks 03KI, the solid square. The square displayed in the example: its valuation ring is the ring k⟦x⟧ of formal power series, its fraction field the field k((x)) of Laurent series, its structure morphism over the base the coordinate map Spec k⟦x⟧ ⟶ 𝔸¹_k of AlgebraicGeometry.TwistedDoubledOrigin.formalDiskBaseMap, and its top edge the point Spec k((x)) ⟶ X of AlgebraicGeometry.TwistedDoubledOrigin.laurentGenericPoint.

Only the top edge carries content: the target of π is the terminal presheaf, so the edge of the square into it, and the commutativity of the square, are the only ones there are.

def formalDiskValuativeSquare :
    Space.ValuativeSquare (quotientBaseMap k K hdegree σ hσ B hS)

AlgebraicGeometry.TwistedDoubledOrigin.isEmpty_lift_formalDiskValuativeSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 555. The attribute's comment: “there cannot exist a dotted arrow”.

Stacks 03KI, the missing dotted arrow. The square of the example has no dotted arrow: a dotted arrow is in particular a point of the quotient over the formal disc, and there is none, the point of X above the origin being Spec k', which has no k-point.

theorem isEmpty_lift_formalDiskValuativeSquare :
    IsEmpty (formalDiskValuativeSquare k K B hS hdegree σ hσ).Lift

AlgebraicGeometry.TwistedDoubledOrigin.existenceFiniteSeparable_and_not_forall_nonempty_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 568. The attribute's comment: “a finite separable field extension is needed in general”.

Stacks 03KI, a finite separable extension is needed. The structure morphism π satisfies the existence part of the valuative criterion when the fraction field may be replaced by a finite separable extension, but not when it may not be extended at all.

The first half is Stacks 0A3X, part (1), for the quasi-separated (Stacks 03FN, part (5)) and universally closed morphism π, refined by Stacks 03KH; the second is the square of the example over k⟦x⟧.

theorem existenceFiniteSeparable_and_not_forall_nonempty_lift :
    Space.ExistenceFiniteSeparable (quotientBaseMap k K hdegree σ hσ B hS) ∧
      ¬ ∀ q : Space.ValuativeSquare (quotientBaseMap k K hdegree σ hσ B hS), Nonempty q.Lift

AlgebraicGeometry.TwistedDoubledOrigin.quotientBaseMap_example, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginUniversallyClosed.lean, line 599. The attribute's comment: “all the assertions of the example together”.

Stacks 03KI. Let k'/k be a degree two Galois extension and let X be the Galois twist of the affine line with zero doubled, the algebraic space of Stacks 03FN over S = 𝔸¹_k, with structure morphism π : X ⟶ S. Then:

• π is quasi-compact and universally closed;
• after base change along 𝔸¹_{k'} = S ×_{Spec k} Spec k' ⟶ S, π is identified with the affine line over k' with zero doubled over the affine line over k', which is universally closed;
• Spec k' ⟶ Spec k is universally closed and surjective;
• the point of X above the origin is a monomorphism Spec k' ⟶ X, the whole fibre of π there;
• the formal disc Spec k⟦x⟧ over S carries no point of X, so the square of the example (AlgebraicGeometry.TwistedDoubledOrigin.formalDiskValuativeSquare) has no dotted arrow;
• π satisfies the existence part of the valuative criterion with finite separable extensions of the fraction field, but not without extending it.

theorem quotientBaseMap_example :
    Space.IsQuasiCompact B (base k) hS (quotientBaseMap k K hdegree σ hσ B hS) ∧
      Space.UniversallyClosed B (base k) hS (quotientBaseMap k K hdegree σ hσ B hS) ∧
      (∃ χ : baseChangePresheaf k K B hS hdegree σ hσ ⟶
          (pointsFunctor k B hS).obj (doubledOverBase k K),
        IsIso χ ∧ χ ≫ (pointsFunctor k B hS).map (doubledProjOver k K) =
          pullback.fst (pointsCoverToBase k K B hS) (quotientBaseMap k K hdegree σ hσ B hS)) ∧
      UniversallyClosed (doubledProjOver k K).left ∧
      (UniversallyClosed (Spec.map (CommRingCat.ofHom (algebraMap k K))) ∧
        Surjective (Spec.map (CommRingCat.ofHom (algebraMap k K)))) ∧
      (∃ m : (pointsFunctor k B hS).obj (zeroCoverOverBase k K) ⟶
          (quadraticGaloisTwistedDoubledOrigin k K hdegree σ hσ B hS).obj,
        Mono m ∧ IsPullback m ((pointsFunctor k B hS).map (zeroCoverToZeroBase k K))
          (quotientBaseMap k K hdegree σ hσ B hS)
          ((pointsFunctor k B hS).map (zeroBaseToBase k))) ∧
      ¬ Nonempty
        (yoneda.obj (siteObject B (base k) hS (contains_powerSeries k B hS)
            (formalDiskBaseMap k)) ⟶
          (quadraticGaloisTwistedDoubledOrigin k K hdegree σ hσ B hS).obj) ∧
      IsEmpty (formalDiskValuativeSquare k K B hS hdegree σ hσ).Lift ∧
      Space.ExistenceFiniteSeparable (quotientBaseMap k K hdegree σ hσ B hS) ∧
      ¬ ∀ q : Space.ValuativeSquare (quotientBaseMap k K hdegree σ hσ B hS), Nonempty q.Lift

AlgebraicGeometry.TwistedDoubledOrigin.not_nonempty_hom_formalDisk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TwistedDoubledOriginValuativeLift.lean, line 129. The attribute's comment: “no_unextended_lift”.

Stacks 03KI, third assertion of the example. For a quadratic Galois extension K/k, the formal disc over k has no point of the quadratic Galois twisted doubled origin lying over AlgebraicGeometry.TwistedDoubledOrigin.formalDiskBaseMap.

So the solid valuative square over the valuation ring k⟦x⟧ whose bottom edge is that coordinate map admits no dotted arrow, and a fortiori none compatible with the generic point coming from the isomorphism of Stacks 03FN away from the origin: a finite separable extension of the fraction field is genuinely needed in the existence part of Stacks 03IX.

theorem not_nonempty_hom_formalDisk
    [FiniteDimensional k K] [IsGalois k K] (hdegree : Module.finrank k K = 2)
    (σ : K ≃ₐ[k] K) (hσ : σ ≠ 1) (B : BigFppfSite.{u}) (hS : B.Contains (base k))
    (hDisk : B.Contains (Spec (.of (PowerSeries k))))
    [HasSheafify (BigFppfOver.topology B (base k) hS) (Type u)] :
    ¬ Nonempty
      (yoneda.obj (siteObject B (base k) hS hDisk (formalDiskBaseMap k)) ⟶
        (quadraticGaloisTwistedDoubledOrigin k K hdegree σ hσ B hS).obj)

Tag 03IY, a lemma

Tag 03IY in the Stacks Project.

AlgebraicGeometry.Space.valuativeCriterion_uniqueness_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ValuativeCriteria.lean, line 219. The attribute's comment: “uniqueness part”.

Stacks 03IY, uniqueness part. The base change of a morphism of algebraic spaces satisfying the uniqueness part of the valuative criterion satisfies it again.

Two lifts of a valuative square for the base change b agree after composing with a, by uniqueness for p applied to the induced valuative square, and after composing with b, because both are lifts; so they agree.

theorem valuativeCriterion_uniqueness_of_isPullback
    {F G F' G' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {a : F ⟶ F'} {b : F ⟶ G} {p : F' ⟶ G'} {q : G ⟶ G'} (sq : IsPullback a b p q)
    (hp : ValuativeCriterion.Uniqueness p) : ValuativeCriterion.Uniqueness b

AlgebraicGeometry.Space.valuativeCriterion_existence_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ValuativeCriteria.lean, line 243. The attribute's comment: “existence part”.

Stacks 03IY, existence part. The base change of a morphism of algebraic spaces satisfying the existence part of the valuative criterion satisfies it again.

A valuative square for the base change b induces one for p; a dominating extension and a lift there, together with the bottom edge pushed along the extension, define a map into the fibre product by the universal property of the cartesian square, and that map is a lift of the dominating extension of the original square.

theorem valuativeCriterion_existence_of_isPullback
    {F G F' G' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {a : F ⟶ F'} {b : F ⟶ G} {p : F' ⟶ G'} {q : G ⟶ G'} (sq : IsPullback a b p q)
    (hp : ValuativeCriterion.Existence p) : ValuativeCriterion.Existence b

Tag 03IZ, a lemma

Tag 03IZ in the Stacks Project.

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

The existence part of the valuative criterion is preserved under composition.

public theorem valuativeCriterionExistence_comp
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ValuativeCriterion.Existence f)
    (hg : ValuativeCriterion.Existence g) :
    ValuativeCriterion.Existence (f ≫ g)

AlgebraicGeometry.Space.valuativeCriterion_uniqueness_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Composition.lean, line 130. The attribute's comment: “composition_valuative_uniqueness”.

Uniqueness of lifts in valuative squares is stable under composition.

public lemma valuativeCriterion_uniqueness_comp (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : ValuativeCriterion.Uniqueness f)
    (hg : ValuativeCriterion.Uniqueness g) :
    ValuativeCriterion.Uniqueness (f ≫ g)

Sources

• Section 67.41, Tag 03IW
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.ValuativeCriterion.Uniqueness · AlgebraicGeometry.Space.ValuativeCriterion.Existence · AlgebraicGeometry.Space.ValuativeCriterion · AlgebraicGeometry.Space.valuativeCriterion_existence_iff_lift · AlgebraicGeometry.Space.valuativeCriterion_existence_iff_finiteSeparable · AlgebraicGeometry.Space.exists_lift_of_dominatingExtension · AlgebraicGeometry.Space.valuativeCriterion_existence_iff_lift_of_isSeparated · AlgebraicGeometry.TwistedDoubledOrigin.universallyClosed_surjective_specMap_algebraMap

Section67.42 Valuative criterion for universal closedness#

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

Tag 03KA, a lemma

Tag 03KA in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_of_isQuasiCompact_of_valuativeCriterion_existence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ValuativeCriteria.lean, line 769.

Stacks 03KA. A quasi-compact morphism of algebraic spaces over S which satisfies the existence part of the valuative criterion is universally closed.

By Stacks 03IT it is enough to check that the base change along every morphism from a represented presheaf with affine scheme is closed on points; such a base change is again quasi-compact (Stacks 03HF) and again satisfies the existence part (Stacks 03IY), so isClosedMap_pointsMap_of_isAffine_target applies.

theorem universallyClosed_of_isQuasiCompact_of_valuativeCriterion_existence
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsQuasiCompact B S hS f) (hval : ValuativeCriterion.Existence f) :
    UniversallyClosed B S hS f

Tag 0A3X, a lemma

Tag 0A3X in the Stacks Project.

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

Stacks 0A3X, part (1). A quasi-separated universally closed morphism of algebraic spaces over S satisfies the existence part of the valuative criterion.

A valuative square for f presents the generic point of its valuation ring A as a point of the base change P = X ×_Y Spec A, through a section g : Spec K ⟶ P. Quasi-separatedness of P ⟶ Spec A makes g quasi-compact (Stacks 03KS), the morphism Spec K ⟶ Spec A being affine, so the points of the scheme-theoretic image Z ⊆ P of g are the closure of the image of g (Stacks 082Z). Universal closedness makes the image of that closed set in |Spec A| closed, and it contains the generic point, hence everything; so some point of |Z| lies over the closed point of Spec A. Stacks 089B realizes that point by a valuation ring A' with fraction field K' and a square Spec K' ⟶ Spec K, Spec A' ⟶ Z; composing with Z ⟶ P ⟶ X gives the lift, and A' dominates A because the closed point of Spec A' maps to the closed point of Spec A.

theorem valuativeCriterion_existence_of_isQuasiSeparated_of_universallyClosed
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) (huc : UniversallyClosed B S hS f) :
    ValuativeCriterion.Existence f

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

Stacks 0A3X, part (2). A quasi-compact quasi-separated morphism of algebraic spaces over S is universally closed exactly when it satisfies the existence part of the valuative criterion.

One direction is Stacks 03KA, the other is part (1).

theorem universallyClosed_iff_valuativeCriterion_existence_of_isQuasiCompact_of_isQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqc : IsQuasiCompact B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    UniversallyClosed B S hS f ↔ ValuativeCriterion.Existence f

Tag 0A3Y, a lemma

Tag 0A3Y in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_tfae_of_isQuasiCompact_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/UniversallyClosedValuative.lean, line 46.

For a quasi-compact separated morphism f : X ⟶ Y of algebraic spaces over S, universal closedness, the existence part of the valuative criterion of Stacks 03IX, and the existence of a lift in every valuative square for f over the valuation ring itself are equivalent.

public theorem universallyClosed_tfae_of_isQuasiCompact_of_isSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqc : IsQuasiCompact B S hS f) (hsep : IsSeparated B S hS f) :
    List.TFAE
      [UniversallyClosed B S hS f,
        ValuativeCriterion.Existence f,
        ∀ q : ValuativeSquare f, Nonempty q.Lift]

Tag 089F, a lemma

Tag 089F in the Stacks Project.

AlgebraicGeometry.Space.exists_valuationRing_extension_lift_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ValuativeCriteria.lean, line 1189.

Stacks 089F. Let f : X ⟶ Y be a flat morphism of algebraic spaces over S and let Spec A ⟶ Y be a morphism with A a valuation ring. If the closed point of Spec A maps to a point of |Y| in the image of |X| → |Y|, then there is an extension of valuation rings A ⟶ A' and a commutative square filling in Spec A' ⟶ X over Spec A ⟶ Y.

The point of |X| above the closed point is produced by a chart U ⟶ X ×_Y Spec A of the fibre product (Stacks 03H4, 03H5). The chart is flat over Spec A because flatness is stable under base change (Stacks 03MO) and may be read on étale charts, so the induced homomorphism A ⟶ 𝒪_{U, u} is flat and local, hence faithfully flat; a prime of the stalk contracting to the zero ideal of A therefore exists, and factoring the resulting map to its fraction field through a valuation subring gives A'.

theorem exists_valuationRing_extension_lift_of_isFlat
    (A : Type u) [CommRing A] [IsDomain A] [ValuationRing A]
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsFlat B S hS f)
    (V : BigFppfOver B S hS)
    (e : (BigFppfOver.toScheme B S hS).obj V ≅ Spec (.of A))
    (g : yoneda.obj V ⟶ Y)
    (p : FieldValuedPoint B S hS (yoneda.obj V))
    (hp : e.hom ((BigFppfOver.toScheme B S hS).map p.value
      (IsLocalRing.closedPoint p.carrier)) = IsLocalRing.closedPoint A)
    (himage : ∃ x : points B S hS X, pointsMap B S hS X f x =
      pointsMap B S hS (yoneda.obj V) g (p.class B S hS (yoneda.obj V))) :
    ∃ (A' : Type u) (_ : CommRing A') (_ : IsDomain A') (_ : ValuationRing A') (ι : A →+* A'),
      ValuationRing.IsExtension ι ∧
      ∃ (V' : BigFppfOver B S hS)
        (e' : (BigFppfOver.toScheme B S hS).obj V' ≅ Spec (.of A'))
        (j : V' ⟶ V) (lift : yoneda.obj V' ⟶ X),
        (BigFppfOver.toScheme B S hS).map j ≫ e.hom =
          e'.hom ≫ Spec.map (CommRingCat.ofHom ι) ∧
        lift ≫ f = yoneda.map j ≫ g

Tag 089G, a lemma

Tag 089G in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_of_refinedValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RefinedValuativeCriterion.lean, line 1808. The attribute's comment: “universally closed conclusion”.

The refined valuative criterion makes f universally closed when the quasi-compact map h has dense image.

public theorem universallyClosed_of_refinedValuativeCriterion
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {U X Y : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hU : AlgebraicGeometry.IsAlgebraicSpace B S hS U)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y)
    (h : U ⟶ X) (f : X ⟶ Y)
    (hf : AlgebraicGeometry.Space.IsQuasiCompact B S hS f)
    (hh : AlgebraicGeometry.Space.IsQuasiCompact B S hS h)
    (hdense : letI : TopologicalSpace (AlgebraicGeometry.Space.points B S hS X) :=
        pointTopology B S hS X
      DenseRange (pointsMap B S hS U h))
    (hunique : ∀ (q : ValuativeSquare f)
      (g : yoneda.obj (siteObject B S hS q.field_mem
        (Spec.map (CommRingCat.ofHom (algebraMap q.R q.K)) ≫ q.base)) ⟶ U),
      g ≫ h = q.generic → Subsingleton q.Lift)
    (hexists : ∀ (q : ValuativeSquare f)
      (g : yoneda.obj (siteObject B S hS q.field_mem
        (Spec.map (CommRingCat.ofHom (algebraMap q.R q.K)) ≫ q.base)) ⟶ U),
      g ≫ h = q.generic →
        ∃ e : q.DominatingExtension, Nonempty e.square.Lift) :
    UniversallyClosed B S hS f

AlgebraicGeometry.Space.isSeparated_of_refinedValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RefinedValuativeCriterion.lean, line 1982. The attribute's comment: “separated conclusion”.

With quasi-separatedness, the same refined valuative criterion makes f separated.

public theorem isSeparated_of_refinedValuativeCriterion
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {U X Y : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hU : AlgebraicGeometry.IsAlgebraicSpace B S hS U)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y)
    (h : U ⟶ X) (f : X ⟶ Y)
    (hf : AlgebraicGeometry.Space.IsQuasiCompact B S hS f)
    (hh : AlgebraicGeometry.Space.IsQuasiCompact B S hS h)
    (hqs : AlgebraicGeometry.Space.IsQuasiSeparated B S hS f)
    (hdense : letI : TopologicalSpace (AlgebraicGeometry.Space.points B S hS X) :=
        pointTopology B S hS X
      DenseRange (pointsMap B S hS U h))
    (hunique : ∀ (q : ValuativeSquare f)
      (g : yoneda.obj (siteObject B S hS q.field_mem
        (Spec.map (CommRingCat.ofHom (algebraMap q.R q.K)) ≫ q.base)) ⟶ U),
      g ≫ h = q.generic → Subsingleton q.Lift)
    (hexists : ∀ (q : ValuativeSquare f)
      (g : yoneda.obj (siteObject B S hS q.field_mem
        (Spec.map (CommRingCat.ofHom (algebraMap q.R q.K)) ≫ q.base)) ⟶ U),
      g ≫ h = q.generic →
        ∃ e : q.DominatingExtension, Nonempty e.square.Lift) :
    AlgebraicGeometry.Space.IsSeparated B S hS f

Sources

• Section 67.42, Tag 03K9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.universallyClosed_of_isQuasiCompact_of_valuativeCriterion_existence · AlgebraicGeometry.Space.valuativeCriterion_existence_of_isQuasiSeparated_of_universallyClosed · AlgebraicGeometry.Space.universallyClosed_iff_valuativeCriterion_existence_of_isQuasiCompact_of_isQuasiSeparated · AlgebraicGeometry.Space.universallyClosed_tfae_of_isQuasiCompact_of_isSeparated · AlgebraicGeometry.Space.exists_valuationRing_extension_lift_of_isFlat · AlgebraicGeometry.Space.universallyClosed_of_refinedValuativeCriterion · AlgebraicGeometry.Space.isSeparated_of_refinedValuativeCriterion

Section67.43 Valuative criterion of separatedness#

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

Tag 03KU, a lemma

Tag 03KU in the Stacks Project.

AlgebraicGeometry.Space.valuativeCriterion_uniqueness_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ValuativeCriteria.lean, line 292. References: EGA II (7.3.2), “more general”.

Stacks 03KU. A separated morphism of algebraic spaces satisfies the uniqueness part of the valuative criterion.

Two lifts of a valuative square assemble into a morphism Spec R ⟶ X ×_Y X; the base change of the relative diagonal along it is a closed immersion of schemes which is surjective on global sections, because the generic point of Spec R lifts through it, hence an isomorphism. The two lifts therefore agree.

theorem valuativeCriterion_uniqueness_of_isSeparated (f : X ⟶ Y)
    (hf : IsSeparated B S hS f) : ValuativeCriterion.Uniqueness f

Tag 03KV, a lemma

Tag 03KV in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_isQuasiSeparated_of_valuativeCriterion_uniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ValuativeCriteria.lean, line 1099.

Stacks 03KV. A quasi-separated morphism of algebraic spaces over S which satisfies the uniqueness part of the valuative criterion is separated.

Quasi-separatedness is quasi-compactness of the relative diagonal, and the diagonal satisfies the existence part of the criterion, so by Stacks 03KA it is universally closed. Being also separated, locally of finite type and locally quasi-finite (Stacks 03HK), every represented base change of it is a proper locally quasi-finite morphism of schemes, hence finite; being in addition a monomorphism, it is a closed immersion.

theorem isSeparated_of_isQuasiSeparated_of_valuativeCriterion_uniqueness
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqs : IsQuasiSeparated B S hS f) (hu : ValuativeCriterion.Uniqueness f) :
    IsSeparated B S hS f

Tag 0A3Z, a lemma

Tag 0A3Z in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_and_universallyClosed_tfae_of_isQuasiCompact_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/SeparatedUniversallyClosed.lean, line 49.

For a quasi-compact and quasi-separated morphism f : X ⟶ Y of algebraic spaces over S, being separated and universally closed, satisfying the valuative criterion of Stacks 03IX, and having exactly one dotted arrow in every valuative square over the given valuation ring are equivalent.

public theorem isSeparated_and_universallyClosed_tfae_of_isQuasiCompact_of_isQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hqc : IsQuasiCompact B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    List.TFAE
      [IsSeparated B S hS f ∧ UniversallyClosed B S hS f,
        ValuativeCriterion f,
        ∀ q : ValuativeSquare f, Nonempty q.Lift ∧ Subsingleton q.Lift]

Sources

• Section 67.43, Tag 03KT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.valuativeCriterion_uniqueness_of_isSeparated · AlgebraicGeometry.Space.isSeparated_of_isQuasiSeparated_of_valuativeCriterion_uniqueness · AlgebraicGeometry.Space.isSeparated_and_universallyClosed_tfae_of_isQuasiCompact_of_isQuasiSeparated

Section67.44 Valuative criterion of properness#

Section 67.44 of the Stacks Project, Tag 0CKZ. 1 tag here is carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A40, a lemma

Tag 0A40 in the Stacks Project.

AlgebraicGeometry.Space.isProper_tfae_of_isFiniteType_of_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Valuative/Properness.lean, line 54.

For a morphism f : X ⟶ Y of algebraic spaces over S which is of finite type and quasi-separated, being proper, satisfying the valuative criterion of Stacks 03IX, and having exactly one dotted arrow in every valuative square over the given valuation ring are equivalent.

public theorem isProper_tfae_of_isFiniteType_of_isQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hft : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    List.TFAE
      [IsProper B S hS f,
        ValuativeCriterion f,
        ∀ q : ValuativeSquare f, Nonempty q.Lift ∧ Subsingleton q.Lift]

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

A morphism of algebraic spaces over S which is of finite type and quasi-separated is proper exactly when it satisfies the valuative criterion of Stacks 03IX.

public theorem isProper_iff_valuativeCriterion_of_isFiniteType_of_isQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hft : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    IsProper B S hS f ↔ ValuativeCriterion f

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

A morphism of algebraic spaces over S which is of finite type and quasi-separated is proper exactly when every valuative square for it has exactly one dotted arrow over the given valuation ring, which is the valuative criterion of Schemes, Stacks 01KD.

public theorem isProper_iff_forall_unique_lift_of_isFiniteType_of_isQuasiSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hft : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f) :
    IsProper B S hS f ↔ ∀ q : ValuativeSquare f, Nonempty q.Lift ∧ Subsingleton q.Lift

Sources

• Section 67.44, Tag 0CKZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isProper_tfae_of_isFiniteType_of_isQuasiSeparated · AlgebraicGeometry.Space.isProper_iff_valuativeCriterion_of_isFiniteType_of_isQuasiSeparated · AlgebraicGeometry.Space.isProper_iff_forall_unique_lift_of_isFiniteType_of_isQuasiSeparated

Section67.45 Integral and finite morphisms#

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

Tag 03ZO, a lemma

Tag 03ZO in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_iff_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralFiniteTfae.lean, line 213. The attribute's comment: “integral case: the affine test criterion for a representable morphism”.

A morphism of algebraic spaces over S is integral in the sense of Stacks 03ZP exactly when it is relatively representable and all of its represented base changes are integral morphisms of schemes.

theorem isIntegralHom_iff_representable {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsIntegralHom B S hS f ↔
      (yoneda.relativelyRepresentable f ∧
        (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.IsIntegralHom.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f)

AlgebraicGeometry.Space.isFinite_iff_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralFiniteTfae.lean, line 229. The attribute's comment: “finite case: the affine test criterion for a representable morphism”.

A morphism of algebraic spaces over S is finite in the sense of Stacks 03ZP exactly when it is relatively representable and all of its represented base changes are finite morphisms of schemes.

theorem isFinite_iff_representable {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsFinite B S hS f ↔
      (yoneda.relativelyRepresentable f ∧
        (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.IsFinite.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f)

Tag 03ZP, a definition

Tag 03ZP in the Stacks Project.

AlgebraicGeometry.Space.IsFinite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Finite.lean, line 49. The attribute's comment: “finite_morphism”.

A morphism of algebraic spaces over S is finite when, for every object U of the big fppf site with affine underlying scheme and every morphism ξ from yoneda.obj U to the target, the base change of f along ξ is represented by an object V of the site with affine underlying scheme whose projection to U is a finite morphism of schemes.

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

AlgebraicGeometry.Space.IsIntegralHom, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Finite.lean, line 65. The attribute's comment: “integral_morphism”.

A morphism of algebraic spaces over S is integral when, for every object Z of the big fppf site with affine underlying scheme and every morphism g from yoneda.obj Z to the target, the base change of f along g is represented by an object W of the site with affine underlying scheme whose projection to Z is an integral morphism of schemes.

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

Tag 03ZQ, a lemma

Tag 03ZQ in the Stacks Project.

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

Stacks 03ZQ for integral morphisms, condition (3) implies condition (2). A morphism of algebraic spaces over S whose base change along some surjective étale morphism from a scheme is integral is itself integral.

theorem isIntegralHom_of_surjectiveEtaleChart (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) {U : BigFppfOver B S hS}
    {q : yoneda.obj U ⟶ Y} (hqs : IsSurjective B S hS q) (hqe : IsEtale B S hS q)
    (hbase : IsIntegralHom B S hS (pullback.snd f q)) :
    IsIntegralHom B S hS f

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

Stacks 03ZQ for finite morphisms, condition (3) implies condition (2). A morphism of algebraic spaces over S whose base change along some surjective étale morphism from a scheme is finite is itself finite.

theorem isFinite_of_surjectiveEtaleChart (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) {U : BigFppfOver B S hS}
    {q : yoneda.obj U ⟶ Y} (hqs : IsSurjective B S hS q) (hqe : IsEtale B S hS q)
    (hbase : IsFinite B S hS (pullback.snd f q)) :
    IsFinite B S hS f

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

Stacks 03ZQ for integral morphisms, conditions (2) and (3). A morphism of algebraic spaces over S is integral in the sense of Stacks 03ZP exactly when there is one surjective étale morphism from a representable presheaf onto its target along which its base change is integral.

theorem isIntegralHom_iff_etaleLocal (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsIntegralHom B S hS f ↔
      ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ Y),
        (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        IsIntegralHom B S hS (pullback.snd f g)

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

Stacks 03ZQ for finite morphisms, conditions (2) and (3). A morphism of algebraic spaces over S is finite in the sense of Stacks 03ZP exactly when there is one surjective étale morphism from a representable presheaf onto its target along which its base change is finite.

theorem isFinite_iff_etaleLocal (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsFinite B S hS f ↔
      ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ Y),
        (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        IsFinite B S hS (pullback.snd f g)

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

A morphism of algebraic spaces over S is integral in the sense of Stacks 03ZP exactly when it is relatively representable and all of its represented base changes are integral morphisms of schemes.

theorem isIntegralHom_iff_representable {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsIntegralHom B S hS f ↔
      (yoneda.relativelyRepresentable f ∧
        (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.IsIntegralHom.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f)

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

A morphism of algebraic spaces over S is finite in the sense of Stacks 03ZP exactly when it is relatively representable and all of its represented base changes are finite morphisms of schemes.

theorem isFinite_iff_representable {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsFinite B S hS f ↔
      (yoneda.relativelyRepresentable f ∧
        (MorphismProperty.inverseImage
          (@_root_.AlgebraicGeometry.IsFinite.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f)

AlgebraicGeometry.Space.isIntegralHom_iff_zariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralFiniteTfae.lean, line 243. The attribute's comment: “integral: conditions (2) and (4)”.

A morphism of algebraic spaces over S is integral in the sense of Stacks 03ZP exactly when there is a Zariski covering of its target over whose members its base changes are integral.

theorem isIntegralHom_iff_zariskiCover {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsIntegralHom B S hS f ↔
      ∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
          ∀ i, IsIntegralHom B S hS (Limits.pullback.snd f (U i).ι)

AlgebraicGeometry.Space.isFinite_iff_zariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralFiniteTfae.lean, line 256. The attribute's comment: “finite: conditions (2) and (4)”.

A morphism of algebraic spaces over S is finite in the sense of Stacks 03ZP exactly when there is a Zariski covering of its target over whose members its base changes are finite.

theorem isFinite_iff_zariskiCover {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsFinite B S hS f ↔
      ∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
          ∀ i, IsFinite B S hS (Limits.pullback.snd f (U i).ι)

AlgebraicGeometry.Space.isIntegralHom_iff_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 512. The attribute's comment: “integral: conditions (2) and (3)”.

A morphism of algebraic spaces over S is integral exactly when its base change along some surjective étale morphism from a representable presheaf onto its target is integral.

theorem isIntegralHom_iff_etaleChart {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsIntegralHom B S hS f ↔
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
          IsIntegralHom B S hS (pullback.snd f g)

AlgebraicGeometry.Space.isFinite_iff_etaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 534. The attribute's comment: “finite: conditions (2) and (3)”.

A morphism of algebraic spaces over S is finite exactly when its base change along some surjective étale morphism from a representable presheaf onto its target is finite.

theorem isFinite_iff_etaleChart {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    IsFinite B S hS f ↔
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage
          (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
          IsFinite B S hS (pullback.snd f g)

Tag 03ZR, a lemma

Tag 03ZR in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Finite.lean, line 130. The attribute's comment: “integral”. References: EGA II (6.1.5), “(ii) integral”.

The composite of two integral morphisms of algebraic spaces over S is integral.

theorem isIntegralHom_comp {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : IsIntegralHom B S hS f) (hg : IsIntegralHom B S hS g) :
    IsIntegralHom B S hS (f ≫ g)

AlgebraicGeometry.Space.isFinite_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Finite.lean, line 142. The attribute's comment: “finite”. References: EGA II (6.1.5), “(ii) finite”.

The composite of two finite morphisms of algebraic spaces over S is finite.

theorem isFinite_comp {f : X ⟶ Y} {g : Y ⟶ Z}
    (hf : IsFinite B S hS f) (hg : IsFinite B S hS g) :
    IsFinite B S hS (f ≫ g)

Tag 03ZS, a lemma

Tag 03ZS in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/IntegralFinite.lean, line 86. The attribute's comment: “integral”.

A base change of an integral morphism of algebraic spaces over S is integral: if f' sits in a Cartesian square over f, then f' is integral as soon as f is.

theorem isIntegralHom_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 : IsIntegralHom B S hS f) : IsIntegralHom B S hS f'

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

A base change of a finite morphism of algebraic spaces over S is finite.

theorem isFinite_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 : IsFinite B S hS f) : IsFinite B S hS f'

Tag 0414, a lemma

Tag 0414 in the Stacks Project.

AlgebraicGeometry.Space.IsFinite.isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyClosed.lean, line 94. The attribute's comment: “first assertion: a finite morphism is integral”.

A finite morphism of algebraic spaces is integral.

theorem IsFinite.isIntegralHom {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y}
    (hf : IsFinite B S hS f) : IsIntegralHom B S hS f

AlgebraicGeometry.Space.isFinite_of_isIntegralHom_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyClosed.lean, line 102. The attribute's comment: “second assertion: an integral morphism locally of finite type is finite”.

An integral morphism of algebraic spaces which is locally of finite type is finite.

theorem isFinite_of_isIntegralHom_of_isLocallyOfFiniteType
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hf : IsIntegralHom B S hS f) (hft : IsLocallyOfFiniteType B S hS f) :
    IsFinite B S hS f

Tag 0415, a lemma

Tag 0415 in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_iff_isAffineHom_and_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralUniversallyClosed.lean, line 153. References: EGA IV (18.12.8), “more general”; EGA II (6.1.10).

A morphism of algebraic spaces over S is integral if and only if it is affine and universally closed.

theorem isIntegralHom_iff_isAffineHom_and_universallyClosed
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsIntegralHom B S hS f ↔
      IsAffineHom B S hS f ∧ UniversallyClosed B S hS f

Tag 04NY, a lemma

Tag 04NY in the Stacks Project.

AlgebraicGeometry.Space.isQuasiFinite_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/IntegralFinite.lean, line 139.

A finite morphism of algebraic spaces over S is quasi-finite.

theorem isQuasiFinite_of_isFinite (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hf : IsFinite B S hS f) :
    IsQuasiFinite B S hS f

Tag 04NZ, a lemma

Tag 04NZ in the Stacks Project.

AlgebraicGeometry.Space.isFinite_iff_isAffineHom_and_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteAffineProper.lean, line 130. References: EGA III (4.4.2), “a) <=> b)”.

A morphism of algebraic spaces over S is finite exactly when it is affine and proper.

theorem isFinite_iff_isAffineHom_and_isProper {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsFinite B S hS f ↔ IsAffineHom B S hS f ∧ IsProper B S hS f

Tag 081Y, a lemma

Tag 081Y in the Stacks Project.

AlgebraicGeometry.Space.isFinite_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 103. The attribute's comment: “finite”. References: EGA II (6.1.5), “(i) finite”.

A closed immersion of algebraic spaces is finite.

theorem isFinite_of_isClosedImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f) :
    IsFinite B S hS f

AlgebraicGeometry.Space.isIntegralHom_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersions.lean, line 114. The attribute's comment: “integral”. References: EGA II (6.1.5), “(i) integral”.

A closed immersion of algebraic spaces is integral.

theorem isIntegralHom_of_isClosedImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsClosedImmersion B S hS f) :
    IsIntegralHom B S hS f

Tag 0CZ2, a lemma

Tag 0CZ2 in the Stacks Project.

AlgebraicGeometry.Space.isFinite_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/IntegralFinite.lean, line 173.

Let F i ⟶ Y, for i in a finite index type, be finite morphisms of algebraic spaces over S, and let G be their coproduct as a sheaf of sets on the big fppf site of S, given by a colimit cofan. Then the induced morphism G ⟶ Y is finite.

theorem isFinite_coproduct {I : Type v} [Finite I]
    (F : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : ∀ i, IsAlgebraicSpace B S hS (F i)) (hY : IsAlgebraicSpace B S hS Y)
    (G : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, (⟨F i, (hF i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ G)
    (hG : IsColimit (Cofan.mk G ι))
    (fᵢ : ∀ i, F i ⟶ Y) (f : G.obj ⟶ Y) (hf : ∀ i, (ι i).hom ≫ f = fᵢ i)
    (hfin : ∀ i, IsFinite B S hS (fᵢ i)) :
    IsFinite B S hS f

Tag 081Z, a lemma

Tag 081Z in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/IntegralFinite.lean, line 116. The attribute's comment: “part (2): integral”. References: EGA II (6.1.5), “(v) integral”.

If a composite of morphisms of algebraic spaces over S is integral and its second leg is separated, then its first leg is integral.

theorem isIntegralHom_of_comp_of_isSeparated (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfg : IsIntegralHom B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    IsIntegralHom B S hS f

AlgebraicGeometry.Space.isFinite_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/IntegralFinite.lean, line 127. The attribute's comment: “part (1): finite”. References: EGA II (6.1.5), “(v) finite”.

If a composite of morphisms of algebraic spaces over S is finite and its second leg is separated, then its first leg is finite.

theorem isFinite_of_comp_of_isSeparated (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfg : IsFinite B S hS (f ≫ g)) (hg : IsSeparated B S hS g) :
    IsFinite B S hS f

Sources

• Section 67.45, Tag 03ZN
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isIntegralHom_iff_representable · AlgebraicGeometry.Space.isFinite_iff_representable · AlgebraicGeometry.Space.IsFinite · AlgebraicGeometry.Space.IsIntegralHom · AlgebraicGeometry.Space.isIntegralHom_of_surjectiveEtaleChart · AlgebraicGeometry.Space.isFinite_of_surjectiveEtaleChart · AlgebraicGeometry.Space.isIntegralHom_iff_etaleLocal · AlgebraicGeometry.Space.isFinite_iff_etaleLocal

Section67.46 Finite locally free morphisms#

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

Tag 03ZU, a lemma

Tag 03ZU in the Stacks Project.

AlgebraicGeometry.Space.presheaf_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartComparisonAssembly.lean, line 255. The attribute's comment: “the only if direction: finite locally free in the sense of 03ZV implies every represented base change is a finite locally free morphism of schemes”.

Stacks 03ZU, the "only if" direction. A representable morphism f : X ⟶ Y of algebraic spaces over S which is finite locally free in the sense of Stacks 03ZV — affine with f_*𝒪_X a finite locally free 𝒪_Y-module — is finite locally free in the sense of Section 03HA: every represented base change of f is a finite locally free morphism of schemes.

This is AlgebraicGeometry.Space.presheaf_of_isFiniteLocallyFree_of_chartComparison_at with its hypothesis hcross discharged by AlgebraicGeometry.Space.isFiniteLocallyFree_baseChangeChartHom_of_isFiniteLocallyFreeOnSite, at an étale chart whose structure morphism is surjective on points; one exists by AlgebraicGeometry.Space.exists_surjective_smallEtale_chart. The affineness that the chart comparison consumes is the first conjunct of Stacks 03ZV, so nothing is assumed beyond it.

theorem presheaf_of_isFiniteLocallyFree (f : X ⟶ Y)
    (hrep : yoneda.relativelyRepresentable f.hom) (h : IsFiniteLocallyFree B S hS f) :
    (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom

AlgebraicGeometry.Space.presheaf_iff_isFiniteLocallyFree_iff_chartComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeRepresentable.lean, line 256. The attribute's comment: “the reduction of the biconditional to the chart comparison: proved unconditionally, that f is finite locally free in the sense of Section 03HA if and only if it is affine with finite locally free pushforward, holds exactly when the chart comparison holds at a surjective etale chart. The biconditional itself is AlgebraicGeometry.Space .presheaf_iff_isFiniteLocallyFree, which discharges that chart comparison”.

The equivalence of Stacks 03ZU for a morphism is equivalent to the chart comparison for that morphism. For a representable f : X ⟶ Y and an étale chart V of Y whose structure morphism is surjective on points, the assertion of Stacks 03ZU for f holds exactly when the scheme-level finite local freeness of the base change of f over V agrees with affineness of f together with finite local freeness of the restriction of f_*𝒪_X to the slice at V.

This statement carries no hypothesis. It says that the chart comparison is not merely one sufficient input for Stacks 03ZU but is equivalent to it, so that nothing is lost by reducing the tag to a statement at a single chart. Affineness appears on the right-hand side because the module conjunct alone does not bound the morphism; it cannot be dropped, as the implementation notes record.

Its @[stacks 03ZU] attribute is clause-labelled for the reduction alone: it is an equivalence between Stacks 03ZU and a chart statement, not Stacks 03ZU. The chart statement is proved, and with it the biconditional, in StacksFrontier.AlgebraicGeometry.Spaces.FiniteLocallyFreeRepresentableChart.

theorem presheaf_iff_isFiniteLocallyFree_iff_chartComparison (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom)
    (V : (smallEtaleRingedSite B S hS Y.1 Y.2).C) (hV : IsSurjective B S hS V.1.hom) :
    (((MorphismProperty.inverseImage
          (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f.hom ↔
        IsFiniteLocallyFree B S hS f) ↔
      (Stacks.Morphisms.IsFiniteLocallyFree
          ((BigFppfOver.toScheme B S hS).map (hf.snd V.1.hom)) ↔
        (IsAffineHom B S hS f.hom ∧
          SheafOfModules.IsFiniteLocallyFreeOnSite
            (R := (Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS Y.1 Y.2).O).over V)
            ((pushforwardStructureModule B S hS f).over V))))

AlgebraicGeometry.Space.presheaf_iff_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeRepresentableChart.lean, line 136.

Let S be a scheme and let f : X ⟶ Y be a representable morphism of algebraic spaces over S. Then f is finite locally free in the sense of Section 03HA — every represented base change of f is a finite locally free morphism of schemes — if and only if f is affine and the sheaf f_*𝒪_X is a finite locally free 𝒪_Y-module, which is the definition of Stacks 03ZV, AlgebraicGeometry.Space.IsFiniteLocallyFree.

theorem presheaf_iff_isFiniteLocallyFree (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f.hom) :
    (MorphismProperty.inverseImage
        (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f.hom ↔
      IsFiniteLocallyFree B S hS f

Declarations registered for the tag:

• AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_isFiniteLocallyFree, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeRepresentableIff.lean, line 167 (StacksFrontier).

Tag 03ZV, a definition

Tag 03ZV in the Stacks Project.

AlgebraicGeometry.Space.IsFiniteLocallyFree, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFree.lean, line 88. The attribute's comment: “finite locally free”.

Stacks 03ZV. A morphism of algebraic spaces is finite locally free when it is affine and the direct image of the structure sheaf of its source is a finite locally free module on the small étale ringed site of its target.

noncomputable abbrev IsFiniteLocallyFree (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsFiniteLocallyFreeOfRank, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFree.lean, line 95. The attribute's comment: “rank or degree”.

Stacks 03ZV. A finite locally free morphism of algebraic spaces has rank (or degree) r when the direct image of the structure sheaf of its source has rank r.

noncomputable abbrev IsFiniteLocallyFreeOfRank (f : X ⟶ Y) (r : ℕ) : Prop

Tag 03ZW, a lemma

Tag 03ZW in the Stacks Project.

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

Stacks 03ZW, conditions (1) and (2). A morphism of algebraic spaces over S is representable with every represented base change a finite locally free morphism of schemes exactly when it is finite locally free in the sense of Stacks 03ZV.

No representability hypothesis is imposed, which is what distinguishes this from Stacks 03ZU, AlgebraicGeometry.Space.presheaf_iff_isFiniteLocallyFree: from condition (1) representability is CategoryTheory.MorphismProperty.relative.rep, and from condition (2) it is AlgebraicGeometry.Space.relativelyRepresentable_of_isFiniteLocallyFree.

theorem isFiniteLocallyFree_presheaf_iff_isFiniteLocallyFree (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
        (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f.hom ↔
      IsFiniteLocallyFree B S hS f

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

Stacks 03ZW, conditions (2) and (3). A morphism of algebraic spaces over S is finite locally free in the sense of Stacks 03ZV exactly when there is one surjective étale morphism from a representable presheaf onto its target along which its base change is representable and finite locally free.

This is AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_isFiniteLocallyFree composed with AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_exists_etaleChart, conditions (1) and (3).

theorem isFiniteLocallyFree_iff_exists_etaleChart (f : X ⟶ Y) :
    IsFiniteLocallyFree B S hS f ↔
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y.1),
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage
          (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f.hom g)

AlgebraicGeometry.Space.isFiniteLocallyFree_iff_exists_zariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeCondition2.lean, line 164. The attribute's comment: “conditions (2) and (4)”.

Stacks 03ZW, conditions (2) and (4). A morphism of algebraic spaces over S is finite locally free in the sense of Stacks 03ZV exactly when there is a Zariski covering Y = ⋃ Yᵢ of its target such that each f⁻¹(Yᵢ) ⟶ Yᵢ is representable and finite locally free.

This is AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_isFiniteLocallyFree composed with AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_exists_zariskiCover, conditions (1) and (4).

theorem isFiniteLocallyFree_iff_exists_zariskiCover (f : X ⟶ Y) :
    IsFiniteLocallyFree B S hS f ↔
      ∃ (I : Type u) (U : I → Subfunctor Y.1),
        IsZariskiCover B S hS I U ∧
        ∀ i, (MorphismProperty.inverseImage
          (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f.hom (U i).ι)

AlgebraicGeometry.Space.isFiniteLocallyFree_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeCondition2.lean, line 193.

Stacks 03ZW. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent:

1. f is representable and finite locally free, i.e. every represented base change of f is a finite locally free morphism of schemes;
2. f is finite locally free in the sense of Stacks 03ZV: affine, with f_*𝒪_X a finite locally free 𝒪_Y-module;
3. there exists a scheme V and a surjective étale morphism V ⟶ Y such that V ×_Y X ⟶ V is (representable and) finite locally free;
4. there exists a Zariski covering Y = ⋃ Yᵢ such that each f⁻¹(Yᵢ) ⟶ Yᵢ is (representable and) finite locally free.

Assembled from the pairwise equivalences AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_isFiniteLocallyFree, AlgebraicGeometry.Space.isFiniteLocallyFree_iff_exists_etaleChart and AlgebraicGeometry.Space.isFiniteLocallyFree_iff_exists_zariskiCover.

theorem isFiniteLocallyFree_tfae (f : X ⟶ Y) :
    List.TFAE
      [(MorphismProperty.inverseImage
          (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf f.hom,
        IsFiniteLocallyFree B S hS f,
        ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y.1),
          (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf g ∧
          (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf g ∧
          (MorphismProperty.inverseImage
            (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f.hom g),
        ∃ (I : Type u) (U : I → Subfunctor Y.1),
          IsZariskiCover B S hS I U ∧
          ∀ i, (MorphismProperty.inverseImage
            (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f.hom (U i).ι)]

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

Stacks 03ZW, conditions (1) and (3). A morphism of algebraic spaces over S is representable and finite locally free exactly when there is one surjective étale morphism from a representable presheaf onto its target along which its base change is representable and finite locally free.

theorem isFiniteLocallyFree_presheaf_iff_exists_etaleChart
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
        (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      ∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y),
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf g ∧
        (MorphismProperty.inverseImage
          (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f g)

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_exists_zariskiCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeZariskiCover.lean, line 64. The attribute's comment: “conditions (1) and (4)”.

Stacks 03ZW, conditions (1) and (4). A morphism of algebraic spaces over S is representable and finite locally free exactly when there is a Zariski covering Y = ⋃ Yᵢ of its target such that each f⁻¹(Yᵢ) ⟶ Yᵢ is.

This is the equivalence the source obtains from the fact that being finite locally free is Zariski local on the target, which it notes is a weakening of the fpqc locality established along the way to conditions (1) and (3). Here it is AlgebraicGeometry.Space.presheaf_tfae — Stacks 03M4 for an arbitrary property of scheme morphisms Zariski local at the target — instantiated at finite local freeness: the restriction f⁻¹(Yᵢ) ⟶ Yᵢ is read, as the source reads it, as the base change of f along the inclusion of the open subspace Yᵢ, and both sides are read in the representable sense of condition (1).

theorem isFiniteLocallyFree_presheaf_iff_exists_zariskiCover
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
        (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      ∃ (I : Type u) (U : I → Subfunctor Y),
        IsZariskiCover B S hS I U ∧
        ∀ i, (MorphismProperty.inverseImage
          (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f (U i).ι)

Tag 03ZX, a lemma

Tag 03ZX in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeComp.lean, line 70. The attribute's comment: “stability under composition”.

Being representable and finite locally free is a composition-stable class of morphisms of presheaves on the big fppf site of S.

instance isFiniteLocallyFree_presheaf_isStableUnderComposition :
    (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf.IsStableUnderComposition

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeComp.lean, line 79.

The composition of representable finite locally free morphisms of algebraic spaces over S is representable and finite locally free.

theorem isFiniteLocallyFree_presheaf_comp
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f)
    (hg : (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf g) :
    (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf (f ≫ g)

Tag 03ZY, a lemma

Tag 03ZY in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeBaseChange.lean, line 110. The attribute's comment: “stability under base change”.

Stacks 03ZY. Being representable and finite locally free is a base-change stable class of morphisms of presheaves on the big fppf site of S.

instance isFiniteLocallyFree_presheaf_isStableUnderBaseChange :
    (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf.IsStableUnderBaseChange

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeBaseChange.lean, line 120.

Stacks 03ZY. A base change of a representable finite locally free morphism of algebraic spaces over S is representable and finite locally free: if f' sits in a Cartesian square over f, then f' is finite locally free as soon as f is.

theorem isFiniteLocallyFree_presheaf_of_isPullback
    {X Y 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 : (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f) :
    (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f'

Tag 0416, a lemma

Tag 0416 in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeFiniteFlat.lean, line 174. The attribute's comment: “conditions (1) and (2), finite local freeness in the representable sense”.

Stacks 0416, conditions (1) and (2). A morphism of algebraic spaces over S is representable and finite locally free exactly when it is finite, flat and locally of finite presentation.

Both sides are conditions on the represented base changes of the morphism, so this is the scheme-level equivalence Stacks 02KB applied to one represented base change at a time.

theorem isFiniteLocallyFree_presheaf_iff (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (MorphismProperty.inverseImage
        (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      IsFinite B S hS f ∧ IsFlat B S hS f ∧ IsLocallyOfFinitePresentation B S hS f

AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeFiniteFlat.lean, line 206. The attribute's comment: “condition (3) over a locally Noetherian target”.

Stacks 0416, condition (3). A morphism of algebraic spaces over S with locally Noetherian target is representable and finite locally free exactly when it is finite and flat.

A finite morphism is locally of finite type, hence locally of finite presentation over a locally Noetherian target by Stacks 06G4, part (1), so the finite presentation condition of conditions (1) and (2) is automatic.

theorem isFiniteLocallyFree_presheaf_iff_of_isLocallyNoetherian
    (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)) :
    (MorphismProperty.inverseImage
        (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf f ↔
      IsFinite B S hS f ∧ IsFlat B S hS f

Sources

• Section 67.46, Tag 03ZT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.presheaf_of_isFiniteLocallyFree · AlgebraicGeometry.Space.presheaf_iff_isFiniteLocallyFree_iff_chartComparison · AlgebraicGeometry.Space.presheaf_iff_isFiniteLocallyFree · AlgebraicGeometry.Space.isFiniteLocallyFree_presheaf_iff_isFiniteLocallyFree · AlgebraicGeometry.Space.IsFiniteLocallyFree · AlgebraicGeometry.Space.IsFiniteLocallyFreeOfRank · AlgebraicGeometry.Space.isFiniteLocallyFree_iff_exists_etaleChart · AlgebraicGeometry.Space.isFiniteLocallyFree_iff_exists_zariskiCover

Section67.47 Rational maps#

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

Tag 0EMM, a definition

Tag 0EMM in the Stacks Project.

AlgebraicGeometry.Space.PartialMap.Equivalent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RationalFunctions.lean, line 173. The attribute's comment: “part (1): equivalence of representatives”. References: EGA I (7.1.1), “equivalence definition”.

Two partial maps agree after restriction to a common dense open subspace.

def Equivalent (f g : PartialMap B S hS hX Y) : Prop

AlgebraicGeometry.Space.PartialMap.equivalence_equivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RationalFunctions.lean, line 186. The attribute's comment: “part (1): equivalence relation”. References: EGA I (7.1.1), “is an equivalence rel.”.

Stacks 0EMM, part (1). Agreement on a common dense open subspace is an equivalence relation.

Transitivity restricts to the dense open subspace common to the two witnesses, which exists by AlgebraicGeometry.Space.exists_isDenseOpenSubspace_le.

theorem equivalence_equivalent :
    Equivalence (Equivalent B S hS (X := X) (Y := Y) (hX := hX))

AlgebraicGeometry.Space.RationalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RationalFunctions.lean, line 214. The attribute's comment: “part (2): rational maps”. References: EGA I (7.1.2), “rational map”.

Stacks 0EMM, part (2). A rational map of algebraic spaces is a class of dense-open representatives.

def RationalMap (hX : IsAlgebraicSpace B S hS X)
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Type _

AlgebraicGeometry.Space.RationalMap.IsOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RationalFunctions.lean, line 250. The attribute's comment: “part (3): relative rational maps”.

Stacks 0EMM, part (3). A rational map is over another algebraic space if one representative is.

abbrev IsOver {T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (xToT : X ⟶ T) (yToT : Y ⟶ T)
    (φ : RationalMap B S hS hX Y) : Prop

Tag 0EMN, a definition

Tag 0EMN in the Stacks Project.

AlgebraicGeometry.Space.rationalFunctions, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RationalFunctions.lean, line 490. The attribute's comment: “rational functions as rational maps to the relative affine line”.

A rational function is a rational map to the relative affine line.

noncomputable abbrev rationalFunctions (hX : IsAlgebraicSpace B S hS X) : Type (u + 1)

Tag 0EMP, a definition

Tag 0EMP in the Stacks Project.

AlgebraicGeometry.Space.rationalFunctionsRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RationalFunctions.lean, line 499.

Stacks 0EMP. Pointwise ring operations on common dense-open representatives determine the commutative ring structure on rational functions.

The ring is the direct limit of the rings of sections over the dense open subspaces, which is a directed system because two dense open subspaces contain a common one.

theorem rationalFunctionsRing (hX : IsAlgebraicSpace B S hS X) :
    ∃ R : CommRing (rationalFunctions B S hS hX),
      letI := R
      (∀ (U : Subfunctor X) (hU : IsDenseOpenSubspace B S hS hX U)
          (f g : U.toFunctor ⟶ affineLineFunctor B S hS),
        ∃ a m : U.toFunctor ⟶ affineLineFunctor B S hS,
          (∀ T x, affineLineCoordinate B S hS T (a.app T x) =
            affineLineCoordinate B S hS T (f.app T x) +
              affineLineCoordinate B S hS T (g.app T x)) ∧
          (∀ T x, affineLineCoordinate B S hS T (m.app T x) =
            affineLineCoordinate B S hS T (f.app T x) *
              affineLineCoordinate B S hS T (g.app T x)) ∧
          (PartialMap.toRationalMap B S hS
            (⟨U, hU, a⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) =
            PartialMap.toRationalMap B S hS
              (⟨U, hU, f⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) +
            PartialMap.toRationalMap B S hS
              (⟨U, hU, g⟩ : PartialMap B S hS hX (affineLineFunctor B S hS))) ∧
          (PartialMap.toRationalMap B S hS
            (⟨U, hU, m⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) =
            PartialMap.toRationalMap B S hS
              (⟨U, hU, f⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) *
            PartialMap.toRationalMap B S hS
              (⟨U, hU, g⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)))) ∧
      (∀ (U : Subfunctor X) (hU : IsDenseOpenSubspace B S hS hX U),
        ∃ z o : U.toFunctor ⟶ affineLineFunctor B S hS,
          (∀ T x, affineLineCoordinate B S hS T (z.app T x) = 0) ∧
          (∀ T x, affineLineCoordinate B S hS T (o.app T x) = 1) ∧
          (PartialMap.toRationalMap B S hS
            (⟨U, hU, z⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) = 0) ∧
          (PartialMap.toRationalMap B S hS
            (⟨U, hU, o⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) = 1)) ∧
      (∀ (U : Subfunctor X) (hU : IsDenseOpenSubspace B S hS hX U)
          (f : U.toFunctor ⟶ affineLineFunctor B S hS),
        ∃ n : U.toFunctor ⟶ affineLineFunctor B S hS,
          (∀ T x, affineLineCoordinate B S hS T (n.app T x) =
            -affineLineCoordinate B S hS T (f.app T x)) ∧
          (PartialMap.toRationalMap B S hS
            (⟨U, hU, n⟩ : PartialMap B S hS hX (affineLineFunctor B S hS)) =
            -PartialMap.toRationalMap B S hS
              (⟨U, hU, f⟩ : PartialMap B S hS hX (affineLineFunctor B S hS))))

Tag 0EMQ, a definition

Tag 0EMQ in the Stacks Project.

AlgebraicGeometry.Space.RationalMap.IsDefinedAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RationalMaps.lean, line 211. The attribute's comment: “defined at a point”. References: EGA I (7.2.1), “defined at a point”; EGA IV (20.2.3), “defined at a point”.

A rational map is defined at a point of its source when it has a representative whose domain contains that point.

abbrev IsDefinedAt (φ : RationalMap B S hS hX Y) (x : points B S hS X) : Prop

AlgebraicGeometry.Space.RationalMap.domainOfDefinition, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RationalMaps.lean, line 219. The attribute's comment: “domain of definition”. References: EGA I (7.2.1), “domain of definition”; EGA IV (20.2.3), “dom(ω)”.

The domain of definition of a rational map is the set of points at which it is defined.

abbrev domainOfDefinition (φ : RationalMap B S hS hX Y) : Set (points B S hS X)

Tag 0EMR, a lemma

Tag 0EMR in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_hom_of_eq_domainOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RationalMapDomainOfDefinition.lean, line 401. References: EGA I (7.2.2).

Stacks 0EMR. Let X be a reduced algebraic space over S and let Y be an algebraic space separated over S. A rational map from X to Y is represented by exactly one morphism on the open subspace of X whose point set is its domain of definition.

theorem existsUnique_hom_of_eq_domainOfDefinition
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hXred : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsReduced T))
    (hYsep : IsSeparatedOver B S hS Y)
    (φ : RationalMap B S hS hX Y)
    (U : Subfunctor X) (hU : IsOpenSubspace B S hS U)
    (hUdom : Set.range (pointsMap B S hS U.toFunctor U.ι) =
      RationalMap.domainOfDefinition B S hS φ) :
    ∃! f : U.toFunctor ⟶ Y, ∃ hUd : IsDenseOpenSubspace B S hS hX U,
      PartialMap.toRationalMap B S hS ⟨U, hUd, f⟩ = φ

Tag 0EMS, a definition

Tag 0EMS in the Stacks Project.

AlgebraicGeometry.Space.RationalMap.IsDominant, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RationalMaps.lean, line 225.

A rational map is dominant when every one of its dense-open representatives is a dominant morphism.

abbrev IsDominant (φ : RationalMap B S hS hX Y) : Prop

Tag 0EMT, a definition

Tag 0EMT in the Stacks Project.

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

Two algebraic spaces over S with irreducible point spaces are birational when they have mutually inverse dominant rational maps: two dominant rational maps whose composites agree with the respective identities on dense open subspaces.

abbrev Birational (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (_hXirr : IrreducibleSpace (points B S hS X))
    (_hYirr : IrreducibleSpace (points B S hS Y)) : Prop

Tag 0EMU, a lemma

Tag 0EMU in the Stacks Project.

AlgebraicGeometry.Space.birational_iff_exists_isOpenSubspace_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RationalMaps.lean, line 319.

Two algebraic spaces over S with irreducible point spaces are birational if and only if they contain nonempty open subspaces which are isomorphic as algebraic spaces over S.

theorem birational_iff_exists_isOpenSubspace_iso (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hXirr : IrreducibleSpace (points B S hS X))
    (hYirr : IrreducibleSpace (points B S hS Y)) :
    Birational B S hS hX hY hXirr hYirr ↔
      ∃ (U : Subfunctor X) (V : Subfunctor Y), IsOpenSubspace B S hS U ∧
        IsOpenSubspace B S hS V ∧ Nonempty (points B S hS U.toFunctor) ∧
        Nonempty (points B S hS V.toFunctor) ∧ Nonempty (U.toFunctor ≅ V.toFunctor)

Sources

• Section 67.47, Tag 0EML
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.PartialMap.Equivalent · AlgebraicGeometry.Space.PartialMap.equivalence_equivalent · AlgebraicGeometry.Space.RationalMap · AlgebraicGeometry.Space.RationalMap.IsOver · AlgebraicGeometry.Space.rationalFunctions · AlgebraicGeometry.Space.rationalFunctionsRing · AlgebraicGeometry.Space.RationalMap.IsDefinedAt · AlgebraicGeometry.Space.RationalMap.domainOfDefinition

Section67.48 Relative normalization of algebraic spaces#

Section 67.48 of the Stacks Project, Tag 0BAZ. 11 tags here are carried by 37 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0820, a lemma

Tag 0820 in the Stacks Project.

AlgebraicGeometry.Space.AlgebraSheaf.range_integralClosureInclusion_app_eq_integralClosure', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralClosureQuasicoherent.lean, line 357. The attribute's comment: “the sections of the integral closure over an affine chart”.

The sections of the integral closure of the structure sheaf in a quasi-coherent algebra sheaf over an affine étale chart are the integral closure of the ring of functions on the chart in the sections of the algebra over it.

theorem range_integralClosureInclusion_app_eq_integralClosure'
    (A : AlgebraSheaf.{u, u} B S hS F hF) (hA : A.IsQuasicoherent) (U : SmallEtale B S hS F)
    (hU : IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj U)) :
    letI : Algebra ((structureSheaf B S hS F hF).obj.obj (op U))
        (A.right.obj.obj (op U)) := (A.algebraMap (op U)).toAlgebra
    Set.range (((integralClosureInclusion A).right.hom.app (op U)).hom) =
      (integralClosure ((structureSheaf B S hS F hF).obj.obj (op U))
        (A.right.obj.obj (op U)) : Set _)

AlgebraicGeometry.Space.AlgebraSheaf.isQuasicoherent_integralClosureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralClosureQuasicoherent.lean, line 410. The attribute's comment: “quasi-coherence of the integral closure”.

Quasi-coherence of the integral closure. The integral closure of the structure sheaf in a quasi-coherent sheaf of 𝒪_F-algebras is again a quasi-coherent sheaf of 𝒪_F-algebras.

theorem isQuasicoherent_integralClosureSheaf (A : AlgebraSheaf.{u, u} B S hS F hF)
    (hA : A.IsQuasicoherent) : (integralClosureSheaf A).IsQuasicoherent

Tag 0821, a definition

Tag 0821 in the Stacks Project.

AlgebraicGeometry.Space.AlgebraSheaf.integralClosureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralClosureSheaf.lean, line 356. The attribute's comment: “the integral closure of the structure sheaf in an algebra”.

The integral closure of the structure sheaf in an algebra sheaf. Its sections over a chart are the locally integral sections of A, and the structure-algebra map is the one of A, whose values are integral.

This is the subalgebra of Stacks 0820 as data, which is what Stacks 0821 names; the two assertions the source makes about it are discussed in the implementation notes.

def integralClosureSheaf (A : AlgebraSheaf.{u, m} B S hS F hF) :
    AlgebraSheaf.{u, m} B S hS F hF

AlgebraicGeometry.Space.AlgebraSheaf.integralClosureInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IntegralClosureSheaf.lean, line 368. The attribute's comment: “the inclusion exhibiting the integral closure as a subalgebra”.

The inclusion of the integral closure into the algebra, as a morphism of algebra sheaves. On each chart it is the inclusion of the subring of locally integral sections. It is what makes the integral closure a subalgebra of A, as Stacks 0821 names it.

def integralClosureInclusion (A : AlgebraSheaf.{u, m} B S hS F hF) :
    integralClosureSheaf A ⟶ A

Tag 0822, a definition

Tag 0822 in the Stacks Project.

AlgebraicGeometry.Space.normalizationIn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationIn.lean, line 115. The attribute's comment: “the normalization of X in Y”.

The normalization of X in Y. For a morphism f : Y ⟶ X of algebraic spaces whose direct image f_* 𝒪_Y is quasi-coherent, it is the relative spectrum ν : X' = \underline{Spec}_X(𝒪') ⟶ X of the integral closure 𝒪' of 𝒪_X in f_* 𝒪_Y, regarded as an algebraic space affine over X.

def normalizationIn (f : Y ⟶ X)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent) :
    AffineOver B S hS X

AlgebraicGeometry.Space.toNormalizationIn, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationIn.lean, line 146. The attribute's comment: “the canonical factorization of f through the normalization”.

The canonical morphism f' : Y ⟶ X' to the normalization of X in Y, as a morphism over X. It is the factorization Y ⟶ \underline{Spec}_X(f_* 𝒪_Y) of Stacks 081X followed by the morphism of relative spectra induced by the inclusion 𝒪' ⊂ f_* 𝒪_Y.

def toNormalizationIn (f : Y ⟶ X)
    (hqc : (pushforwardAlgebra B S hS (Over.mk f)).IsQuasicoherent)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent)
    (hid : pushforwardAlgebra B S hS (idAffineOver B S hS Y).obj ≅ unitAlgebra B S hS Y) :
    Over.mk f ⟶ (normalizationIn B S hS E f hqc').obj

AlgebraicGeometry.Space.normalizationInQcqsHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqs.lean, line 150. The attribute's comment: “the normalization ν : X' = Spec_X(𝒪') ⟶ X of X in Y, for f qcqs”.

The normalization morphism ν : X' ⟶ X of X in Y (Definition 0822), for a quasi-compact quasi-separated f : Y ⟶ X. It is affine (AlgebraicGeometry.Space.isAffineHom_normalizationInQcqsHom) with ν_* 𝒪_{X'} the integral closure 𝒪' of 𝒪_X in f_* 𝒪_Y (AlgebraicGeometry.Space.normalizationInQcqsPushforwardIso), which is what X' = \underline{Spec}_X(𝒪') means.

def normalizationInQcqsHom : normalizationInQcqs B S hS f hfqc hfqs ⟶ X

AlgebraicGeometry.Space.isAffineHom_normalizationInQcqsHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqs.lean, line 155. The attribute's comment: “ν : X' ⟶ X is affine, X' being a relative spectrum over X”.

ν : X' ⟶ X is affine.

theorem isAffineHom_normalizationInQcqsHom :
    IsAffineHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom

AlgebraicGeometry.Space.normalizationInQcqsPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqs.lean, line 163. The attribute's comment: “ν_* 𝒪_{X'} = 𝒪', i.e. X' = Spec_X(𝒪')”.

ν_* 𝒪_{X'} ≅ 𝒪': the direct image of the structure sheaf of the normalization is the integral closure of 𝒪_X in f_* 𝒪_Y, as sheaves of 𝒪_X-algebras. With affineness of ν this identifies X' with \underline{Spec}_X(𝒪').

def normalizationInQcqsPushforwardIso :
    pushforwardAlgebra B S hS (Over.mk (normalizationInQcqsHom B S hS f hfqc hfqs)) ≅
      AlgebraSheaf.integralClosureSheaf (pushforwardAlgebra B S hS (Over.mk f))

AlgebraicGeometry.Space.toNormalizationInQcqs, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqs.lean, line 306. The attribute's comment: “the canonical morphism f' : Y ⟶ X'”.

The canonical morphism f' : Y ⟶ X' of Definition 0822: on a T-point y of Y it is the unique morphism T ⟶ X' over X inducing ν_* 𝒪_{X'} ≅ 𝒪' ⊂ f_* 𝒪_Y ⟶ (f ∘ y)_* 𝒪_T.

def toNormalizationInQcqs : Y ⟶ normalizationInQcqs B S hS f hfqc hfqs

AlgebraicGeometry.Space.toNormalizationInQcqs_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqs.lean, line 321. The attribute's comment: “the natural factorization Y ⟶ X' ⟶ X of f”.

The factorization of Definition 0822: ν ∘ f' = f.

theorem toNormalizationInQcqs_comp :
    toNormalizationInQcqs f hfqc hfqs ≫ normalizationInQcqsHom B S hS f hfqc hfqs = f

Tag 0ABP, a lemma

Tag 0ABP in the Stacks Project.

AlgebraicGeometry.Space.etaleAlgebraRestrictionIntegralClosureIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInComparison.lean, line 276. The attribute's comment: “part (1), étale base change: the integral closure of the structure sheaf in an algebra is unchanged by restriction along an étale morphism, which is the construction of the normalization commuting with étale base change. The geometric form, for the relative spectra, is normalizationInBaseChangeIso.”.

Stacks 0ABP, part (1), at the level of algebras. The integral closure of the structure sheaf in an algebra commutes with restriction along an étale morphism g : W ⟶ X.

This is the whole of the source's reason for part (1): the normalization of X in Y is the relative spectrum of the integral closure of 𝒪_X in f_* 𝒪_Y, and that construction is étale-local, hence "commutes with étale base change".

def etaleAlgebraRestrictionIntegralClosureIso (g : W ⟶ X) (hg : IsEtale B S hS g.hom)
    (A : AlgebraSheaf.{u, m} B S hS X.1 X.2) :
    (etaleAlgebraRestriction B S hS g hg).obj (AlgebraSheaf.integralClosureSheaf A) ≅
      AlgebraSheaf.integralClosureSheaf ((etaleAlgebraRestriction B S hS g hg).obj A)

AlgebraicGeometry.Space.normalizationInBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInComparison.lean, line 373. The attribute's comment: “part (1), étale base change, in its geometric form. halg is the identification of the algebra pullback of Stacks 081V along an étale morphism with étale restriction and hbc is Stacks 03LX for the direct image of the structure sheaf, read as algebras; neither is part (1), and the module docstring records why each is carried. The content of part (1) is etaleAlgebraRestrictionIntegralClosureIso, which is unconditional.”.

Stacks 0ABP, part (1). For an étale morphism g : W ⟶ X the fibre product W ×_X X' is the normalization of W in W ×_X Y.

The identification of the two algebras is étale-locality of the integral closure, etaleAlgebraRestrictionIntegralClosureIso, together with halg and hbc; the identification of the two relative spectra is the base-change clause of Stacks 081V.

def normalizationInBaseChangeIso {Y YW : AlgebraicSpaces B S hS}
    (g : W ⟶ X) (hg : IsEtale B S hS g.hom) (f : Y ⟶ X) (p : YW ⟶ Y) (fW : YW ⟶ W)
    (_sq : IsPullback p fW f g)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent)
    (hqcW' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk fW))).IsQuasicoherent)
    (halg : C.algebraPullback g ≅ etaleAlgebraRestriction.{u, u} B S hS g hg)
    (hbc : (etaleAlgebraRestriction.{u, u} B S hS g hg).obj
        (pushforwardAlgebra B S hS (Over.mk f)) ≅
      pushforwardAlgebra B S hS (Over.mk fW)) :
    (C.affineBaseChange g).obj (normalizationIn B S hS E f hqc') ≅
      normalizationIn B S hS E fW hqcW'

AlgebraicGeometry.Space.normalizationInRepresentableIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInComparison.lean, line 420. The attribute's comment: “part (2), comparison with the normalization of schemes. Z is the scheme normalization AlgebraicGeometry.Scheme.Hom.normalization of Stacks 035E, read inside the site as an algebraic space affine over X, and hcmp identifies its direct image of the structure sheaf with the integral closure of 𝒪_X in f_* 𝒪_Y. That identification is the source's computation of ν⁻¹(U). It is not Descent, Proposition 03DX(2): that proposition for the small étale site of an algebraic space is available here, unconditionally, as AlgebraicGeometry.Space.isQuasicoherentOnSite_iff_isCartesianOnAffineCharts, and it compares the sections over two affine charts rather than computing the sections of the integral closure. The module docstring lists what hcmp still needs.”.

Stacks 0ABP, part (2). Let X and Y be representable, by X₀ and Y₀, and let N₀ represent the normalization of the scheme X₀ in the scheme Y₀ of Stacks 035E. Then the normalization X' of X in Y is representable by N₀.

def normalizationInRepresentableIso {Y : AlgebraicSpaces B S hS} (f : Y ⟶ X)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent)
    {X₀ Y₀ N₀ : BigFppfOver B S hS} (_eX : X.1 ≅ yoneda.obj X₀) (_eY : Y.1 ≅ yoneda.obj Y₀)
    (f₀ : Y₀ ⟶ X₀) (_hf₀ : yoneda.map f₀ = _eY.inv ≫ f.hom ≫ _eX.hom)
    [QuasiCompact ((BigFppfOver.toScheme B S hS).map f₀)]
    [QuasiSeparated ((BigFppfOver.toScheme B S hS).map f₀)]
    (_hN : (BigFppfOver.toScheme B S hS).obj N₀ ≅
      ((BigFppfOver.toScheme B S hS).map f₀).normalization)
    (Z : AffineOver B S hS X) (eZ : Z.obj.left.1 ≅ yoneda.obj N₀)
    (hcmp : pushforwardAlgebra B S hS Z.obj ≅
      AlgebraSheaf.integralClosureSheaf (pushforwardAlgebra B S hS (Over.mk f))) :
    (normalizationIn B S hS E f hqc').obj.left.1 ≅ yoneda.obj N₀

AlgebraicGeometry.Space.isRepresentable_normalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInComparison.lean, line 440. The attribute's comment: “part (2), representability of the normalization. The hypotheses are those of normalizationInRepresentableIso.”.

Stacks 0ABP, part (2), representability. In the representable case the normalization X' of X in Y is representable.

theorem isRepresentable_normalizationIn {Y : AlgebraicSpaces B S hS} (f : Y ⟶ X)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent)
    {X₀ Y₀ N₀ : BigFppfOver B S hS} (eX : X.1 ≅ yoneda.obj X₀) (eY : Y.1 ≅ yoneda.obj Y₀)
    (f₀ : Y₀ ⟶ X₀) (hf₀ : yoneda.map f₀ = eY.inv ≫ f.hom ≫ eX.hom)
    [QuasiCompact ((BigFppfOver.toScheme B S hS).map f₀)]
    [QuasiSeparated ((BigFppfOver.toScheme B S hS).map f₀)]
    (hN : (BigFppfOver.toScheme B S hS).obj N₀ ≅
      ((BigFppfOver.toScheme B S hS).map f₀).normalization)
    (Z : AffineOver B S hS X) (eZ : Z.obj.left.1 ≅ yoneda.obj N₀)
    (hcmp : pushforwardAlgebra B S hS Z.obj ≅
      AlgebraSheaf.integralClosureSheaf (pushforwardAlgebra B S hS (Over.mk f))) :
    (normalizationIn B S hS E f hqc').obj.left.1.IsRepresentable

AlgebraicGeometry.Space.isRelativeNormalization_normalizationInQcqs_etaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsComparison.lean, line 100. The attribute's comment: “part (1): for W ⟶ X étale, W ×_X X' is the normalization of W in W ×_X Y”.

Stacks 0ABP, part (1). Let f : Y ⟶ X be a quasi-compact and quasi-separated morphism of algebraic spaces over S, with normalization Y ⟶ X' ⟶ X (Definition 0822), and let g : W ⟶ X be étale. Let P = W ×_X X' and Y' = W ×_X Y, with f'_P : Y' ⟶ P the base change of f' : Y ⟶ X'. Then Y' ⟶ P ⟶ W is the normalization of W in Y': it has the universal property of Stacks 0823, and it is joined to the normalization of W in Y' of Definition 0822 by a unique isomorphism compatible with both factorizations.

theorem isRelativeNormalization_normalizationInQcqs_etaleBaseChange
    {W P Y' : AlgebraicSpaces B S hS} (g : W ⟶ X) (hg : IsEtale B S hS g.hom)
    (i : P ⟶ normalizationInQcqs B S hS f hfqc hfqs) (νP : P ⟶ W)
    (hP : IsPullback i νP (normalizationInQcqsHom B S hS f hfqc hfqs) g)
    (j : Y' ⟶ Y) (fW : Y' ⟶ W) (hY : IsPullback j fW f g) (f'P : Y' ⟶ P)
    (h₁ : f'P ≫ i = j ≫ toNormalizationInQcqs f hfqc hfqs) (h₂ : f'P ≫ νP = fW) :
    IsRelativeNormalization B S hS fW.hom νP.hom f'P.hom ∧
      ∃ (hWqc : IsQuasiCompact B S hS fW.hom) (hWqs : IsQuasiSeparated B S hS fW.hom),
        ∃! e : (normalizationInQcqs B S hS fW hWqc hWqs).1 ≅ P.1,
          (toNormalizationInQcqs fW hWqc hWqs).hom ≫ e.hom = f'P.hom ∧
            e.hom ≫ νP.hom = (normalizationInQcqsHom B S hS fW hWqc hWqs).hom

AlgebraicGeometry.Space.isRepresentable_normalizationInQcqs_and_iso_normalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsComparison.lean, line 158. The attribute's comment: “part (2): for X and Y representable, X' is representable and canonically isomorphic to the normalization of the scheme X in the scheme Y of 035E”.

Stacks 0ABP, part (2). Let f : Y ⟶ X be a quasi-compact and quasi-separated morphism of algebraic spaces over S with X and Y representable, by objects X₀ and Y₀ of the site, and let f₀ : Y₀ ⟶ X₀ be the induced morphism. Then the normalization X' of X in Y (Definition 0822) is representable, and canonically isomorphic to the normalization of the scheme X₀ in the scheme Y₀ (Morphisms, Section 035E): there is an object N₀ of the site whose underlying scheme is that normalization, compatibly with both of its legs, and a unique isomorphism X' ≅ N₀ compatible with both factorizations.

theorem isRepresentable_normalizationInQcqs_and_iso_normalization {X₀ Y₀ : BigFppfOver B S hS}
    (eX : X.1 ≅ yoneda.obj X₀) (eY : Y.1 ≅ yoneda.obj Y₀) (f₀ : Y₀ ⟶ X₀)
    (hf₀ : yoneda.map f₀ = eY.inv ≫ f.hom ≫ eX.hom) :
    (normalizationInQcqs B S hS f hfqc hfqs).1.IsRepresentable ∧
      ∃ (_ : QuasiCompact ((BigFppfOver.toScheme B S hS).map f₀))
        (_ : QuasiSeparated ((BigFppfOver.toScheme B S hS).map f₀))
        (N₀ : BigFppfOver B S hS) (t : Y₀ ⟶ N₀) (ν₀ : N₀ ⟶ X₀)
        (e : (BigFppfOver.toScheme B S hS).obj N₀ ≅
          ((BigFppfOver.toScheme B S hS).map f₀).normalization),
        (BigFppfOver.toScheme B S hS).map t ≫ e.hom =
            ((BigFppfOver.toScheme B S hS).map f₀).toNormalization ∧
          e.hom ≫ ((BigFppfOver.toScheme B S hS).map f₀).fromNormalization =
            (BigFppfOver.toScheme B S hS).map ν₀ ∧
          ∃! φ : (normalizationInQcqs B S hS f hfqc hfqs).1 ≅ yoneda.obj N₀,
            (toNormalizationInQcqs f hfqc hfqs).hom ≫ φ.hom = eY.hom ≫ yoneda.map t ∧
              φ.hom ≫ yoneda.map ν₀ = (normalizationInQcqsHom B S hS f hfqc hfqs).hom ≫ eX.hom

Tag 0823, a lemma

Tag 0823 in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_normalizationInQcqsHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsUniversalProperty.lean, line 90. The attribute's comment: “property (1): ν is integral”.

Stacks 0823, property (1): the normalization ν : X' ⟶ X is integral. It is the relative spectrum of the integral closure 𝒪', an integral 𝒪_X-algebra.

theorem isIntegralHom_normalizationInQcqsHom :
    IsIntegralHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom

AlgebraicGeometry.Space.isRelativeNormalization_normalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsUniversalProperty.lean, line 116. The attribute's comment: “properties (1) and (2) hold for the normalization f = ν ∘ f' of Stacks 0822”.

Stacks 0823, properties (1) and (2) for the normalization of Stacks 0822. Let f : Y ⟶ X be a quasi-compact and quasi-separated morphism of algebraic spaces over S, and f = ν ∘ f' its factorization through the normalization ν : X' ⟶ X of X in Y. Then ν is integral, and for every factorization f = π ∘ g with π : Z ⟶ X an integral morphism of algebraic spaces over S there is a unique h : X' ⟶ Z with h ∘ f' = g and π ∘ h = ν.

theorem isRelativeNormalization_normalizationInQcqs :
    IsRelativeNormalization B S hS f.hom (normalizationInQcqsHom B S hS f hfqc hfqs).hom
      (toNormalizationInQcqs f hfqc hfqs).hom

AlgebraicGeometry.Space.isRelativeNormalization_iff_exists_iso_normalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsUniversalProperty.lean, line 168. The attribute's comment: “the factorization through the normalization is characterized by (1) and (2)”.

Stacks 0823: the normalization is characterized by properties (1) and (2). Let f : Y ⟶ X be quasi-compact and quasi-separated. A factorization f = ν'' ∘ f'' of f through an algebraic space X'' has properties (1) and (2) — ν'' integral, and every factorization of f through an integral morphism receiving a unique compatible morphism from X'' — if and only if it is isomorphic to the factorization f = ν ∘ f' through the normalization of X in Y; the isomorphism is then unique, by AlgebraicGeometry.Space.existsUnique_iso_normalizationInQcqs_of_isRelativeNormalization.

theorem isRelativeNormalization_iff_exists_iso_normalizationInQcqs
    {X'' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX'' : IsAlgebraicSpace B S hS X'')
    (ν'' : X'' ⟶ X.1) (f'' : Y.1 ⟶ X'') :
    IsRelativeNormalization B S hS f.hom ν'' f'' ↔
      ∃ e : (normalizationInQcqs B S hS f hfqc hfqs).1 ≅ X'',
        (toNormalizationInQcqs f hfqc hfqs).hom ≫ e.hom = f'' ∧
          e.hom ≫ ν'' = (normalizationInQcqsHom B S hS f hfqc hfqs).hom

AlgebraicGeometry.Space.isRelativeNormalization_comparison_normalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsUniversalProperty.lean, line 188. The attribute's comment: “moreover, in (2) the morphism h : X' ⟶ Z is the normalization of Z in Y”.

Stacks 0823, the final clause. Let f : Y ⟶ X be quasi-compact and quasi-separated, let f = π ∘ g with π : Z ⟶ X an integral morphism of algebraic spaces, and let h : X' ⟶ Z be the morphism of property (2), so h ∘ f' = g and π ∘ h = ν. Then h : X' ⟶ Z is the normalization of Z in Y: the factorization g = h ∘ f' has properties (1) and (2) for g, and it is uniquely isomorphic to the factorization of g through the normalization of Z in Y of Stacks 0822, g being quasi-compact and quasi-separated.

theorem isRelativeNormalization_comparison_normalizationInQcqs {Z : AlgebraicSpaces B S hS}
    (π : Z ⟶ X) (hπ : IsIntegralHom B S hS π.hom) (g : Y ⟶ Z) (hg : g ≫ π = f)
    (h : normalizationInQcqs B S hS f hfqc hfqs ⟶ Z)
    (hh : toNormalizationInQcqs f hfqc hfqs ≫ h = g)
    (hhπ : h ≫ π = normalizationInQcqsHom B S hS f hfqc hfqs) :
    IsRelativeNormalization B S hS g.hom h.hom (toNormalizationInQcqs f hfqc hfqs).hom ∧
      ∃ (hgqc : IsQuasiCompact B S hS g.hom) (hgqs : IsQuasiSeparated B S hS g.hom),
        ∃! e : (normalizationInQcqs B S hS g hgqc hgqs).1 ≅
            (normalizationInQcqs B S hS f hfqc hfqs).1,
          (toNormalizationInQcqs g hgqc hgqs).hom ≫ e.hom =
              (toNormalizationInQcqs f hfqc hfqs).hom ∧
            e.hom ≫ h.hom = (normalizationInQcqsHom B S hS g hgqc hgqs).hom

AlgebraicGeometry.Space.IsRelativeNormalization.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInUniversalProperty.lean, line 165. The attribute's comment: “properties (1) and (2) characterize the factorization”.

Stacks 0823, the characterization. Two factorizations of f through an integral morphism of algebraic spaces which both have the universal property are joined by a unique isomorphism compatible with the two factorizations and the two integral morphisms.

theorem existsUnique_iso {ν' : X'' ⟶ X} {f'' : Y ⟶ X''}
    (h : IsRelativeNormalization B S hS f ν f')
    (h' : IsRelativeNormalization B S hS f ν' f'')
    (hX' : IsAlgebraicSpace B S hS X') (hX'' : IsAlgebraicSpace B S hS X'') :
    ∃! e : X' ≅ X'', f' ≫ e.hom = f'' ∧ e.hom ≫ ν' = ν

AlgebraicGeometry.Space.IsRelativeNormalization.comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInUniversalProperty.lean, line 184. The attribute's comment: “moreover, the comparison morphism is the normalization of Z in Y”.

Stacks 0823, the final clause. Let f = π ∘ g be a factorization of f through an integral morphism π : Z ⟶ X, and let k : X' ⟶ Z be the comparison morphism supplied by the universal property. Then k exhibits X' as the normalization of Z in Y.

theorem comparison {Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (h : IsRelativeNormalization B S hS f ν f')
    (hX : IsAlgebraicSpace B S hS X) (hZ : IsAlgebraicSpace B S hS Z)
    {π : Z ⟶ X} (hπ : IsIntegralHom B S hS π) {g : Y ⟶ Z}
    {k : X' ⟶ Z} (hk : f' ≫ k = g) (hkν : k ≫ π = ν) :
    IsRelativeNormalization B S hS g k f'

AlgebraicGeometry.Space.isRelativeNormalization_toNormalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInUniversalProperty.lean, line 370. The attribute's comment: “the canonical factorization has properties (1) and (2)”.

Stacks 0823, properties (1) and (2) for the canonical factorization. The factorization f = ν ∘ f' of f through the normalization ν : X' ⟶ X of X in Y has ν integral, and every factorization of f through an integral morphism π : Z ⟶ X of algebraic spaces receives a unique morphism h : X' ⟶ Z with f' ∘ h = g and π ∘ h = ν.

theorem isRelativeNormalization_toNormalizationIn
    (P : RelativeSpecUniversalProperty B S hS E C)
    (D : IntegralAlgebraDictionary B S hS E) (f : Y ⟶ X)
    (hqc : (pushforwardAlgebra B S hS (Over.mk f)).IsQuasicoherent)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent)
    (hid : pushforwardAlgebra B S hS (idAffineOver B S hS Y).obj ≅ unitAlgebra B S hS Y)
    (hloc : (pushforwardAlgebra B S hS (Over.mk f)).IsIntegralLocalOnAffineCharts) :
    IsRelativeNormalization B S hS f.hom
      (normalizationIn B S hS E f hqc').obj.hom.hom
      (toNormalizationIn B S hS E C f hqc hqc' hid).left.hom

Tag 0AYF, a lemma

Tag 0AYF in the Stacks Project.

AlgebraicGeometry.Space.IsRelativeNormalization.hasEtaleLocalProperty_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeNormalization.lean, line 197.

Stacks 0AYF. The normalization of an algebraic space X in a reduced algebraic space Y is reduced.

Reducedness is asked of an algebraic space as the étale-local property of schemes of Tag 03E6. The reduction of the normalization is constructed here rather than taken as an input: it is AlgebraicGeometry.Space.reduction, the reduced induced structure of Tag 03IQ on the whole point set of X'.

theorem hasEtaleLocalProperty_isReduced (hnorm : IsRelativeNormalization B S hS f ν f')
    (hX' : IsAlgebraicSpace B S hS X') (hY : IsAlgebraicSpace B S hS Y)
    (hYred : HasEtaleLocalProperty B S hS Y fun T : Scheme.{u} => IsReduced T) :
    HasEtaleLocalProperty B S hS X' fun T : Scheme.{u} => IsReduced T

Tag 0AYG, a lemma

Tag 0AYG in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.exists_genericPoint_irreducibleComponent_mapping_to, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Normalization.lean, line 1150 (StacksFrontier).

Tag 0824, a lemma

Tag 0824 in the Stacks Project.

AlgebraicGeometry.Space.isRelativeNormalization_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeNormalization.lean, line 298.

Stacks 0824. Let f : Y ⟶ X be a morphism of algebraic spaces over S whose source is a disjoint union of finitely many algebraic spaces Y i, and let X' i be the normalization of X in Y i. Then a disjoint union of the X' i is the normalization of X in Y.

The normalization morphism is integral because its base change along a morphism from an affine object of the site is the induced morphism out of the coproduct of the base changes of the summands, which is a finite coproduct of integral morphisms of schemes; the universal property is checked summand by summand, each factorization of f through an integral morphism restricting to one of f i.

theorem isRelativeNormalization_coproduct {I : Type v} [Finite I]
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (F : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : ∀ i, IsAlgebraicSpace B S hS (F i))
    (Y : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, (⟨F i, (hF i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ Y)
    (hY : IsColimit (Cofan.mk Y ι)) (f : Y.obj ⟶ X)
    (N : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hN : ∀ i, IsAlgebraicSpace B S hS (N i))
    (νs : ∀ i, N i ⟶ X) (fs : ∀ i, F i ⟶ N i)
    (hnorm : ∀ i, IsRelativeNormalization B S hS ((ι i).hom ≫ f) (νs i) (fs i))
    (P : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (κ : ∀ i, (⟨N i, (hN i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ P)
    (hP : IsColimit (Cofan.mk P κ))
    (ν : P.obj ⟶ X) (hν : ∀ i, (κ i).hom ≫ ν = νs i)
    (f' : Y.obj ⟶ P.obj) (hf' : ∀ i, (ι i).hom ≫ f' = fs i ≫ (κ i).hom) :
    IsRelativeNormalization B S hS f ν f'

Tag 0A0Q, a lemma

Tag 0A0Q in the Stacks Project.

AlgebraicGeometry.Space.isIntegral_pushforwardAlgebra_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageSectionsGlobalFunctions.lean, line 344. The attribute's comment: “first sentence: f_*O_X is integral over O_Y; only universal closedness of f is used”. References: EGA II (7.3.11), “Integrality of Γ(X”.

Stacks 0A0Q, first assertion. For a universally closed morphism f : X ⟶ Y of algebraic spaces over S, the direct image f_*𝒪_X is integral over 𝒪_Y.

The assertion is étale local on Y: on an affine étale scheme chart V of Y the sections of f_*𝒪_X are the global regular functions on the algebraic space X ×_Y V (AlgebraicGeometry.Space.directImageSectionsToGlobalFunctions, which is injective), the projection X ×_Y V ⟶ V is universally closed because f is, and the global functions of a universally closed algebraic space over an affine base are integral over the base (AlgebraicGeometry.Space.isIntegral_globalFunctions_of_universallyClosed).

theorem isIntegral_pushforwardAlgebra_of_universallyClosed (f : X ⟶ Y)
    (huc : UniversallyClosed B S hS f.hom) :
    (pushforwardAlgebra B S hS (Over.mk f)).IsIntegral

AlgebraicGeometry.Space.isIso_pushforwardAlgebraMap_toNormalizationInQcqsOver_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInUniversallyClosed.lean, line 118. The attribute's comment: “second sentence: the normalization X ⟶ Y' ⟶ Y of Y in X induces ν_O_{Y'} ≅ f_O_X, i.e. Y' = Spec_Y(f_*O_X) with the factorization of 081X”.

Stacks 0A0Q, second sentence: the normalization of Y in X is \underline{Spec}_Y(f_*𝒪_X). Let f : X ⟶ Y be a quasi-compact, quasi-separated and universally closed morphism of algebraic spaces, and let X ⟶ Y' ⟶ Y be the normalization of Y in X (Stacks 0822; ν : Y' ⟶ Y is affine). Then the map ν_*𝒪_{Y'} ⟶ f_*𝒪_X of 𝒪_Y-algebras induced by the canonical morphism f' : X ⟶ Y' is an isomorphism, so Y' = \underline{Spec}_Y(f_*𝒪_X) and f' is the canonical morphism of Stacks 081X.

The map induced by f' is ν_*𝒪_{Y'} ≅ 𝒪' ⊂ f_*𝒪_X (AlgebraicGeometry.Space.pushforwardAlgebraMap_toNormalizationInQcqsOver), and the inclusion of the integral closure 𝒪' is all of f_*𝒪_X because f_*𝒪_X is integral over 𝒪_Y, the first sentence of the tag.

theorem isIso_pushforwardAlgebraMap_toNormalizationInQcqsOver_of_universallyClosed :
    IsIso (pushforwardAlgebraMap B S hS (toNormalizationInQcqsOver f hfqc hfqs))

AlgebraicGeometry.Space.existsUnique_iso_normalizationInQcqs_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInUniversallyClosed.lean, line 133. The attribute's comment: “second sentence: the normalization of Y in X is, uniquely, the factorization X ⟶ Spec_Y(f_*O_X) ⟶ Y of 081X”.

Stacks 0A0Q, second sentence, as an identification of factorizations. For a quasi-compact, quasi-separated and universally closed f : X ⟶ Y, every factorization X ⟶ Z ⟶ Y of f of the kind Stacks 081X constructs — Z affine over Y and the induced map (Z ⟶ Y)_*𝒪_Z ⟶ f_*𝒪_X an isomorphism, i.e. Z = \underline{Spec}_Y(f_*𝒪_X) with its canonical morphism from X — is the normalization of Y in X: there is a unique isomorphism Y' ≅ Z over Y from the normalization carrying the canonical f' : X ⟶ Y' to X ⟶ Z.

theorem existsUnique_iso_normalizationInQcqs_of_universallyClosed
    (Z : AffineOver B S hS Y) (g : Over.mk f ⟶ Z.obj)
    [IsIso (pushforwardAlgebraMap B S hS g)] :
    ∃! k : (normalizationInQcqsAffineOver B S hS f hfqc hfqs).obj ≅ Z.obj,
      toNormalizationInQcqsOver f hfqc hfqs ≫ k.hom = g

AlgebraicGeometry.Space.isIso_integralClosureInclusion_pushforwardAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PushforwardStructureSheafIntegral.lean, line 266. The attribute's comment: “second assertion: the normalization of Y in X is the factorization through Spec_Y(f_O_X), with the integrality of f_O_X assumed rather than proved”.

For a morphism f : X ⟶ Y of algebraic spaces whose direct image f_*𝒪_X is integral over 𝒪_Y, the inclusion of the integral closure 𝒪' of 𝒪_Y in f_*𝒪_X is an isomorphism of algebra sheaves, so 𝒪' = f_*𝒪_X and the normalization of Y in X — the relative spectrum of 𝒪', Stacks 0821 — is the factorization X ⟶ Spec_Y(f_*𝒪_X) ⟶ Y of Stacks 081X.

theorem isIso_integralClosureInclusion_pushforwardAlgebra (f : X ⟶ Y)
    (hf : (pushforwardAlgebra B S hS (Over.mk f)).IsIntegral) :
    IsIso (AlgebraSheaf.integralClosureInclusion (pushforwardAlgebra B S hS (Over.mk f)))

Tag 0825, a lemma

Tag 0825 in the Stacks Project.

AlgebraicGeometry.Space.normalizationInIsoOfIsIntegralHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInIntegralMorphism.lean, line 82.

Stacks 0825. The integral closure of X in Y is Y: for an integral morphism f : Y ⟶ X of algebraic spaces whose direct image f_* 𝒪_Y is integral over 𝒪_X, the normalization X' ⟶ X of X in Y is canonically isomorphic to Y over X.

def normalizationInIsoOfIsIntegralHom (f : Y ⟶ X) (hf : IsIntegralHom B S hS f.hom)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent)
    (hint : (pushforwardAlgebra B S hS (Over.mk f)).IsIntegral) :
    (normalizationIn B S hS E f hqc').obj ≅ Over.mk f

AlgebraicGeometry.Space.normalizationInIsoOfIsIntegralHom', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInIntegralMorphismSupplement.lean, line 37.

For an integral morphism f : Y ⟶ X of algebraic spaces, the normalization X' ⟶ X of X in Y is canonically isomorphic to Y over X.

def normalizationInIsoOfIsIntegralHom' (f : Y ⟶ X) (hf : IsIntegralHom B S hS f.hom)
    (hqc' : (AlgebraSheaf.integralClosureSheaf
      (pushforwardAlgebra B S hS (Over.mk f))).IsQuasicoherent) :
    (normalizationIn B S hS E f hqc').obj ≅ Over.mk f

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

Stacks 0825. Let f : Y ⟶ X be an integral morphism of algebraic spaces over S. Then the integral closure of X in Y is equal to Y: the canonical morphism f' : Y ⟶ X' of Stacks 0822 from Y to the normalization ν : X' ⟶ X of X in Y is an isomorphism.

An integral morphism is quasi-compact and quasi-separated, so the normalization is defined at no further hypothesis. By Stacks 0415 f is affine and universally closed; universal closedness makes f_* 𝒪_Y integral over 𝒪_X (Stacks 0A0Q), so the integral closure 𝒪' = ν_* 𝒪_{X'} is all of f_* 𝒪_Y, and since Y and X' are both affine over X, direct image reflects that isomorphism of algebras to f'.

theorem isIso_toNormalizationInQcqs_of_isIntegralHom (f : Y ⟶ X)
    (hf : IsIntegralHom B S hS f.hom) :
    IsIso (toNormalizationInQcqs f
      (isQuasiCompact_of_isIntegralHom f.hom Y.property X.property hf)
      (isQuasiSeparated_of_isIntegralHom f.hom Y.property X.property hf))

AlgebraicGeometry.Space.isRelativeNormalization_id_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQuasiFiniteLocus.lean, line 100. The attribute's comment: “in the form of the characterization of Tag 0823: an integral morphism is the normalization of its target in its source”.

Stacks 0825, in the form of the characterization of Tag 0823. An integral morphism f : X ⟶ Y of algebraic spaces over S is the normalization of Y in X: the factorization of f as the identity of X followed by f itself has the two characterizing properties.

Integrality of the second factor is the hypothesis, and a factorization f = g ≫ π through an integral morphism π : Z ⟶ Y already has g as a morphism out of X, which is therefore the unique morphism compatible with the two factorizations.

theorem isRelativeNormalization_id_of_isIntegralHom (hf : IsIntegralHom B S hS f) :
    IsRelativeNormalization B S hS f f (𝟙 X)

Tag 0BB0, a lemma

Tag 0BB0 in the Stacks Project.

AlgebraicGeometry.Space.IsRelativeNormalization.isFinite_of_isNagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeNormalizationNagata.lean, line 286. The attribute's comment: “granted Tag 081V, the relative spectrum of a quasi-coherent algebra on an algebraic space, in the shape of the hypothesis hdom: over an affine étale chart of the base the functions on the chart base change of the normalization embed into the functions on an affine surjective étale cover of the corresponding part of the source”.

Stacks 0BB0. Let f : Y ⟶ X be a quasi-separated morphism of finite type of algebraic spaces over S with X Nagata and Y reduced. Then the normalization ν : X' ⟶ X of X in Y is finite.

Nagata-ness and reducedness are the étale-local properties of schemes of Tag 03E6. The hypothesis hdom is the affine-chart description of the normalization of Tag 0822: over an affine étale chart of X the functions on the base change of X' embed into the functions on an affine surjective étale cover of the part of Y over the chart.

theorem IsRelativeNormalization.isFinite_of_isNagata
    (hnorm : IsRelativeNormalization B S hS f ν f')
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hX' : IsAlgebraicSpace B S hS X')
    (hXnagata : HasEtaleLocalProperty B S hS X fun Z : Scheme.{u} => IsNagataScheme Z)
    (hYred : HasEtaleLocalProperty B S hS Y fun Z : Scheme.{u} => IsReduced Z)
    (hft : IsFiniteType B S hS f) (_hqs : IsQuasiSeparated B S hS f)
    (hdom : ∀ (V N W : BigFppfOver B S hS) (q : yoneda.obj V ⟶ X) (n : N ⟶ V)
      (i : yoneda.obj N ⟶ X') (w : yoneda.obj W ⟶ Limits.pullback q f) (c : W ⟶ N),
      IsAffine ((BigFppfOver.toScheme B S hS).obj V) →
      IsAffine ((BigFppfOver.toScheme B S hS).obj W) →
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q →
      IsPullback i (yoneda.map n) ν q →
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf w →
      IsEtale B S hS w →
      yoneda.map c ≫ i = w ≫ Limits.pullback.snd q f ≫ f' →
      Function.Injective ((BigFppfOver.toScheme B S hS).map c).appTop.hom) :
    IsFinite B S hS ν

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

Let f : Y ⟶ X be a quasi-separated morphism of finite type of algebraic spaces over S with X Nagata and Y reduced. Then the normalization ν : X' ⟶ X of X in Y, any factorization Y ⟶ X' ⟶ X of f satisfying AlgebraicGeometry.Space.IsRelativeNormalization, is finite.

theorem IsRelativeNormalization.isFinite_of_isNagata_of_isReduced
    (hnorm : IsRelativeNormalization B S hS f ν f')
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hX' : IsAlgebraicSpace B S hS X')
    (hXnagata : HasEtaleLocalProperty B S hS X fun Z : Scheme.{u} => IsNagataScheme Z)
    (hYred : HasEtaleLocalProperty B S hS Y fun Z : Scheme.{u} => IsReduced Z)
    (hft : IsFiniteType B S hS f) (_hqs : IsQuasiSeparated B S hS f) :
    IsFinite B S hS ν

AlgebraicGeometry.Space.isFinite_normalizationInQcqsHom_of_isNagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQcqsNagataFinite.lean, line 51.

Stacks 0BB0. Let f : Y ⟶ X be a morphism of algebraic spaces over S such that X is Nagata, f is quasi-separated of finite type, and Y is reduced. Then the normalization ν : X' ⟶ X of X in Y (Stacks 0822) is finite.

Being Nagata and being reduced are the étale-local properties of schemes of Tag 03E6; the quasi-compactness that the normalization of Stacks 0822 requires of f is the second half of f being of finite type.

theorem isFinite_normalizationInQcqsHom_of_isNagata {X Y : AlgebraicSpaces B S hS} (f : Y ⟶ X)
    (hXnagata : HasEtaleLocalProperty B S hS X.1 fun Z : Scheme.{u} => IsNagataScheme Z)
    (hYred : HasEtaleLocalProperty B S hS Y.1 fun Z : Scheme.{u} => IsReduced Z)
    (hft : IsFiniteType B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom) :
    IsFinite B S hS (normalizationInQcqsHom B S hS f hft.2 hfqs).hom

Sources

• Section 67.48, Tag 0BAZ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.AlgebraSheaf.range_integralClosureInclusion_app_eq_integralClosure' · AlgebraicGeometry.Space.AlgebraSheaf.isQuasicoherent_integralClosureSheaf · AlgebraicGeometry.Space.AlgebraSheaf.integralClosureSheaf · AlgebraicGeometry.Space.AlgebraSheaf.integralClosureInclusion · AlgebraicGeometry.Space.normalizationIn · AlgebraicGeometry.Space.toNormalizationIn · AlgebraicGeometry.Space.normalizationInQcqsHom · AlgebraicGeometry.Space.isAffineHom_normalizationInQcqsHom

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.