76.33 Étale localization of… to 76.48 Local complete…

Section76.33 Étale localization of morphisms #

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

Tag 082H, a lemma

Tag 082H in the Stacks Project.

AlgebraicGeometry.Space.exists_etale_decomposition_isFinite_of_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSplitQuasiFinitePart.lean, line 338.

Stacks Project, Tag 082H. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let y be a point of |Y| and let x₁, …, x_n be points of |X| mapping to y. Assume that f is locally of finite type, that f is separated, that f is quasi-finite at each xᵢ, and that f is quasi-compact or Y is decent. Then there are an object U of the big fppf category over S, an étale morphism g : h_U ⟶ Y and a point u of |h_U| over y, together with a decomposition of U ×_Y X into two open-and-closed subspaces W and V — their join sheafifies to everything and their meet is the sheafification of nothing — such that

V ⟶ U is finite;

every point of the fibre of |V| ⟶ |U| over u maps to one of the xᵢ;

no point of the fibre of |W| ⟶ |U| over u maps to any xᵢ.

This is the composite of the three paragraphs of the source proof with its finiteness clause; see the module documentation for which file carries which. The hypotheses are those of the tag and nothing else, apart from the ambient HasSheafify assumption on the site discussed there.

theorem exists_etale_decomposition_isFinite_of_isQuasiFiniteAt
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (y : points B S hS Y) {n : ℕ} (x : Fin n → points B S hS X)
    (hx : ∀ i, pointsMap B S hS X f (x i) = y)
    (hft : IsLocallyOfFiniteType B S hS f) (hsep : IsSeparated B S hS f)
    (hqf : ∀ i, IsQuasiFiniteAt B S hS f (x i))
    (hqc : IsQuasiCompact B S hS f ∨ IsDecentSpace B S hS Y) :
    ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ Y)
      (u : points B S hS (yoneda.obj U)) (W V : Subfunctor (pullback g f)),
      IsEtale B S hS g ∧
      pointsMap B S hS (yoneda.obj U) g u = y ∧
      IsOpenSubspace B S hS W ∧ IsClosedSubspace B S hS W ∧
      IsOpenSubspace B S hS V ∧ IsClosedSubspace B S hS V ∧
      (W ⊔ V).sheafify (BigFppfOver.topology B S hS) = ⊤ ∧
      W ⊓ V = (⊥ : Subfunctor (pullback g f)).sheafify (BigFppfOver.topology B S hS) ∧
      IsFinite B S hS (V.ι ≫ pullback.fst g f) ∧
      (∀ v : points B S hS V.toFunctor,
        pointsMap B S hS V.toFunctor (V.ι ≫ pullback.fst g f) v = u →
          ∃ i, pointsMap B S hS V.toFunctor (V.ι ≫ pullback.snd g f) v = x i) ∧
      (∀ t : points B S hS W.toFunctor,
        pointsMap B S hS W.toFunctor (W.ι ≫ pullback.fst g f) t = u →
          ∀ i, pointsMap B S hS W.toFunctor (W.ι ≫ pullback.snd g f) t ≠ x i)

Tag 0ADU, a lemma

Tag 0ADU in the Stacks Project.

AlgebraicGeometry.Space.exists_etale_finite_clopen_part, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleQuasiFinitePart.lean, line 383.

Stacks 0ADU. An étale neighbourhood of the image of x splits the pullback into two open-and-closed parts, one of them finite over the neighbourhood and containing a point above x.

public theorem exists_etale_finite_clopen_part
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (x : points B S hS X.1)
    (hft : IsLocallyOfFiniteType B S hS f.hom)
    (hsep : IsSeparated B S hS f.hom)
    (hqf : IsQuasiFiniteAt B S hS f.hom x) :
    ∃ (U : AlgebraicSpaces B S hS) (g : U ⟶ Y)
      (u : points B S hS U.1)
      (W V : Subfunctor (pullback g.hom f.hom)),
      IsEtale B S hS g.hom ∧
      pointsMap B S hS U.1 g.hom u = pointsMap B S hS X.1 f.hom x ∧
      IsOpenSubspace B S hS W ∧
      IsClosedSubspace B S hS W ∧
      IsOpenSubspace B S hS V ∧
      IsClosedSubspace B S hS V ∧
      (W ⊔ V).sheafify (BigFppfOver.topology B S hS) = ⊤ ∧
      W ⊓ V = (⊥ : Subfunctor (pullback g.hom f.hom)).sheafify
        (BigFppfOver.topology B S hS) ∧
      IsFinite B S hS (V.ι ≫ pullback.fst g.hom f.hom) ∧
      ∃ v : points B S hS V.toFunctor,
        pointsMap B S hS V.toFunctor (V.ι ≫ pullback.snd g.hom f.hom) v = x ∧
        pointsMap B S hS V.toFunctor (V.ι ≫ pullback.fst g.hom f.hom) v = u

AlgebraicGeometry.Space.exists_etale_decomposition_isFinite_point_of_isQuasiFiniteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSplitQuasiFinitePoint.lean, line 201.

Stacks Project, Tag 0ADU. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let x be a point of |X| and let y be its image in |Y|. Assume that f is locally of finite type, that f is separated and that f is quasi-finite at x. Then there are an object U of the big fppf category over S, an étale morphism g : h_U ⟶ Y and a point u of |h_U| over y, together with a decomposition of U ×_Y X into two open-and-closed subspaces W and V — their join sheafifies to everything and their meet is the sheafification of nothing — such that V ⟶ U is finite and some point of |V| lies over x in |X| and over u in |U|.

This is the single-point case of Stacks 082H, AlgebraicGeometry.Space.exists_etale_decomposition_isFinite_of_isQuasiFiniteAt, applied over an étale scheme chart of Y through y; see the module documentation for how the extra hypothesis of that lemma and its standing HasSheafify assumption on the site are both discharged. The hypotheses are those of the tag and nothing else.

theorem exists_etale_decomposition_isFinite_point_of_isQuasiFiniteAt
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (x : points B S hS X) (y : points B S hS Y)
    (hxy : pointsMap B S hS X f x = y)
    (hft : IsLocallyOfFiniteType B S hS f) (hsep : IsSeparated B S hS f)
    (hqf : IsQuasiFiniteAt B S hS f x) :
    ∃ (U : BigFppfOver B S hS) (g : yoneda.obj U ⟶ Y)
      (u : points B S hS (yoneda.obj U)) (W V : Subfunctor (pullback g f)),
      IsEtale B S hS g ∧
      pointsMap B S hS (yoneda.obj U) g u = y ∧
      IsOpenSubspace B S hS W ∧ IsClosedSubspace B S hS W ∧
      IsOpenSubspace B S hS V ∧ IsClosedSubspace B S hS V ∧
      (W ⊔ V).sheafify (BigFppfOver.topology B S hS) = ⊤ ∧
      W ⊓ V = (⊥ : Subfunctor (pullback g f)).sheafify (BigFppfOver.topology B S hS) ∧
      IsFinite B S hS (V.ι ≫ pullback.fst g f) ∧
      ∃ v : points B S hS V.toFunctor,
        pointsMap B S hS V.toFunctor (V.ι ≫ pullback.snd g f) v = x ∧
        pointsMap B S hS V.toFunctor (V.ι ≫ pullback.fst g f) v = u

Sources

LeanAlgebraicGeometry.Space.exists_etale_decomposition_isFinite_of_isQuasiFiniteAt · AlgebraicGeometry.Space.exists_etale_finite_clopen_part · AlgebraicGeometry.Space.exists_etale_decomposition_isFinite_point_of_isQuasiFiniteAt

Section76.34 Zariski's Main Theorem #

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

Tag 082I, a lemma

Tag 082I in the Stacks Project.

AlgebraicGeometry.Space.IsRelativeNormalization.isIso_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQuasiFiniteLocus.lean, line 118. The attribute's comment: “the isomorphism conclusion when f is integral: the canonical morphism to the normalization is an isomorphism, so the open subspace may be taken to be the whole normalization”.

Stacks 082I, the isomorphism conclusion for an integral morphism. Let f : X ⟶ Y be an integral morphism of algebraic spaces over S and let ν : Y' ⟶ Y, f' : X ⟶ Y' be the normalization of Y in X. Then f' is an isomorphism, so the open subspace U' ⊆ Y' of the tag may be taken to be all of Y'.

The identity of X factors f through the integral morphism f, so the universal property yields k : Y' ⟶ X with f' ≫ k = 𝟙 and k ≫ f = ν; uniqueness in the universal property for the factorization f = f' ≫ ν identifies k ≫ f' with 𝟙.

theorem isIso_of_isIntegralHom (h : IsRelativeNormalization B S hS f ν f')
    (hX : IsAlgebraicSpace B S hS X) (hY' : IsAlgebraicSpace B S hS Y')
    (hf : IsIntegralHom B S hS f) : IsIso f'

AlgebraicGeometry.Space.exists_isOpenSubspace_isIso_fromPreimage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInQuasiFiniteLocus.lean, line 141. The attribute's comment: “both numbered conclusions in the case of a finite morphism, with the open subspace the whole normalization”.

Stacks 082I for a finite morphism. Let f : X ⟶ Y be a finite morphism of algebraic spaces over S and let ν : Y' ⟶ Y, f' : X ⟶ Y' be the normalization of Y in X. Then there is an open subspace U' ⊆ Y' such that (f')⁻¹(U') ⟶ U' is an isomorphism and the point set of (f')⁻¹(U') is the set of points of X at which f is quasi-finite; one may take U' = Y'.

A finite morphism is integral by Tag 0414, so f' is an isomorphism and hence so is its base change (f')⁻¹(Y') ⟶ Y'; and a finite morphism is locally quasi-finite by Tag 0A4X, hence quasi-finite at every point of its source, which is the whole of (f')⁻¹(Y').

theorem exists_isOpenSubspace_isIso_fromPreimage_of_isFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (h : IsRelativeNormalization B S hS f ν f')
    (hf : IsFinite B S hS f) :
    ∃ U' : Subfunctor Y', IsOpenSubspace B S hS U' ∧ IsIso (U'.fromPreimage f') ∧
      ∀ x : points B S hS X,
        x ∈ Set.range (pointsMap B S hS (U'.preimage f').toFunctor (U'.preimage f').ι) ↔
          IsQuasiFiniteAt B S hS f x

AlgebraicGeometry.Space.IsRelativeNormalization.exists_isOpenSubspace_isIso_fromPreimage_and_range_pointsMap_preimage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremFiniteTypeSeparated.lean, line 284. The attribute's comment: “both numbered conclusions, for every factorization of f with the universal property of Tag 0823 (the normalization of Y in X)”.

Stacks 082I. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is of finite type and separated, and let ν : Y' ⟶ Y, f' : X ⟶ Y' be the normalization of Y in X, in the sense of the characterization of Tag 0823. Then there is an open subspace U' ⊆ Y' such that (f')⁻¹(U') ⟶ U' is an isomorphism and the point set of (f')⁻¹(U') is the set of points of X at which f is quasi-finite.

The open subspace is the image of the quasi-finite locus. It is covered by the étale morphisms of IsRelativeNormalization.exists_isEtale_isPullback_of_isQuasiFiniteAt, one for each point of quasi-finiteness, which makes it open and identifies its inverse image; and (f')⁻¹(U') ⟶ U' is an isomorphism after base change to each of them, hence an isomorphism by Tag 041Y.

theorem exists_isOpenSubspace_isIso_fromPreimage_and_range_pointsMap_preimage_eq
    {X Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : X ⟶ Y} {ν : Y' ⟶ Y} {f' : X ⟶ Y'}
    (h : IsRelativeNormalization B S hS f ν f')
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') (hft : IsFiniteType B S hS f)
    (hsep : IsSeparated B S hS f) :
    ∃ U' : Subfunctor Y', IsOpenSubspace B S hS U' ∧ IsIso (U'.fromPreimage f') ∧
      Set.range (pointsMap B S hS (U'.preimage f').toFunctor (U'.preimage f').ι) =
        {x : points B S hS X | IsQuasiFiniteAt B S hS f x}

AlgebraicGeometry.Space.exists_isOpenSubspace_isIso_fromPreimage_toNormalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremFiniteTypeSeparated.lean, line 388. The attribute's comment: “both numbered conclusions, at the normalization of Y in X constructed in Definition 0822”.

Stacks 082I, at the normalization of Definition 0822. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is of finite type and separated, and let X ⟶ Y' ⟶ Y be the normalization of Y in X constructed in Definition 0822 (it exists since f is quasi-compact and quasi-separated). Then there is an open subspace U' ⊆ Y' such that (f')⁻¹(U') ⟶ U' is an isomorphism and the point set of (f')⁻¹(U') is the set of points of X at which f is quasi-finite.

theorem exists_isOpenSubspace_isIso_fromPreimage_toNormalizationInQcqs
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hft : IsFiniteType B S hS f.hom)
    (hsep : IsSeparated B S hS f.hom) :
    ∃ U' : Subfunctor (normalizationInQcqs B S hS f hft.2
        (isQuasiSeparated_of_isSeparated B S hS hsep)).obj,
      IsOpenSubspace B S hS U' ∧
      IsIso (U'.fromPreimage (toNormalizationInQcqs f hft.2
        (isQuasiSeparated_of_isSeparated B S hS hsep)).hom) ∧
      Set.range (pointsMap B S hS (U'.preimage (toNormalizationInQcqs f hft.2
          (isQuasiSeparated_of_isSeparated B S hS hsep)).hom).toFunctor
          (U'.preimage (toNormalizationInQcqs f hft.2
            (isQuasiSeparated_of_isSeparated B S hS hsep)).hom).ι) =
        {x : points B S hS X.obj | IsQuasiFiniteAt B S hS f.hom x}

Tag 082J, a lemma

Tag 082J in the Stacks Project.

AlgebraicGeometry.Space.NormalizationInData.isIntegralHom_fromNorm_of_isQuasiFinite_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremQuasiFinite.lean, line 290. The attribute's comment: “the normalization morphism is integral”.

Stacks 0ABS and 082J, integrality of the normalization morphism. Let f : X ⟶ Y be a quasi-finite separated morphism of algebraic spaces over S and let ν : Y' ⟶ Y, f' : X ⟶ Y' be the normalization of Y in X. Then ν is integral.

Over a surjective étale scheme chart w : W ⟶ Y the chart description of the normalization identifies the base change of ν with the morphism fromNormalization of the induced morphism of schemes W ×_Y X ⟶ W, which is integral; condition (3) of Tag 03ZQ promotes that to integrality of ν. The chart description is applicable because f is representable by Tag 0418, quasi-compact, and separated, hence quasi-separated.

theorem isIntegralHom_fromNorm_of_isQuasiFinite_isSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f) :
    IsIntegralHom B S hS N.fromNorm

AlgebraicGeometry.Space.NormalizationInData.isOpenImmersion_toNorm_of_isQuasiFinite_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremQuasiFinite.lean, line 311. The attribute's comment: “the canonical morphism to the normalization is an open immersion”.

Stacks 0ABS and 082J, the open immersion. Let f : X ⟶ Y be a quasi-finite separated morphism of algebraic spaces over S and let ν : Y' ⟶ Y, f' : X ⟶ Y' be the normalization of Y in X. Then f' is an open immersion.

By Tag 0ABR the image U' in Y' of the quasi-finite locus of f is an open subspace whose inverse image under f' is that locus and over which f' restricts to an isomorphism. Local quasi-finiteness makes the locus the whole of X, so both the inclusion of the inverse image and the restriction of f' are isomorphisms, and f' is their composite with the inclusion of U'.

theorem isOpenImmersion_toNorm_of_isQuasiFinite_isSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f) :
    IsOpenImmersion B S hS N.toNorm

AlgebraicGeometry.Space.NormalizationInData.isQuasiCompact_toNorm_of_isQuasiFinite_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremQuasiFinite.lean, line 342. The attribute's comment: “the canonical morphism to the normalization is quasi-compact”.

Stacks 0ABS and 082J, quasi-compactness of the open immersion. Let f : X ⟶ Y be a quasi-finite separated morphism of algebraic spaces over S and let ν : Y' ⟶ Y, f' : X ⟶ Y' be the normalization of Y in X. Then f' is quasi-compact.

This is Tag 03KS applied to the factorization f = f' ≫ ν: the composite is quasi-compact because f is quasi-finite, and ν is quasi-separated because an integral morphism is separated.

theorem isQuasiCompact_toNorm_of_isQuasiFinite_isSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f) :
    IsQuasiCompact B S hS N.toNorm

AlgebraicGeometry.Space.isQuasiAffineHom_of_isQuasiFinite_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremQuasiFinite.lean, line 369. The attribute's comment: “a quasi-finite separated morphism is quasi-affine”. References: EGA IV (18.12.12), “more general”; EGA IV (8.11.2), “more general”.

Stacks 0ABS and 082J, quasi-affineness. A quasi-finite separated morphism of algebraic spaces over S is quasi-affine.

Such a morphism is representable by Tag 0418, so each of its represented base changes is a morphism of schemes which is separated, locally of finite type, locally quasi-finite and quasi-compact, hence quasi-affine by Tag 02LR — the statement for schemes, proved there by exactly the factorization through the relative normalization that the source uses here.

theorem isQuasiAffineHom_of_isQuasiFinite_isSeparated
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f) :
    IsQuasiAffineHom B S hS f

Tag 082K, a lemma

Tag 082K in the Stacks Project.

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

Stacks 082K, Zariski's main theorem, the finite factorization. Let f : X ⟶ Y be a quasi-finite separated morphism of algebraic spaces over S, with Y quasi-compact and quasi-separated. Then f = π ∘ j with j : X ⟶ T a quasi-compact open immersion into an algebraic space T and π : T ⟶ Y finite.

theorem exists_isOpenImmersion_isFinite_comp_eq_of_isQuasiFinite
    (f : X ⟶ Y) (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y) :
    ∃ (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (j : X ⟶ T) (π : T ⟶ Y),
      IsAlgebraicSpace B S hS T ∧ IsOpenImmersion B S hS j ∧ IsQuasiCompact B S hS j ∧
        IsFinite B S hS π ∧ j ≫ π = f

Tag 0874, a lemma

Tag 0874 in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenImmersion_isFinitePresentation_comp_eq_of_isQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiMainTheoremFinitePresentationUnconditional.lean, line 51.

Stacks 0874. Let f : X ⟶ Y be a quasi-finite separated morphism of algebraic spaces over S which is locally of finite presentation, with Y quasi-compact and quasi-separated. Then f = π ∘ j with j : X ⟶ T a quasi-compact open immersion into an algebraic space T and π : T ⟶ Y finite and of finite presentation.

theorem exists_isOpenImmersion_isFinitePresentation_comp_eq_of_isQuasiFinite
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hqf : IsQuasiFinite B S hS f) (hsep : IsSeparated B S hS f)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (hfp : IsLocallyOfFinitePresentation B S hS f) :
    ∃ (T : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (j : X ⟶ T) (π : T ⟶ Y),
      IsAlgebraicSpace B S hS T ∧ IsOpenImmersion B S hS j ∧ IsQuasiCompact B S hS j ∧
        IsFinite B S hS π ∧ IsFinitePresentation B S hS π ∧ j ≫ π = f

Sources

LeanAlgebraicGeometry.Space.IsRelativeNormalization.isIso_of_isIntegralHom · AlgebraicGeometry.Space.exists_isOpenSubspace_isIso_fromPreimage_of_isFinite · AlgebraicGeometry.Space.IsRelativeNormalization.exists_isOpenSubspace_isIso_fromPreimage_and_range_pointsMap_preimage_eq · AlgebraicGeometry.Space.exists_isOpenSubspace_isIso_fromPreimage_toNormalizationInQcqs · AlgebraicGeometry.Space.NormalizationInData.isIntegralHom_fromNorm_of_isQuasiFinite_isSeparated · AlgebraicGeometry.Space.NormalizationInData.isOpenImmersion_toNorm_of_isQuasiFinite_isSeparated · AlgebraicGeometry.Space.NormalizationInData.isQuasiCompact_toNorm_of_isQuasiFinite_isSeparated · AlgebraicGeometry.Space.isQuasiAffineHom_of_isQuasiFinite_isSeparated

Section76.35 Applications of Zariski's Main Theorem, I #

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

Tag 0A4X, a lemma

Tag 0A4X in the Stacks Project.

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

Stacks 0A4X, conditions (2) and (3). A proper morphism of algebraic spaces over S is locally quasi-finite exactly when the point space of its fibre over every field-valued point of its target is discrete.

A proper morphism is locally of finite type, and for a morphism locally of finite type the two conditions are compared by Stacks 06RW.

theorem isProper_and_isLocallyQuasiFinite_iff_isProper_and_discreteFibres
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (IsProper B S hS f ∧ IsLocallyQuasiFinite B S hS f) ↔
      (IsProper B S hS f ∧ ∀ p : FieldValuedPoint B S hS Y,
        DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f)))

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

Stacks 0A4X, conditions (3) and (4). A morphism of algebraic spaces over S is proper exactly when it is universally closed, separated and locally of finite type.

Properness of Stacks 03ZM is separatedness together with being of finite type and universally closed, and being of finite type is being locally of finite type together with quasi-compactness; quasi-compactness is implied by universal closedness alone, by Stacks 04XW, so it is not an extra condition. Conditions (3) and (4) of Stacks 0A4X share their discreteness clause and differ only by this comparison.

theorem isProper_iff_universallyClosed_isSeparated_isLocallyOfFiniteType
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsProper B S hS f ↔
      UniversallyClosed B S hS f ∧ IsSeparated B S hS f ∧ IsLocallyOfFiniteType B S hS f

AlgebraicGeometry.Space.isFinite_of_isProper_of_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperQuasiFinite.lean, line 425. The attribute's comment: “condition (2) implies condition (1)”. References: EGA III (4.4.11), “proper q-finite ⇒ finite”; EGA IV (18.12.4), “proper q-finite⇒finite”; EGA III (4.4.2), “c) => a)”.

Stacks 0A4X, condition (2) implies condition (1). A proper, locally quasi-finite morphism of algebraic spaces over S is finite.

Every point of |Y| has an étale neighbourhood over which f becomes finite, by AlgebraicGeometry.Space.exists_etale_isFinite_pullback_snd_of_isProper. Replacing such a neighbourhood by the open subspace of Y it sweeps out, which receives a surjective étale chart from it by Stacks 06NF, finiteness descends along that chart by Stacks 03ZQ; the resulting open subspaces cover |Y|, indexed by the points of the underlying scheme of an étale atlas of Y so that the index type has the right size, and finiteness is Zariski-local on the target, again by Stacks 03ZQ.

theorem isFinite_of_isProper_of_isLocallyQuasiFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hp : IsProper B S hS f) (hqf : IsLocallyQuasiFinite B S hS f) :
    IsFinite B S hS f

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

Stacks 0A4X, condition (1) implies condition (2). A finite morphism of algebraic spaces over S is proper and locally quasi-finite.

Properness is the second half of the characterization of finiteness as affineness together with properness, Stacks 04NZ, and local quasi-finiteness is the first half of quasi-finiteness of a finite morphism, Stacks 04NY.

theorem isProper_and_isLocallyQuasiFinite_of_isFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsFinite B S hS f) :
    IsProper B S hS f ∧ IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Space.isProper_and_discreteFibres_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperQuasiFinite.lean, line 490. The attribute's comment: “condition (1) implies condition (3)”. References: EGA IV (18.12.4), “finite⇒proper+discrete”; EGA II (6.1.7), “discrete fibres”; EGA III (4.4.2), “a) => c)”.

Stacks 0A4X, condition (1) implies condition (3). A finite morphism of algebraic spaces over S is proper and the point space of its fibre over every field-valued point of its target is discrete.

theorem isProper_and_discreteFibres_of_isFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsFinite B S hS f) :
    IsProper B S hS f ∧ ∀ p : FieldValuedPoint B S hS Y,
      DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f))

AlgebraicGeometry.Space.universallyClosed_isSeparated_isLocallyOfFiniteType_and_discreteFibres_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperQuasiFinite.lean, line 502. The attribute's comment: “condition (1) implies condition (4)”.

Stacks 0A4X, condition (1) implies condition (4). A finite morphism of algebraic spaces over S is universally closed, separated and locally of finite type, and the point space of its fibre over every field-valued point of its target is discrete.

theorem universallyClosed_isSeparated_isLocallyOfFiniteType_and_discreteFibres_of_isFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsFinite B S hS f) :
    UniversallyClosed B S hS f ∧ IsSeparated B S hS f ∧ IsLocallyOfFiniteType B S hS f ∧
      ∀ p : FieldValuedPoint B S hS Y,
        DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f))

AlgebraicGeometry.Space.isFinite_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperQuasiFiniteTfae.lean, line 89. The attribute's comment: “the four conditions collected as a TFAE”. References: EGA IV (18.12.4); EGA III (4.4.11), “proper q-finite ⇒ finite”; EGA III (4.4.2), “a) <=> c)”.

Stacks 0A4X, the four conditions collected as a List.TFAE. For a morphism f : X ⟶ Y of algebraic spaces over S the following are equivalent: f is finite; f is proper and locally quasi-finite; f is proper and the point space of its fibre over every field-valued point of Y is discrete; f is universally closed, separated and locally of finite type, and the point space of its fibre over every field-valued point of Y is discrete.

The entries are listed in the source's numbering, and each is the proposition the corresponding pairwise comparison in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperQuasiFinite.lean speaks about, from which this equivalence is assembled.

theorem isFinite_tfae (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [IsFinite B S hS f,
        IsProper B S hS f ∧ IsLocallyQuasiFinite B S hS f,
        IsProper B S hS f ∧ ∀ p : FieldValuedPoint B S hS Y,
          DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f)),
        UniversallyClosed B S hS f ∧ IsSeparated B S hS f ∧ IsLocallyOfFiniteType B S hS f ∧
          ∀ p : FieldValuedPoint B S hS Y,
            DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f))]

Tag 0A4Y, a lemma

Tag 0A4Y in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperQuasiFinite.lean, line 530.

Stacks 0A4Y. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S and let y be a point of |Y| such that f is quasi-finite at every point of |X| lying over y. Then y has an open neighbourhood V ⊆ Y over which f becomes finite, in the sense that the base change f^{-1}(V) ⟶ V is finite.

The locus in |X| where f is quasi-finite is open — that is Stacks 04NW, in the point-set form of part (1) of Stacks 0ABM — so its complement Z is closed; f is universally closed, hence closed, so the image of Z is closed in |Y|, and the hypothesis at y says exactly that y is not in that image. Take for V the open subspace of Y with point set the complement of the image of Z, which exists by part (1) of Stacks 03BZ. The base change f^{-1}(V) ⟶ V is proper, and it is locally quasi-finite because each of its points maps to a point of |X| whose image in |Y| avoids the image of Z, hence lies outside Z, and quasi-finiteness at a point transfers to a base change by part (2) of Stacks 0ABM. It is therefore finite by Stacks 0A4X.

theorem exists_isOpenSubspace_isFinite_pullback_snd_of_isProper
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hp : IsProper B S hS f) (y : points B S hS Y)
    (hqf : ∀ x : points B S hS X, pointsMap B S hS X f x = y → IsQuasiFiniteAt B S hS f x) :
    ∃ V : Subfunctor Y, IsOpenSubspace B S hS V ∧
      y ∈ Set.range (pointsMap B S hS V.toFunctor V.ι) ∧
      IsFinite B S hS (pullback.snd f V.ι)

Tag 0AEJ, a lemma

Tag 0AEJ in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isClosedSubspace_isFinite_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperFiniteImageNearFibre.lean, line 318.

Stacks 0AEJ. Let h : X ⟶ Y, f : X ⟶ T and g : Y ⟶ T be morphisms of algebraic spaces over S with h ≫ g = f, with f proper and g separated and locally of finite type, and let b ∈ |T| be represented by a field-valued point p with field of definition k. If the image of |X_k| in |Y_k| is finite, or if T is decent and the image in |Y| of the set-theoretic fibre of f over b is finite, then b has an open neighbourhood U ⊆ T and X ×_T U ⟶ Y ×_T U factors through a closed subspace of Y ×_T U which is finite over U.

theorem exists_isOpenSubspace_isClosedSubspace_isFinite_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)
    (comm : h ≫ g = f) (b : points B S hS T) (p : FieldValuedPoint B S hS T)
    (hp : p.class B S hS T = b) (hf : IsProper B S hS f)
    (hg_sep : IsSeparated B S hS g) (hg_lft : IsLocallyOfFiniteType B S hS g)
    (hfinite :
      Set.Finite (Set.range (pointsMap B S hS (pullback f (fieldMorphism B S hS T p))
        (pullback.map f (fieldMorphism B S hS T p) g (fieldMorphism B S hS T p) h
          (𝟙 _) (𝟙 _) (by simp [comm]) (by simp)))) ∨
      (Set.Finite (pointsMap B S hS X h ''
          {x : points B S hS X | pointsMap B S hS X f x = b}) ∧
        IsDecentSpace B S hS T)) :
    ∃ U : Subfunctor T,
      IsOpenSubspace B S hS U ∧
      b ∈ Set.range (pointsMap B S hS U.toFunctor U.ι) ∧
      ∃ Z : Subfunctor (pullback g U.ι),
        IsClosedSubspace B S hS Z ∧
        (∃ m : pullback f U.ι ⟶ Z.toFunctor, m ≫ Z.ι =
          pullback.map f U.ι g U.ι h (𝟙 _) (𝟙 _) (by simp [comm]) (by simp)) ∧
        IsFinite B S hS (Z.ι ≫ pullback.snd g U.ι)

Sources

LeanAlgebraicGeometry.Space.isProper_and_isLocallyQuasiFinite_iff_isProper_and_discreteFibres · AlgebraicGeometry.Space.isProper_iff_universallyClosed_isSeparated_isLocallyOfFiniteType · AlgebraicGeometry.Space.isFinite_of_isProper_of_isLocallyQuasiFinite · AlgebraicGeometry.Space.isProper_and_isLocallyQuasiFinite_of_isFinite · AlgebraicGeometry.Space.isProper_and_discreteFibres_of_isFinite · AlgebraicGeometry.Space.universallyClosed_isSeparated_isLocallyOfFiniteType_and_discreteFibres_of_isFinite · AlgebraicGeometry.Space.isFinite_tfae · AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_isProper

Section76.36 Stein factorization #

Section 76.36 of the Stacks Project, Tag 0A18. 10 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A19, a lemma

Tag 0A19 in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_toNormalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 174. The attribute's comment: “part (1): the morphism to the normalization is universally closed”.

Stacks 0A19, clause (1): f' is universally closed. By Stacks 04NX part (1), since the composite f = f' ≫ π is universally closed and π is separated.

theorem universallyClosed_toNormalizationIn
    (hfuc : UniversallyClosed B S hS f.hom) :
    UniversallyClosed B S hS (toNormalizationIn B S hS E C f hqc hqc' hid).left.hom

AlgebraicGeometry.Space.isQuasiCompact_toNormalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 186. The attribute's comment: “part (1): the morphism to the normalization is quasi-compact”.

Stacks 0A19, clause (1): f' is quasi-compact. By Stacks 03KS, since the composite f = f' ≫ π is quasi-compact — a universally closed morphism is quasi-compact by Stacks 04XW — and π is quasi-separated.

theorem isQuasiCompact_toNormalizationIn
    (hfuc : UniversallyClosed B S hS f.hom) :
    IsQuasiCompact B S hS (toNormalizationIn B S hS E C f hqc hqc' hid).left.hom

AlgebraicGeometry.Space.isQuasiSeparated_toNormalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 197. The attribute's comment: “part (1): the morphism to the normalization is quasi-separated”.

Stacks 0A19, clause (1): f' is quasi-separated. By Stacks 03KR, since the composite f = f' ≫ π is quasi-separated. Nothing is required of π.

theorem isQuasiSeparated_toNormalizationIn
    (hfqs : IsQuasiSeparated B S hS f.hom) :
    IsQuasiSeparated B S hS (toNormalizationIn B S hS E C f hqc hqc' hid).left.hom

AlgebraicGeometry.Space.isSurjective_toNormalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 253. The attribute's comment: “part (1): the morphism to the normalization is surjective”.

Stacks 0A19, clause (1): f' is surjective. The scheme-theoretic image of f' inside the normalization Y' of Y in X is a closed subspace, hence integral over Y, through which f factors; the characterization of Stacks 0823 therefore retracts Y' onto it, and f' has closed image because it is universally closed.

theorem isSurjective_toNormalizationIn
    (P : RelativeSpecUniversalProperty B S hS E C) (D : IntegralAlgebraDictionary B S hS E)
    (hloc : (pushforwardAlgebra B S hS (Over.mk f)).IsIntegralLocalOnAffineCharts)
    (hfuc : UniversallyClosed B S hS f.hom) :
    IsSurjective B S hS (toNormalizationIn B S hS E C f hqc hqc' hid).left.hom

AlgebraicGeometry.Space.isIntegralHom_normalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 274. The attribute's comment: “part (2): the normalization morphism is integral”.

Stacks 0A19, clause (2): π is integral. This is clause (1) of Stacks 0823 for the same factorization, proved as AlgebraicGeometry.Space.isRelativeNormalization_toNormalizationIn, and it carries that theorem's inputs: the universal property P of the relative spectrum, the dictionary D of Stacks 03ZP between integral morphisms affine over Y and integral algebras, and the clause hloc of Stacks 0820 that a locally integral section over an affine chart is integral.

theorem isIntegralHom_normalizationIn
    (P : RelativeSpecUniversalProperty B S hS E C) (D : IntegralAlgebraDictionary B S hS E)
    (hloc : (pushforwardAlgebra B S hS (Over.mk f)).IsIntegralLocalOnAffineCharts) :
    IsIntegralHom B S hS (normalizationIn B S hS E f hqc').obj.hom.hom

AlgebraicGeometry.Space.isRelativeNormalization_steinFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 288. The attribute's comment: “part (5): the intermediate space is the normalization of Y in X”.

Stacks 0A19, clause (5): Y' is the normalization of Y in X. The factorization f = f' ≫ π has the two properties of Stacks 0823 which characterize the normalization: π is integral, and every factorization of f through an integral morphism of algebraic spaces to Y receives a unique compatible morphism from Y'.

theorem isRelativeNormalization_steinFactorization
    (P : RelativeSpecUniversalProperty B S hS E C) (D : IntegralAlgebraDictionary B S hS E)
    (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

AlgebraicGeometry.Space.steinFactorization_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationFlatBaseChange.lean, line 297. The attribute's comment: “all five clauses and the compatibility with flat base change, for the factorization through the normalization of Stacks 0822”. References: EGA III (4.3.4), “more general”; EGA III (7.8.10), “partial”.

Stacks 0A19 (Stein factorization). Let f : X ⟶ Y be a universally closed and quasi-separated morphism of algebraic spaces over S. It is quasi-compact (Stacks 04XW); let Y' be the normalization of Y in X (Stacks 0822), with π : Y' ⟶ Y and the canonical f' : X ⟶ Y'. Then f = π ∘ f', and

f' is universally closed, quasi-compact, quasi-separated and surjective;

π is integral;

f'_* 𝒪_X = 𝒪_{Y'}: the structure map 𝒪_{Y'} ⟶ f'_* 𝒪_X is an isomorphism;

Y' = \underline{Spec}_Y(f_* 𝒪_X): π is affine and the map π_* 𝒪_{Y'} ⟶ f_* 𝒪_X of 𝒪_Y-algebras induced by f' is an isomorphism;

Y' is the normalization of Y in X, here in the characterizing form of Stacks 0823 (it is that normalization by construction).

Moreover formation of the factorization commutes with flat base change: for a flat g : Y₁ ⟶ Y, a fibre product X₁ = Y₁ ×_Y X with f₁ : X₁ ⟶ Y₁, a fibre product P = Y₁ ×_Y Y' with p : P ⟶ Y₁, and the base change h : X₁ ⟶ P of f', the morphism f₁ is again universally closed and quasi-separated (so quasi-compact), the factorization X₁ ⟶ P ⟶ Y₁ is the normalization of Y₁ in X₁ in the sense of Stacks 0823, and it is identified with the factorization of f₁ through its own normalization by a unique isomorphism compatible with both factorizations.

theorem steinFactorization_of_universallyClosed (huc : UniversallyClosed B S hS f.hom)
    (hfqs : IsQuasiSeparated B S hS f.hom) :
    let hfqc := isQuasiCompact_of_universallyClosed B S hS X.2 Y.2 f.hom huc
    toNormalizationInQcqs f hfqc hfqs ≫ normalizationInQcqsHom B S hS f hfqc hfqs = f ∧
      (UniversallyClosed B S hS (toNormalizationInQcqs f hfqc hfqs).hom ∧
        IsQuasiCompact B S hS (toNormalizationInQcqs f hfqc hfqs).hom ∧
        IsQuasiSeparated B S hS (toNormalizationInQcqs f hfqc hfqs).hom ∧
        IsSurjective B S hS (toNormalizationInQcqs f hfqc hfqs).hom) ∧
      IsIntegralHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom ∧
      IsIso (smallEtaleRingedToposHom B S hS (toNormalizationInQcqs f hfqc hfqs)).fSharp ∧
      (IsAffineHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom ∧
        IsIso (pushforwardAlgebraMap B S hS (toNormalizationInQcqsOver f hfqc hfqs))) ∧
      IsRelativeNormalization B S hS f.hom (normalizationInQcqsHom B S hS f hfqc hfqs).hom
        (toNormalizationInQcqs f hfqc hfqs).hom ∧
      ∀ {X₁ Y₁ P : AlgebraicSpaces B S hS} {g : Y₁ ⟶ Y} {f₁ : X₁ ⟶ Y₁} {g' : X₁ ⟶ X},
        IsPullback g' f₁ f g → IsFlat B S hS g.hom →
        ∀ {q : P ⟶ normalizationInQcqs B S hS f hfqc hfqs} {p : P ⟶ Y₁},
          IsPullback q p (normalizationInQcqsHom B S hS f hfqc hfqs) g →
          ∀ h : X₁ ⟶ P, h ≫ q = g' ≫ toNormalizationInQcqs f hfqc hfqs → h ≫ p = f₁ →
            UniversallyClosed B S hS f₁.hom ∧
              ∃ (hf₁qc : IsQuasiCompact B S hS f₁.hom) (hf₁qs : IsQuasiSeparated B S hS f₁.hom),
                IsRelativeNormalization B S hS f₁.hom p.hom h.hom ∧
                  ∃! e : normalizationInQcqs B S hS f₁ hf₁qc hf₁qs ≅ P,
                    toNormalizationInQcqs f₁ hf₁qc hf₁qs ≫ e.hom = h ∧
                      e.hom ≫ p = normalizationInQcqsHom B S hS f₁ hf₁qc hf₁qs

AlgebraicGeometry.Space.isSurjective_toNormalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationGeneral.lean, line 208. The attribute's comment: “clause (1): the morphism f' : X ⟶ Y' to the normalization of Y in X is surjective, for a universally closed f”.

f' is surjective, which is the remaining assertion of clause (1) of Stacks 0A19. The factorization f = f' ≫ π has the characterizing property of Stacks 0823 (AlgebraicGeometry.Space.isRelativeNormalization_normalizationInQcqs), and f' is quasi-compact and universally closed, so AlgebraicGeometry.Space.isSurjective_of_isRelativeNormalization applies.

theorem isSurjective_toNormalizationInQcqs (hfuc : UniversallyClosed B S hS f.hom) :
    IsSurjective B S hS (toNormalizationInQcqs f hfqc hfqs).hom

Tag 0E1C, a lemma

Tag 0E1C in the Stacks Project.

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

Stacks 0E1C. Let f : X ⟶ Y be a universally closed and quasi-separated morphism of algebraic spaces over S and X ⟶ Y' ⟶ Y its Stein factorization of Stacks 0A19, the normalization π : Y' ⟶ Y of Y in X. Assume in addition that f is locally of finite type and that Y is affine, represented by an affine T. Then Y' is represented by an affine T', with π represented by p : T' ⟶ T, and for every point y of Y the fibre π⁻¹({y}) is finite and the residue field extension κ(y')/κ(y) is finite for every y' in it.

theorem exists_isAffine_finite_fibres_normalizationInQcqs {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (huc : UniversallyClosed B S hS f.hom) (hfqs : IsQuasiSeparated B S hS f.hom)
    (hlft : IsLocallyOfFiniteType B S hS f.hom)
    (T : BigFppfOver B S hS) (hT : IsAffine ((BigFppfOver.toScheme B S hS).obj T))
    (eY : yoneda.obj T ⟶ Y.obj) [IsIso eY] :
    ∃ (T' : BigFppfOver B S hS) (p : T' ⟶ T)
      (e : yoneda.obj T' ⟶ (normalizationInQcqs B S hS f
        (isQuasiCompact_of_universallyClosed B S hS X.property Y.property f.hom huc) hfqs).obj),
      IsAffine ((BigFppfOver.toScheme B S hS).obj T') ∧ IsIso e ∧
      yoneda.map p ≫ eY = e ≫ (normalizationInQcqsHom B S hS f
        (isQuasiCompact_of_universallyClosed B S hS X.property Y.property f.hom huc) hfqs).hom ∧
      ∀ y : (BigFppfOver.toScheme B S hS).obj T,
        (((BigFppfOver.toScheme B S hS).map p) ⁻¹' {y}).Finite ∧
        ∀ y' ∈ ((BigFppfOver.toScheme B S hS).map p) ⁻¹' {y},
          (((BigFppfOver.toScheme B S hS).map p).residueFieldMap y').hom.Finite

Tag 0A1A, a lemma

Tag 0A1A in the Stacks Project.

AlgebraicGeometry.Space.connectedSpace_geometricFiber_iff_forall_scheme_etaleNeighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GeometricFibreConnected.lean, line 270.

Stacks 0A1A. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S of a big fppf site and let y be a geometric point of Y. The geometric fibre of f above y is connected if and only if, for every étale neighbourhood of y whose underlying algebraic space is isomorphic to a scheme W of the site, the base change of f to that neighbourhood has connected fibre above the point of W underlying the chosen lift of y.

Both fibres are presheaf fibre products, and the fibre above the point of W is the one above the residue field point there (AlgebraicGeometry.Space.representedResidueFieldPointInNeighborhood).

theorem connectedSpace_geometricFiber_iff_forall_scheme_etaleNeighborhood
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (y : GeometricPoint B S hS Y) :
    ConnectedPullback B S hS f (yonedaEquiv.symm y.val.value) ↔
      ∀ (U : EtaleNeighborhood B S hS Y hY y) (W : BigFppfOver B S hS)
        (e : U.space ≅ yoneda.obj W),
        ConnectedPullback B S hS f
          (yonedaEquiv.symm (representedResidueFieldPointInNeighborhood B S hS U W e).value ≫
            U.toBase)

Tag 0A1B, a theorem

Tag 0A1B in the Stacks Project.

AlgebraicGeometry.Space.isFinite_normalizationInQcqsHom_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NormalizationInFiniteOfProper.lean, line 251. The attribute's comment: “part (2): for f proper with Y locally Noetherian, the morphism pi : Y' -> Y from the normalization of Y in X (Stacks 0822), through which f factors as X -> Y' -> Y, is finite”.

Stacks 0A1B, clause (2): π : Y' ⟶ Y is finite. For a proper morphism f : X ⟶ Y of algebraic spaces with Y locally Noetherian, the normalization ν : Y' ⟶ Y of Y in X (Stacks 0822) is a finite morphism: it is the relative spectrum of the integral closure 𝒪' of 𝒪_Y in f_* 𝒪_X, which is a finite 𝒪_Y-algebra.

theorem isFinite_normalizationInQcqsHom_of_isProper (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    IsFinite B S hS (normalizationInQcqsHom B S hS f hf.2.1.2
      (isQuasiSeparated_of_isSeparated B S hS hf.1)).hom

AlgebraicGeometry.Space.isProper_toNormalizationIn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorization.lean, line 362. The attribute's comment: “part (1): the morphism to the normalization is proper”.

Stacks 0A1B, clause (1): f' is proper. By Stacks 04NX part (2), since the composite f = f' ≫ π is proper and π is separated.

theorem isProper_toNormalizationIn (hf : IsProper B S hS f.hom) :
    IsProper B S hS (toNormalizationIn B S hS E C f hqc hqc' hid).left.hom

AlgebraicGeometry.Space.isProper_and_connectedPullback_toNormalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationNoetherianConnectedFibres.lean, line 55. The attribute's comment: “part (1): for f proper with Y locally Noetherian, the morphism f' : X -> Y' to the normalization of Y in X (Stacks 0822), with f = pi o f', is proper and its geometric fibres are connected”.

Stacks 0A1B, clause (1). Let f : X ⟶ Y be a proper morphism of algebraic spaces with Y locally Noetherian. The morphism f' : X ⟶ Y' to the normalization of Y in X (Stacks 0822), through which f factors as f = π ∘ f', is proper, and its geometric fibres are connected: for every geometric point ȳ of Y' the fibre X ×_{Y'} ȳ has connected point space.

theorem isProper_and_connectedPullback_toNormalizationInQcqs (f : X ⟶ Y)
    (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    IsProper B S hS
        (toNormalizationInQcqs f hf.2.1.2 (isQuasiSeparated_of_isSeparated B S hS hf.1)).hom ∧
      ∀ y : GeometricPoint B S hS (normalizationInQcqs B S hS f hf.2.1.2
          (isQuasiSeparated_of_isSeparated B S hS hf.1)).1,
        ConnectedPullback B S hS
          (toNormalizationInQcqs f hf.2.1.2 (isQuasiSeparated_of_isSeparated B S hS hf.1)).hom
          (yonedaEquiv.symm y.val.value)

Declarations registered for the tag:

AlgebraicGeometry.Space.isIso_fSharp_toNormalizationInQcqs, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationNoetherianQcqs.lean, line 84 (StacksFrontier): “part (3): f'_O_X = O_{Y'} for the factorization X -> Y' -> Y through the normalization of Stacks 0822 -- the structure map O_{Y'} -> f'_O_X is an isomorphism of sheaves of rings; proved for every quasi-compact, quasi-separated, universally closed f, which a proper f is”.
AlgebraicGeometry.Space.isIso_pushforwardAlgebraMap_toNormalizationInQcqsOver_of_universallyClosed, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationNoetherianQcqs.lean, line 90 (StacksFrontier): “part (4): Y' = Spec_Y(f_O_X) for the factorization through the normalization of Stacks 0822 -- pi is affine and the map pi_O_{Y'} -> f_*O_X induced by f' is an isomorphism of O_Y-algebras; proved for every quasi-compact, quasi-separated, universally closed f, which a proper f is”.
AlgebraicGeometry.Space.isRelativeNormalization_normalizationInQcqs, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationNoetherianQcqs.lean, line 96 (StacksFrontier): “part (5): the intermediate space Y' of the factorization X -> Y' -> Y is the normalization of Y in X, in the characterization of Stacks 0823; proved for every quasi-compact quasi-separated f, which a proper f is”.

Tag 0A1C, a theorem

Tag 0A1C in the Stacks Project.

AlgebraicGeometry.Space.isProper_toNormalizationInQcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationGeneral.lean, line 177. The attribute's comment: “clause (1): the morphism f' : X ⟶ Y' to the normalization of Y in X is proper, for a proper f and an arbitrary base Y”.

Clause (1) of Stacks 0A1C: f' is proper. By Stacks 04NX part (2), since the composite f = f' ≫ π is proper and π is separated.

theorem isProper_toNormalizationInQcqs (hf : IsProper B S hS f.hom) :
    IsProper B S hS (toNormalizationInQcqs f hfqc hfqs).hom

AlgebraicGeometry.Space.steinFactorization_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationGeneral.lean, line 242. The attribute's comment: “clause (1) properness together with the surjectivity of f', clause (2) integrality of pi, clause (4) and clause (5), for a proper morphism of algebraic spaces over an arbitrary base. Clause (3) and the connectedness of the geometric fibres of f' in clause (1) are not asserted”. References: EGA III (7.8.10), “partial”.

Stacks 0A1C, clauses (1) properness, (2), (4) and (5). Let f : X ⟶ Y be a proper morphism of algebraic spaces over S, let Y' be the normalization of Y in X and let f = f' ≫ π be the factorization of Stacks 0822. Then

f' is proper, and surjective — the properness assertion of clause (1), together with the surjectivity that clause (1) of Stacks 0A19 states separately;

π : Y' ⟶ Y is integral, clause (2) in the form the general case asserts it;

Y' = \underline{Spec}_Y(f_* 𝒪_X), clause (4), in the form of Stacks 0A0Q: the map π_* 𝒪_{Y'} ⟶ f_* 𝒪_X of 𝒪_Y-algebras induced by f' is invertible;

Y' is the normalization of Y in X, clause (5), in the sense of AlgebraicGeometry.Space.IsRelativeNormalization.

The conclusion also records the factorization equation itself.

Nothing is assumed about Y; no finiteness enters, which is the point of the general case against Stacks 0A1B. The two statements of the tag that do not appear here are clause (3) and the connectedness of the geometric fibres of f' in clause (1); the module documentation says what each would need, and AlgebraicGeometry.Space.steinFactorization_general_of_connectedFibres adds them as named inputs.

theorem steinFactorization_general (hf : IsProper B S hS f.hom) :
    toNormalizationInQcqs f hfqc hfqs ≫ normalizationInQcqsHom B S hS f hfqc hfqs = f ∧
      IsProper B S hS (toNormalizationInQcqs f hfqc hfqs).hom ∧
      IsSurjective B S hS (toNormalizationInQcqs f hfqc hfqs).hom ∧
      IsIntegralHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom ∧
      IsIso (pushforwardAlgebraMap B S hS (toNormalizationInQcqsOver f hfqc hfqs)) ∧
      IsRelativeNormalization B S hS f.hom
        (normalizationInQcqsHom B S hS f hfqc hfqs).hom
        (toNormalizationInQcqs f hfqc hfqs).hom

AlgebraicGeometry.Space.steinFactorization_general_complete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationGeneralRegistration.lean, line 191. The attribute's comment: “all five clauses, for the factorization X ⟶ Y' ⟶ Y through the normalization of Y in X (0822): f' proper with connected geometric fibres, π integral, f'_O_X = O_{Y'} as the invertibility of the structure map, Y' = Spec_Y(f_O_X) as π affine with π_O_{Y'} ≅ f_O_X, and the 0823 characterization of the normalization”.

Stacks 0A1C (Stein factorization; general case). Let f : X ⟶ Y be a proper morphism of algebraic spaces over a scheme S. Let π : Y' ⟶ Y be the normalization of Y in X (Stacks 0822, AlgebraicGeometry.Space.normalizationInQcqs, which needs f quasi-compact and quasi-separated, as a proper morphism is) and f' : X ⟶ Y' the canonical morphism, so that f = π ∘ f'. Then:

f' is proper with connected geometric fibres: for every geometric point ȳ of Y' the fibre X ×_{Y'} ȳ has connected point space;

π : Y' ⟶ Y is integral;

f'_*𝒪_X = 𝒪_{Y'}: the structure map 𝒪_{Y'} ⟶ f'_*𝒪_X of Stacks 03G8 is an isomorphism;

Y' = \underline{Spec}_Y(f_*𝒪_X): π is affine and the map π_*𝒪_{Y'} ⟶ f_*𝒪_X of 𝒪_Y-algebras induced by f' is an isomorphism;

Y' is the normalization of Y in X: the factorization has the two properties of Stacks 0823 which characterize it.

The conclusion also records the factorization f = π ∘ f' itself. No hypothesis beyond properness of f is used.

theorem steinFactorization_general_complete (f : X ⟶ Y) (hf : IsProper B S hS f.hom) :
    let hfqc := isQuasiCompact_of_universallyClosed B S hS X.2 Y.2 f.hom hf.2.2
    let hfqs := isQuasiSeparated_of_isSeparated B S hS hf.1
    toNormalizationInQcqs f hfqc hfqs ≫ normalizationInQcqsHom B S hS f hfqc hfqs = f ∧
      (IsProper B S hS (toNormalizationInQcqs f hfqc hfqs).hom ∧
        ∀ y : GeometricPoint B S hS (normalizationInQcqs B S hS f hfqc hfqs).1,
          ConnectedPullback B S hS (toNormalizationInQcqs f hfqc hfqs).hom
            (yonedaEquiv.symm y.val.value)) ∧
      IsIntegralHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom ∧
      IsIso (smallEtaleRingedToposHom B S hS (toNormalizationInQcqs f hfqc hfqs)).fSharp ∧
      (IsAffineHom B S hS (normalizationInQcqsHom B S hS f hfqc hfqs).hom ∧
        IsIso (pushforwardAlgebraMap B S hS (toNormalizationInQcqsOver f hfqc hfqs))) ∧
      IsRelativeNormalization B S hS f.hom (normalizationInQcqsHom B S hS f hfqc hfqs).hom
        (toNormalizationInQcqs f hfqc hfqs).hom

Tag 0AYI, a lemma

Tag 0AYI in the Stacks Project.

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

Stacks 0AYI. Let f : X ⟶ Y be a morphism of algebraic spaces over S such that

f is proper,

Y is integral (Stacks 0AD4, AlgebraicGeometry.Space.IsIntegralSpace) with generic point ξ,

Y is normal,

X is reduced,

every generic point of an irreducible component of |X| maps to ξ,

H⁰(X_ξ, 𝒪) = κ(ξ): for the monomorphism Spec κ(ξ) ⟶ Y from the spectrum of the residue field at ξ (Stacks 0EMW) and the fibre X_ξ = X ×_Y Spec κ(ξ), pullback of global functions κ(ξ) = Γ(Spec κ(ξ), 𝒪) ⟶ Γ(X_ξ, 𝒪) along the projection is bijective.

Then

f_* 𝒪_X = 𝒪_Y: the canonical map 𝒪_Y ⟶ f_* 𝒪_X (Stacks 03G8) is an isomorphism;

f has geometrically connected fibres: for every field k and every morphism Spec k ⟶ Y, the fibre X ×_Y Spec k has connected point space. Taking Spec k ⟶ Spec κ(y) ⟶ Y for the field extensions k of the residue field at a point y, this says that the fibre X_y is geometrically connected over κ(y).

Normality and reducedness are the étale-local properties of schemes of Stacks 03E6, as elsewhere in the library.

theorem isIso_fSharp_and_connectedPullback_of_isNormal_of_isIntegralSpace
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsProper B S hS f.hom) (hYint : IsIntegralSpace B S hS Y.1)
    {ξ : points B S hS Y.1} (hξ : IsGenericPoint ξ Set.univ)
    (hYnormal : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsNormal T))
    (hXred : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsReduced T))
    (hgen : ∀ x ∈ genericPoints (points B S hS X.1), pointsMap B S hS X.1 f.hom x = ξ)
    (h6 : Function.Bijective (globalFunctionsMap B S hS (pullback.snd f
      (ObjectProperty.homMk (residueFieldMorphism B S hS Y.1 hYint.2.1 ξ) :
        schemeSpace ((residueFieldRepresentative B S hS Y.1 hYint.2.1 ξ).1.siteObject B S hS Y.1) ⟶
          Y)))) :
    IsIso (smallEtaleRingedToposHom B S hS f).fSharp ∧
      ∀ p : FieldValuedPoint B S hS Y.1,
        ConnectedPullback B S hS f.hom (fieldMorphism B S hS Y.1 p)

Tag 0E1D, a lemma

Tag 0E1D in the Stacks Project.

AlgebraicGeometry.Space.lowerSemicontinuous_numberGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricComponentsLowerSemicontinuous.lean, line 475. References: EGA IV (15.5.9), “more general”.

Stacks 0E1D. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is proper, flat and of finite presentation. Then the function n_{X/Y} : |Y| → ℕ∞ counting the geometric connected components of the fibres of f (Stacks 0E1B, AlgebraicGeometry.Space.numberGeometricConnectedComponents) is lower semicontinuous.

theorem lowerSemicontinuous_numberGeometricConnectedComponents
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hproper : IsProper B S hS f)
    (hflat : IsFlat B S hS f) (hfp : IsFinitePresentation B S hS f) :
    LowerSemicontinuous (numberGeometricConnectedComponents B S hS f)

Tag 0E1E, a lemma

Tag 0E1E in the Stacks Project.

AlgebraicGeometry.Space.isLocallyConstant_numberGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/GeometricComponentsLocallyConstantUnconditional.lean, line 192.

Stacks 0E1E. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is proper, flat and of finite presentation, and whose geometric fibres are reduced. Then the function n_{X/Y} : |Y| → ℕ∞ counting the geometric connected components of the fibres of f (Stacks 0E1B) is locally constant.

theorem isLocallyConstant_numberGeometricConnectedComponents
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : IsProper B S hS f) (hfl : IsFlat B S hS f) (hfp : IsFinitePresentation B S hS f)
    (hred : ∀ y, IsGeometricallyReducedFibreAt B S hS f hX hY y) :
    IsLocallyConstant (numberGeometricConnectedComponents B S hS f)

Tag 0E0D, a lemma

Tag 0E0D in the Stacks Project.

AlgebraicGeometry.Space.isFinite_and_isEtale_normalizationInQcqsHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SteinFactorizationFlatProperFiniteEtale.lean, line 50. The attribute's comment: “for the Stein factorization X ⟶ Y' ⟶ Y of 0A1C, Y' the normalization of Y in X: Y' ⟶ Y is finite and étale when f is proper, flat, of finite presentation, with geometrically reduced fibres”.

Stacks 0E0D. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S, and let X ⟶ Y' ⟶ Y be its Stein factorization (Stacks 0A1C): Y' is the normalization of Y in X, AlgebraicGeometry.Space.normalizationInQcqs, with structure morphism AlgebraicGeometry.Space.normalizationInQcqsHom. If f is of finite presentation, flat, with geometrically reduced fibres (Stacks 0E08), then Y' ⟶ Y is finite étale.

theorem isFinite_and_isEtale_normalizationInQcqsHom
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (hfp : IsFinitePresentation B S hS f.hom) (hfl : IsFlat B S hS f.hom)
    (hred : ∀ y, IsGeometricallyReducedFibreAt B S hS f.hom X.2 Y.2 y) :
    let h := isQuasiCompact_isQuasiSeparated_of_isProper B S hS f hf
    IsFinite B S hS (normalizationInQcqsHom B S hS f h.1 h.2).hom ∧
      IsEtale B S hS (normalizationInQcqsHom B S hS f h.1 h.2).hom

Tag 0CWI, a lemma

Tag 0CWI in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.exists_isOpenSubspace_isClosedSubspace_isProper_of_henselianPair, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ProperPartOverHenselianPairTag.lean, line 24 (StacksFrontier): “the whole tag, on the theorem proved in ClopenLiftOverHenselianPair”.

Sources

LeanAlgebraicGeometry.Space.universallyClosed_toNormalizationIn · AlgebraicGeometry.Space.isQuasiCompact_toNormalizationIn · AlgebraicGeometry.Space.isQuasiSeparated_toNormalizationIn · AlgebraicGeometry.Space.isSurjective_toNormalizationIn · AlgebraicGeometry.Space.isIntegralHom_normalizationIn · AlgebraicGeometry.Space.isRelativeNormalization_steinFactorization · AlgebraicGeometry.Space.steinFactorization_of_universallyClosed · AlgebraicGeometry.Space.isSurjective_toNormalizationInQcqs

Section76.37 Extending properties from an open #

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

Tag 0876, a lemma

Tag 0876 in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentation_chartModule_of_isFlatOver_of_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FinitePresentationFromDenseOpen.lean, line 435. The attribute's comment: “hypotheses (1) and (2) and the conclusion are read on the etale scheme charts: they are the corresponding properties of the restriction of the module to the charts, as for Space.IsFlatOver of Tag 05VV. Hypothesis (4) is read on the open subscheme that V cuts out in each chart of the target, which by Space.preimage_chartOpenOfOpenSubspace is the chart-level inverse image of V. The conclusion is stated on a commuting square of charts of f rather than on an arbitrary chart of the source, since not every chart of the source is the source of such a square”.

Stacks 0876. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S contained in a big fppf site B which is locally of finite presentation, let F be an 𝒪_X-module which is quasi-coherent of finite type on charts and flat over Y, and let V ⊆ Y be an open subspace whose inclusion is quasi-compact and which is scheme-theoretically dense in the sense of Tag 0834. If F restricted to f⁻¹V is of finite presentation on charts, then on every commuting square of étale scheme charts the restriction of F to the chart of X is of finite presentation.

Hypothesis (3) of the source is exactly the two hypotheses hVqc and hVdense here. They give the chartwise conditions of AlgebraicGeometry.Space.isFinitePresentation_chartModule_of_isFlatOver_of_dense_open_charts by AlgebraicGeometry.Space.isRetrocompactOnCharts_of_isQuasiCompact (Stacks 03HD) and AlgebraicGeometry.Space.isSchemeTheoreticallyDenseOnCharts_of_isSchemeTheoreticallyDense (Stacks 0836), and on one commuting square of charts the statement is then Stacks 081N for the vertical morphism of schemes.

theorem isFinitePresentation_chartModule_of_isFlatOver_of_dense_open
    (hX : IsAlgebraicSpace B S hS X) {f : X ⟶ Y} (F : Modules.{u, u} B S hS X hX)
    (hf : IsLocallyOfFinitePresentation B S hS f)
    (hqc : IsQuasicoherentOnCharts B S hS hX F) (hft : IsFiniteTypeOnCharts B S hS hX F)
    (hflat : IsFlatOver B S hS hX f F)
    (V : Subfunctor Y) (hV : IsOpenSubspace B S hS V)
    (hVqc : IsQuasiCompact B S hS V.ι)
    (hVdense : IsSchemeTheoreticallyDense B S hS V)
    (hfp : IsFinitePresentationOverOpenOnCharts B S hS hX f F V hV)
    (d : ChartDiagram B S hS X Y f) :
    (chartModule B S hS hX F d.U).IsFinitePresentation

Tag 0877, a lemma

Tag 0877 in the Stacks Project.

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

Stacks 0877. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S contained in a big fppf site B which is locally of finite type and flat, and let V ⊆ Y be an open subspace whose inclusion is quasi-compact and which is scheme-theoretically dense in the sense of Tag 0834. If the restriction f⁻¹V ⟶ V of f is locally of finite presentation, then f is locally of finite presentation.

Local finite presentation is the every-étale-chart condition of Tag 03MJ, so this is AlgebraicGeometry.Space.locallyOfFinitePresentation_chartDiagram_of_fromPreimage for the commuting square of charts given by the chart data.

theorem isLocallyOfFinitePresentation_of_fromPreimage
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hlft : IsLocallyOfFiniteType B S hS f) (hflat : IsFlat B S hS f)
    (V : Subfunctor Y) (hV : IsOpenSubspace B S hS V)
    (hVqc : IsQuasiCompact B S hS V.ι)
    (hVdense : IsSchemeTheoreticallyDense B S hS V)
    (hfV : IsLocallyOfFinitePresentation B S hS (V.fromPreimage f)) :
    IsLocallyOfFinitePresentation B S hS f

Tag 0878, a lemma

Tag 0878 in the Stacks Project.

AlgebraicGeometry.Space.relativeDimensionLE_of_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/RelativeDimensionDenseOpen.lean, line 393.

Stacks 0878. A flat morphism of algebraic spaces over S locally of finite type has relative dimension at most d if its restriction over a dense open subspace of the target does, provided the morphism is locally of finite presentation or the open immersion is quasi-compact.

theorem relativeDimensionLE_of_dense_open (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (V : Subfunctor Y)
    (hV : IsOpenSubspace B S hS V)
    (hVdense : Dense (Set.range (pointsMap B S hS V.toFunctor V.ι)))
    (hflat : IsFlat B S hS f) (hlft : IsLocallyOfFiniteType B S hS f) (d : ℕ)
    (hdim : HasRelativeDimensionLE d B S hS (pullback.snd f V.ι))
    (hfin : IsLocallyOfFinitePresentation B S hS f ∨ IsQuasiCompact B S hS V.ι) :
    HasRelativeDimensionLE d B S hS f

Tag 0B4J, a lemma

Tag 0B4J in the Stacks Project.

AlgebraicGeometry.Space.isFinite_of_isFinite_over_dense_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FiniteDenseOpen.lean, line 119.

Stacks 0B4J. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat and proper. Let V be an open subspace of Y whose points are dense in the points of Y and such that the base change X_V ⟶ V of f is finite. If moreover f is locally of finite presentation or the open immersion V ⟶ Y is quasi-compact, then f is finite.

theorem isFinite_of_isFinite_over_dense_open
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hproper : IsProper B S hS f)
    (V : Subfunctor Y) (hV : IsOpenSubspace B S hS V)
    (hVdense : Dense (Set.range (pointsMap B S hS V.toFunctor V.ι)))
    (hfinite : IsFinite B S hS (pullback.snd f V.ι))
    (hfin : IsLocallyOfFinitePresentation B S hS f ∨ IsQuasiCompact B S hS V.ι) :
    IsFinite B S hS f

Tag 0879, a lemma

Tag 0879 in the Stacks Project.

AlgebraicGeometry.Space.isOpenImmersion_of_isIso_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/OpenImmersionFromDenseOpen.lean, line 177.

Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S contained in a big fppf site B which is separated, locally of finite type and flat, and let V ⊆ Y be an open subspace such that f^{-1}V ⟶ V is an isomorphism and the inclusion of V is quasi-compact and scheme-theoretically dense. Then f is an open immersion.

theorem isOpenImmersion_of_isIso_pullback_snd (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (V : Subfunctor Y)
    (hV : IsOpenSubspace B S hS V)
    (hsep : IsSeparated B S hS f) (hlft : IsLocallyOfFiniteType B S hS f)
    (hflat : IsFlat B S hS f) (hiso : IsIso (pullback.snd f V.ι))
    (hVqc : IsQuasiCompact B S hS V.ι)
    (hVdense : IsSchemeTheoreticallyDense B S hS V) :
    IsOpenImmersion B S hS f

Sources

LeanAlgebraicGeometry.Space.isFinitePresentation_chartModule_of_isFlatOver_of_dense_open · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_fromPreimage · AlgebraicGeometry.Space.relativeDimensionLE_of_dense_open · AlgebraicGeometry.Space.isFinite_of_isFinite_over_dense_open · AlgebraicGeometry.Space.isOpenImmersion_of_isIso_pullback_snd

Section76.38 Blowing up and flatness #

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

Tag 087B, a lemma

Tag 087B in the Stacks Project.

AlgebraicGeometry.Space.exists_isFiniteTypeQuasicoherentIdeal_disjoint_pullbackIdealSubsheaf_eq_idealSmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeIdealEtaleFittingDescentUnconditional.lean, line 61.

Stacks 087B. Let X be a quasi-compact and quasi-separated algebraic space over S, let φ : W ⟶ X be a quasi-compact separated étale morphism, let U ⊆ X be a quasi-compact open subspace and let 𝓘 ⊆ 𝒪_W be a finite type quasi-coherent sheaf of ideals with V(𝓘) ∩ φ⁻¹(U) = ∅. Then there is a finite type quasi-coherent sheaf of ideals 𝓙 ⊆ 𝒪_X such that

V(𝓙) ∩ U = ∅, and

φ⁻¹(𝓙) 𝒪_W = 𝓘 𝓘' for some finite type quasi-coherent sheaf of ideals 𝓘' ⊆ 𝒪_W.

The inverse-image ideal φ⁻¹(𝓙) 𝒪_W is AlgebraicGeometry.Space.pullbackIdealSubsheaf, which is defined for representable morphisms; a separated étale morphism is representable by Stacks 0418, and the statement names that proof.

theorem exists_isFiniteTypeQuasicoherentIdeal_disjoint_pullbackIdealSubsheaf_eq_idealSmul
    {X W : AlgebraicSpaces B S hS} (hXqc : IsQuasiCompactSpace B S hS X.1)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X.1)
    (φ : W ⟶ X) (hφqc : IsQuasiCompact B S hS φ.hom) (hφsep : IsSeparated B S hS φ.hom)
    (hφet : IsEtale B S hS φ.hom)
    (U : Subfunctor X.1) (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompactSpace B S hS U.toFunctor)
    (I : (SheafOfModules.unit (structureRingSheaf B S hS W)).Submodule)
    (hI : IsFiniteTypeQuasicoherentIdeal B S hS W I)
    (hIU : Disjoint (idealZeroLocus B S hS W I)
      (subspacePointSet B S hS W.1 (U.preimage φ.hom))) :
    ∃ J : (SheafOfModules.unit (structureRingSheaf B S hS X)).Submodule,
      IsFiniteTypeQuasicoherentIdeal B S hS X J ∧
        Disjoint (idealZeroLocus B S hS X J) (subspacePointSet B S hS X.1 U) ∧
        ∃ I' : (SheafOfModules.unit (structureRingSheaf B S hS W)).Submodule,
          IsFiniteTypeQuasicoherentIdeal B S hS W I' ∧
            pullbackIdealSubsheaf B S hS φ
                (relativelyRepresentable_of_isLocallyQuasiFinite_isSeparated B S hS φ.hom W.2 X.2
                  (isLocallyQuasiFinite_of_isEtale' B S hS hφet) hφsep) J =
              Stacks.Sites.idealSmul (O := structureSheaf B S hS W.1 W.2) I I'

Tag 087C, a theorem

Tag 087C in the Stacks Project.

AlgebraicGeometry.Space.exists_isFlatteningBlowup_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningByBlowupAlgebraicSpaceUnconditional.lean, line 51.

Flattening by blowing up for algebraic spaces. Let A be a quasi-compact and quasi-separated algebraic space over S, let f : X ⟶ A be locally of finite presentation with X quasi-compact, let F be a quasi-coherent 𝒪_X-module of finite type and let U ⊆ A be a quasi-compact open subspace such that F_U = F|_{X ×_A U} is of finite presentation and flat over U. Then there is a blowup b : A' ⟶ A in a finitely presented closed subspace Z disjoint from U (a U-admissible blowup) such that the strict transform of F with respect to b is an 𝒪_{X ×_A A'}-module of finite presentation, flat over A'.

theorem exists_isFlatteningBlowup_of_isLocallyOfFinitePresentation
    {A : AlgebraicSpaces B S hS} (hAqc : IsQuasiCompactSpace B S hS A.1)
    (hAqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal A.1)
    (U : OpenSubspaces B S hS A.1) (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    {X : AlgebraicSpaces B S hS} (f : X ⟶ A)
    (hXqc : IsQuasiCompactSpace B S hS X.1) (hf : IsLocallyOfFinitePresentation B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hFqc : F.IsQuasicoherentOnSite)
    (hFft : F.IsFiniteTypeOnSite)
    (hFUfp : ((modulePullback B S hS (restrictOverι f U)).obj F).IsFinitePresentationOnSite)
    (hFUflat : IsFlatOver B S hS (restrictOver f U).2 (restrictOverHom f U).hom
      ((modulePullback B S hS (restrictOverι f U)).obj F)) :
    ∃ (Z : ClosedSubspaces B S hS A.1) (A' : AlgebraicSpaces B S hS) (b : A' ⟶ A),
      IsFlatteningBlowup f F U Z b

Sources

LeanAlgebraicGeometry.Space.exists_isFiniteTypeQuasicoherentIdeal_disjoint_pullbackIdealSubsheaf_eq_idealSmul · AlgebraicGeometry.Space.exists_isFlatteningBlowup_of_isLocallyOfFinitePresentation

Section76.39 Applications #

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

Tag 087E, a lemma

Tag 087E in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.exists_isBlowupAlong_isFlat_isFinitePresentation_strictTransformSpaceToBlowUp_of_isFiniteType, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FlatteningFiniteTypeMorphismByBlowupTag.lean, line 36 (StacksFrontier).

Tag 0B4K, a lemma

Tag 0B4K in the Stacks Project.

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

Let f : X ⟶ A be a morphism of algebraic spaces over S and let U ⊆ A be an open subspace. Assume that 1. A is quasi-compact and quasi-separated, 2. U is quasi-compact, 3. f is proper, and 4. f⁻¹(U) ⟶ U (the restriction X ×_A U ⟶ U) is finite locally free.

Then there is a U-admissible blowup b : A' ⟶ A -- the blowup of A in a closed subspace Z of finite presentation whose points avoid those of U -- such that the strict transform X' ⟶ A' of X with respect to b is finite locally free.

theorem exists_admissibleBlowup_isFiniteLocallyFree_strictTransform
    {A X : AlgebraicSpaces B S hS} (f : X ⟶ A) (U : OpenSubspaces B S hS A.1)
    (hAqc : IsQuasiCompactSpace B S hS A.1)
    (hAqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal A.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hf : IsProper B S hS f.hom) (hflf : IsFiniteLocallyFree B S hS (restrictOverHom f U)) :
    ∃ (A' : AlgebraicSpaces B S hS) (b : A' ⟶ A) (Z : ClosedSubspaces B S hS A.1),
      IsFinitePresentation B S hS Z.1.ι ∧
        Disjoint (subspacePointSet B S hS A.1 U.1) (subspacePointSet B S hS A.1 Z.1) ∧
          IsBlowupAlong B S hS Z b ∧
            IsFiniteLocallyFree B S hS
              (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom))

Tag 0GUW, a lemma

Tag 0GUW in the Stacks Project.

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

Let f : X ⟶ A be a morphism of algebraic spaces over S and let U ⊆ A be an open subspace. Assume that A is quasi-compact and quasi-separated, that U is quasi-compact, that f is proper and that f⁻¹(U) ⟶ U (the restriction X ×_A U ⟶ U) is an isomorphism. Then there is a U-admissible blowup b : A' ⟶ A -- the blowup of A in a closed subspace Z of finite presentation whose points avoid those of U -- such that the strict transform of X with respect to b maps isomorphically to A'.

theorem exists_isBlowupAlong_isIso_strictTransformSpaceToBlowUp_of_isProper_unconditional
    {A X : AlgebraicSpaces B S hS} (f : X ⟶ A) (U : OpenSubspaces B S hS A.1)
    (hAqc : IsQuasiCompactSpace B S hS A.1)
    (hAqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal A.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hf : IsProper B S hS f.hom) (hiso : IsIso (pullback.snd f.hom U.1.ι)) :
    ∃ (A' : AlgebraicSpaces B S hS) (b : A' ⟶ A) (Z : ClosedSubspaces B S hS A.1),
      IsFinitePresentation B S hS Z.1.ι ∧
        Disjoint (subspacePointSet B S hS A.1 U.1) (subspacePointSet B S hS A.1 Z.1) ∧
          IsBlowupAlong B S hS Z b ∧
            IsIso (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)).hom

Tag 087F, a lemma

Tag 087F in the Stacks Project.

AlgebraicGeometry.Space.exists_isBlowupAlong_isOpenImmersion_strictTransformSpaceToBlowUp_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenImmersionAfterAdmissibleBlowupUnconditional.lean, line 68. The attribute's comment: “corrected: f separated; as published the statement is false (the affine line with doubled origin over 𝐀¹, with U = 𝐀¹ minus the origin)”.

Stacks 087F, corrected. Let f : X ⟶ A be a morphism of algebraic spaces over S and let U ⊆ A be an open subspace. Assume that A is quasi-compact and quasi-separated, that U is quasi-compact, that f is of finite type and separated, and that f⁻¹(U) ⟶ U is an isomorphism. Then there is a U-admissible blowup b : A' ⟶ A, with centre Z, such that b⁻¹(U) is scheme-theoretically dense in A' and the strict transform of X is an open immersion into A'.

Without separatedness the statement is false; see the module documentation.

theorem exists_isBlowupAlong_isOpenImmersion_strictTransformSpaceToBlowUp_unconditional
    (hZ : B.Contains (⊤_ Scheme.{u})) {A X : AlgebraicSpaces B S hS} (f : X ⟶ A)
    (U : OpenSubspaces B S hS A.1)
    (hAqc : IsQuasiCompactSpace B S hS A.1) (hAqs : IsAbsolutelyQuasiSeparated B S hS hZ A.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hft : IsFiniteType B S hS f.hom) (hsep : IsSeparated B S hS f.hom)
    (hiso : IsIso (pullback.snd f.hom U.1.ι)) :
    ∃ (A' : AlgebraicSpaces B S hS) (b : A' ⟶ A) (Z : ClosedSubspaces B S hS A.1),
      IsFinitePresentation B S hS Z.1.ι ∧
        Disjoint (subspacePointSet B S hS A.1 U.1) (subspacePointSet B S hS A.1 Z.1) ∧
          IsBlowupAlong B S hS Z b ∧
            IsSchemeTheoreticallyDense B S hS (U.1.preimage b.hom) ∧
              IsOpenImmersion B S hS
                (strictTransformSpaceToBlowUp B S hS f b (Z.1.preimage b.hom)).hom

Tag 087G, a lemma

Tag 087G in the Stacks Project.

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

Stacks 087G. Let S be a scheme, let f : X ⟶ Y be a morphism of algebraic spaces over S and let U ⊆ Y be an open subspace. Assume that Y is quasi-compact and quasi-separated, that U is quasi-compact, that f is proper and that f⁻¹(U) ⟶ U is an isomorphism. Then there is a U-admissible blowup b : Y' ⟶ Y which dominates X, that is, there is a factorization Y' ⟶ X ⟶ Y of the blowup morphism.

Being a U-admissible blowup is Stacks 086B, AlgebraicGeometry.Space.IsAdmissibleBlowup; quasi-separatedness of Y is absolute quasi-separatedness; and f⁻¹(U) ⟶ U is the projection X ×_Y U ⟶ U.

theorem exists_isAdmissibleBlowup_dominating_of_isProper {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.1)
    (U : OpenSubspaces B S hS Y.1) (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hf : IsProper B S hS f.hom) (hfU : IsIso (pullback.snd f.hom U.1.ι)) :
    ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ Y), IsAdmissibleBlowup B S hS U b ∧
      ∃ g : Y' ⟶ X, g ≫ f = b

Tag 0CPI, a lemma

Tag 0CPI in the Stacks Project.

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

Stacks 0CPI. Let S be a scheme, let X, Y be algebraic spaces over S, let U ⊆ W ⊆ Y be open subspaces, and let f : X ⟶ W and s : U ⟶ X be morphisms with f ∘ s = id_U. Assume that f is proper, that Y is quasi-compact and quasi-separated, and that U and W are quasi-compact. Then there are a U-admissible blowup b : Y' ⟶ Y and a morphism s' : b⁻¹(W) ⟶ X extending s with f ∘ s' = b|_{b⁻¹(W)}.

Here W is the algebraic space AlgebraicGeometry.Space.openSubspace B S hS Y W, so f ∘ s = id_U reads s ≫ f = U ↪ W; quasi-separatedness of Y is absolute quasi-separatedness; being a U-admissible blowup is Stacks 086B, AlgebraicGeometry.Space.IsAdmissibleBlowup; b⁻¹(W) is the inverse image subfunctor W.1.preimage b.hom, and b|_{b⁻¹(W)} is W.1.fromPreimage b.hom; and s' extends s in that its restriction to b⁻¹(U) ⊆ b⁻¹(W) is s ∘ b|_{b⁻¹(U)} (the morphism b⁻¹(U) ⟶ U being an isomorphism, as b is U-admissible).

theorem exists_isAdmissibleBlowup_extending_section_of_isProper {X Y : AlgebraicSpaces B S hS}
    (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.1)
    (U W : OpenSubspaces B S hS Y.1) (hUW : U.1 ≤ W.1)
    (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor)
    (hWqc : IsQuasiCompactSpace B S hS W.1.toFunctor)
    (f : X ⟶ openSubspace B S hS Y W) (hf : IsProper B S hS f.hom)
    (s : U.1.toFunctor ⟶ X.1) (hs : s ≫ f.hom = Subfunctor.homOfLe hUW) :
    ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ Y), IsAdmissibleBlowup B S hS U b ∧
      ∃ s' : (W.1.preimage b.hom).toFunctor ⟶ X.1, s' ≫ f.hom = W.1.fromPreimage b.hom ∧
        Subfunctor.homOfLe (fun T _ hx => hUW T hx :
          U.1.preimage b.hom ≤ W.1.preimage b.hom) ≫ s' = U.1.fromPreimage b.hom ≫ s

Sources

LeanAlgebraicGeometry.Space.exists_isBlowupAlong_isFlat_isFinitePresentation_strictTransformSpaceToBlowUp_of_isFiniteType · AlgebraicGeometry.Space.exists_admissibleBlowup_isFiniteLocallyFree_strictTransform · AlgebraicGeometry.Space.exists_isBlowupAlong_isIso_strictTransformSpaceToBlowUp_of_isProper_unconditional · AlgebraicGeometry.Space.exists_isBlowupAlong_isOpenImmersion_strictTransformSpaceToBlowUp_unconditional · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_dominating_of_isProper · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_extending_section_of_isProper

Section76.40 Chow's lemma #

Section 76.40 of the Stacks Project, Tag 088P. 5 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 088Q, a lemma

Tag 088Q in the Stacks Project.

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

Stacks 088Q. Let Y be a quasi-compact and quasi-separated algebraic space over S and let j₁ : U ⟶ X₁, j₂ : U ⟶ X₂ be open immersions of algebraic spaces over Y, with U, X₁ and X₂ separated and of finite type over Y. There is a commutative diagram X₁ ⟵ X₁' ⟶ X ⟵ X₂' ⟶ X₂ under U and over Y, in which b_k : X_k' ⟶ X_k is a U-admissible blowup (U being the open subspace j_k(U) of X_k), i_k : X_k' ⟶ X is an open immersion, and X is separated and of finite type over Y. Moreover the morphisms u_k : U ⟶ X_k' of the diagram are open immersions.

theorem exists_isAdmissibleBlowup_isOpenImmersion_of_isOpenImmersion_unconditional
    {Y U X₁ X₂ : AlgebraicSpaces B S hS}
    (f₁ : X₁ ⟶ Y) (f₂ : X₂ ⟶ Y) (j₁ : U ⟶ X₁) (j₂ : U ⟶ X₂)
    (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.1)
    (hj₁ : IsOpenImmersion B S hS j₁.hom) (hj₂ : IsOpenImmersion B S hS j₂.hom)
    (hj : j₁ ≫ f₁ = j₂ ≫ f₂)
    (hUft : IsFiniteType B S hS (j₁ ≫ f₁).hom) (hUsep : IsSeparated B S hS (j₁ ≫ f₁).hom)
    (hX₁ft : IsFiniteType B S hS f₁.hom) (hX₁sep : IsSeparated B S hS f₁.hom)
    (hX₂ft : IsFiniteType B S hS f₂.hom) (hX₂sep : IsSeparated B S hS f₂.hom) :
    ∃ (X₁' X₂' X : AlgebraicSpaces B S hS) (b₁ : X₁' ⟶ X₁) (b₂ : X₂' ⟶ X₂)
      (i₁ : X₁' ⟶ X) (i₂ : X₂' ⟶ X) (g : X ⟶ Y) (u₁ : U ⟶ X₁') (u₂ : U ⟶ X₂'),
      IsAdmissibleBlowup B S hS ⟨Subfunctor.range j₁.hom, @isOpenSubspace_range_of_open B S hS
        _ _ j₁.hom (mono_of_isOpenImmersion B S hS _ hj₁) U.2 hj₁⟩ b₁ ∧
      IsAdmissibleBlowup B S hS ⟨Subfunctor.range j₂.hom, @isOpenSubspace_range_of_open B S hS
        _ _ j₂.hom (mono_of_isOpenImmersion B S hS _ hj₂) U.2 hj₂⟩ b₂ ∧
      IsOpenImmersion B S hS i₁.hom ∧ IsOpenImmersion B S hS i₂.hom ∧
      IsSeparated B S hS g.hom ∧ IsFiniteType B S hS g.hom ∧
      i₁ ≫ g = b₁ ≫ f₁ ∧ i₂ ≫ g = b₂ ≫ f₂ ∧
      u₁ ≫ b₁ = j₁ ∧ u₂ ≫ b₂ = j₂ ∧ u₁ ≫ i₁ = u₂ ≫ i₂ ∧
      IsOpenImmersion B S hS u₁.hom ∧ IsOpenImmersion B S hS u₂.hom

Tag 088R, a lemma

Tag 088R in the Stacks Project.

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

Let f : X ⟶ Y be a morphism of algebraic spaces over S and let U ⊆ X be an open subspace. Assume that U is quasi-compact, that Y is quasi-compact and quasi-separated, that i : U ⟶ ℙⁿ_Y is an immersion over Y, and that f is of finite type and separated. Then there is a commutative diagram
        U
     ↙  ↓  ↘  ↘
   X ← X' → Z' → Z
     ↘  ↓  ↙    ↓
        Y  ←  ℙⁿ_Y
in which the arrows with source U are open immersions, X' ⟶ X is a U-admissible blowup, X' ⟶ Z' is an open immersion and Z' ⟶ Y is proper and representable; more precisely Z' ⟶ Z is a U-admissible blowup and Z ⟶ ℙⁿ_Y is a closed immersion, through which i factors (AlgebraicGeometry.Space.HasChowBlowupDiagram).

theorem hasChowBlowupDiagram_of_isFiniteType_of_isSeparated
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (U : Subfunctor X) (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompactSpace B S hS U.toFunctor)
    (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y)
    (n : ℕ) (i : U.toFunctor ⟶ projectiveSpaceOver B S hS Y n) (hi : IsImmersion B S hS i)
    (hiY : i ≫ prod.fst = U.ι ≫ f)
    (hft : IsFiniteType B S hS f) (hsep : IsSeparated B S hS f) :
    HasChowBlowupDiagram B S hS hX f U hU n i

Tag 088S, a lemma

Tag 088S in the Stacks Project.

AlgebraicGeometry.Space.exists_denseOpen_hasChowBlowupDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChowBlowupDiagramNoetherian.lean, line 62.

Stacks 088S. Let f : X ⟶ Y be a separated morphism of finite type of algebraic spaces over S, with Y Noetherian. Then there are a dense open subspace U ⊆ X, an integer n and an immersion i : U ⟶ ℙⁿ_Y over Y for which the diagram of Stacks 088S exists (AlgebraicGeometry.Space.HasChowBlowupDiagram): a U-admissible blowup X' ⟶ X, an open immersion X' ⟶ Z', a proper representable Z' ⟶ Y, a U-admissible blowup Z' ⟶ Z and a closed immersion Z ⟶ ℙⁿ_Y, with the arrows out of U open immersions and everything commuting.

theorem exists_denseOpen_hasChowBlowupDiagram (hTop : B.Contains (⊤_ Scheme.{u}))
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hsep : IsSeparated B S hS f) (hft : IsFiniteType B S hS f)
    (hYnoeth : IsNoetherian B S hS hTop Y) :
    ∃ (U : Subfunctor X) (hU : IsOpenSubspace B S hS U),
      (letI : TopologicalSpace (points B S hS X) := pointTopology B S hS X;
        DenseRange (pointsMap B S hS U.toFunctor U.ι)) ∧
      ∃ (n : ℕ) (i : U.toFunctor ⟶ projectiveSpaceOver B S hS Y n),
        IsImmersion B S hS i ∧ i ≫ prod.fst = U.ι ≫ f ∧
          HasChowBlowupDiagram B S hS hX f U hU n i

Tag 088T, a remark

Tag 088T in the Stacks Project.

AlgebraicGeometry.Space.exists_isRelativelyAmple_of_isAdmissibleBlowup_of_projectiveSpaceImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupProjectiveRelativeAmple.lean, line 69.

Stacks 088T. Let Y be a quasi-compact algebraic space, i : Z ⟶ ℙⁿ_Y a closed immersion, U ⊆ Z an open subspace and b : Z' ⟶ Z a U-admissible blowup, as in Lemmas 088R and 088S, and let g = b ≫ (Z ⟶ ℙⁿ_Y ⟶ Y). Then

g is a composition of projective morphisms: b is proper and representable and carries a b-ample invertible module, and Z ⟶ Y is proper and representable and carries an ample invertible module relative to it;

there exists a g-ample invertible 𝒪_{Z'}-module.

theorem exists_isRelativelyAmple_of_isAdmissibleBlowup_of_projectiveSpaceImmersion
    {Y Z Z' : AlgebraicSpaces B S hS} (hY : IsQuasiCompactSpace B S hS Y.1) {n : ℕ}
    {hP : B.Contains (projectiveSpaceOver n S)} (D : ProjectiveSpaceImmersion B S hS n hP Z Y)
    (U : OpenSubspaces B S hS Z.1) {b : Z' ⟶ Z} (hb : IsAdmissibleBlowup B S hS U b) :
    (IsProper B S hS b.hom ∧ yoneda.relativelyRepresentable b.hom ∧
        ∃ L : Modules.{u, u} B S hS Z'.1 Z'.2,
          Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS Z'.1)
            ((Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS Z'.1 Z'.2).O)).property L ∧
          IsRelativelyAmple B S hS b L) ∧
      (IsProper B S hS D.hom.hom ∧ yoneda.relativelyRepresentable D.hom.hom ∧
        ∃ M : Modules.{u, u} B S hS Z.1 Z.2,
          Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS Z.1)
            ((Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS Z.1 Z.2).O)).property M ∧
          IsRelativelyAmple B S hS D.hom M) ∧
      ∃ L : Modules.{u, u} B S hS Z'.1 Z'.2,
        Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS Z'.1)
          ((Stacks.SheafOfModules.Tensor.ringSheaf
            (smallEtaleRingedSite B S hS Z'.1 Z'.2).O)).property L ∧
        IsRelativelyAmple B S hS (b ≫ D.hom) L

Tag 088U, a lemma

Tag 088U in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.exists_isAdmissibleBlowup_isImmersion_projectiveSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ChowLemma/Main.lean, line 38 (StacksFrontier).
AlgebraicGeometry.Space.C1573.exists_isAdmissibleBlowup_isImmersion_projectiveSpace, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ChowLemmaTag.lean, line 25 (StacksFrontier).

Sources

LeanAlgebraicGeometry.Space.exists_isAdmissibleBlowup_isOpenImmersion_of_isOpenImmersion_unconditional · AlgebraicGeometry.Space.hasChowBlowupDiagram_of_isFiniteType_of_isSeparated · AlgebraicGeometry.Space.exists_denseOpen_hasChowBlowupDiagram · AlgebraicGeometry.Space.exists_isRelativelyAmple_of_isAdmissibleBlowup_of_projectiveSpaceImmersion · AlgebraicGeometry.Space.C1573.exists_isAdmissibleBlowup_isImmersion_projectiveSpace

Section76.41 Variants of Chow's Lemma #

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

Tag 089L, a lemma

Tag 089L in the Stacks Project.

AlgebraicGeometry.Space.exists_chowDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChowLemma/ChowDiagram.lean, line 300.

Chow's lemma for algebraic spaces, [Stacks, Tag 089L]. Let Y be a quasi-compact and quasi-separated algebraic space over S and let f : X ⟶ Y be a separated morphism of finite type. Then there are algebraic spaces X' and X̄' and a commutative diagram X ⟵ X' ⟶ X̄' ⟶ Y over Y in which X' ⟶ X is proper and surjective, X' ⟶ X̄' is an open immersion and X̄' ⟶ Y is proper and representable.

Every quasi-compact quasi-separated algebraic space has a finite surjective scheme cover (AlgebraicGeometry.Space.existsFiniteSurjectiveSchemeCover_of_isQuasiCompactSpace), so AlgebraicGeometry.Space.exists_chowDiagram_of_forall_finiteSchemeCover applies.

theorem exists_chowDiagram (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hYqc : IsQuasiCompactSpace B S hS Y) (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y)
    (hfsep : IsSeparated B S hS f) (hfft : IsFiniteType B S hS f) :
    ∃ (X' Xbar : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hX' : IsAlgebraicSpace B S hS X')
      (_hXbar : IsAlgebraicSpace B S hS Xbar) (q : X' ⟶ X) (j : X' ⟶ Xbar) (g : Xbar ⟶ Y),
      IsProper B S hS q ∧ IsSurjective B S hS q ∧ IsOpenImmersion B S hS j ∧
        IsProper B S hS g ∧ yoneda.relativelyRepresentable g ∧ q ≫ f = j ≫ g

Tag 089M, a lemma

Tag 089M in the Stacks Project.

AlgebraicGeometry.Space.exists_isProper_isSurjective_isImmersion_projectiveSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChowLemma/ProjectiveImmersionCover.lean, line 545.

Chow's lemma over a quasi-compact separated base, [Stacks, Tag 089M]. Let S be a scheme and f : X ⟶ Y a morphism of algebraic spaces over S, separated and of finite type, with Y separated and quasi-compact. Then there are an algebraic space X', a proper surjective morphism q : X' ⟶ X and an immersion i : X' ⟶ ℙⁿ_Y with q ≫ f = i ≫ (ℙⁿ_Y ⟶ Y).

Relative projective space ℙⁿ_Y is the fibre product Y ×_S ℙⁿ_S over the presheaf represented by S, which is terminal, with ℙⁿ_S the object AlgebraicGeometry.Space.projectiveSpaceSiteObj of the site; ℙⁿ_Y ⟶ Y is the first projection. "Separated" for Y is the absolute notion of [Stacks, Tag 03BS].

theorem exists_isProper_isSurjective_isImmersion_projectiveSpace
    (hZ : B.Contains (⊤_ Scheme.{u})) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hfsep : IsSeparated B S hS f) (hfft : IsFiniteType B S hS f)
    (hYsep : IsAbsolutelySeparated B S hS hZ Y) (hYqc : IsQuasiCompactSpace B S hS Y) :
    ∃ (n : ℕ) (hP : B.Contains (projectiveSpaceOver n S))
      (X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS X') (q : X' ⟶ X)
      (i : X' ⟶ pullback ((isTerminal_yoneda_obj_base B S hS).from Y)
        ((isTerminal_yoneda_obj_base B S hS).from
          (yoneda.obj (projectiveSpaceSiteObj B S hS n hP)))),
      IsProper B S hS q ∧ IsSurjective B S hS q ∧ IsImmersion B S hS i ∧
        q ≫ f = i ≫ pullback.fst _ _

Sources

LeanAlgebraicGeometry.Space.exists_chowDiagram · AlgebraicGeometry.Space.exists_isProper_isSurjective_isImmersion_projectiveSpace

Section76.42 Grothendieck's existence theorem #

Section 76.42 of the Stacks Project, Tag 089N. 14 tags here are carried by 36 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 089P, a lemma

Tag 089P in the Stacks Project.

AlgebraicGeometry.Space.abelian_coherentAdicSystems, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicAbelian.lean, line 424. The attribute's comment: “the category is abelian”.

The category Coh(F, 𝓘) of coherent adic systems on a Noetherian algebraic space is abelian.

It is preadditive, has finite products, kernels and cokernels, and every monomorphism is a kernel and every epimorphism a cokernel.

def abelian_coherentAdicSystems : Abelian (CoherentAdicSystems B S hS F hF 𝓘)

AlgebraicGeometry.Space.coherentAdicInverseImage_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInverseImageIdeal.lean, line 110. The attribute's comment: “part (3): the inverse image along a flat morphism of Noetherian algebraic spaces is exact”.

Part (3) of Stacks 089P: the inverse image along a flat morphism of Noetherian algebraic spaces is exact. For a flat morphism f : X' ⟶ X of Noetherian algebraic spaces and a quasi-coherent sheaf of ideals 𝓘 ⊆ 𝒪_X, the functor f^* : Coh(X, 𝓘) ⥤ Coh(X', f⁻¹𝓘 · 𝒪_{X'}) preserves finite limits and finite colimits.

theorem coherentAdicInverseImage_exact (hf : IsFlat B S hS f.hom) :
    exactFunctor (CoherentAdicSystems B S hS X.1 X.2 𝓘)
      (CoherentAdicSystems B S hS X'.1 X'.2 (pullbackIdealImage B S hS f 𝓘))
      (coherentAdicInverseImage B S hS f 𝓘 hN'.2.2)

AlgebraicGeometry.Space.exact_iff_forall_exact_coherentAdicChartRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInverseImageIdeal.lean, line 149. The attribute's comment: “part (2): exactness can be checked on an étale covering by affine charts”.

Part (2) of Stacks 089P: exactness in Coh(X, 𝓘) can be checked étale locally. For a Noetherian algebraic space X, a quasi-coherent sheaf of ideals 𝓘 ⊆ 𝒪_X and an étale covering of X by affine charts U i, a short complex E ⟶ G ⟶ H of Coh(X, 𝓘) is exact exactly when its restriction E|_{U i} ⟶ G|_{U i} ⟶ H|_{U i} to Coh(U i, 𝓘 · 𝒪_{U i}) is exact for every i.

theorem exact_iff_forall_exact_coherentAdicChartRestriction {I : Type v}
    (U : I → SmallEtale B S hS X.1) (hU : ∀ i, IsAffine (chartScheme (U i)))
    (hcov : IsEtaleCovering B S hS (fun i => (chartSpace B S hS X (U i)).1)
      (fun i => (chartToSpace B S hS X (U i)).hom))
    (T : ShortComplex (CoherentAdicSystems B S hS X.1 X.2 𝓘)) :
    T.Exact ↔ ∀ i, (coherentAdicRestrictToChartShortComplex B S hS X 𝓘 hZ hN (U i)
      (pullbackIdealImage B S hS (chartToSpace B S hS X (U i)) 𝓘) (hU i)
      (idealPowerMultipleCompatible_pullbackIdealImage B S hS (chartToSpace B S hS X (U i)) 𝓘)
      T).Exact

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

Stacks 089P. Let X be a Noetherian algebraic space over a scheme S and 𝓘 ⊆ 𝒪_X a quasi-coherent sheaf of ideals.

Coh(X, 𝓘) is abelian.

Exactness in Coh(X, 𝓘) can be checked étale locally: on every étale covering of X by affine charts U i, a short complex is exact exactly when its restrictions to the categories Coh(U i, 𝓘 · 𝒪_{U i}) are.

For every flat morphism f : X' ⟶ X of Noetherian algebraic spaces the inverse image f^* : Coh(X, 𝓘) ⥤ Coh(X', f⁻¹𝓘 · 𝒪_{X'}) is exact.

theorem coherentAdicSystems_abelian_and_exact :
    Nonempty (Abelian (CoherentAdicSystems B S hS X.1 X.2 𝓘)) ∧
    (∀ {I : Type v} (U : I → SmallEtale B S hS X.1) (hU : ∀ i, IsAffine (chartScheme (U i))),
      IsEtaleCovering B S hS (fun i => (chartSpace B S hS X (U i)).1)
          (fun i => (chartToSpace B S hS X (U i)).hom) →
        ∀ T : ShortComplex (CoherentAdicSystems B S hS X.1 X.2 𝓘),
          T.Exact ↔ ∀ i, (coherentAdicRestrictToChartShortComplex B S hS X 𝓘 hZ hN (U i)
            (pullbackIdealImage B S hS (chartToSpace B S hS X (U i)) 𝓘) (hU i)
            (idealPowerMultipleCompatible_pullbackIdealImage B S hS
              (chartToSpace B S hS X (U i)) 𝓘) T).Exact) ∧
    (∀ {X' : AlgebraicSpaces B S hS} (f : X' ⟶ X) (hN' : IsNoetherian B S hS hZ X'.1),
      IsFlat B S hS f.hom →
        exactFunctor (CoherentAdicSystems B S hS X.1 X.2 𝓘)
          (CoherentAdicSystems B S hS X'.1 X'.2 (pullbackIdealImage B S hS f 𝓘))
          (coherentAdicInverseImage B S hS f 𝓘 hN'.2.2))

Tag 08B3, a lemma

Tag 08B3 in the Stacks Project.

AlgebraicGeometry.Space.epi_iff_epi_app_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicSystem.lean, line 486.

A map of coherent adic systems on an algebraic space is surjective in Coh(F, 𝓘) exactly when its component at the lowest level is surjective.

theorem epi_iff_epi_app_zero {E E' : CoherentAdicSystems B S hS F hF 𝓘} (f : E ⟶ E') :
    Epi f ↔ Epi (f.hom.app (op 0))

Tag 08B4, an equation

Tag 08B4 in the Stacks Project.

AlgebraicGeometry.Space.completionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionFunctor.lean, line 326.

The completion functor Coh(𝒪_F) ⟶ Coh(F, 𝓘) on a locally Noetherian algebraic space, for a quasi-coherent sheaf of ideals 𝓘, sending a coherent 𝒪_F-module 𝓖 to the coherent 𝓘-adic system 𝓖^∧ = (𝓖 / 𝓘 ^ (n + 1) 𝓖)_n.

def completionFunctor
    [Fact (HasEtaleLocalProperty B S hS F (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    (hI : 𝓘.toSheafOfModules.IsQuasicoherentOnSite) :
    CoherentModules.{u, u} B S hS F hF ⥤ CoherentAdicSystems B S hS F hF 𝓘

Tag 08B5, a lemma

Tag 08B5 in the Stacks Project.

AlgebraicGeometry.Space.preservesFiniteColimits_completionFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionExact.lean, line 340. The attribute's comment: “right exactness: preservation of finite colimits”.

Stacks 08B5, right exactness. The completion functor Coh(𝒪_F) ⥤ Coh(F, 𝓘) preserves finite colimits.

No Noetherian hypothesis is needed: the term at n of a completion is the reflection of a coherent module onto the modules annihilated by 𝓘 ^ (n + 1), and every term of a coherent 𝓘-adic system is so annihilated.

instance preservesFiniteColimits_completionFunctor :
    PreservesFiniteColimits (completionFunctor B S hS F hF 𝓘 hI)

AlgebraicGeometry.Space.preservesMonomorphisms_completionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionExact.lean, line 432. The attribute's comment: “preservation of monomorphisms”.

Stacks 08B5, preservation of monomorphisms. On a Noetherian algebraic space the completion functor Coh(𝒪_F) ⥤ Coh(F, 𝓘) carries a monomorphism to a monomorphism.

Let f : M ⟶ N be a monomorphism and let c be the Artin-Rees constant of AlgebraicGeometry.Space.exists_comp_completionTermProjection_eq_zero_of_mono. A morphism into M ^ ∧ killed by f ^ ∧ is tested level by level; at level n the transition map down from level n + c is an epimorphism, so it suffices to kill the morphism at level n + c after that transition, and the quotient projection out of M is an epimorphism, so that in turn is the Artin-Rees step.

theorem preservesMonomorphisms_completionFunctor (hZ : B.Contains (⊤_ Scheme.{u}))
    (hN : IsNoetherian B S hS hZ F) :
    (completionFunctor B S hS F hF 𝓘 hI).PreservesMonomorphisms

AlgebraicGeometry.Space.preservesFiniteLimits_completionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionExact.lean, line 531. The attribute's comment: “left exactness: the completion functor preserves finite limits”.

Stacks 08B5, left exactness. On a Noetherian algebraic space the completion functor Coh(𝒪_F) ⥤ Coh(F, 𝓘) of Stacks 08B4 preserves finite limits.

It preserves homology by AlgebraicGeometry.Space.preservesHomology_completionFunctor, given that every monomorphism of Coh(F, 𝓘) is a kernel; and that holds by AlgebraicGeometry.Space.isNormalMonoCategory_coherentAdicSystems, from part (1) of Stacks 089P, since 𝓘 is cartesian on the affine charts by AlgebraicGeometry.Space.isCartesianOnAffineCharts_of_isQuasicoherentOnSite. The hypotheses are the source's own: F is Noetherian — which is where Artin–Rees, Stacks 07UL, enters through AlgebraicGeometry.Space.preservesMonomorphisms_completionFunctor — and 𝓘 is quasi-coherent.

theorem preservesFiniteLimits_completionFunctor (hZ : B.Contains (⊤_ Scheme.{u}))
    (hN : IsNoetherian B S hS hZ F) :
    PreservesFiniteLimits (completionFunctor B S hS F hF 𝓘 hI)

AlgebraicGeometry.Space.exactFunctor_completionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionExact.lean, line 547. The attribute's comment: “exactness: the completion functor is exact”.

Stacks 08B5. On a Noetherian algebraic space the completion functor Coh(𝒪_F) ⥤ Coh(F, 𝓘) of Stacks 08B4 is exact.

Right exactness is AlgebraicGeometry.Space.preservesFiniteColimits_completionFunctor and needs no Noetherian hypothesis; left exactness is AlgebraicGeometry.Space.preservesFiniteLimits_completionFunctor.

theorem exactFunctor_completionFunctor (hZ : B.Contains (⊤_ Scheme.{u}))
    (hN : IsNoetherian B S hS hZ F) :
    exactFunctor (CoherentModules.{u, u} B S hS F hF) (CoherentAdicSystems B S hS F hF 𝓘)
      (completionFunctor B S hS F hF 𝓘 hI)

AlgebraicGeometry.Space.preservesFiniteLimits_completionFunctor_of_isNoetherian, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionLeftExact.lean, line 103. The attribute's comment: “left exactness: the completion functor preserves finite limits, over the source's own hypotheses that the algebraic space is Noetherian and the sheaf of ideals quasi-coherent”.

Stacks 08B5, left exactness. On a Noetherian algebraic space the completion functor Coh(𝒪_F) ⥤ Coh(F, 𝓘) of Stacks 08B4 preserves finite limits.

This is AlgebraicGeometry.Space.preservesFiniteLimits_completionFunctor.

alias preservesFiniteLimits_completionFunctor_of_isNoetherian

AlgebraicGeometry.Space.exactFunctor_completionFunctor_of_isNoetherian, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionLeftExact.lean, line 112. The attribute's comment: “exactness of the completion functor over the source's own hypotheses that the algebraic space is Noetherian and the sheaf of ideals quasi-coherent”.

Stacks 08B5. On a Noetherian algebraic space the completion functor Coh(𝒪_F) ⥤ Coh(F, 𝓘) of Stacks 08B4 is exact.

This is AlgebraicGeometry.Space.exactFunctor_completionFunctor.

alias exactFunctor_completionFunctor_of_isNoetherian

Tag 08B6, a lemma

Tag 08B6 in the Stacks Project.

AlgebraicGeometry.Space.smallEtaleInternalHomAdicEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInternalHom.lean, line 607. The attribute's comment: “granted Stacks 0882, the case of schemes, on each étale chart as the hypothesis h0882; the étale-descent globalisation is proved”.

Stacks 08B6. Let F be an algebraic space over a scheme S, let 𝓘 ⊆ 𝒪_F be a sheaf of ideals and let M, N be 𝒪_F-modules. Put 𝓗 = 𝓗om_{𝒪_F}(M, N). Then

lim_n H⁰(F, 𝓗 / 𝓘 ^ n 𝓗) = Mor((M / 𝓘 ^ n M), (N / 𝓘 ^ n N)),

the inverse limit of the global sections of the ideal-power quotients of 𝓗 being the morphisms of inverse systems of 𝒪_F-modules from the completion of M to the completion of N. Since Coh(F, 𝓘) is a full subcategory of the inverse systems of 𝒪_F-modules, the right-hand side is Mor_{Coh(F, 𝓘)}(M^∧, N^∧) whenever the two completions are objects of it.

The source argues that both sides are sheaves on F_étale and so the identity may be checked étale locally, where it is the case of schemes. That reduction is the hypothesis h0882: it asks, for every étale chart U, that the comparison be bijective on the inverse limits of the sections over U, which on a chart is Stacks 0882 for the scheme U. What is proved here is the globalisation, in three steps: the comparison is a morphism of inverse systems of sheaves (smallEtaleInternalHomAdicComparison_compat), so a chartwise bijection is a bijection on global sections (bijective_adicSectionsMap_of_bijective_adicSectionsMapAt); the global sections of 𝓗om(M, N / 𝓘 ^ n N) are the morphisms M ⟶ N / 𝓘 ^ n N (smallEtaleInternalHomSectionsEquiv); and such a morphism is the same as a morphism M / 𝓘 ^ n M ⟶ N / 𝓘 ^ n N, compatibly in n (bijective_smallEtaleInternalHomAdicSection).

The Noetherian hypothesis on F and the coherence of M and N are not used: they enter only through h0882, whose chartwise content is the Noetherian scheme case.

def smallEtaleInternalHomAdicEquiv
    (h0882 : ∀ U, Function.Bijective (adicSectionsMapAt B S hS F hF
      (fun n => smallEtaleAdicQuotient B S hS F hF 𝓘 (n + 1)
        (smallEtaleInternalHom B S hS F hF M N))
      (fun n => smallEtaleInternalHom B S hS F hF M
        (smallEtaleAdicQuotient B S hS F hF 𝓘 (n + 1) N))
      (fun n => smallEtaleAdicQuotientTransition B S hS F hF 𝓘 (n + 1)
        (smallEtaleInternalHom B S hS F hF M N))
      (fun n => smallEtaleInternalHomMapRight B S hS F hF M
        (smallEtaleAdicQuotientTransition B S hS F hF 𝓘 (n + 1) N))
      (smallEtaleInternalHomAdicComparisonApp B S hS F hF 𝓘 M N)
      (smallEtaleInternalHomAdicComparison_compat B S hS F hF 𝓘 M N) U)) :
    adicSections B S hS F hF
        (fun n => smallEtaleAdicQuotient B S hS F hF 𝓘 (n + 1)
          (smallEtaleInternalHom B S hS F hF M N))
        (fun n => smallEtaleAdicQuotientTransition B S hS F hF 𝓘 (n + 1)
          (smallEtaleInternalHom B S hS F hF M N)) ≃
      (smallEtaleAdicQuotientSystem B S hS F hF 𝓘 M ⟶
        smallEtaleAdicQuotientSystem B S hS F hF 𝓘 N)

AlgebraicGeometry.Space.smallEtaleInternalHomSmallAdicEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInternalHomAffine.lean, line 80.

Stacks 08B6. Let F be a locally Noetherian algebraic space over a scheme S, let 𝓘 ⊆ 𝒪_F be a quasi-coherent sheaf of ideals and let M, N be coherent 𝒪_F-modules. Put 𝓗 = 𝓗om_{𝒪_F}(M, N). Then

lim_n H⁰(F, 𝓗 / 𝓘 ^ n 𝓗) = Mor((M / 𝓘 ^ n M), (N / 𝓘 ^ n N)),

the inverse limit of the global sections of the ideal-power quotients of 𝓗 being the morphisms of inverse systems of 𝒪_F-modules from the completion of M to the completion of N; since Coh(F, 𝓘) is a full subcategory of the inverse systems of 𝒪_F-modules, this is Mor_{Coh(F, 𝓘)}(M^∧, N^∧). Here 𝓗 is the internal hom at the module universe of the schemes, AlgebraicGeometry.Space.smallEtaleInternalHomSmall, whose universe lift is AlgebraicGeometry.Space.smallEtaleInternalHom. The source asks for F Noetherian; local Noetherianity is all that is used.

def smallEtaleInternalHomSmallAdicEquiv :
    adicSections B S hS F hF
        (fun n => smallEtaleAdicQuotient B S hS F hF 𝓘 (n + 1)
          (smallEtaleInternalHomSmall B S hS F hF M N))
        (fun n => smallEtaleAdicQuotientTransition B S hS F hF 𝓘 (n + 1)
          (smallEtaleInternalHomSmall B S hS F hF M N)) ≃
      (smallEtaleAdicQuotientSystem B S hS F hF 𝓘 M ⟶
        smallEtaleAdicQuotientSystem B S hS F hF 𝓘 N)

AlgebraicGeometry.Space.bijective_adicSectionsMap_of_isSeqProIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInternalHomProIso.lean, line 391. The attribute's comment: “the pro-isomorphism step: pro-isomorphic inverse systems of 𝒪_F-modules have the same inverse limit of global sections, which is what identifies the tag's two limits lim H⁰(𝓗 / 𝓘 ^ n 𝓗) and lim H⁰(𝓗om(M, N / 𝓘 ^ n N)) from a pro-isomorphism of the comparison”.

A pro-isomorphism of inverse systems of 𝒪_F-modules induces a bijection on the inverse limits of their global sections. Pro-isomorphic systems therefore have the same lim_n H⁰(F, -), although they are nowhere isomorphic level by level. The chartwise statement is bijective_adicSectionsMapAt_of_isSeqProIso and the passage to global sections is the étale descent of bijective_adicSectionsMap_of_bijective_adicSectionsMapAt.

This is the step by which Stacks 08B6 identifies its left-hand side lim_n H⁰(F, 𝓗 / 𝓘 ^ n 𝓗) with lim_n H⁰(F, 𝓗om(M, N / 𝓘 ^ n N)): the comparison AlgebraicGeometry.Space.smallEtaleInternalHomAdicComparisonApp between those two systems is not an isomorphism at any single level, and the source's Noetherian and coherence hypotheses enter only to make it a pro-isomorphism. Once that is known, this theorem turns it into the identity of inverse limits, with no hypothesis on the systems at all.

theorem bijective_adicSectionsMap_of_isSeqProIso
    (hβ : ∀ n : ℕ, trX n ≫ β n = β (n + 1) ≫ trY n)
    (hpro : IsSeqProIso B S hS F hF X Y trX trY β) :
    Function.Bijective (adicSectionsMap B S hS F hF X Y trX trY β hβ)

AlgebraicGeometry.Space.smallEtaleInternalHomAdicEquivOfNoetherian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleInternalHomAdicNoetherian.lean, line 141.

Stacks 08B6. Let X be a Noetherian algebraic space over a scheme S, let 𝓘 ⊆ 𝒪_X be a quasi-coherent sheaf of ideals and let M, N be coherent 𝒪_X-modules. Put 𝓗 = 𝓗om_{𝒪_X}(M, N). Then

lim_n H⁰(X, 𝓗 / 𝓘 ^ n 𝓗) = Mor((M / 𝓘 ^ n M), (N / 𝓘 ^ n N)),

the inverse limit of the global sections of the ideal-power quotients of 𝓗 being the morphisms of inverse systems of 𝒪_X-modules from the completion of M to the completion of N.

This is AlgebraicGeometry.Space.smallEtaleInternalHomAdicEquiv with its assumed chartwise input h0882 discharged, so the hypotheses are exactly the source's: Noetherianness of X, quasi-coherence of 𝓘, coherence of M and of N.

The tag is registered here, bare, because this is where the source's identity is proved outright under the source's own hypotheses and nothing else. The two registrations on StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInternalHom.lean carry clause strings naming the two steps proved there — the pro-isomorphism step and the morphism step — and stay as they are; by the covering-set rule they and this one together carry the tag. No registration is placed on AlgebraicGeometry.Space.smallEtaleInternalHomAdicEquiv itself, which still takes h0882 as an assumed input: a tag may not sit on a declaration that assumes the thing it asserts.

def smallEtaleInternalHomAdicEquivOfNoetherian
    (hZ : B.Contains (⊤_ Scheme.{u})) (hFN : IsNoetherian B S hS hZ X.1)
    (hI : 𝓘.toSheafOfModules.IsQuasicoherentOnSite)
    (hM : IsCoherent B S hS X.1 X.2 M) (hN : IsCoherent B S hS X.1 X.2 N) :
    adicSections B S hS X.1 X.2
        (fun n => smallEtaleAdicQuotient B S hS X.1 X.2 𝓘 (n + 1)
          (smallEtaleInternalHom B S hS X.1 X.2 M N))
        (fun n => smallEtaleAdicQuotientTransition B S hS X.1 X.2 𝓘 (n + 1)
          (smallEtaleInternalHom B S hS X.1 X.2 M N)) ≃
      (smallEtaleAdicQuotientSystem B S hS X.1 X.2 𝓘 M ⟶
        smallEtaleAdicQuotientSystem B S hS X.1 X.2 𝓘 N)

Declarations registered for the tag:

bijective_smallEtaleInternalHomAdicSection registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicInternalHomProIso.lean, line 442 (StacksFrontier): “the morphism step of the identity: morphisms of the inverse systems of ideal-power quotients are exactly the compatible families of global sections of the internal homs into those quotients, so that Mor((M / 𝓘 ^ n M), (N / 𝓘 ^ n N)) is lim_n H⁰(F, 𝓗om(M, N / 𝓘 ^ n N))”.

Tag 08B7, a situation

Tag 08B7 in the Stacks Project.

AlgebraicGeometry.Space.ExistenceSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/GrothendieckExistence.lean, line 63.

Stacks 08B7. The standing data of Grothendieck's existence theorem: a Noetherian ring A complete with respect to an ideal I, together with a separated algebraic space X of finite type over Spec A.

structure ExistenceSituation

Tag 08B8, an equation

Tag 08B8 in the Stacks Project.

AlgebraicGeometry.Space.hasProperSupport_idealPowerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicSystemProperSupport.lean, line 132. The attribute's comment: “the support condition, by which equation 76.42.2.1 restricts to the two full subcategories constructed below: the completion M / 𝓘 ^ n M of a coherent module with support proper over the base again has support proper over the base. The arrow itself is the completion functor of Stacks 08B4, which is AlgebraicGeometry.Space.completionFunctor”.

Stacks 08B8, the support condition. The terms M / 𝓘 ^ n M of the completion of a coherent 𝒪_X-module M whose support is proper over Y again have support proper over Y.

A coherent module is of finite type, and M / 𝓘 ^ n M is a quotient of M, so this is the quotient clause of Stacks 0CZK part (1).

theorem hasProperSupport_idealPowerQuotient (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (𝓘 : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X hX).O))).Submodule)
    (n : ℕ) (M : Modules.{u, u} B S hS X hX) (hMcoh : IsCoherent B S hS X hX M)
    (hM : HasProperSupport B S hS hX hY f hf ((SheafOfModules.toSheaf _).obj M)) :
    HasProperSupport B S hS hX hY f hf
      ((SheafOfModules.toSheaf _).obj (idealPowerQuotient B S hS X hX 𝓘 n M))

AlgebraicGeometry.Space.completionFunctorProperOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionProperSupport.lean, line 84. The attribute's comment: “the arrow, restricting the completion functor of Stacks 08B4 to the two full subcategories of objects with support proper over the base”.

Stacks 08B8, the arrow. The completion functor Coh_{support proper over Y}(𝒪_X) ⟶ Coh_{support proper over Y}(X, 𝓘) of equation 76.42.5.1, the restriction of the completion functor of Stacks 08B4 to the full subcategories of objects whose support is proper over Y.

It is well defined because the completion of a coherent module with support proper over Y has all of its terms supported inside the support of the module, which is AlgebraicGeometry.Space.hasProperSupport_idealPowerQuotient.

def completionFunctorProperOver
    [Fact (HasEtaleLocalProperty B S hS X (fun V : Scheme.{u} => IsLocallyNoetherian V))]
    (hI : 𝓘.toSheafOfModules.IsQuasicoherentOnSite) :
    CoherentModulesProperOver B S hS hX hY g hg ⥤
      CoherentAdicSystemsProperOver B S hS hX hY g hg 𝓘

Tag 08B9, a lemma

Tag 08B9 in the Stacks Project.

AlgebraicGeometry.Space.bijective_completionFunctor_map_of_isProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CompletionFullyFaithfulProperSupport.lean, line 82. The attribute's comment: “the bijection on morphisms; the source's Situation 08B7 asks X separated of finite type over Spec A, of which only local finite type is used”.

Stacks 08B9, the bijection on morphisms. Let A be a Noetherian ring complete with respect to an ideal I, let X be an algebraic space with a morphism f : X ⟶ Spec A locally of finite type, and let F, G be coherent 𝒪_X-modules such that the intersection of their supports is proper over Spec A. Then completion along I 𝒪_X (Stacks 08B4) is a bijection Mor_{Coh(𝒪_X)}(F, G) ⟶ Mor_{Coh(X, I 𝒪_X)}(F^∧, G^∧).

The source's Situation 08B7 has X separated and of finite type over Spec A, so locally Noetherian (AlgebraicGeometry.Space.isLocallyNoetherian_of_isLocallyOfFiniteType with AlgebraicGeometry.Space.hasEtaleLocalProperty_isLocallyNoetherian_baseObject supply the Fact instance the completion functor of Stacks 08B4 is stated with); neither separatedness nor quasi-compactness is used.

theorem bijective_completionFunctor_map_of_isProperOver [IsNoetherianRing A] [IsAdicComplete I A]
    (f : X ⟶ schemeSpace (baseObject A B hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f.hom)
    (F G : CoherentModules.{u, u} B (Spec (.of A)) hA X.1 X.2)
    (hcl : IsClosed (supportOfSheaf B (Spec (.of A)) hA X.1 ((SheafOfModules.toSheaf _).obj F.obj) ∩
      supportOfSheaf B (Spec (.of A)) hA X.1 ((SheafOfModules.toSheaf _).obj G.obj)))
    (hp : IsProperOver B (Spec (.of A)) hA X.2 (schemeSpace (baseObject A B hA)).2 f.hom hf _ hcl) :
    letI := C1573.fact_isLocallyNoetherian_of_baseObject X f hf
    Function.Bijective ((completionFunctor B (Spec (.of A)) hA X.1 X.2
      (C1573.baseIdealSubmodule X.1 X.2 I)
      (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).map
        (X := F) (Y := G))

AlgebraicGeometry.Space.completionFunctorProperOverFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CompletionFullyFaithfulProperSupport.lean, line 101. The attribute's comment: “in particular, the completion functor of 08B8 is fully faithful”.

Stacks 08B9, full faithfulness. In the situation of AlgebraicGeometry.Space.bijective_completionFunctor_map_of_isProperOver, the completion functor Coh_{support proper over A}(𝒪_X) ⟶ Coh_{support proper over A}(X, I 𝒪_X) of Stacks 08B8 is fully faithful.

def completionFunctorProperOverFullyFaithful [IsNoetherianRing A] [IsAdicComplete I A]
    (f : X ⟶ schemeSpace (baseObject A B hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f.hom) :
    letI := C1573.fact_isLocallyNoetherian_of_baseObject X f hf
    (completionFunctorProperOver B (Spec (.of A)) hA X.1
      (schemeSpace (baseObject A B hA)).1 X.2 (schemeSpace (baseObject A B hA)).2 f.hom hf
      (C1573.baseIdealSubmodule X.1 X.2 I)
      (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).FullyFaithful

AlgebraicGeometry.Space.bijective_completionFunctor_map_and_fullyFaithful_of_isProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CompletionFullyFaithfulProperSupportTag.lean, line 72.

Stacks 08B9. Let A be a Noetherian ring complete with respect to an ideal I and let X be an algebraic space with a morphism f : X ⟶ Spec A locally of finite type.

For coherent 𝒪_X-modules F, G such that the intersection of their supports is proper over Spec A, completion along I 𝒪_X (Stacks 08B4) is a bijection Mor_{Coh(𝒪_X)}(F, G) ⟶ Mor_{Coh(X, I 𝒪_X)}(F^∧, G^∧).

In particular, the completion functor Coh_{support proper over A}(𝒪_X) ⟶ Coh_{support proper over A}(X, I 𝒪_X) of Stacks 08B8 is fully faithful.

The source's Situation 08B7 has X separated and of finite type over Spec A, so locally Noetherian (AlgebraicGeometry.Space.C1573.fact_isLocallyNoetherian_of_baseObject supplies the Fact instance the completion functor of Stacks 08B4 is stated with); neither separatedness nor quasi-compactness is used. The properness of Supp F ∩ Supp G is stated in the curried form IsProperOver … hcl of AlgebraicGeometry.Space.IsProperOver, which takes the closedness hcl of the subset as an argument.

theorem bijective_completionFunctor_map_and_fullyFaithful_of_isProperOver
    [IsNoetherianRing A] [IsAdicComplete I A]
    (f : X ⟶ schemeSpace (baseObject A B hA))
    (hf : IsLocallyOfFiniteType B (Spec (.of A)) hA f.hom) :
    letI := C1573.fact_isLocallyNoetherian_of_baseObject X f hf
    (∀ (F G : CoherentModules.{u, u} B (Spec (.of A)) hA X.1 X.2)
      (hcl : IsClosed
        (supportOfSheaf B (Spec (.of A)) hA X.1 ((SheafOfModules.toSheaf _).obj F.obj) ∩
          supportOfSheaf B (Spec (.of A)) hA X.1 ((SheafOfModules.toSheaf _).obj G.obj))),
      IsProperOver B (Spec (.of A)) hA X.2 (schemeSpace (baseObject A B hA)).2 f.hom hf _ hcl →
      Function.Bijective ((completionFunctor B (Spec (.of A)) hA X.1 X.2
        (C1573.baseIdealSubmodule X.1 X.2 I)
        (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).map
          (X := F) (Y := G))) ∧
    Nonempty (completionFunctorProperOver B (Spec (.of A)) hA X.1
      (schemeSpace (baseObject A B hA)).1 X.2 (schemeSpace (baseObject A B hA)).2 f.hom hf
      (C1573.baseIdealSubmodule X.1 X.2 I)
      (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).FullyFaithful

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.bijective_completionFunctor_map_of_isProperOver, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/CompletionFullyFaithfulProperSupportTag.lean, line 93 (StacksFrontier): “the bijection on morphisms; the source's Situation 08B7 asks X separated of finite type over Spec A, of which only local finite type is used”.
AlgebraicGeometry.Space.C1573.completionFunctorProperOverFullyFaithful, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/CompletionFullyFaithfulProperSupportTag.lean, line 97 (StacksFrontier): “in particular, the completion functor of 08B8 is fully faithful”.

Tag 08BA, a remark

Tag 08BA in the Stacks Project.

Ideal.exists_pow_le_annihilator_ker_and_coker_mapQ_pow_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Annihilator.lean, line 341. The attribute's comment: “equivalence of the annihilation conditions”.

Stacks Project, Tag 08BA. For a linear map φ : M → N of I-adically complete modules, one positive power of K annihilates the kernels and the cokernels of all the reductions M / Iⁿ⁺¹ M → N / Iⁿ⁺¹ N if and only if one positive power of K annihilates Ker(φ) and Coker(φ).

theorem exists_pow_le_annihilator_ker_and_coker_mapQ_pow_iff (I K : Ideal A)
    [IsAdicComplete I M] [IsHausdorff I N] (φ : M →ₗ[A] N) :
    (∃ t : ℕ, 0 < t ∧ ∀ n : ℕ,
        K ^ t ≤ Module.annihilator A
          ↑(LinearMap.ker (Submodule.mapQ (I ^ (n + 1) • (⊤ : Submodule A M))
            (I ^ (n + 1) • (⊤ : Submodule A N)) φ
            (Submodule.smul_top_le_comap_smul_top _ φ))) ∧
        K ^ t ≤ Module.annihilator A
          (_ ⧸ LinearMap.range (Submodule.mapQ (I ^ (n + 1) • (⊤ : Submodule A M))
            (I ^ (n + 1) • (⊤ : Submodule A N)) φ
            (Submodule.smul_top_le_comap_smul_top _ φ)))) ↔
      ∃ t : ℕ, 0 < t ∧ K ^ t ≤ Module.annihilator A ↑(LinearMap.ker φ) ∧
        K ^ t ≤ Module.annihilator A (N ⧸ LinearMap.range φ)

AlgebraicGeometry.Space.IsKernelCokernelAnnihilatedByPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicKernelCokernelAnnihilated.lean, line 195. The attribute's comment: “the notion named by the remark: condition (1), one power of K annihilating every levelwise kernel and cokernel”.

Stacks 08BA, the notion. A map α : (F_n) ⟶ (G_n) of inverse systems of 𝒪_X-modules on an algebraic space is a map whose kernel and cokernel are annihilated by a power of 𝓚 if one integer t ≥ 1 works for every level: 𝓚 ^ t annihilates Ker(α_n) and Coker(α_n) for all n. This is condition (1) of the remark; its equivalence with condition (2), which is what makes the notion the one the remark names, is AlgebraicGeometry.Space.isKernelCokernelAnnihilatedByPower_tfae.

The systems are indexed from 0, the term at n being the source's term at n + 1; the condition quantifies over every level, so this is the source's condition for all n ≥ 1.

def IsKernelCokernelAnnihilatedByPower
    (𝓚 : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS F hF).O))).Submodule)
    {E E' : ℕᵒᵖ ⥤ Modules.{u, u} B S hS F hF} (α : E ⟶ E') : Prop

AlgebraicGeometry.Space.isKernelCokernelAnnihilatedByPower_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicKernelCokernelAnnihilated.lean, line 371. The attribute's comment: “the equivalence of (1) with (2) for any, and for some, surjective etale affine chart U = Spec(A), with alpha_U the map of 087W”.

Stacks Project, Tag 08BA. Let X be a Noetherian algebraic space over a scheme S, let 𝓘, 𝓚 ⊆ 𝒪_X be quasi-coherent sheaves of ideals and let α : (F_n) ⟶ (G_n) be a morphism of Coh(X, 𝓘). For a surjective étale morphism U = Spec(A) ⟶ X write I, K ⊆ A for the ideals of 𝓘|_U, 𝓚|_U and α_U : M ⟶ N for the map of finite A^∧-modules attached to α|_U by Stacks 087W. The following are equivalent:

there is an integer t ≥ 1 such that Ker(α_n) and Coker(α_n) are annihilated by 𝓚 ^ t for all n;

for any such U, the modules Ker(α_U) and Coker(α_U) are annihilated by K ^ t for some integer t ≥ 1;

for some such U, the modules Ker(α_U) and Coker(α_U) are annihilated by K ^ t for some integer t ≥ 1.

A chart U ⟶ X is an object of the small étale site of X, so étale; "U = Spec(A)" is affineness of its underlying scheme; surjectivity is surjectivity after every representable base change. Such a chart exists, by AlgebraicGeometry.Space.exists_surjective_isNoetherianAffineChart, which is what makes (3) follow from (2).

theorem isKernelCokernelAnnihilatedByPower_tfae
    (hZ : B.Contains (⊤_ Scheme.{u})) (hN : IsNoetherian B S hS hZ F)
    (h𝓘 : 𝓘.toSheafOfModules.IsQuasicoherentOnSite)
    (h𝓚 : 𝓚.toSheafOfModules.IsQuasicoherentOnSite)
    {E E' : CoherentAdicSystems B S hS F hF 𝓘} (α : E ⟶ E') :
    List.TFAE
      [IsKernelCokernelAnnihilatedByPower B S hS F hF 𝓚 α.hom,
        ∀ U : SmallEtale B S hS F, IsAffine (chartScheme U) →
          (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf U.1.hom →
          IsChartKernelCokernelAnnihilated B S hS F hF 𝓘 𝓚 α.hom U,
        ∃ U : SmallEtale B S hS F, IsAffine (chartScheme U) ∧
          (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
            (BigFppfOver.toScheme B S hS)).presheaf U.1.hom ∧
          IsChartKernelCokernelAnnihilated B S hS F hF 𝓘 𝓚 α.hom U]

Tag 08BB, a lemma

Tag 08BB in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_iso_of_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionAlgebraization.lean, line 482. The attribute's comment: “uniqueness, carrying left exactness of completion (08B5) as a hypothesis”.

Stacks 08BB, uniqueness of the algebraization.

Let 𝓘 ⊆ 𝒪_F be a quasi-coherent sheaf of ideals on an algebraic space F with locally Noetherian étale charts, let G be a coherent 𝒪_F-module and let E be a coherent 𝓘-adic system with a map α : E ⟶ G^∧. Given two algebraizations of α — coherent modules M, N with maps a : M ⟶ G, a' : N ⟶ G whose kernels and cokernels are annihilated by a power of 𝓘, and isomorphisms β : E ≅ M^∧, β' : E ≅ N^∧ with α = β ≫ a^∧ = β' ≫ a'^∧ — there is a unique isomorphism e : M ≅ N compatible with the maps to G and with the comparison isomorphisms.

Left exactness of the completion functor is carried as a hypothesis, in the form of the instance argument PreservesFiniteLimits (completionFunctor B S hS F hF 𝓘 hI). It is not a hypothesis of the source, which proves it beforehand as Stacks 08B5; it enters this proof only through the step that recognizes the completion of the pullback M ×_G N as the pullback of the completions. Local Noetherianity replaces the source's Noetherian hypothesis, exactly as for the completion functor itself.

The existence of an algebraization is not proved here: the source obtains it by étale descent from the case of a Noetherian scheme, and the restriction of coherent adic systems to an étale chart is not available in this tree.

theorem existsUnique_iso_of_algebraization {G M N : CoherentModules.{u, u} B S hS F hF}
    {E : CoherentAdicSystems B S hS F hF 𝓘}
    (α : E ⟶ (completionFunctor B S hS F hF 𝓘 hI).obj G) (a : M ⟶ G) (a' : N ⟶ G)
    (β : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj M)
    (β' : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj N)
    (ha : IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a)
    (ha' : IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a')
    (hα : α = β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a)
    (hα' : α = β'.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a') :
    ∃! e : M ≅ N, e.hom ≫ a' = a ∧
      β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map e.hom = β'.hom

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

Stacks 08BB. Let F be a Noetherian algebraic space over S and 𝓘 ⊆ 𝒪_F a quasi-coherent sheaf of ideals. Let G be a coherent 𝒪_F-module, E an object of Coh(F, 𝓘) and α : E ⟶ G^∧ a map whose kernel and cokernel are annihilated by a power of 𝓘. Then there exists a triple (M, a, β) where

M is a coherent 𝒪_F-module,

a : M ⟶ G is an 𝒪_F-module map whose kernel and cokernel are annihilated by a power of 𝓘,

β : E ≅ M^∧ is an isomorphism, and

α = a^∧ ∘ β,

and it is unique up to unique isomorphism: for any two such triples (M, a, β) and (N, a', β') there is exactly one isomorphism e : M ≅ N with a' ∘ e = a and e^∧ ∘ β = β'.

theorem exists_algebraization_and_existsUnique_iso
    (hZ : B.Contains (⊤_ Scheme.{u})) (hN : IsNoetherian B S hS hZ F)
    {G : CoherentModules.{u, u} B S hS F hF} {E : CoherentAdicSystems B S hS F hF 𝓘}
    (α : E ⟶ (completionFunctor B S hS F hF 𝓘 hI).obj G)
    (hα : IsSystemKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 α.hom) :
    (∃ (M : CoherentModules.{u, u} B S hS F hF) (a : M ⟶ G)
      (β : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj M),
      IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a ∧
        α = β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a) ∧
    ∀ {M N : CoherentModules.{u, u} B S hS F hF} (a : M ⟶ G) (a' : N ⟶ G)
      (β : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj M)
      (β' : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj N),
      IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a →
      IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a' →
      α = β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a →
      α = β'.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a' →
      ∃! e : M ≅ N, e.hom ≫ a' = a ∧
        β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map e.hom = β'.hom

AlgebraicGeometry.Space.existsUnique_iso_of_algebraization_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionLeftExact.lean, line 133. The attribute's comment: “uniqueness of the algebraization over the source's own hypotheses, with left exactness of completion (Stacks 08B5) supplied”.

Stacks 08BB, uniqueness of the algebraization, over the source's own hypotheses.

Let 𝓘 ⊆ 𝒪_F be a quasi-coherent sheaf of ideals on a Noetherian algebraic space F, let G be a coherent 𝒪_F-module and let E be a coherent 𝓘-adic system with a map α : E ⟶ G^∧. Two algebraizations of α — coherent modules M, N with maps a : M ⟶ G, a' : N ⟶ G whose kernels and cokernels are annihilated by a power of 𝓘, and isomorphisms β : E ≅ M^∧, β' : E ≅ N^∧ factoring α — differ by a unique isomorphism M ≅ N compatible with the maps to G and with the comparison isomorphisms.

AlgebraicGeometry.Space.existsUnique_iso_of_algebraization states this with left exactness of the completion functor as an instance argument, because Stacks 08B5 was not available where it was proved; here that argument is supplied by AlgebraicGeometry.Space.preservesFiniteLimits_completionFunctor_of_isNoetherian, so the only hypotheses left are the source's.

theorem existsUnique_iso_of_algebraization_of_isNoetherian
    (hZ : B.Contains (⊤_ Scheme.{u})) (hN : IsNoetherian B S hS hZ F)
    {G M N : CoherentModules.{u, u} B S hS F hF} {E : CoherentAdicSystems B S hS F hF 𝓘}
    (α : E ⟶ (completionFunctor B S hS F hF 𝓘 hI).obj G) (a : M ⟶ G) (a' : N ⟶ G)
    (β : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj M)
    (β' : E ≅ (completionFunctor B S hS F hF 𝓘 hI).obj N)
    (ha : IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a)
    (ha' : IsMapKernelCokernelAnnihilatedByPower B S hS F hF 𝓘 a')
    (hα : α = β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a)
    (hα' : α = β'.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map a') :
    ∃! e : M ≅ N, e.hom ≫ a' = a ∧
      β.hom ≫ (completionFunctor B S hS F hF 𝓘 hI).map e.hom = β'.hom

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.exists_algebraization, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionAlgebraizationTag.lean, line 93 (StacksFrontier): “existence of the algebraization (F, a, β), over the source's hypotheses with Noetherianity of the algebraic space weakened to local Noetherianity of its étale charts”.
AlgebraicGeometry.Space.C1573.exists_algebraization, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/CoherentCompletionExistence.lean, line 76 (StacksFrontier): “existence of the algebraization (F, a, β), over the source's hypotheses with Noetherianity of the algebraic space weakened to local Noetherianity of its étale charts”.

Tag 08BC, a lemma

Tag 08BC in the Stacks Project.

AlgebraicGeometry.Space.essImage_completionFunctorProperOver_of_auxiliaryIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AuxiliaryIdealClosedSubspace.lean, line 138.

Stacks 08BC. In Situation 08B7 — A Noetherian and I-adically complete, f : X ⟶ Spec A of finite type and separated, 𝓘 = I 𝒪_X — let 𝓚 ⊆ 𝒪_X be a quasi-coherent sheaf of ideals and (F_n) an object of Coh_{support proper over A}(X, 𝓘). Assume

for every e ≥ 1, the closed subspace X_e cut out by 𝓚^e is such that completion along 𝓘_e = I 𝒪_{X_e} is an equivalence Coh_{support proper over A}(𝒪_{X_e}) ≌ Coh_{support proper over A}(X_e, 𝓘_e), and

there are an object 𝓗 of Coh_{support proper over A}(𝒪_X) and a map α : (F_n) ⟶ 𝓗^∧ whose kernel and cokernel are annihilated by a power of 𝓚.

Then (F_n) is in the essential image of the completion functor of Stacks 08B8.

The closed subspace X_e of (1) is given as a closed immersion i : Z ⟶ X whose ideal sheaf ker(𝒪_X ⟶ i_* 𝒪_Z) is 𝓚^e. The proof follows the source: the systems (F_n / 𝓚^(e+1) F_n)_n are algebraized on X_(e+1) and pushed to X (AlgebraicGeometry.Space.C1573.kTorsionEssSurj_of_essSurj); the algebraizations G_e form a coherent 𝓚-adic system mapping to 𝓗^∧ with kernels and cokernels killed by 𝓚^(2t) — the bound the source leaves as "details omitted" (C1573.TorsionAlgebraization.isSystemKernelCokernelAnnihilatedByPower_γSystem, a sharper exponent than the source's 𝓚^(4t)); Stacks 08BB along 𝓚 algebraizes this map to a : 𝓕 ⟶ 𝓗; reducing modulo 𝓘^(n+1) identifies 𝓕 / 𝓘^(n+1) 𝓕 with F_n; and the kernel of a embeds into some G_e by Artin–Rees, so 𝓕 has proper support by Stacks 0CZH (AlgebraicGeometry.Space.C1573.essImage_completionFunctorProperOver_of_kTorsionEssSurj).

theorem essImage_completionFunctorProperOver_of_auxiliaryIdeal [IsNoetherianRing A] (I : Ideal A)
    [IsAdicComplete I A] (X : AlgebraicSpaces B (Spec (.of A)) hA)
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsFiniteType B (Spec (.of A)) hA f.hom)
    (hsep : IsSeparated B (Spec (.of A)) hA f.hom)
    (K : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B (Spec (.of A)) hA X.1
        X.2).O))).Submodule) (hK : K.toSheafOfModules.IsQuasicoherentOnSite)
    (h1 : ∀ e : ℕ, 0 < e → ∃ (Z : AlgebraicSpaces B (Spec (.of A)) hA) (i : Z ⟶ X)
      (hi : IsClosedImmersion B (Spec (.of A)) hA i.hom),
      SheafOfModules.kerIdeal (structureSharp B (Spec (.of A)) hA i) =
        idealPowerMultiple B (Spec (.of A)) hA X.1 X.2 K e (SheafOfModules.unit _) ∧
      letI := C1573.fact_isLocallyNoetherian_of_baseObject Z (i ≫ f)
        (C1573.isLocallyOfFiniteType_closedImmersion_comp i hi f hf.1)
      (completionFunctorProperOver B (Spec (.of A)) hA Z.1 (schemeSpace (baseObject A B hA)).1
        Z.2 (schemeSpace (baseObject A B hA)).2 (i ≫ f).hom
        (C1573.isLocallyOfFiniteType_closedImmersion_comp i hi f hf.1)
        (C1573.baseIdealSubmodule Z.1 Z.2 I)
        (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := Z.1) (hX := Z.2) I)).IsEquivalence)
    (E : CoherentAdicSystemsProperOver B (Spec (.of A)) hA X.2 (schemeSpace (baseObject A B hA)).2
      f.hom hf.1 (C1573.baseIdealSubmodule X.1 X.2 I))
    (H : CoherentModulesProperOver B (Spec (.of A)) hA X.2 (schemeSpace (baseObject A B hA)).2
      f.hom hf.1)
    (α : E ⟶ letI := C1573.fact_isLocallyNoetherian_of_baseObject X f hf.1
      (completionFunctorProperOver B (Spec (.of A)) hA X.1 (schemeSpace (baseObject A B hA)).1 X.2
        (schemeSpace (baseObject A B hA)).2 f.hom hf.1 (C1573.baseIdealSubmodule X.1 X.2 I)
        (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).obj H)
    (hα : IsSystemKernelCokernelAnnihilatedByPower B (Spec (.of A)) hA X.1 X.2 K α.hom.hom) :
    letI := C1573.fact_isLocallyNoetherian_of_baseObject X f hf.1
    (completionFunctorProperOver B (Spec (.of A)) hA X.1 (schemeSpace (baseObject A B hA)).1 X.2
      (schemeSpace (baseObject A B hA)).2 f.hom hf.1 (C1573.baseIdealSubmodule X.1 X.2 I)
      (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).essImage E

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.essImage_completionFunctorProperOver_of_auxiliaryIdeal, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistenceTags.lean, line 33 (StacksFrontier).

Tag 08BD, a lemma

Tag 08BD in the Stacks Project.

AlgebraicGeometry.Space.exists_completionMap_kernel_cokernel_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicCompletionMap.lean, line 221. The attribute's comment: “the full statement: for a representable proper morphism of Noetherian algebraic spaces which is an isomorphism over Y minus V(K), a map alpha from (G_n) to the completion of f_*F in Coh(Y, J) whose levelwise kernels and cokernels are all annihilated by one positive power of K”.

Stacks 08BD. Let f : X ⟶ Y be a representable proper morphism of Noetherian algebraic spaces over S, let 𝓙, 𝓚 ⊆ 𝒪_Y be quasi-coherent sheaves of ideals, and assume f is an isomorphism over Y ∖ V(𝓚). Set 𝓘 = f⁻¹𝓙 𝒪_X. Let (𝓖_n) be an object of Coh(Y, 𝓙), 𝓕 a coherent 𝒪_X-module and β : (f^*𝓖_n) ≅ 𝓕^∧ an isomorphism in Coh(X, 𝓘). Then there is a map α : (𝓖_n) ⟶ (f_*𝓕)^∧ in Coh(Y, 𝓙) whose kernel and cokernel are annihilated by a power of 𝓚 (AlgebraicGeometry.Space.IsKernelCokernelAnnihilatedByPower, the notion of Stacks 08BA: one exponent t > 0 with 𝓚 ^ t killing every levelwise kernel and cokernel).

α is the map whose composite with the comparison (f_*𝓕)^∧ ⟶ f_*(𝓕^∧) is the system of adjunction maps followed by f_*β; it exists because that comparison is an isomorphism on limits (the theorem on formal functions, checked on affine charts), and the annihilation is the scheme case Stacks 088B on one surjective affine chart of Y, spread over Y by quasi-coherence.

theorem exists_completionMap_kernel_cokernel_annihilated (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : yoneda.relativelyRepresentable f.hom)
    (hfp : IsProper B S hS f.hom) (hX : IsNoetherian B S hS hZ X.1)
    (hY : IsNoetherian B S hS hZ Y.1)
    (J K : (SheafOfModules.unit.{u}
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))).Submodule)
    (hJ : J.toSheafOfModules.IsQuasicoherentOnSite) (hK : K.toSheafOfModules.IsQuasicoherentOnSite)
    (hiso : IsIso ((idealComplementSubfunctor B S hS Y K).fromPreimage f.hom))
    (G : CoherentAdicSystems B S hS Y.1 Y.2 J) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : IsCoherent B S hS X.1 X.2 F) :
    letI : Fact (HasEtaleLocalProperty B S hS X.1 (fun V : Scheme.{u} => IsLocallyNoetherian V)) :=
      ⟨hX.2.2⟩
    letI : Fact (HasEtaleLocalProperty B S hS Y.1 (fun V : Scheme.{u} => IsLocallyNoetherian V)) :=
      ⟨hY.2.2⟩
    ∀ _β : G.obj ⋙ modulePullback B S hS f ≅
        ((completionFunctor B S hS X.1 X.2 (pullbackIdealSubsheaf B S hS f hf J)
          (isQuasicoherentOnSite_pullbackIdealSubsheaf B S hS f hf J hJ)).obj ⟨F, hF⟩).obj,
      ∃ α : G ⟶ (completionFunctor B S hS Y.1 Y.2 J hJ).obj
          ⟨(modulePushforward B S hS f).obj F,
            isCoherent_modulePushforward_of_isProper B S hS f hf hfp hY.2.2 F hF⟩,
        IsKernelCokernelAnnihilatedByPower B S hS Y.1 Y.2 K α.hom

AlgebraicGeometry.Space.directImageComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicDirectImageComparison.lean, line 163. The attribute's comment: “the maps gamma_n of the proof: the adjunction map followed by f_beta_n. The map alpha into (f_F)^ is a different declaration and is not constructed in this library”.

The maps γ_n : 𝓖_n ⟶ f_*f^*𝓖_n ⟶ f_*(𝓕/𝓘 ⁿ⁺¹𝓕) of the proof of Stacks 08BD, as a morphism of inverse systems of 𝒪_Y-modules on an algebraic space: the adjunction map followed by f_*β_n.

def directImageComparison :
    G.obj ⟶ ((completionFunctor B S hS X.1 X.2 𝓘 hI).obj F).obj ⋙ modulePushforward B S hS f

AlgebraicGeometry.Space.exists_pos_idealPowerMultiple_kernel_cokernel_directImageComparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoherentAdicDirectImageComparison.lean, line 210. The attribute's comment: “the reduction of the lemma's kernel-cokernel condition from gamma to the adjunction maps. The map alpha into (f_*F)^ is not constructed in this library, which proves neither 08AR for a representable proper morphism nor the uniform Artin-Rees bounds 02OB behind the scheme case 088B”.

The reduction of the kernel–cokernel condition of Stacks 08BD to the adjunction maps. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S, let 𝓙, 𝓚 ⊆ 𝒪_Y and 𝓘 ⊆ 𝒪_X be sheaves of ideals, let (𝓖_n) be an object of Coh(Y, 𝓙), let 𝓕 be a coherent 𝒪_X-module and let β : (f^*𝓖_n) ⟶ 𝓕^∧ be an isomorphism in Coh(X, 𝓘). The maps

γ_n : 𝓖_n ⟶ f_*f^*𝓖_n ⟶ f_*(𝓕/𝓘 ⁿ⁺¹𝓕)

have their levelwise kernels and cokernels annihilated by one positive power of 𝓚 exactly when the adjunction maps 𝓖_n ⟶ f_*f^*𝓖_n do, because γ_n differs from the adjunction map by the isomorphism f_*β_n. This is the step of the source's proof which makes the isomorphism β disappear from the annihilation statement, leaving the adjunction map that the closing paragraph of the scheme case is about.

The map α : (𝓖_n) ⟶ (f_*𝓕)^∧ which the source produces out of γ is not constructed; see the implementation notes of this file.

theorem exists_pos_idealPowerMultiple_kernel_cokernel_directImageComparison_iff
    (𝓚 : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))).Submodule) :
    (∃ t : ℕ, 0 < t ∧ ∀ k : ℕ,
        idealPowerMultiple B S hS Y.1 Y.2 𝓚 t
            (kernel ((directImageComparison B S hS f 𝓙 𝓘 hI G F β).app (op k))) = ⊥ ∧
          idealPowerMultiple B S hS Y.1 Y.2 𝓚 t
            (cokernel ((directImageComparison B S hS f 𝓙 𝓘 hI G F β).app (op k))) = ⊥) ↔
      ∃ t : ℕ, 0 < t ∧ ∀ k : ℕ,
        idealPowerMultiple B S hS Y.1 Y.2 𝓚 t
            (kernel ((pullbackPushforwardUnitSystem B S hS f G.obj).app (op k))) = ⊥ ∧
          idealPowerMultiple B S hS Y.1 Y.2 𝓚 t
            (cokernel ((pullbackPushforwardUnitSystem B S hS f G.obj).app (op k))) = ⊥

AlgebraicGeometry.Space.exists_hom_completion_modulePushforward_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperDirectImageCompletionMap.lean, line 71.

Stacks 08BD. For a representable proper morphism f : X ⟶ Y of Noetherian algebraic spaces which is an isomorphism over the complement of the closed subspace Z = V(𝒦), a coherent 𝒥-adic system (𝒢_n) on Y, a coherent 𝒪_X-module 𝓕 and an isomorphism β : (f^*𝒢_n) ≅ 𝓕^∧ of inverse systems on X (for the ideal 𝓘 = f⁻¹𝒥 𝒪_X), the direct image f_*𝓕 is coherent and there is a map α : (𝒢_n) ⟶ (f_*𝓕)^∧ of coherent 𝒥-adic systems whose kernel and cokernel are annihilated by a power of 𝒦.

theorem exists_hom_completion_modulePushforward_annihilated
    (hZ0 : B.Contains (⊤_ Scheme.{u})) {X Y : AlgebraicSpaces B S hS}
    (hX : IsNoetherian B S hS hZ0 X.1) (hY : IsNoetherian B S hS hZ0 Y.1)
    (f : X ⟶ Y) (hf : yoneda.relativelyRepresentable f.hom) (hfp : IsProper B S hS f.hom)
    (J K : (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))).Submodule)
    (hJ : J.toSheafOfModules.IsQuasicoherentOnSite)
    (Z : ClosedSubspaces B S hS Y.1) (hZ : definingIdealSheaf B S hS Y Z = K)
    (hiso : IsIso ((openComplement B S hS Z.1).fromPreimage f.hom))
    (G : CoherentAdicSystems B S hS Y.1 Y.2 J)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F)
    (β : G.obj ⋙ modulePullback B S hS f ≅
      adicQuotientSystem B S hS X.1 X.2 (C1573.inverseImageIdeal B S hS f hf J) F) :
    haveI : Fact (HasEtaleLocalProperty B S hS Y.1
        (fun T : Scheme.{u} => IsLocallyNoetherian T)) := ⟨hY.2.2⟩
    ∃ hP : IsCoherent B S hS Y.1 Y.2 ((modulePushforward B S hS f).obj F),
      ∃ α : G ⟶ (completionFunctor B S hS Y.1 Y.2 J hJ).obj
          ⟨(modulePushforward B S hS f).obj F, hP⟩,
        IsSystemKernelCokernelAnnihilatedByPower B S hS Y.1 Y.2 K α.hom

Tag 08BE, a theorem

Tag 08BE in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_completionFunctorProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistenceSpaces.lean, line 53.

Stacks 08BE, Grothendieck's existence theorem for algebraic spaces. Let A be a Noetherian ring complete with respect to an ideal I, and let f : X ⟶ Spec A be a separated morphism of finite type of algebraic spaces (Situation 08B7, with 𝓘 = I 𝒪_X). Then the completion functor

Coh_{support proper over A}(𝒪_X) ⟶ Coh_{support proper over A}(X, 𝓘)

of Stacks 08B8 is an equivalence of categories.

theorem isEquivalence_completionFunctorProperOver [IsNoetherianRing A] (I : Ideal A)
    [IsAdicComplete I A] (X : AlgebraicSpaces B (Spec (.of A)) hA)
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsFiniteType B (Spec (.of A)) hA f.hom)
    (hsep : IsSeparated B (Spec (.of A)) hA f.hom) :
    letI := C1573.fact_isLocallyNoetherian_of_baseObject X f hf.1
    (completionFunctorProperOver B (Spec (.of A)) hA X.1 (schemeSpace (baseObject A B hA)).1 X.2
      (schemeSpace (baseObject A B hA)).2 f.hom hf.1 (C1573.baseIdealSubmodule X.1 X.2 I)
      (C1573.isQuasicoherentOnSite_baseIdealSubmodule (X := X.1) (hX := X.2) I)).IsEquivalence

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.isEquivalence_completionFunctorProperOver, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/GrothendieckExistenceTags.lean, line 36 (StacksFrontier).

Tag 08BF, a remark

Tag 08BF in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_adicFibreRestrictionProperOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdicFibreSystem.lean, line 410.

Stacks 08BF. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec(A/Iⁿ), and let X ⟶ S be a separated morphism of algebraic spaces of finite type, with Xₙ = X ×_S Sₙ. Then the completion functor 𝓕 ↦ (𝓕|_{Xₙ})ₙ, from coherent 𝒪_X-modules with support proper over A to systems (𝓕ₙ, φₙ) of coherent 𝒪_{Xₙ}-modules 𝓕ₙ with isomorphisms φₙ : iₙ^* 𝓕ₙ₊₁ ≅ 𝓕ₙ such that Supp(𝓕₁) is proper over S₁, is an equivalence of categories.

The adic fibres are indexed from 0: adicFibreSpaceOf A I B hA X f n is the source's Xₙ₊₁.

theorem isEquivalence_adicFibreRestrictionProperOver [IsNoetherianRing A] [IsAdicComplete I A]
    (hf : IsFiniteType B (Spec (.of A)) hA f.hom) (hsep : IsSeparated B (Spec (.of A)) hA f.hom) :
    (adicFibreRestrictionProperOver I X f hf.1).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_adicFibreRestriction_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdicFibreSystem.lean, line 434. The attribute's comment: “the special case of X proper over A, where the conditions on the supports are omitted”.

Stacks 08BF, the case of X proper over A. If X ⟶ S = Spec A is proper, the completion functor 𝓕 ↦ (𝓕|_{Xₙ})ₙ from all coherent 𝒪_X-modules to all systems (𝓕ₙ, φₙ) of coherent 𝒪_{Xₙ}-modules with isomorphisms φₙ : iₙ^* 𝓕ₙ₊₁ ≅ 𝓕ₙ is an equivalence of categories: the conditions on the supports can be omitted.

theorem isEquivalence_adicFibreRestriction_of_isProper [IsNoetherianRing A] [IsAdicComplete I A]
    (hf : IsProper B (Spec (.of A)) hA f.hom) :
    (adicFibreRestrictionOf I X f hf.2.1.1).IsEquivalence

Sources

LeanAlgebraicGeometry.Space.abelian_coherentAdicSystems · AlgebraicGeometry.Space.coherentAdicInverseImage_exact · AlgebraicGeometry.Space.exact_iff_forall_exact_coherentAdicChartRestriction · AlgebraicGeometry.Space.coherentAdicSystems_abelian_and_exact · AlgebraicGeometry.Space.epi_iff_epi_app_zero · AlgebraicGeometry.Space.completionFunctor · AlgebraicGeometry.Space.preservesFiniteColimits_completionFunctor · AlgebraicGeometry.Space.preservesMonomorphisms_completionFunctor

Section76.43 Grothendieck's algebraization theorem #

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

Tag 08BG, a lemma

Tag 08BG in the Stacks Project.

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

Stacks 08BG. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and S_n = Spec(A / I^{n+1}), and let X ⟶ S be a separated morphism of finite type of algebraic spaces, with adic fibres X_n = X ×_S S_n. Let Z_n be algebraic spaces with morphisms j_n : Z_n ⟶ X_n and t_n : Z_n ⟶ Z_{n+1} making every square Z_n ⟶ Z_{n+1} over X_n ⟶ X_{n+1} cartesian. If Z_0 ⟶ X_0 is a closed immersion and Z_0 ⟶ S_0 is proper, then there is a closed immersion i : Z ⟶ X of algebraic spaces with Z ⟶ S proper and isomorphisms Z_n ≅ Z ×_S S_n over X_n, compatible with the transition maps.

The index n stands for the source's n + 1: Z 0 = Z_1, X 0 = X_1, S 0 = S_1.

theorem exists_isClosedImmersion_adicFibre_iso [IsNoetherianRing A] [IsAdicComplete I A]
    {X : (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B (Spec (.of A)) hS X)
    (fX : X ⟶ yoneda.obj (baseObject A B hS)) (hft : IsFiniteType B (Spec (.of A)) hS fX)
    (hsep : IsSeparated B (Spec (.of A)) hS fX)
    (Z : ℕ → (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u)
    (hZ : ∀ n, IsAlgebraicSpace B (Spec (.of A)) hS (Z n))
    (j : ∀ n, Z n ⟶ adicFibre A I B hS hSn fX n) (t : ∀ n, Z n ⟶ Z (n + 1))
    (hcart : ∀ n, IsPullback (t n) (j n) (j (n + 1)) (adicFibreSucc A I B hS hSn fX n))
    (hj : IsClosedImmersion B (Spec (.of A)) hS (j 0))
    (hprop : IsProper B (Spec (.of A)) hS
      (j 0 ≫ pullback.snd fX (yoneda.map (adicThickeningMap A I B hS hSn 0)))) :
    ∃ (W : (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u)
      (_ : IsAlgebraicSpace B (Spec (.of A)) hS W) (i : W ⟶ X),
      IsClosedImmersion B (Spec (.of A)) hS i ∧ IsProper B (Spec (.of A)) hS (i ≫ fX) ∧
      ∃ e : ∀ n, Z n ≅ adicFibre A I B hS hSn (i ≫ fX) n,
        (∀ n, (e n).hom ≫ adicFibreMap A I B hS hSn i rfl n = j n) ∧
        (∀ n, t n ≫ (e (n + 1)).hom = (e n).hom ≫ adicFibreSucc A I B hS hSn (i ≫ fX) n)

Tag 0A01, a lemma

Tag 0A01 in the Stacks Project.

AlgebraicGeometry.Space.exists_isFinite_adicFibre_iso_of_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdicFiniteAlgebraization/FiniteAlgebraization.lean, line 62.

Algebraization of a finite tower over the adic fibres. Let A be a Noetherian ring complete along I, S = Spec A, and f : X ⟶ S a separated morphism of finite type of algebraic spaces with adic fibres X_n = X ×_S S_n. Let y_n : Y_n ⟶ X_n be algebraic spaces over the adic fibres with transitions t_n : Y_n ⟶ Y_{n + 1} making cartesian squares over the transitions X_n ⟶ X_{n + 1}, with Y_0 ⟶ X_0 finite and Y_0 ⟶ S_0 proper. Then there is a finite π : Y ⟶ X with Y proper over S, and isomorphisms Y_n ≅ Y ×_S S_n lying over X_n, compatible with the transitions, and exhibiting Y_n as Y ×_X X_n.

The tower is indexed from 0: S_n is Spec (A / I ^ (n + 1)), so the n-th term here is the (n + 1)-st term Y_{n + 1} of Stacks, and Y_0 ⟶ X_0, Y_0 ⟶ S_0 are Stacks' Y_1 ⟶ X_1, Y_1 ⟶ S_1.

theorem exists_isFinite_adicFibre_iso_of_tower [IsAdicComplete I A]
    (hsep : IsSeparated B (Spec (.of A)) hA f) (hft : IsFiniteType B (Spec (.of A)) hA f)
    (Y : ℕ → AlgebraicSpaces B (Spec (.of A)) hA) (y : ∀ n, Y n ⟶ adicFibreSpace A I B hA hX f n)
    (tY : ∀ n, Y n ⟶ Y (n + 1))
    (hcart : ∀ n, IsPullback (tY n) (y n) (y (n + 1)) (adicFibreSuccHom A I B hA hX f n))
    (hfin0 : IsFinite B (Spec (.of A)) hA (y 0).hom)
    (hprop : IsProper B (Spec (.of A)) hA ((y 0).hom ≫ adicFibreSnd A I B hA f 0)) :
    ∃ (Z : AlgebraicSpaces B (Spec (.of A)) hA) (π : Z ⟶ ⟨X, hX⟩),
      IsFinite B (Spec (.of A)) hA π.hom ∧ IsProper B (Spec (.of A)) hA (π.hom ≫ f) ∧
      ∃ e : ∀ n, Y n ≅ adicFibreSpace A I B hA Z.2 (π.hom ≫ f) n,
        (∀ n, (e n).hom.hom ≫
          adicFibreMap A I B hA (contains_adicThickening A I B hA) π.hom rfl n = (y n).hom) ∧
        (∀ n, tY n ≫ (e (n + 1)).hom =
          (e n).hom ≫ adicFibreSuccHom A I B hA Z.2 (π.hom ≫ f) n) ∧
        (∀ n, IsPullback ((e n).hom ≫ adicFibreFst A I B hA Z.2 (π.hom ≫ f) n) (y n) π
          (adicFibreFstHom A I B hA hX f n))

Tag 0A4Z, a lemma

Tag 0A4Z in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.existsUnique_adicFibreMap_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/MorphismAlgebraizationTag.lean, line 23 (StacksFrontier).

Tag 0GHK, a remark

Tag 0GHK in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_adicFibreMap_eq_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MorphismAlgebraizationLocallyFiniteType.lean, line 248. The attribute's comment: “the separated case: Y ⟶ S separated and locally of finite type; the quasi-separated case rests on Bhatt and Hall–Rydh, outside the Stacks project, and the open general question is not a statement”.

Stacks 0GHK, the separated case. Let A be a Noetherian ring complete with respect to an ideal I, S = Spec A, S_n = Spec (A / I^{n+1}), and let X, Y be algebraic spaces over S with X ⟶ S proper and Y ⟶ S separated and locally of finite type. A compatible system of morphisms g_n : X_n ⟶ Y_n over the S_n between the adic fibres is the system of adic fibres of exactly one morphism g : X ⟶ Y over S.

Remark 0GHK asks whether Stacks 0A4Z survives with Y ⟶ S only locally of finite type. This declaration formalizes the remark's assertion that the answer is yes when Y ⟶ S is separated, by the remark's reduction to a quasi-compact open of Y containing the image of g_1 (here g 0); uniqueness is included, as in Stacks 0A4Z. The remark's statement "we don't know the answer in general" is an open question, not a mathematical assertion, and is not formalized. The remark's further assertion for Y ⟶ S only quasi-separated is not formalized: the remark gives no proof inside the Stacks project, deferring to Bhatt's algebraization theorem for D_perf and to Hall–Rydh's coherent Tannaka duality, papers outside the project.

theorem existsUnique_adicFibreMap_eq_of_isLocallyOfFiniteType [IsNoetherianRing A]
    [IsAdicComplete I A] (hX : IsAlgebraicSpace B _ hS X) (hY : IsAlgebraicSpace B _ hS Y)
    (fX : X ⟶ yoneda.obj (baseObject A B hS)) (fY : Y ⟶ yoneda.obj (baseObject A B hS))
    (hpX : IsProper B _ hS fX) (hsY : IsSeparated B _ hS fY)
    (hlY : IsLocallyOfFiniteType B _ hS fY)
    (g : ∀ n, adicFibre A I B hS hSn fX n ⟶ adicFibre A I B hS hSn fY n)
    (hg : ∀ n, g n ≫ pullback.snd fY (yoneda.map (adicThickeningMap A I B hS hSn n)) =
      pullback.snd fX (yoneda.map (adicThickeningMap A I B hS hSn n)))
    (hgc : ∀ n, adicFibreSucc A I B hS hSn fX n ≫ g (n + 1) =
      g n ≫ adicFibreSucc A I B hS hSn fY n) :
    ∃! φ : X ⟶ Y, ∃ hφ : φ ≫ fY = fX, ∀ n, adicFibreMap A I B hS hSn φ hφ n = g n

Tag 0E7R, a lemma

Tag 0E7R in the Stacks Project.

AlgebraicGeometry.Space.exists_isProjective_algebraization_of_dimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalCurve/SpaceAlgebraization.lean, line 72.

[Stacks, Tag 0E7R], algebraization of formal curves. Let A be a complete local Noetherian ring, S = Spec A, Sₙ = Spec (A / 𝔪 ^ (n + 1)), and let Xₙ ⟶ Sₙ be algebraic spaces with transition maps iₙ : Xₙ ⟶ Xₙ₊₁ making every square over Sₙ ⟶ Sₙ₊₁ cartesian. If X₀ ⟶ S₀ is proper and dim X₀ ≤ 1, there are a projective morphism of schemes fY : Y ⟶ S and morphisms kₙ : Xₙ ⟶ Y, compatible with the iₙ, identifying each Xₙ with Y ×_S Sₙ.

theorem exists_isProjective_algebraization_of_dimension_le_one
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [IsAdicComplete (maximalIdeal A) A]
    (B : BigFppfSite.{u}) (hS : B.Contains (Spec (.of A)))
    (X : ℕ → (BigFppfOver B (Spec (.of A)) hS)ᵒᵖ ⥤ Type u)
    (hX : ∀ n, IsAlgebraicSpace B (Spec (.of A)) hS (X n))
    (p : ∀ n, X n ⟶ yoneda.obj (adicThickeningObject A (maximalIdeal A) B hS
      (contains_adicThickening A (maximalIdeal A) B hS) n))
    (i : ∀ n, X n ⟶ X (n + 1))
    (hcart : ∀ n, IsPullback (i n) (p n) (p (n + 1))
      (yoneda.map (adicThickeningSuccMap A (maximalIdeal A) B hS
        (contains_adicThickening A (maximalIdeal A) B hS) n)))
    (hproper : IsProper B (Spec (.of A)) hS (p 0))
    (hdim : dimension B (Spec (.of A)) hS (X 0) (hX 0) ≤ 1) :
    ∃ (Y : Scheme.{u}) (hY : B.Contains Y) (fY : Y ⟶ Spec (.of A)),
      IsProjective fY ∧ IsProjectiveMorphism fY ∧
      ∃ k : ∀ n, X n ⟶ yoneda.obj (siteObject B (Spec (.of A)) hS hY fY),
        (∀ n, i n ≫ k (n + 1) = k n) ∧
        ∀ n, IsPullback (k n) (p n) (yoneda.map (siteObjectToBase A B hS hY fY))
          (yoneda.map (adicThickeningMap A (maximalIdeal A) B hS
            (contains_adicThickening A (maximalIdeal A) B hS) n))

Tag 0AE7, a lemma

Tag 0AE7 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.C1605.exists_iso_isProjective_of_isProper_of_dimension_adicFibre_le_one, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ProperCurveOverCompleteLocalScheme.lean, line 25 (StacksFrontier).

Sources

LeanAlgebraicGeometry.Space.exists_isClosedImmersion_adicFibre_iso · AlgebraicGeometry.Space.exists_isFinite_adicFibre_iso_of_tower · AlgebraicGeometry.Space.existsUnique_adicFibreMap_eq · AlgebraicGeometry.Space.existsUnique_adicFibreMap_eq_of_isLocallyOfFiniteType · AlgebraicGeometry.Space.exists_isProjective_algebraization_of_dimension_le_one · AlgebraicGeometry.Space.C1605.exists_iso_isProjective_of_isProper_of_dimension_adicFibre_le_one

Section76.44 Regular immersions #

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

Tag 06BM, a lemma

Tag 06BM in the Stacks Project.

AlgebraicGeometry.Space.property_on_all_etale_charts_iff_exists_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersion.lean, line 134. The attribute's comment: “equivalence of all charts and one surjective chart”.

Stacks 06BM, the equivalence of conditions (1) and (2). For a property P of scheme morphisms which is étale local on the target and a representable morphism f of algebraic spaces over S, the projection of the represented fibre product has P over every étale scheme chart of the target if and only if it has P over some surjective étale chart.

theorem property_on_all_etale_charts_iff_exists_atlas (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (P : MorphismProperty Scheme.{u})
    [P.IsLocalAtTarget Scheme.etalePrecoverage]
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (_hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hf : yoneda.relativelyRepresentable f) :
    (∀ (V : BigFppfOver B S hS) (q : yoneda.obj V ⟶ Y),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q →
      P ((BigFppfOver.toScheme B S hS).map (hf.snd q))) ↔
    (∃ (V : BigFppfOver B S hS) (q : yoneda.obj V ⟶ Y),
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q ∧
      P ((BigFppfOver.toScheme B S hS).map (hf.snd q)))

AlgebraicGeometry.Space.property_on_all_etale_charts_iff_of_schemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersion.lean, line 222. The attribute's comment: “comparison when both spaces are schemes”.

Stacks 06BM, the comparison with the scheme-theoretic property. When the source and target of a representable morphism of algebraic spaces over S are representable, the condition of Stacks 06BM on all étale charts holds exactly when the morphism of schemes they represent has the property.

theorem property_on_all_etale_charts_iff_of_schemes (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (P : MorphismProperty Scheme.{u})
    [P.IsLocalAtTarget Scheme.etalePrecoverage]
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} [X.IsRepresentable] [Y.IsRepresentable]
    (f : X ⟶ Y) (hf : yoneda.relativelyRepresentable f) :
    (∀ (W : BigFppfOver B S hS) (q : yoneda.obj W ⟶ Y),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf q →
      P ((BigFppfOver.toScheme B S hS).map (hf.snd q))) ↔
    P ((BigFppfOver.toScheme B S hS).map
      (yoneda.preimage (X.reprW.hom ≫ f ≫ Y.reprW.inv)))

Tag 06BN, a definition

Tag 06BN in the Stacks Project.

AlgebraicGeometry.Space.IsKoszulRegularImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersion.lean, line 268. The attribute's comment: “part (1): Koszul-regular immersion”.

Stacks 06BN, part (1). A representable morphism of algebraic spaces over S is a Koszul-regular immersion when its base change to every étale scheme chart of the target is a Koszul-regular immersion of schemes.

abbrev IsKoszulRegularImmersion (i : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsH1RegularImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersion.lean, line 282. The attribute's comment: “part (2): H₁-regular immersion”.

Stacks 06BN, part (2). A representable morphism of algebraic spaces over S is an H₁-regular immersion when its base change to every étale scheme chart of the target is an H₁-regular immersion of schemes.

abbrev IsH1RegularImmersion (i : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsQuasiRegularImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersion.lean, line 296. The attribute's comment: “part (3): quasi-regular immersion”.

Stacks 06BN, part (3). A representable morphism of algebraic spaces over S is a quasi-regular immersion when its base change to every étale scheme chart of the target is a quasi-regular immersion of schemes.

abbrev IsQuasiRegularImmersion (i : X ⟶ Y) : Prop

Tag 06BP, a lemma

Tag 06BP in the Stacks Project.

AlgebraicGeometry.Space.isH1RegularImmersion_of_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionImplications.lean, line 71. The attribute's comment: “Koszul-regular implies H₁-regular”.

Stacks tag 06BP, the first implication. A Koszul-regular immersion of algebraic spaces over S is an H₁-regular immersion: degree 1 is a positive degree, so the condition on each étale chart becomes weaker.

theorem isH1RegularImmersion_of_isKoszulRegularImmersion (i : Z ⟶ X)
    (h : IsKoszulRegularImmersion B S hS i) : IsH1RegularImmersion B S hS i

AlgebraicGeometry.Space.isQuasiRegularImmersion_of_isH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionImplications.lean, line 81. The attribute's comment: “H₁-regular implies quasi-regular”.

Stacks tag 06BP, the second implication. An H₁-regular immersion of algebraic spaces over S is a quasi-regular immersion.

theorem isQuasiRegularImmersion_of_isH1RegularImmersion (i : Z ⟶ X)
    (h : IsH1RegularImmersion B S hS i) : IsQuasiRegularImmersion B S hS i

Tag 09RW, a lemma

Tag 09RW in the Stacks Project.

AlgebraicGeometry.Space.isKoszulRegularImmersion_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionImplications.lean, line 109.

Stacks tag 09RW. For an immersion of algebraic spaces over S into a locally Noetherian algebraic space, Koszul-regularity, H₁-regularity and quasi-regularity agree.

theorem isKoszulRegularImmersion_tfae (_hZ : IsAlgebraicSpace B S hS Z)
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X) (_hi : IsImmersion B S hS i)
    (hnoeth : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    List.TFAE
      [IsKoszulRegularImmersion B S hS i,
        IsH1RegularImmersion B S hS i,
        IsQuasiRegularImmersion B S hS i]

Tag 09RX, a lemma

Tag 09RX in the Stacks Project.

AlgebraicGeometry.Space.isKoszulRegularImmersion_pullback_snd_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersionFlatBaseChange.lean, line 231. The attribute's comment: “koszul”.

Stacks 09RX, the Koszul-regular clause. The base change Z ×_X X' ⟶ X' of a Koszul-regular immersion i : Z ⟶ X of algebraic spaces over S along a flat morphism g : X' ⟶ X is a Koszul-regular immersion.

theorem isKoszulRegularImmersion_pullback_snd_of_isFlat (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {Z X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X) (g : X' ⟶ X) (hg : IsFlat B S hS g)
    (hi : IsKoszulRegularImmersion B S hS i) :
    IsKoszulRegularImmersion B S hS (pullback.snd i g)

AlgebraicGeometry.Space.isH1RegularImmersion_pullback_snd_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersionFlatBaseChange.lean, line 271. The attribute's comment: “h1”.

Stacks 09RX, the H₁-regular clause. The base change Z ×_X X' ⟶ X' of an H₁-regular immersion i : Z ⟶ X of algebraic spaces over S along a flat morphism g : X' ⟶ X is an H₁-regular immersion.

theorem isH1RegularImmersion_pullback_snd_of_isFlat (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {Z X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X) (g : X' ⟶ X) (hg : IsFlat B S hS g)
    (hi : IsH1RegularImmersion B S hS i) :
    IsH1RegularImmersion B S hS (pullback.snd i g)

AlgebraicGeometry.Space.isQuasiRegularImmersion_pullback_snd_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersionFlatBaseChange.lean, line 312. The attribute's comment: “quasi”.

Stacks 09RX, the quasi-regular clause. The base change Z ×_X X' ⟶ X' of a quasi-regular immersion i : Z ⟶ X of algebraic spaces over S along a flat morphism g : X' ⟶ X is a quasi-regular immersion.

theorem isQuasiRegularImmersion_pullback_snd_of_isFlat (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {Z X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X) (g : X' ⟶ X) (hg : IsFlat B S hS g)
    (hi : IsQuasiRegularImmersion B S hS i) :
    IsQuasiRegularImmersion B S hS (pullback.snd i g)

Tag 09RY, a lemma

Tag 09RY in the Stacks Project.

AlgebraicGeometry.Space.isQuasiRegularImmersion_iff_conormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/QuasiRegularConormalCriterion.lean, line 81. The attribute's comment: “the whole statement: an immersion of algebraic spaces is quasi-regular iff it is locally of finite presentation, its conormal sheaf is finite locally free, and the map of 09RQ from the symmetric algebra on the conormal sheaf is an isomorphism in every degree, for every symmetric algebra”.

Stacks Project, Tag 09RY. An immersion i : Z ⟶ X of algebraic spaces is a quasi-regular immersion if and only if (1) it is locally of finite presentation, (2) its conormal sheaf 𝒞_{Z/X} is finite locally free, and (3) the canonical map Sym^*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} of Stacks 09RQ is an isomorphism in every degree, for every symmetric algebra Sym^*(𝒞_{Z/X}) on the conormal sheaf.

The proof reduces to the closed factorisation Z ⟶ X ∖ ∂Z of Stacks 04CE and its base changes to the étale charts of X ∖ ∂Z, where the case of schemes, Stacks 063M, is run on the sections of the conormal algebra over affine charts; see the module documentation.

theorem isQuasiRegularImmersion_iff_conormal (hX : IsAlgebraicSpace B S hS X₀)
    (hZ : IsAlgebraicSpace B S hS Z₀) (i : Z₀ ⟶ X₀) (hi : IsImmersion B S hS i) :
    IsQuasiRegularImmersion B S hS i ↔
      IsLocallyOfFinitePresentation B S hS i ∧
        SheafOfModules.IsFiniteLocallyFreeOnSite (conormalModuleOfImmersion B S hS hX hZ i hi) ∧
        ∀ (A : SheafOfModules.GradedAlgebra.{u, u}
            (structureRingSheaf B S hS (⟨Z₀, hZ⟩ : AlgebraicSpaces B S hS)))
          (ι : (conormalAlgebraOfImmersion B S hS hX hZ i hi).piece 1 ⟶ A.piece 1)
          (hA : SheafOfModules.GradedAlgebra.IsSymmetricAlgebra A ι) (n : ℤ),
          IsIso ((symmetricAlgebraToConormalAlgebraOfImmersion B S hS hX hZ i hi A ι hA).app
            n)

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isQuasiRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersion.lean, line 359. The attribute's comment: “the direction out of quasi-regularity, condition (1) only: a quasi-regular immersion of algebraic spaces is locally of finite presentation. Conditions (2) and (3) and the converse are not transported, because the case of schemes, Tag 063M, is itself carried only as conditions (1) and (2) out of quasi-regularity”.

Stacks 09RY, condition (1) in the direction out of quasi-regularity. A quasi-regular immersion of algebraic spaces over S is locally of finite presentation.

Each represented base change of i to an étale scheme chart of the target is a quasi-regular immersion of schemes, hence locally of finite presentation by the case of schemes [Stacks, Tag 063M]; local finite presentation is étale local on the source and target [Stacks, Tag 04R3], so those chart conditions are the local finite presentation of i.

theorem isLocallyOfFinitePresentation_of_isQuasiRegularImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {Z X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hZ : IsAlgebraicSpace B S hS Z)
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ X)
    (_hIm : IsImmersion B S hS i) (h : IsQuasiRegularImmersion B S hS i) :
    IsLocallyOfFinitePresentation B S hS i

Tag 09RZ, a lemma

Tag 09RZ in the Stacks Project.

AlgebraicGeometry.Space.isSplitExactConormalSequenceOnEtaleCharts_of_isH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionConormalSequence.lean, line 108. The attribute's comment: “both conclusions — exactness and local splitness — of the conormal sequence of Tag 06BD for an H₁-regular immersion, read on the étale scheme charts of X as IsSplitExactConormalSequenceOnEtaleCharts, which is how this development states every condition on algebraic spaces whose scheme analogue it localizes. The sequence has no left-hand map as a sequence of modules on Z in this development, so nothing is asserted about it on Z itself; the splitting is étale-local, Zariski-local on each chart of an étale cover, and is neither global nor claimed on a single chart”. References: SGA 6 VIII (2.2), “partial”.

[Stacks Project, Tag 09RZ]. Let i : Z ⟶ Y and j : Y ⟶ X be morphisms of algebraic spaces over S with j an immersion and i an H₁-regular immersion. Then the conormal sequence 0 ⟶ i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0 of [Stacks Project, Tag 06BD] is exact and locally split, read on the étale scheme charts of X: over every such chart the base changes of j and of i are immersions of schemes whose conormal sequence is short exact and splits on a neighbourhood of every point.

Over a chart c of X the pair of scheme immersions is the base change of j to c together with the base change of i to the chart of Y that j pulls back from c. That chart of Y is étale, because étaleness of a morphism of presheaves is stable under base change, so H₁-regularity of i gives it for the base change of i; the case of schemes, [Stacks Project, Tag 063N] in the bundled form Stacks.AlgebraicGeometry.isSplitExactConormalSequence_of_isH1RegularImmersion, then applies.

This is the hypothesis of the three clauses of [Stacks Project, Tag 09S1]; see AlgebraicGeometry.Space.isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence and its siblings.

theorem isSplitExactConormalSequenceOnEtaleCharts_of_isH1RegularImmersion (i : Z ⟶ Y) (j : Y ⟶ X)
    (hj : IsImmersion B S hS j) (hi : IsH1RegularImmersion B S hS i) :
    IsSplitExactConormalSequenceOnEtaleCharts B S hS i j

Tag 09S0, a lemma

Tag 09S0 in the Stacks Project.

AlgebraicGeometry.Space.isKoszulRegularImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionComposition.lean, line 415. The attribute's comment: “composition of Koszul-regular immersions”.

Stacks 09S0, the Koszul-regular case. The composite of two Koszul-regular immersions of algebraic spaces over S is a Koszul-regular immersion.

theorem isKoszulRegularImmersion_comp (i : Z ⟶ Y) (j : Y ⟶ X)
    (hi : IsKoszulRegularImmersion B S hS i) (hj : IsKoszulRegularImmersion B S hS j) :
    IsKoszulRegularImmersion B S hS (i ≫ j)

AlgebraicGeometry.Space.isH1RegularImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionComposition.lean, line 424. The attribute's comment: “composition of H₁-regular immersions”.

Stacks 09S0, the H₁-regular case. The composite of two H₁-regular immersions of algebraic spaces over S is an H₁-regular immersion.

theorem isH1RegularImmersion_comp (i : Z ⟶ Y) (j : Y ⟶ X)
    (hi : IsH1RegularImmersion B S hS i) (hj : IsH1RegularImmersion B S hS j) :
    IsH1RegularImmersion B S hS (i ≫ j)

AlgebraicGeometry.Space.isQuasiRegularImmersion_comp_of_isH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionComposition.lean, line 434. The attribute's comment: “composition of an H₁-regular and a quasi-regular immersion”.

Stacks 09S0, the mixed case. The composite of an H₁-regular immersion of algebraic spaces over S and a quasi-regular immersion of algebraic spaces over S is a quasi-regular immersion.

theorem isQuasiRegularImmersion_comp_of_isH1RegularImmersion (i : Z ⟶ Y) (j : Y ⟶ X)
    (hi : IsH1RegularImmersion B S hS i) (hj : IsQuasiRegularImmersion B S hS j) :
    IsQuasiRegularImmersion B S hS (i ≫ j)

Tag 09S1, a lemma

Tag 09S1 in the Stacks Project.

AlgebraicGeometry.Space.isQuasiRegularImmersion_of_comp_of_isSplitExactConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionSplitConormal.lean, line 223. The attribute's comment: “(1) quasi-regularity descends to the first immersion, with the conormal hypothesis read on the étale charts of X”.

Stacks tag 09S1, clause (1). Let i : Z ⟶ Y and j : Y ⟶ X be representable morphisms of algebraic spaces over S with j locally of finite presentation and with the conormal sequence of Stacks tag 06BD exact and locally split on the étale charts of X. If i ≫ j is a quasi-regular immersion, so is i.

The sibling clauses are AlgebraicGeometry.Space.isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence, clause (2) for H₁-regularity, and AlgebraicGeometry.Space.isKoszulRegularImmersion_of_comp_of_isSplitExactConormalSequence, clause (3) for Koszul-regularity.

theorem isQuasiRegularImmersion_of_comp_of_isSplitExactConormalSequence
    (hZ : IsAlgebraicSpace B S hS Z) (hY : IsAlgebraicSpace B S hS Y)
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ Y) (j : Y ⟶ X)
    (hjfp : IsLocallyOfFinitePresentation B S hS j)
    (hcon : IsSplitExactConormalSequenceOnEtaleCharts B S hS i j)
    (hij : IsQuasiRegularImmersion B S hS (i ≫ j)) :
    IsQuasiRegularImmersion B S hS i

AlgebraicGeometry.Space.isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionSplitConormal.lean, line 265. The attribute's comment: “(2) H₁-regularity descends to the first immersion, with the conormal hypothesis read on the étale charts of X”.

Stacks tag 09S1, clause (2). Let i : Z ⟶ Y and j : Y ⟶ X be representable morphisms of algebraic spaces over S with j locally of finite presentation and with the conormal sequence of Stacks tag 06BD exact and locally split on the étale charts of X. If i ≫ j is an H₁-regular immersion, so is i.

The sibling clauses are AlgebraicGeometry.Space.isQuasiRegularImmersion_of_comp_of_isSplitExactConormalSequence, clause (1) for quasi-regularity, and AlgebraicGeometry.Space.isKoszulRegularImmersion_of_comp_of_isSplitExactConormalSequence, clause (3) for Koszul-regularity.

theorem isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence
    (hZ : IsAlgebraicSpace B S hS Z) (hY : IsAlgebraicSpace B S hS Y)
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ Y) (j : Y ⟶ X)
    (hjfp : IsLocallyOfFinitePresentation B S hS j)
    (hcon : IsSplitExactConormalSequenceOnEtaleCharts B S hS i j)
    (hij : IsH1RegularImmersion B S hS (i ≫ j)) :
    IsH1RegularImmersion B S hS i

AlgebraicGeometry.Space.isKoszulRegularImmersion_of_comp_of_isSplitExactConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionSplitConormal.lean, line 307. The attribute's comment: “(3) Koszul-regularity of the first immersion, with the conormal hypothesis read on the étale charts of X”.

Stacks tag 09S1, clause (3). Let i : Z ⟶ Y and j : Y ⟶ X be representable morphisms of algebraic spaces over S with j locally of finite presentation and with the conormal sequence of Stacks tag 06BD exact and locally split on the étale charts of X. If both j and i ≫ j are Koszul-regular immersions, so is i.

The sibling clauses are AlgebraicGeometry.Space.isQuasiRegularImmersion_of_comp_of_isSplitExactConormalSequence, clause (1) for quasi-regularity, and AlgebraicGeometry.Space.isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence, clause (2) for H₁-regularity.

theorem isKoszulRegularImmersion_of_comp_of_isSplitExactConormalSequence
    (hZ : IsAlgebraicSpace B S hS Z) (hY : IsAlgebraicSpace B S hS Y)
    (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ Y) (j : Y ⟶ X)
    (hjfp : IsLocallyOfFinitePresentation B S hS j)
    (hcon : IsSplitExactConormalSequenceOnEtaleCharts B S hS i j)
    (hj : IsKoszulRegularImmersion B S hS j)
    (hij : IsKoszulRegularImmersion B S hS (i ≫ j)) :
    IsKoszulRegularImmersion B S hS i

Tag 09S2, a lemma

Tag 09S2 in the Stacks Project.

AlgebraicGeometry.Space.isKoszulRegularImmersion_tfae_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionNoetherianSplitConormal.lean, line 318. The attribute's comment: “all three conditions, with the second clause of condition (1) — Koszul-regularity of j — localized to a neighbourhood of the image of i and read on the étale charts of X. The source states that clause on all of Y, which is false: for Z empty, conditions (2) and (3) hold for every j, while j need not be Koszul-regular. The localized clause is what the cited scheme-level Tag 0690 proves, that tag being stated at a point of Z”.

Stacks tag 09S2. Let i : Z ⟶ Y and j : Y ⟶ X be immersions of algebraic spaces over a scheme S with X locally Noetherian. Then the following are equivalent:

i is a Koszul-regular immersion and j is a Koszul-regular immersion near the image of i,

i and i ≫ j are Koszul-regular immersions,

i ≫ j is a Koszul-regular immersion and the conormal sequence 0 ⟶ i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0 of Stacks tag 06BD is exact and locally split.

Conditions (1) and (3) are read on the étale scheme charts of X, as every condition on algebraic spaces whose scheme analogue this development localizes. The second clause of condition (1) is Koszul-regularity of j on a neighbourhood of the image of i, not on all of Y: the source states it on all of Y, which is false, and the module documentation gives the counterexample and the reason the cited scheme-level Stacks tag 0690 is itself pointwise.

theorem isKoszulRegularImmersion_tfae_of_isLocallyNoetherian (hZ : IsAlgebraicSpace B S hS Z)
    (hY : IsAlgebraicSpace B S hS Y) (hX : IsAlgebraicSpace B S hS X) (i : Z ⟶ Y) (j : Y ⟶ X)
    (_hi : IsImmersion B S hS i) (hj : IsImmersion B S hS j)
    (hnoeth : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    List.TFAE
      [IsKoszulRegularImmersion B S hS i ∧
          IsKoszulRegularImmersionNearImageOnEtaleCharts B S hS i j,
        IsKoszulRegularImmersion B S hS i ∧ IsKoszulRegularImmersion B S hS (i ≫ j),
        IsKoszulRegularImmersion B S hS (i ≫ j) ∧
          IsSplitExactConormalSequenceOnEtaleCharts B S hS i j]

Sources

Section76.45 Relative pseudo-coherence #

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

Tag 0CSW, a remark

Tag 0CSW in the Stacks Project.

AlgebraicGeometry.Space.locallyOfFiniteType_of_represents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Representable.lean, line 52. The attribute's comment: “representing_locally_finite_type”.

Stacks 0CSW. If a morphism f of algebraic spaces over S is locally of finite type and a morphism f₀ of objects of the site represents it, through isomorphisms yoneda.obj U ≅ X and yoneda.obj V ≅ Y, then the scheme morphism underlying f₀ is locally of finite type.

theorem locallyOfFiniteType_of_represents (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f) (U V : BigFppfOver B S hS) (f₀ : U ⟶ V)
    (eX : yoneda.obj U ≅ X) (eY : yoneda.obj V ≅ Y)
    (hrep : yoneda.map f₀ ≫ eY.hom = eX.hom ≫ f) :
    LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map f₀)

AlgebraicGeometry.Space.existsUnique_representableDerivedPullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RepresentableDescent.lean, line 150. The attribute's comment: “every E in D_QCoh(O_X) is the pullback of a unique E_0 in D_QCoh(O_{X_0}), by Tag 071Q”.

Let X be an algebraic space represented by the scheme X₀ underlying U, through eX : h_U ≅ X. Every object E of D_QCoh(𝒪_X) is the pullback of an object E₀ of D(𝒪_{X₀}) with quasi-coherent cohomology sheaves, and E₀ is unique: any object of D_QCoh(𝒪_{X₀}) whose pullback is isomorphic to E is isomorphic to E₀.

theorem existsUnique_representableDerivedPullback_iso
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) :
    ∃ E₀ : DerivedCategory ((BigFppfOver.toScheme B S hS).obj U).Modules,
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor _ i).obj E₀).IsQuasicoherent) ∧
        Nonempty ((representableDerivedPullback B S hS hX eX).obj E₀ ≅ E.obj) ∧
          ∀ E₀' : DerivedCategory ((BigFppfOver.toScheme B S hS).obj U).Modules,
            (∀ i : ℤ, ((DerivedCategory.homologyFunctor _ i).obj E₀').IsQuasicoherent) →
              Nonempty ((representableDerivedPullback B S hS hX eX).obj E₀' ≅ E.obj) →
                Nonempty (E₀' ≅ E₀)

AlgebraicGeometry.Space.IsRepresentablyRelativelyPseudoCoherentFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RepresentableDescent.lean, line 213. The attribute's comment: “the convention: E is m-pseudo-coherent relative to Y when E_0 is m-pseudo-coherent relative to Y_0 (Tag 09UI)”.

Let f : X → Y be a morphism of representable algebraic spaces over S which is locally of finite type, represented by the morphism of schemes f₀ : X₀ → Y₀ underlying f₀ : U ⟶ V through eX : h_U ≅ X and eY : h_V ≅ Y. An object E of D_QCoh(𝒪_X) is m-pseudo-coherent relative to Y when the object E₀ of D_QCoh(𝒪_{X₀}) whose pullback is E is m-pseudo-coherent relative to Y₀ in the sense of Stacks 09UI. This makes sense because f₀ is locally of finite type (AlgebraicGeometry.Space.locallyOfFiniteType_of_represents), and it does not depend on the choice of E₀ (AlgebraicGeometry.Space.isRepresentablyRelativelyPseudoCoherentFrom_iff).

def IsRepresentablyRelativelyPseudoCoherentFrom
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) (m : ℤ) : Prop

Tag 0CSX, a lemma

Tag 0CSX in the Stacks Project.

AlgebraicGeometry.Space.relativePseudoCoherence_chart_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Relative.lean, line 565. The attribute's comment: “proved relative to the carried inputs h. Its comparison field is the second sentence of Remark 0CSW — that an object of D_QCoh of a representable algebraic space is the pullback of a unique object of D_QCoh of a representing scheme, which is what gives E|_U its meaning — and is absent from the library, whose 0CSW is the first sentence only; chartComplexPullback is its compatibility with passing to a finer chart. The descent half of 0CSN is carried as fppfDescent because only the forward half is proved. 09US is not carried: it is recovered from its own 0E23 input, carried through as torIndependentBaseChange.”.

Stacks 0CSX. Let f : X ⟶ Y be a morphism of algebraic spaces over S locally of finite type, let m be an integer and let E be an object of D_QCoh(𝒪_X). With the complex E|_U of Remark 0CSW the following are equivalent:

for every commuting square of étale scheme charts U ⟶ V over X ⟶ Y, the complex E|_U is m-pseudo-coherent relative to V;

for some such square with U ⟶ X surjective, the complex E|_U is m-pseudo-coherent relative to V;

for every such square with U and V affine, the complex RΓ(U, E) of 𝒪_X(U)-modules is m-pseudo-coherent relative to 𝒪_Y(V).

See the module docstring for the four inputs that h carries.

theorem relativePseudoCoherence_chart_tfae (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (h : RelativePseudoCoherenceInput B S hS)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f)
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) (m : ℤ) :
    List.TFAE
      [∀ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (g : U ⟶ V)
          (ha : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) a)
          (hb : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) b)
          (hc : yoneda.map g ≫ b = a ≫ f),
          IsPseudoCoherentFromOnChart B S hS h hX f hf E m U V a b g ha hb hc,
       ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (g : U ⟶ V)
          (ha : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) a)
          (hb : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) b),
          IsSurjective B S hS a ∧ ∃ hc : yoneda.map g ≫ b = a ≫ f,
            IsPseudoCoherentFromOnChart B S hS h hX f hf E m U V a b g ha hb hc,
       ∀ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (g : U ⟶ V)
          (ha : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) a)
          (hb : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) b)
          (hc : yoneda.map g ≫ b = a ≫ f)
          (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
          (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj V)),
          haveI : LocallyOfFiniteType ((BigFppfOver.toScheme B S hS).map g) :=
            hf U V a b g ha hb hc
          haveI := hU
          haveI := hV
          ((BigFppfOver.toScheme B S hS).map g).DerivedSectionsPseudoCoherentOn'
            (h.chartComplex hX E ha).obj m (isAffineOpen_top _) (isAffineOpen_top _)
            (by simp)]

AlgebraicGeometry.Space.relativePseudoCoherence_etaleSquare_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeChartTests.lean, line 480. The attribute's comment: “all three conditions and their equivalence, at the source's hypotheses: f a morphism of algebraic spaces over S locally of finite type, E in D_QCoh(O_X), any m; the phrase 'E|_U is m-pseudo-coherent relative to V' is the convention of Remark 0CSW”.

Stacks 0CSX. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is locally of finite type, let m be an integer and let E be an object of D_QCoh(𝒪_X). With the notation of Remark 0CSW the following are equivalent:

for every commutative square U ⟶ V over f of schemes U, V with étale charts U ⟶ X, V ⟶ Y, the complex E|_U is m-pseudo-coherent relative to V;

for some such square with U ⟶ X surjective, E|_U is m-pseudo-coherent relative to V;

for every such square with U and V affine, the complex RΓ(U, E) of 𝒪_X(U)-modules is m-pseudo-coherent relative to 𝒪_Y(V).

(1) ⟹ (2) and (1) ⟹ (3) and (3) ⟹ (1) are AlgebraicGeometry.Space.exists_surjective_isPseudoCoherentFromOnEtaleSquare, AlgebraicGeometry.Space.derivedSectionsPseudoCoherentOnEtaleSquare_of_forall and AlgebraicGeometry.Space.isPseudoCoherentFromOnEtaleSquare_of_forall_derivedSections. For (2) ⟹ (1), AlgebraicGeometry.Space.exists_surjective_etale_isPseudoCoherentFrom_derivedPullback gives, on a second square, relative m-pseudo-coherence of the pullback of E|_{U'} along a surjective étale morphism W ⟶ U'; that morphism alone is an fppf covering, and Stacks 0CSN descends the property to E|_{U'}.

theorem relativePseudoCoherence_etaleSquare_tfae :
    List.TFAE
      [∀ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (g : U ⟶ V)
          (ha : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) a)
          (hb : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) b)
          (hc : yoneda.map g ≫ b = a ≫ f),
          IsPseudoCoherentFromOnEtaleSquare hX f hf E m U V a b g ha hb hc,
       ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (g : U ⟶ V)
          (ha : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) a)
          (hb : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) b),
          IsSurjective B S hS a ∧ ∃ hc : yoneda.map g ≫ b = a ≫ f,
            IsPseudoCoherentFromOnEtaleSquare hX f hf E m U V a b g ha hb hc,
       ∀ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (g : U ⟶ V)
          (ha : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) a)
          (hb : HasSchemeProperty B S hS (@AlgebraicGeometry.Etale.{u}) b)
          (hc : yoneda.map g ≫ b = a ≫ f)
          (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj U))
          (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj V)),
          DerivedSectionsPseudoCoherentOnEtaleSquare hX f hf E m U V a b g ha hb hc hU hV]

Tag 0CSY, a definition

Tag 0CSY in the Stacks Project.

AlgebraicGeometry.Space.IsRelativelyPseudoCoherentFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeDefinition.lean, line 200. The attribute's comment: “part (1): m-pseudo-coherence relative to Y of an object of D_QCoh, through condition (3) of Tag 0CSX”.

Stacks 0CSY, part (1). An object E of D_QCoh(𝒪_X) is m-pseudo-coherent relative to Y when, for every commuting square of étale scheme charts U of X and V of Y over f with U and V affine, the complex RΓ(U, E) of 𝒪_X(U)-modules is m-pseudo-coherent relative to the ring 𝒪_Y(V) in the sense of Tag 065I.

This is condition (3) of Tag 0CSX; see "Which of the equivalent conditions of Tag 0CSX is taken as the definition" in the module docstring.

def IsRelativelyPseudoCoherentFrom {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) (m : ℤ) : Prop

AlgebraicGeometry.Space.IsRelativelyPseudoCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeDefinition.lean, line 225. The attribute's comment: “part (2): pseudo-coherence relative to Y of an object of D_QCoh”.

Stacks 0CSY, part (2). An object of D_QCoh(𝒪_X) is pseudo-coherent relative to Y when it is m-pseudo-coherent relative to Y for every integer m.

def IsRelativelyPseudoCoherent {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) : Prop

AlgebraicGeometry.Space.IsModuleRelativelyPseudoCoherentFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeDefinition.lean, line 236. The attribute's comment: “part (3): m-pseudo-coherence relative to Y of a quasi-coherent module”.

Stacks 0CSY, part (3). A quasi-coherent 𝒪_X-module is m-pseudo-coherent relative to Y when the complex it determines in degree zero, an object of D_QCoh(𝒪_X) by AlgebraicGeometry.Space.derivedCategoryB_singleFunctor_obj, is.

def IsModuleRelativelyPseudoCoherentFrom {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX) (hF : F.IsQuasicoherentOnSite) (m : ℤ) : Prop

AlgebraicGeometry.Space.IsModuleRelativelyPseudoCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeDefinition.lean, line 246. The attribute's comment: “part (4): pseudo-coherence relative to Y of a quasi-coherent module”.

Stacks 0CSY, part (4). A quasi-coherent 𝒪_X-module is pseudo-coherent relative to Y when the complex it determines in degree zero is.

def IsModuleRelativelyPseudoCoherent {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsLocallyOfFiniteType B S hS f)
    (F : Modules.{u, u} B S hS X hX) (hF : F.IsQuasicoherentOnSite) : Prop

Tag 0DII, a lemma

Tag 0DII in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherent_iff_of_flat_of_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeAbsolute.lean, line 229. The attribute's comment: “the case of schemes”.

Stacks 0DII, the case of schemes. Let f : X ⟶ Y be a flat morphism of schemes locally of finite presentation and let E be an object of D(𝒪_X). Then E is pseudo-coherent relative to Y in the sense of Stacks 09UI if and only if E is pseudo-coherent on X in the sheaf-level sense of Stacks 08CB.

public theorem isPseudoCoherent_iff_of_flat_of_locallyOfFinitePresentation {X Y : Scheme.{u}}
    (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] (E : DerivedCategory X.Modules) :
    f.IsPseudoCoherent E ↔ RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E

AlgebraicGeometry.Space.isRelativelyPseudoCoherentFrom_iff_forall_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeAbsolute.lean, line 1022. The attribute's comment: “the fixed-degree etale-chart localization: relative m-pseudo-coherence over Y is m-pseudo-coherence of RGamma(U, E) over O_X(U) on every square of affine etale charts”.

Stacks 0DII in a fixed degree, by étale localization. Let f : X ⟶ Y be a flat morphism of algebraic spaces over S which is locally of finite presentation, let E be an object of D_QCoh(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent relative to Y if and only if, on every commuting square of affine étale scheme charts U of X and V of Y over f, the complex RΓ(U, E) is m-pseudo-coherent over the ring 𝒪_X(U).

Relative m-pseudo-coherence is by definition the relative condition on those same squares, so the two sides differ square by square only, and on one square the equivalence is AlgebraicGeometry.Space.relativePseudoCoherence_chart_iff.

theorem isRelativelyPseudoCoherentFrom_iff_forall_chart
    (hflat : IsFlat B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f)
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) (m : ℤ) :
    IsRelativelyPseudoCoherentFrom B S hS X hX f
        (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hfp) E m ↔
      ∀ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
          (g : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V),
          yoneda.map g ≫ V.obj.hom = U.obj.hom ≫ f →
          IsAffine (chartScheme U) → IsAffine (chartScheme V) →
        StacksDraft.PseudoCoherence.IsPseudoCoherentFrom
          (chartDerivedSections B S hS X hX U E) m

AlgebraicGeometry.Space.isRelativelyPseudoCoherent_iff_forall_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeAbsolute.lean, line 1049. The attribute's comment: “the etale-chart localization: pseudo-coherence relative to Y is pseudo-coherence of RGamma(U, E) over O_X(U) on every square of affine etale charts”.

Stacks 0DII by étale localization. Let f : X ⟶ Y be a flat morphism of algebraic spaces over S which is locally of finite presentation and let E be an object of D_QCoh(𝒪_X). Then E is pseudo-coherent relative to Y if and only if, on every commuting square of affine étale scheme charts U of X and V of Y over f, the complex RΓ(U, E) is pseudo-coherent over the ring 𝒪_X(U) — the target playing no role.

This is the all-degrees clause of AlgebraicGeometry.Space.relativePseudoCoherence_chart_iff on each of the squares that relative pseudo-coherence of Stacks 0CSY is tested on; see "What is proved, and what the right-hand side says" in the module docstring for the sense in which the right-hand side is the absolute condition.

theorem isRelativelyPseudoCoherent_iff_forall_chart
    (hflat : IsFlat B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f)
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X hX) :
    IsRelativelyPseudoCoherent B S hS X hX f
        (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hfp) E ↔
      ∀ (U : SmallEtale B S hS X) (V : SmallEtale B S hS Y)
          (g : (SmallEtale.toOver B S hS X).obj U ⟶ (SmallEtale.toOver B S hS Y).obj V),
          yoneda.map g ≫ V.obj.hom = U.obj.hom ≫ f →
          IsAffine (chartScheme U) → IsAffine (chartScheme V) →
        StacksDraft.PseudoCoherence.IsPseudoCoherent
          (chartDerivedSections B S hS X hX U E)

AlgebraicGeometry.Space.isRelativelyPseudoCoherent_iff_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativeAbsoluteChartDictionary.lean, line 353.

Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat and locally of finite presentation. Let E be an object of D_QCoh(𝒪_X). Then E is pseudo-coherent relative to Y if and only if E is pseudo-coherent on X, the latter read on the small étale ringed site of X.

This is AlgebraicGeometry.Space.isRelativelyPseudoCoherent_iff_isPseudoCoherent_of_chartDictionary at AlgebraicGeometry.Space.chartPseudoCoherenceDictionaryFrom_holds in every degree. It is not the fixed-degree statement above read degree by degree: the all-degrees clause of Stacks 08FT (3) asks for one complex which is m-pseudo-coherent for every m, and the quantifier swap happens on the site side, inside that theorem.

public theorem isRelativelyPseudoCoherent_iff_isPseudoCoherent (f : X ⟶ Y)
    (hflat : IsFlat B S hS f.hom) (hfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (E : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2) :
    IsRelativelyPseudoCoherent B S hS X.1 X.2 f.hom
        (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B S hS hfp) E ↔
      (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent E.obj

Sources

Section76.46 Pseudo-coherent morphisms #

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

Tag 06BR, a definition

Tag 06BR in the Stacks Project.

AlgebraicGeometry.Space.IsPseudoCoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Basic.lean, line 69. The attribute's comment: “part (1): pseudo-coherent morphism”.

Stacks 06BR, part (1). A morphism of algebraic spaces over S is pseudo-coherent when every commuting square of étale scheme charts induces a pseudo-coherent scheme morphism.

abbrev IsPseudoCoherent (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsPseudoCoherentAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Basic.lean, line 77. The attribute's comment: “part (2): pseudo-coherent at a point”.

Stacks 06BR, part (2). A morphism of algebraic spaces over S is pseudo-coherent at a point x of its source when it is pseudo-coherent on an open subspace of the source containing x.

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

Tag 06BS, a lemma

Tag 06BS in the Stacks Project.

AlgebraicGeometry.Space.isPseudoCoherent_baseChange_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/FlatBaseChange.lean, line 234.

Stacks 06BS. A flat base change of a pseudo-coherent morphism of algebraic spaces over S is pseudo-coherent: in a cartesian square with g : Y ⟶ Z pseudo-coherent and f : X ⟶ Z flat, the base change g' : Y' ⟶ X of g along f is pseudo-coherent.

theorem isPseudoCoherent_baseChange_of_isFlat
    {X Y Y' Z : AlgebraicSpaces B S hS} {f : X ⟶ Z} {g : Y ⟶ Z} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}
    (sq : IsPullback f' g' g f) (hflat : IsFlat B S hS f.hom)
    (hf : IsPseudoCoherent B S hS g.hom) :
    IsPseudoCoherent B S hS g'.hom

Tag 06BT, a lemma

Tag 06BT in the Stacks Project.

AlgebraicGeometry.Space.isPseudoCoherent_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Composition.lean, line 95.

Stacks 06BT. A composition of pseudo-coherent morphisms of algebraic spaces over S is pseudo-coherent.

This is the case at pseudo-coherence of Stacks 0AML, the composition law for an every-étale-chart property, whose inputs are Stacks 0681 and étale locality on the source and target.

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

Tag 06BU, a lemma

Tag 06BU in the Stacks Project.

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

Stacks 06BU. A pseudo-coherent morphism of algebraic spaces over S is locally of finite presentation.

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

Tag 06BV, a lemma

Tag 06BV in the Stacks Project.

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

Stacks 06BV. A flat morphism of algebraic spaces over S which is locally of finite presentation is pseudo-coherent.

theorem isPseudoCoherent_of_isFlat_of_isLocallyOfFinitePresentation (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f) :
    IsPseudoCoherent B S hS f

Tag 06BW, a lemma

Tag 06BW in the Stacks Project.

AlgebraicGeometry.Space.isPseudoCoherent_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Composition.lean, line 111. References: SGA 6 III (1.14), “partial”.

Stacks 06BW. A morphism of algebraic spaces over S between two algebraic spaces pseudo-coherent over a base algebraic space is pseudo-coherent.

An étale atlas of the base is lifted twice to produce a square of étale charts of f whose chart of the source is surjective, and the scheme-level cancellation of Stacks 0683 applies to the two factors of the induced chart morphism of f ≫ g.

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

Tag 06BX, a lemma

Tag 06BX in the Stacks Project.

AlgebraicGeometry.Space.isPseudoCoherent_iff_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Noetherian.lean, line 50. References: SGA 6 III (1.3), “Y loc. noetherian case”.

Stacks 06BX. For a morphism of algebraic spaces over S whose target is locally Noetherian, pseudo-coherence is equivalent to being locally of finite type.

theorem isPseudoCoherent_iff_isLocallyOfFiniteType (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)
    (hYNoetherian : HasEtaleLocalProperty B S hS Y
      (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (f : X ⟶ Y) :
    IsPseudoCoherent B S hS f ↔ IsLocallyOfFiniteType B S hS f

Sources

LeanAlgebraicGeometry.Space.IsPseudoCoherent · AlgebraicGeometry.Space.IsPseudoCoherentAt · AlgebraicGeometry.Space.isPseudoCoherent_baseChange_of_isFlat · AlgebraicGeometry.Space.isPseudoCoherent_comp · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isPseudoCoherent · AlgebraicGeometry.Space.isPseudoCoherent_of_isFlat_of_isLocallyOfFinitePresentation · AlgebraicGeometry.Space.isPseudoCoherent_of_comp · AlgebraicGeometry.Space.isPseudoCoherent_iff_isLocallyOfFiniteType

Section76.47 Perfect morphisms #

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

Tag 06BZ, a definition

Tag 06BZ in the Stacks Project.

AlgebraicGeometry.Space.IsPerfect, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Perfect.lean, line 65. The attribute's comment: “part (1): perfect morphism”.

Stacks 06BZ, part (1). A morphism of algebraic spaces over S is perfect when every commuting square of étale scheme charts induces a perfect scheme morphism.

abbrev IsPerfect (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.IsPerfectAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Perfect.lean, line 73. The attribute's comment: “part (2): perfect at a point”.

Stacks 06BZ, part (2). A morphism of algebraic spaces over S is perfect at a point x of its source when it is perfect on an open subspace of the source containing x.

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

Tag 06C0, a lemma

Tag 06C0 in the Stacks Project.

AlgebraicGeometry.Space.IsPerfect.of_isPullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/PerfectStability.lean, line 73.

Stacks 06C0. A flat base change of a perfect morphism of algebraic spaces over S is perfect: in a cartesian square with g : Y ⟶ Z perfect and f : X ⟶ Z flat, the base change g' : Y' ⟶ X of g along f is perfect.

theorem IsPerfect.of_isPullback_of_isFlat
    {X Y Y' Z : AlgebraicSpaces B S hS} {f : X ⟶ Z} {g : Y ⟶ Z} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}
    (sq : IsPullback f' g' g f) (hflat : IsFlat B S hS f.hom) (hf : IsPerfect B S hS g.hom) :
    IsPerfect B S hS g'.hom

AlgebraicGeometry.Space.IsPerfect.pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/PerfectStability.lean, line 83. The attribute's comment: “pullback spelling”.

Stacks 06C0 in the pullback spelling: if f : X ⟶ Y is a perfect morphism of algebraic spaces over S and g : Y' ⟶ Y is flat, then the projection X ×_Y Y' ⟶ Y' is perfect.

theorem IsPerfect.pullback_snd {X Y Y' : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hg : IsFlat B S hS g.hom) (hf : IsPerfect B S hS f.hom) :
    IsPerfect B S hS (Limits.pullback.snd f.hom g.hom)

Tag 06C1, a lemma

Tag 06C1 in the Stacks Project.

AlgebraicGeometry.Space.IsPerfect.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/PerfectStability.lean, line 92.

Stacks 06C1. A composition of perfect morphisms of algebraic spaces over S is perfect.

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

Tag 06C2, a lemma

Tag 06C2 in the Stacks Project.

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

Stacks 06C2. A morphism of algebraic spaces over S is flat and perfect if and only if it is flat and locally of finite presentation.

theorem isFlat_and_isPerfect_iff_isFlat_and_isLocallyOfFinitePresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) :
    (IsFlat B S hS f ∧ IsPerfect B S hS f) ↔
      (IsFlat B S hS f ∧ IsLocallyOfFinitePresentation B S hS f)

Tag 0E4U, a lemma

Tag 0E4U in the Stacks Project.

AlgebraicGeometry.Space.isPerfect_derivedModulePushforward_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/PerfectProperPushforward.lean, line 255.

Stacks 0E4U. Let S be a scheme, let Y be a Noetherian algebraic space over S, let f : X ⟶ Y be a perfect proper morphism of algebraic spaces over S, and let E be a perfect object of D(𝒪_X). Then Rf_*E is a perfect object of D(𝒪_Y).

Perfectness is tested on the affine étale charts of Y, over which the restriction of Rf_*E is the derived direct image along the base change of f (Stacks 08GE), and the affine case is AlgebraicGeometry.Space.isPerfect_derivedModulePushforward_of_isProper_of_isAffine.

theorem isPerfect_derivedModulePushforward_of_isProper
    (hZ : B.Contains (⊤_ Scheme.{u})) {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hY : IsNoetherian B S hS hZ Y.1) (hfPerfect : IsPerfect B S hS f.hom)
    (hfProper : IsProper B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : (smallEtaleRingedSite B S hS X.1 X.2).IsPerfect E) :
    (smallEtaleRingedSite B S hS Y.1 Y.2).IsPerfect
      ((Stacks.DerivedFunctor.totalRightDerived (modulePushforward B S hS f)).obj E)

Sources

LeanAlgebraicGeometry.Space.IsPerfect · AlgebraicGeometry.Space.IsPerfectAt · AlgebraicGeometry.Space.IsPerfect.of_isPullback_of_isFlat · AlgebraicGeometry.Space.IsPerfect.pullback_snd · AlgebraicGeometry.Space.IsPerfect.comp · AlgebraicGeometry.Space.isFlat_and_isPerfect_iff_isFlat_and_isLocallyOfFinitePresentation · AlgebraicGeometry.Space.isPerfect_derivedModulePushforward_of_isProper

Section76.48 Local complete intersection morphisms #

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

Tag 06C4, a definition

Tag 06C4 in the Stacks Project.

AlgebraicGeometry.Space.IsLocalCompleteIntersection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection.lean, line 77. The attribute's comment: “part (1): local complete intersection morphisms”.

Stacks 06C4, part (1). A morphism of algebraic spaces over S is a local complete intersection morphism, or a Koszul morphism, when every commuting square of étale scheme charts induces a local complete intersection morphism of schemes.

abbrev IsLocalCompleteIntersection (f : X ⟶ Y) : Prop

AlgebraicGeometry.Space.KoszulAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection.lean, line 86. The attribute's comment: “part (2): Koszul at a point”.

Stacks 06C4, part (2). A morphism of algebraic spaces over S is Koszul at a point x of its source when it is a local complete intersection morphism on an open subspace of the source containing x.

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

Tag 06C5, a lemma

Tag 06C5 in the Stacks Project.

AlgebraicGeometry.Space.isKoszulRegularImmersion_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/ImmersionIntoSmooth.lean, line 236.

Stacks 06C5. Let f : X ⟶ Y be a local complete intersection morphism of algebraic spaces over S, let p : P ⟶ Y be smooth, let a : U ⟶ X be étale and let i : U ⟶ P be an immersion over Y. Then i is a Koszul-regular immersion of algebraic spaces.

theorem isKoszulRegularImmersion_of_isLocalCompleteIntersection (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {X Y U P : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (_hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (_hU : IsAlgebraicSpace B S hS U) (_hP : IsAlgebraicSpace B S hS P)
    (f : X ⟶ Y) (a : U ⟶ X) (i : U ⟶ P) (p : P ⟶ Y)
    (hf : IsLocalCompleteIntersection B S hS f) (ha : IsEtale B S hS a)
    (hi : IsImmersion B S hS i) (hp : IsSmooth B S hS p) (hcomm : a ≫ f = i ≫ p) :
    IsKoszulRegularImmersion B S hS i

Tag 06C6, a lemma

Tag 06C6 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Perfect.lean, line 56. The attribute's comment: “part (1): locally of finite presentation”.

Stacks 06C6, part (1). A local complete intersection morphism of algebraic spaces over S is locally of finite presentation.

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

AlgebraicGeometry.Space.isPseudoCoherent_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Perfect.lean, line 66. The attribute's comment: “part (2): pseudo-coherent”.

Stacks 06C6, part (2). A local complete intersection morphism of algebraic spaces over S is pseudo-coherent.

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

AlgebraicGeometry.Space.isPerfect_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Perfect.lean, line 76. The attribute's comment: “part (3): perfect”.

Stacks 06C6, part (3). A local complete intersection morphism of algebraic spaces over S is perfect.

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

Tag 06C7, a lemma

Tag 06C7 in the Stacks Project.

AlgebraicGeometry.Space.isLocalCompleteIntersection_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/FlatBaseChange.lean, line 109.

A flat base change of a local complete intersection morphism of algebraic spaces is a local complete intersection morphism: if f : X ⟶ Y is Koszul and g : Y' ⟶ Y is flat, then the projection X ×_Y Y' ⟶ Y' is Koszul.

public theorem isLocalCompleteIntersection_pullback_snd
    {X Y Y' : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hg : IsFlat B S hS g.hom)
    (hf : IsLocalCompleteIntersection B S hS f.hom) :
    IsLocalCompleteIntersection B S hS (Limits.pullback.snd f.hom g.hom)

Tag 06C8, a lemma

Tag 06C8 in the Stacks Project.

AlgebraicGeometry.Space.isLocalCompleteIntersection_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Composition.lean, line 36.

A composition of local complete intersection morphisms of algebraic spaces over S is a local complete intersection morphism: if f : X ⟶ Y and g : Y ⟶ Z are local complete intersection morphisms, so is f ≫ g.

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

Tag 06C9, a lemma

Tag 06C9 in the Stacks Project.

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

Stacks 06C9. A morphism of algebraic spaces over S is syntomic if and only if it is flat and a local complete intersection morphism.

All three properties are the condition of Tag 03MJ on every commuting square of étale charts, so the statement is the scheme-level equivalence of Tag 069K quantified over the charts.

theorem isSyntomic_iff_isFlat_and_isLocalCompleteIntersection (f : X ⟶ Y) :
    IsSyntomic B S hS f ↔ IsFlat B S hS f ∧ IsLocalCompleteIntersection B S hS f

Tag 0CHK, a lemma

Tag 0CHK in the Stacks Project.

AlgebraicGeometry.Space.isLocalCompleteIntersection_of_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RegularImmersionLocalCompleteIntersection.lean, line 73.

Stacks 0CHK. A Koszul-regular immersion of algebraic spaces over S is a local complete intersection morphism.

theorem isLocalCompleteIntersection_of_isKoszulRegularImmersion (i : X ⟶ Y)
    (hi : IsKoszulRegularImmersion B S hS i) :
    IsLocalCompleteIntersection B S hS i

Tag 0CHL, a lemma

Tag 0CHL in the Stacks Project.

AlgebraicGeometry.Space.isLocalCompleteIntersection_of_comp_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/SmoothPermanence.lean, line 105.

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of algebraic spaces over S with g smooth. If the composite f ≫ g is a local complete intersection morphism, then so is f.

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

Tag 0CHM, a lemma

Tag 0CHM in the Stacks Project.

AlgebraicGeometry.Space.isLocalCompleteIntersection_isLocalAtTarget_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/FpqcLocalAtTarget.lean, line 210.

Stacks 0CHM. The property of being a local complete intersection morphism of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH: a morphism is Koszul exactly when its base changes along the members of an fpqc covering of its target are.

theorem isLocalCompleteIntersection_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) =>
        IsLocalCompleteIntersection B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 0CHN, a lemma

Tag 0CHN in the Stacks Project.

AlgebraicGeometry.Space.isLocalCompleteIntersection_isLocalAtSource_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Locality.lean, line 127.

Stacks 0CHN. The property of being a local complete intersection morphism of algebraic spaces over S is local on the source for the syntomic topology of Stacks 03YH.

The schemes case, Stacks 069P, is AlgebraicGeometry.isLocalAtSource_syntomic_isLocalCompleteIntersectionMorphism; the étale locality on source and target that the transfer also consumes needs only its étale restriction, AlgebraicGeometry.isLocalCompleteIntersectionMorphism_isLocalAtSource_etale.

public theorem isLocalCompleteIntersection_isLocalAtSource_syntomic :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        IsLocalCompleteIntersection B S hS f.hom)
      (Topology.precoverage.{u, v} .syntomic B S hS)

Tag 06CA, a lemma

Tag 06CA in the Stacks Project.

AlgebraicGeometry.Space.koszulOpenSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocus.lean, line 88. The attribute's comment: “part (1): the open subspace of Koszul points”.

Stacks 06CA, part (1). The open subspace U(f) ⊂ X of the Koszul points of a morphism f : X ⟶ Y of algebraic spaces: the subfunctor of the source whose sections are those all of whose points are Koszul points of f.

def koszulOpenSubspace (f : X ⟶ Y) : Subfunctor X

AlgebraicGeometry.Space.range_pointsMap_ι_koszulOpenSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocus.lean, line 94. The attribute's comment: “part (1): the open subspace of Koszul points”.

Stacks 06CA, part (1). The point set of U(f) is the set of points at which f is Koszul.

theorem range_pointsMap_ι_koszulOpenSubspace (f : X ⟶ Y) :
    Set.range (pointsMap B S hS (koszulOpenSubspace B S hS X f).toFunctor
      (koszulOpenSubspace B S hS X f).ι) = {x | KoszulAt B S hS f x}

AlgebraicGeometry.Space.isOpenSubspace_koszulOpenSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocus.lean, line 101. The attribute's comment: “part (1): the open subspace of Koszul points”.

Stacks 06CA, part (1). U(f) is an open subspace of the source.

theorem isOpenSubspace_koszulOpenSubspace (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    IsOpenSubspace B S hS (koszulOpenSubspace B S hS X f)

AlgebraicGeometry.Space.exists_isOpenSubspace_range_pointsMap_eq_setOf_koszulAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocus.lean, line 110. The attribute's comment: “part (1): the open subspace of Koszul points”.

Stacks 06CA, part (1). There is an open subspace of the source of a morphism of algebraic spaces whose point set is exactly the set of points at which the morphism is Koszul.

theorem exists_isOpenSubspace_range_pointsMap_eq_setOf_koszulAt
    (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y) :
    ∃ U : Subfunctor X, IsOpenSubspace B S hS U ∧
      Set.range (pointsMap B S hS U.toFunctor U.ι) = {x | KoszulAt B S hS f x}

AlgebraicGeometry.Space.koszulOpenSubspace_pullbackMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusBaseChange.lean, line 385. The attribute's comment: “part (2): base change of the Koszul open subspace”.

Stacks 06CA, part (2). The open subspace U(f') of the Koszul points of the base change f' of f along an arbitrary Z' ⟶ Z is the inverse image of U(f) under the projection X' ⟶ X.

The one input from the theory of schemes is that the Koszul property of morphisms of schemes is local on the source for the étale topology — Stacks 069P restricted to étale coverings.

theorem koszulOpenSubspace_pullbackMap
    {X Y Z 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) (hZ' : IsAlgebraicSpace B S hS Z')
    (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hpq : f ≫ q = p)
    (hp : IsFlat B S hS p) (hplfp : IsLocallyOfFinitePresentation B S hS p)
    (hq : IsFlat B S hS q) (hqlfp : IsLocallyOfFinitePresentation B S hS q)
    (z : Z' ⟶ Z) :
    koszulOpenSubspace B S hS (pullback p z)
        (pullback.map p z q z f (𝟙 _) (𝟙 _)
          (by simpa only [Category.comp_id] using hpq.symm) (by simp)) =
      (koszulOpenSubspace B S hS X f).preimage (pullback.fst p z)

AlgebraicGeometry.Space.koszulLocusStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusOnBaseUnconditional.lean, line 92. The attribute's comment: “part (2) in the pointwise form the hypothesis of Stacks 06CE asks for”.

The base-change assertion of Stacks 06CA holds. For a commutative triangle of algebraic spaces over S with p and q flat and locally of finite presentation, the base change of f along any Z' ⟶ Z is Koszul at a point of |X ×_Z Z'| exactly when f is Koszul at its image in |X|.

This is AlgebraicGeometry.Space.setOf_koszulAt_pullbackMap read at one point, its hypothesis of étale source locality of the Koszul property of morphisms of schemes supplied by AlgebraicGeometry.isLocalCompleteIntersectionMorphism_isLocalAtSource_etale.

theorem koszulLocusStableUnderBaseChange : KoszulLocusStableUnderBaseChange B S hS

Tag 06CB, a lemma

Tag 06CB in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_conormalSheaf_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Conormal.lean, line 255. The attribute's comment: “the conormal sheaf is finite locally free”.

Stacks 06CB, second clause. For a local complete intersection morphism f : X ⟶ Y of algebraic spaces over S which is formally unramified, the conormal sheaf 𝒞_{X/Y} of Stacks 0607 is finite locally free on the small étale site of X.

Formal unramifiedness is a field of the universal first-order thickening, and the statement is about an arbitrary one. The hypothesis hcmp is the comparison with the scheme-level Stacks 06B9 which this library lacks; see the section What is not proved here of this file.

public theorem isFiniteLocallyFreeOnSite_conormalSheaf_of_isLocalCompleteIntersection
    {X Y : AlgebraicSpaces B S hS} {f : X ⟶ Y}
    (t : UniversalFirstOrderThickening B S hS f)
    (hf : IsLocalCompleteIntersection B S hS f.hom)
    (hcmp : RepresentableConormalSheafComparison B S hS) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (conormalSheaf B S hS t)

AlgebraicGeometry.Space.unramified_iff_formallyUnramified_and_isFiniteLocallyFreeOnSite_conormalSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/ConormalFiniteLocallyFree.lean, line 107.

Stacks 06CB. Let f : X ⟶ Y be a local complete intersection morphism of algebraic spaces over S. Then f is unramified if and only if it is formally unramified, and in this case the conormal sheaf 𝒞_{X/Y} is finite locally free on X: for every universal first order thickening t of f — which exists exactly when f is formally unramified, by Stacks 0606 — the conormal sheaf of Stacks 0607 is finite locally free on the small étale site of X.

theorem unramified_iff_formallyUnramified_and_isFiniteLocallyFreeOnSite_conormalSheaf
    {X Y : AlgebraicSpaces B S hS} {f : X ⟶ Y}
    (hf : IsLocalCompleteIntersection B S hS f.hom) :
    (IsUnramified B S hS f.hom ↔ FormallyUnramified f.hom) ∧
      ∀ t : UniversalFirstOrderThickening B S hS f,
        SheafOfModules.IsFiniteLocallyFreeOnSite (conormalSheaf B S hS t)

AlgebraicGeometry.Space.isUnramified_iff_formallyUnramified_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/Unramified.lean, line 53. The attribute's comment: “the equivalence: unramified iff formally unramified”.

A local complete intersection morphism of algebraic spaces over S is unramified if and only if it is formally unramified.

public theorem isUnramified_iff_formallyUnramified_of_isLocalCompleteIntersection
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    (hf : IsLocalCompleteIntersection B S hS f) :
    IsUnramified B S hS f ↔ FormallyUnramified f

Tag 06CC, a lemma

Tag 06CC in the Stacks Project.

AlgebraicGeometry.Space.conormalSequence_shortExact_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/ConormalShortExactUnconditional.lean, line 411.

Stacks 06CC. Let Z ⟶ Y ⟶ X be formally unramified morphisms of algebraic spaces over a scheme S, presented by universal first-order thickenings Z ⊂ X₁ and Y ⊂ X₂ over X, let g₁ : X₁ ⟶ X₂ be a morphism over X restricting to f₁ : Z ⟶ Y (by Stacks 060A it is the canonical one), and let F = Y ×_{X₂} X₁ ⊆ X₁ be the fibre product, inside which Z sits as the inverse image W of Z ⊆ X₁; by Stacks 06BF it is the universal first-order thickening of Z over Y. If f₁ is a local complete intersection morphism then the conormal sequence

0 ⟶ f₁^*𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0

of Stacks 06BD, read on W, is short exact: its first arrow is the inverse image along W ⟶ Z of the conormal map of Stacks 04CP of the square over g₁, and its second arrow is the conormal map of the fibre product square of W ⊆ F over Z ⊆ X₁.

theorem conormalSequence_shortExact_of_isLocalCompleteIntersection
    (hZ : IsUniversalFirstOrderThickening B S hS Z.1 p₁)
    (hY : IsUniversalFirstOrderThickening B S hS Y.1 p₂) (hg : g₁ ≫ p₂ = p₁)
    (hlci : IsLocalCompleteIntersection B S hS f₁.hom) :
    ∃ h : (modulePullback B S hS
          (X := ⟨(preimageSubspace B S hS (subspaceInclusion B S hS X₁
                (preimageSubspace B S hS g₁ Y)) Z).1.toFunctor,
              (preimageSubspace B S hS (subspaceInclusion B S hS X₁
                (preimageSubspace B S hS g₁ Y)) Z).2.1⟩)
          (preimageProjection B S hS (subspaceInclusion B S hS X₁
            (preimageSubspace B S hS g₁ Y)) Z)).map (conormalMap B S hS Z Y g₁ f₁ sq₁) ≫
        conormalMap B S hS
          (preimageSubspace B S hS (subspaceInclusion B S hS X₁ (preimageSubspace B S hS g₁ Y)) Z)
          Z (subspaceInclusion B S hS X₁ (preimageSubspace B S hS g₁ Y))
          (preimageProjection B S hS (subspaceInclusion B S hS X₁
            (preimageSubspace B S hS g₁ Y)) Z)
          (conormalEtaleRestrictionSquare B S hS
            (subspaceInclusion B S hS X₁ (preimageSubspace B S hS g₁ Y)) Z) = 0,
      (ShortComplex.mk _ _ h).ShortExact

Sources

LeanAlgebraicGeometry.Space.IsLocalCompleteIntersection · AlgebraicGeometry.Space.KoszulAt · AlgebraicGeometry.Space.isKoszulRegularImmersion_of_isLocalCompleteIntersection · AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_isLocalCompleteIntersection · AlgebraicGeometry.Space.isPseudoCoherent_of_isLocalCompleteIntersection · AlgebraicGeometry.Space.isPerfect_of_isLocalCompleteIntersection · AlgebraicGeometry.Space.isLocalCompleteIntersection_pullback_snd · AlgebraicGeometry.Space.isLocalCompleteIntersection_comp

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

76.33 Étale localization of… to 76.48 Local complete…

Section76.33 Étale localization of morphisms#

Tag 082H, a lemma

Tag 0ADU, a lemma

Sources

Section76.34 Zariski's Main Theorem#

Tag 082I, a lemma

Tag 082J, a lemma

Tag 082K, a lemma

Tag 0874, a lemma

Sources

Section76.35 Applications of Zariski's Main Theorem, I#

Tag 0A4X, a lemma

Tag 0A4Y, a lemma

Tag 0AEJ, a lemma

Sources

Section76.36 Stein factorization#

Tag 0A19, a lemma

Tag 0E1C, a lemma

Tag 0A1A, a lemma

Tag 0A1B, a theorem

Tag 0A1C, a theorem

Tag 0AYI, a lemma

Tag 0E1D, a lemma

Tag 0E1E, a lemma

Tag 0E0D, a lemma

Tag 0CWI, a lemma

Sources

Section76.37 Extending properties from an open#

Tag 0876, a lemma

Tag 0877, a lemma

Tag 0878, a lemma

Tag 0B4J, a lemma

Tag 0879, a lemma

Sources

Section76.38 Blowing up and flatness#

Tag 087B, a lemma

Tag 087C, a theorem

Sources

Section76.39 Applications#

Tag 087E, a lemma

Tag 0B4K, a lemma

Tag 0GUW, a lemma

Tag 087F, a lemma

Tag 087G, a lemma

Tag 0CPI, a lemma

Sources

Section76.40 Chow's lemma#

Tag 088Q, a lemma

Tag 088R, a lemma

Tag 088S, a lemma

Tag 088T, a remark

Tag 088U, a lemma

Sources

Section76.41 Variants of Chow's Lemma#

Tag 089L, a lemma

Tag 089M, a lemma

Sources

Section76.42 Grothendieck's existence theorem#

Tag 089P, a lemma

Tag 08B3, a lemma

Tag 08B4, an equation

Tag 08B5, a lemma

Tag 08B6, a lemma

Tag 08B7, a situation

Tag 08B8, an equation

Tag 08B9, a lemma

Tag 08BA, a remark

Tag 08BB, a lemma

Tag 08BC, a lemma

Tag 08BD, a lemma

Tag 08BE, a theorem

Tag 08BF, a remark

Sources

Section76.43 Grothendieck's algebraization theorem#

Tag 08BG, a lemma

Tag 0A01, a lemma

Tag 0A4Z, a lemma

Tag 0GHK, a remark

Tag 0E7R, a lemma

Section76.33 Étale localization of morphisms #

Section76.34 Zariski's Main Theorem #

Section76.35 Applications of Zariski's Main Theorem, I #

Section76.36 Stein factorization #

Section76.37 Extending properties from an open #

Section76.38 Blowing up and flatness #

Section76.39 Applications #

Section76.40 Chow's lemma #

Section76.41 Variants of Chow's Lemma #

Section76.42 Grothendieck's existence theorem #

Section76.43 Grothendieck's algebraization theorem #

Section76.44 Regular immersions #

Section76.45 Relative pseudo-coherence #

Section76.46 Pseudo-coherent morphisms #

Section76.47 Perfect morphisms #

Section76.48 Local complete intersection morphisms #