37.68 Relative morphisms to 37.81 The extensive criterion…

Section37.68 Relative morphisms #

Section 37.68 of the Stacks Project, Tag 0BL0. 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 0BL1, an equation

Tag 0BL1 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.relativeHomObjEquivOverBase, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeMorphismDiagram.lean, line 26 (StacksFrontier): “the datum pictured by diagram (37.68.0.1), a morphism b : T ×_S Z ⟶ T ×_S X over T, identified with its description as a morphism T ×_S Z ⟶ X over S”.

Tag 0BL2, an equation

Tag 0BL2 in the Stacks Project.

AlgebraicGeometry.relativeHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeMorphismFunctor.lean, line 50.

The relative morphism functor Mor_S(Z, X) of two schemes Z and X over S: it sends a scheme T over S to the set of morphisms T ×_S Z ⟶ X over S, and a morphism T' ⟶ T over S to the operation of base change along it.

noncomputable def relativeHom (Z X : Over S) : (Over S)ᵒᵖ ⥤ Type u

Tag 05Y6, a lemma

Tag 05Y6 in the Stacks Project.

AlgebraicGeometry.relativeHom_representableBy_affine, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/RelativeMorphisms.lean, line 417.

Stacks Project, Tag 05Y6. If Z and X are affine schemes over an affine scheme S and Γ(Z, 𝒪_Z) is finite free over Γ(S, 𝒪_S), then the relative morphism functor Mor_S(Z, X) is represented by an affine scheme over S.

lemma relativeHom_representableBy_affine
    (S Z X : Scheme.{u}) (f : Z ⟶ S) (g : X ⟶ S)
    [IsAffine S] [IsAffine Z] [IsAffine X]
    (hfinite : letI := f.appTop.hom.toAlgebra
      Module.Finite Γ(S, ⊤) Γ(Z, ⊤))
    (hfree : letI := f.appTop.hom.toAlgebra
      Module.Free Γ(S, ⊤) Γ(Z, ⊤)) :
    ∃ W : Over S, IsAffine W.left ∧
      Nonempty
        (((Limits.prod.functor.obj (Over.mk f)).op ⋙
          yoneda.obj (Over.mk g)).RepresentableBy W)

Tag 0BL3, a lemma

Tag 0BL3 in the Stacks Project.

Stacks.Morphisms.relativeHom_representableBy_affineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/AffineRepresentability.lean, line 136.

If Z ⟶ S is finite locally free and X ⟶ S is affine, then the relative morphism functor Mor_S(Z, X) is represented by a scheme affine over S.

theorem relativeHom_representableBy_affineHom {S Z X : Scheme.{u}} (f : Z ⟶ S) (g : X ⟶ S)
    [IsFiniteLocallyFree f] [IsAffineHom g] :
    ∃ W : Over S, IsAffineHom W.hom ∧
      Nonempty
        (((prod.functor.obj (Over.mk f)).op ⋙ yoneda.obj (Over.mk g)).RepresentableBy W)

Tag 0BL4, a lemma

Tag 0BL4 in the Stacks Project.

Stacks.Morphisms.homFromFiniteLocallyFree_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/Representability.lean, line 904.

Stacks Project, Tag 0BL4. If Z is finite locally free over S and every finite set of points in a fibre of X lies in an affine open of X, then the functor of S-morphisms from Z to X is representable.

theorem homFromFiniteLocallyFree_isRepresentable
    {S Z X : Scheme.{u}} (f : Z ⟶ S) (g : X ⟶ S)
    [IsFiniteLocallyFree f]
    (hX : ∀ (s : S) (t : Set X), t.Finite →
      (∀ x ∈ t, g.base x = s) →
      ∃ U : X.Opens, IsAffineOpen U ∧ t ⊆ U) :
    ((prod.functor.obj (Over.mk f)).op ⋙ yoneda.obj (Over.mk g)).IsRepresentable

Tag 0BL5, a lemma

Tag 0BL5 in the Stacks Project.

Stacks.Morphisms.relativeHom_isRepresentable_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/Representability.lean, line 921.

Stacks Project, Tag 0BL5. If Z is finite locally free over S and X is separated and quasi-finite over S, then the functor of S-morphisms from Z to X is representable.

The hypothesis of Stacks Tag 0BL4 is supplied by Stacks Tag 07S0: a finite set of points of X in one fibre over s : S lies above an affine open U ∋ s, so it is a finite set of points of g ⁻¹ᵁ U, which is separated and quasi-finite over the affine scheme U.

theorem relativeHom_isRepresentable_of_locallyQuasiFinite
    {S Z X : Scheme.{u}} (f : Z ⟶ S) (g : X ⟶ S)
    [IsFiniteLocallyFree f] [IsSeparated g] [LocallyOfFiniteType g] [LocallyQuasiFinite g] :
    ((prod.functor.obj (Over.mk f)).op ⋙ yoneda.obj (Over.mk g)).IsRepresentable

Sources

LeanAlgebraicGeometry.relativeHomObjEquivOverBase · AlgebraicGeometry.relativeHom · AlgebraicGeometry.relativeHom_representableBy_affine · Stacks.Morphisms.relativeHom_representableBy_affineHom · Stacks.Morphisms.homFromFiniteLocallyFree_isRepresentable · Stacks.Morphisms.relativeHom_isRepresentable_of_locallyQuasiFinite

Section37.69 Characterizing pseudo-coherent complexes, III #

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

Tag 0CTA, a lemma

Tag 0CTA in the Stacks Project.

AlgebraicGeometry.torIndependent_pullback_product_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/TorIndependenceBaseChange.lean, line 272.

In a commutative square, flatness of the right-hand object over the base and of the upper-left object over the lower-left object implies the indicated Tor independence after arbitrary base change.

theorem torIndependent_pullback_product_of_flat
    {S S' X' Y' Z' : Scheme.{u}}
    (s : S ⟶ S') (x : X' ⟶ S') (y : Y' ⟶ S')
    (zx : Z' ⟶ X') (zy : Z' ⟶ Y') (hz : zx ≫ x = zy ≫ y)
    [Flat y] [Flat zx] :
    let _X := pullback x s
    let _Y := pullback y s
    let P := pullback (pullback.snd x s) (pullback.snd y s)
    let P' := pullback x y
    let pToP' : P ⟶ P' :=
      pullback.lift
        (pullback.fst (pullback.snd x s) (pullback.snd y s) ≫ pullback.fst x s)
        (pullback.snd (pullback.snd x s) (pullback.snd y s) ≫ pullback.fst y s)
        (by
          calc
            _ = pullback.fst (pullback.snd x s) (pullback.snd y s) ≫
                (pullback.fst x s ≫ x) := Category.assoc _ _ _
            _ = pullback.fst (pullback.snd x s) (pullback.snd y s) ≫
                (pullback.snd x s ≫ s) := by rw [pullback.condition]
            _ = (pullback.fst (pullback.snd x s) (pullback.snd y s) ≫
                pullback.snd x s) ≫ s := (Category.assoc _ _ _).symm
            _ = (pullback.snd (pullback.snd x s) (pullback.snd y s) ≫
                pullback.snd y s) ≫ s := by rw [pullback.condition]
            _ = pullback.snd (pullback.snd x s) (pullback.snd y s) ≫
                (pullback.snd y s ≫ s) := Category.assoc _ _ _
            _ = pullback.snd (pullback.snd x s) (pullback.snd y s) ≫
                (pullback.fst y s ≫ y) := by rw [pullback.condition]
            _ = _ := (Category.assoc _ _ _).symm)
    let zToP' : Z' ⟶ P' := pullback.lift zx zy hz
    TorIndependent pToP' zToP'

Tag 0CSJ, a lemma

Tag 0CSJ in the Stacks Project.

AlgebraicGeometry.exists_derivedChowDatum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowLemmaGeneral.lean, line 348.

Derived Chow's lemma, [Stacks, Tag 0CSJ]. Let A be a ring and let X be a separated scheme of finite presentation over A, with structure morphism f : X ⟶ Spec A. For every point x of X there are an open neighbourhood U of x, an m ≥ 0, an open V of ℙᵐ_A, a closed subscheme iZ : Z ⟶ X ×_A ℙᵐ_A, a point z of Z and an object E of D(𝒪_{X ×_A ℙᵐ_A}) such that, writing b : Z ⟶ X and c : Z ⟶ ℙᵐ_A for the two projections of Z:

iZ is of finite presentation;

b is an isomorphism over U, and b z = x;

c is a closed immersion over V;

b ⁻¹ᵁ U = c ⁻¹ᵁ V, and in particular c z ∈ V;

the restriction of E to X ×_A V is isomorphic to the restriction of (b, c)_* 𝒪_Z;

E is pseudo-coherent and its cohomology is supported on Z.

The proof is the source's: write X as the base change of a separated scheme of finite presentation X' over a finitely generated subring A' of A, apply the Noetherian case AlgebraicGeometry.exists_chowDatum_isPseudoCoherent_of_isNoetherian to X', and pull the datum back (AlgebraicGeometry.hasDerivedChowDatum_of_isPullback).

theorem exists_derivedChowDatum {A : Type u} [CommRing A] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of A)) [IsSeparated f] [LocallyOfFinitePresentation f] [QuasiCompact f]
    (x : X) :
    ∃ (U : X.Opens) (m : ℕ) (V : (projectiveSpaceOver m (Spec (.of A))).Opens) (Z : Scheme.{u})
      (iZ : Z ⟶ pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) (z : Z)
      (E : DerivedCategory
        (pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).Modules),
      x ∈ U ∧ IsClosedImmersion iZ ∧ FinitePresentation iZ ∧
        IsIso ((iZ ≫ pullback.fst f
          (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ∣_ U) ∧
        (iZ ≫ pullback.fst f
          (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).base z = x ∧
        IsClosedImmersion ((iZ ≫ pullback.snd f
          (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ∣_ V) ∧
        (iZ ≫ pullback.fst f
            (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ⁻¹ᵁ U =
          (iZ ≫ pullback.snd f
            (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ⁻¹ᵁ V ∧
        (iZ ≫ pullback.snd f
          (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).base z ∈ V ∧
        Nonempty ((derivedPullback (ofScheme (pullback.snd f
            (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A)) ⁻¹ᵁ V).ι)).obj E ≅
          (derivedPullback (ofScheme (pullback.snd f
            (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A)) ⁻¹ᵁ V).ι)).obj
            ((DerivedCategory.singleFunctor
              (pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).Modules 0).obj
              ((Scheme.Modules.pushforward iZ).obj (SheafOfModules.unit Z.ringCatSheaf)))) ∧
        RingedSpace.IsPseudoCoherent (X := (pullback f
          (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).toRingedSpace) E ∧
        CohomologySupportedOn (pullback f
            (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).ringCatSheaf
          (Set.range iZ.base) E

Tag 0CSK, a lemma

Tag 0CSK in the Stacks Project.

AlgebraicGeometry.isClosedImmersion_chowDatumMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowFourierMukai.lean, line 333. The attribute's comment: “the morphism U ⟶ V of the statement is a closed immersion; the derived comparison is chowDatum_derivedPushforward_tensor_restrict_iso”.

[Stacks, Tag 0CSK], first assertion: U ⟶ V is a closed immersion. It is the inverse of an isomorphism, a transport along an equality of opens, and the closed immersion c|_V.

theorem isClosedImmersion_chowDatumMorphism (hb : IsIso ((iZ ≫ p) ∣_ U))
    (hc : IsClosedImmersion ((iZ ≫ q) ∣_ V))
    (hW : (iZ ≫ p) ⁻¹ᵁ U = (iZ ≫ q) ⁻¹ᵁ V) :
    IsClosedImmersion (chowDatumMorphism p q iZ U V hb hW)

AlgebraicGeometry.finitePresentation_chowDatumMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowFourierMukai.lean, line 349. The attribute's comment: “the morphism U ⟶ V of the statement is of finite presentation, given that U and V are of finite presentation over the base; the derived comparison is chowDatum_derivedPushforward_tensor_restrict_iso”.

[Stacks, Tag 0CSK], first assertion: U ⟶ V is of finite presentation. The two factorization identities show that U ⟶ V is a morphism over the base S, and [Stacks, Tag 02FV] then deduces finite presentation of U ⟶ V from finite presentation of U ⟶ S and of V ⟶ S.

theorem finitePresentation_chowDatumMorphism {S : Scheme.{u}} (f : X ⟶ S) (g : P ⟶ S)
    (hpq : p ≫ f = q ≫ g) (hb : IsIso ((iZ ≫ p) ∣_ U))
    (hW : (iZ ≫ p) ⁻¹ᵁ U = (iZ ≫ q) ⁻¹ᵁ V)
    (hU : AlgebraicGeometry.FinitePresentation (U.ι ≫ f))
    (hV : AlgebraicGeometry.FinitePresentation (V.ι ≫ g)) :
    AlgebraicGeometry.FinitePresentation (chowDatumMorphism p q iZ U V hb hW)

AlgebraicGeometry.chowDatum_derivedPushforward_tensor_restrict_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowFourierMukai.lean, line 416. The attribute's comment: “the derived comparison Rq_(Lp^K ⊗ᴸ E)|_V ≅ R(U → V)_(K|_U), for arbitrary K in D(O_X) — more general than the source, which takes K in D_QCoh(O_X) — carrying two inputs as named hypotheses. (i) hproj is Tag 08EU, the projection formula, at the closed immersion i : W ⟶ q⁻¹V and at a GENERAL target complex: this library carries Tag 08EU only at the unit object (see the restriction on isIso_projectionFormulaMap_unitObject) and the source's devissage to that case is not available; it is also stated with the direct image on the right of the tensor product, so it differs from the Tag 0B53 map by the commutativity of ⊗ᴸ, which is likewise not carried. (ii) hE is clause (5) of Tag 0CSJ in the restricted form the source uses, that E restricted to q⁻¹V is Ri_O_W: the library's Tag 0CSJ gives the stronger global form E ≅ (iZ)_O_Z[0], but descending it to q⁻¹V needs exactness of direct image along a closed immersion and the unit comparison Lj^(O_T[0]) ≅ O_W[0], which the Tag 08EU file records as unavailable. Everything else is proved here: Tag 08FE (localization of the total direct image, proved in this file for the standard functors), Tag 079U, Tags 0D5S and 0D5T, and the invertibility of the derived adjunction unit along the isomorphism b|_U. The two geometric assertions of the statement, that U ⟶ V is a closed immersion and is of finite presentation, are isClosedImmersion_chowDatumMorphism and finitePresentation_chowDatumMorphism”.

[Stacks, Tag 0CSK], the derived comparison. In the situation of Chow's lemma in the derived category — p : T ⟶ X and q : T ⟶ P the two projections of T = X ×_A P, iZ : Z ⟶ T the closed subscheme, b = iZ ≫ p an isomorphism over the open U ⊆ X, c = iZ ≫ q a closed immersion over the open V ⊆ P, and b ⁻¹ᵁ U = c ⁻¹ᵁ V — for every E ∈ D(𝒪_T) and every K ∈ D(𝒪_X)

Rq_*(Lp^*K ⊗^𝐋 E)|_V ≅ R(c ∘ (b|_U)⁻¹)_*(K|_U).

The two hypotheses are the inputs the source cites and this library does not carry: hE is clause (5) of [Stacks, Tag 0CSJ], that the restriction of E to q ⁻¹ᵁ V is the direct image of the structure sheaf of W = c ⁻¹ᵁ V along the closed immersion i = iZ ∣_ (q ⁻¹ᵁ V); and hproj is [Stacks, Tag 08EU] at i and at the target complex Lp^*K restricted, which is the projection formula at a general complex, the case the library's [Stacks, Tag 08EU] excludes.

Everything else is proved: the localization of the direct image is [Stacks, Tag 08FE], here AlgebraicGeometry.DerivedChow.derivedPushforwardRestrictOpenIso; the monoidality of derived pullback is [Stacks, Tag 079U]; the two composition isomorphisms are [Stacks, Tag 0D5S] and [Stacks, Tag 0D5T]; and the final identification uses that b|_U is an isomorphism, so that the unit of the derived adjunction of [Stacks, Tag 079W] along it is invertible.

theorem chowDatum_derivedPushforward_tensor_restrict_iso
    (hE : (derivedPullback (ofScheme (q ⁻¹ᵁ V).ι)).obj E ≅
      (derivedPushforward (ofScheme (iZ ∣_ (q ⁻¹ᵁ V)))).obj
        (structureSheafSingle (iZ ⁻¹ᵁ (q ⁻¹ᵁ V)).toScheme))
    (hproj : ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
            (q ⁻¹ᵁ V).toScheme.sheaf).obj
          ((derivedPullback (ofScheme (q ⁻¹ᵁ V).ι)).obj
            ((derivedPullback (ofScheme p)).obj K))).obj
        ((derivedPushforward (ofScheme (iZ ∣_ (q ⁻¹ᵁ V)))).obj
          (structureSheafSingle (iZ ⁻¹ᵁ (q ⁻¹ᵁ V)).toScheme)) ≅
      (derivedPushforward (ofScheme (iZ ∣_ (q ⁻¹ᵁ V)))).obj
        ((derivedPullback (ofScheme (iZ ∣_ (q ⁻¹ᵁ V)))).obj
          ((derivedPullback (ofScheme (q ⁻¹ᵁ V).ι)).obj
            ((derivedPullback (ofScheme p)).obj K)))) :
    Nonempty ((derivedPullback (ofScheme V.ι)).obj ((derivedPushforward (ofScheme q)).obj
        (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor T.sheaf).obj
          ((derivedPullback (ofScheme p)).obj K)).obj E)) ≅
      (derivedPushforward (ofScheme (chowDatumMorphism p q iZ U V hb hW))).obj
        ((derivedPullback (ofScheme U.ι)).obj K))

AlgebraicGeometry.chowDatum_derivedPushforward_tensor_restrict_iso_of_isDQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowFourierMukaiQCoh.lean, line 200. The attribute's comment: “the derived comparison Rq_(Lp^K ⊗ᴸ E)|_V ≅ R(U → V)_*(K|_U) for K in D_QCoh(O_X), which is the condition on K that Tag 0CSK itself states. Everything else the statement fixes — p, q, iZ, U, V, E and the three conditions hb, hW, hE on them — is the datum of Lemma 0CSJ, hE being clause (5) of that lemma in the very shape exists_derivedChowDatum produces it. Nothing further enters: the projection formula of Tag 08EU and clause (5) in the restricted form the computation reads it in are both proved here, as derivedProjectionFormulaUnitRightIso and DerivedChow.pushforwardUnitRestrictIso. The whole statement, with the two geometric assertions that U ⟶ V is a closed immersion and is of finite presentation, is chowDatum_fourierMukai”.

[Stacks, Tag 0CSK], the derived comparison, at a quasi-coherent complex. In the situation of derived Chow's lemma — p : T ⟶ X and q : T ⟶ P the two projections of T = X ×_A ℙⁿ_A, iZ : Z ⟶ T the closed subscheme, b = iZ ≫ p an isomorphism over the open U ⊆ X, c = iZ ≫ q, and b ⁻¹ᵁ U = c ⁻¹ᵁ V for an open V ⊆ P — let E satisfy clause (5) of [Stacks, Tag 0CSJ], that its restriction to q ⁻¹ᵁ V agrees with that of (iZ)_*𝒪_Z. Then for every K ∈ D_QCoh(𝒪_X)

Rq_*(Lp^*K ⊗^𝐋 E)|_V ≅ R(c ∘ (b|_U)⁻¹)_*(K|_U).

This statement stands at the data of [Stacks, Tag 0CSJ] and nothing else: hb, hW and hE are clauses (2), (4) and (5) of that lemma, in the shape AlgebraicGeometry.exists_derivedChowDatum produces them, and hK is the quasi-coherence condition on K that [Stacks, Tag 0CSK] states. The whole of Tag 0CSK, at the projections of X ×_A ℙᵐ_A, is AlgebraicGeometry.chowDatum_fourierMukai below. The proof is AlgebraicGeometry.chowDatum_derivedPushforward_tensor_restrict_iso, whose two inputs are supplied by AlgebraicGeometry.DerivedChow.pushforwardUnitRestrictIso and by AlgebraicGeometry.derivedProjectionFormulaUnitRightIso.

theorem chowDatum_derivedPushforward_tensor_restrict_iso_of_isDQCoh
    {X P T Z : Scheme.{u}} (p : T ⟶ X) (q : T ⟶ P) (iZ : Z ⟶ T) [IsClosedImmersion iZ]
    (U : X.Opens) (V : P.Opens) (hb : IsIso ((iZ ≫ p) ∣_ U))
    (hW : (iZ ≫ p) ⁻¹ᵁ U = (iZ ≫ q) ⁻¹ᵁ V)
    (E : DerivedCategory T.Modules)
    (hE : (derivedPullback (ofScheme (q ⁻¹ᵁ V).ι)).obj E ≅
      (derivedPullback (ofScheme (q ⁻¹ᵁ V).ι)).obj
        ((DerivedCategory.singleFunctor T.Modules 0).obj
          ((Scheme.Modules.pushforward iZ).obj (SheafOfModules.unit Z.ringCatSheaf))))
    (K : DerivedCategory X.Modules)
    (hK : ∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) :
    Nonempty ((derivedPullback (ofScheme V.ι)).obj ((derivedPushforward (ofScheme q)).obj
        (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor T.sheaf).obj
          ((derivedPullback (ofScheme p)).obj K)).obj E)) ≅
      (derivedPushforward (ofScheme (chowDatumMorphism p q iZ U V hb hW))).obj
        ((derivedPullback (ofScheme U.ι)).obj K))

AlgebraicGeometry.chowDatum_fourierMukai, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowFourierMukaiQCoh.lean, line 288.

[Stacks, Tag 0CSK]. Let A be a ring, let f : X ⟶ Spec A be locally of finite presentation (in the source, X is separated and of finite presentation over A), let p : X ×_A ℙᵐ_A ⟶ X and q : X ×_A ℙᵐ_A ⟶ ℙᵐ_A be the two projections, and let U ⊆ X, V ⊆ ℙᵐ_A, iZ : Z ⟶ X ×_A ℙᵐ_A and E ∈ D(𝒪_{X ×_A ℙᵐ_A}) be as in [Stacks, Tag 0CSJ]: iZ is a closed immersion, b = iZ ≫ p is an isomorphism over U, c = iZ ≫ q is a closed immersion over V, b ⁻¹ᵁ U = c ⁻¹ᵁ V, and the restriction of E to X ×_A V is that of (b, c)_*𝒪_Z — each in the very shape AlgebraicGeometry.exists_derivedChowDatum produces it. Then the morphism c ∘ (b|_U)⁻¹ : U ⟶ V is a closed immersion of finite presentation, and for every K ∈ D_QCoh(𝒪_X)

Rq_*(Lp^*K ⊗^𝐋 E)|_V ≅ R(c ∘ (b|_U)⁻¹)_*(K|_U).

The clauses of [Stacks, Tag 0CSJ] not listed — finite presentation of iZ, the point z, separatedness and quasi-compactness of X, pseudo-coherence and support of E — are not used, so the statement is given without them.

theorem chowDatum_fourierMukai {A : Type u} [CommRing A] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of A)) [LocallyOfFinitePresentation f] (m : ℕ) (U : X.Opens)
    (V : (projectiveSpaceOver m (Spec (.of A))).Opens) {Z : Scheme.{u}}
    (iZ : Z ⟶ pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A)))
    [IsClosedImmersion iZ]
    (hb : IsIso ((iZ ≫ pullback.fst f
      (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ∣_ U))
    (hc : IsClosedImmersion ((iZ ≫ pullback.snd f
      (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ∣_ V))
    (hW : (iZ ≫ pullback.fst f
        (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ⁻¹ᵁ U =
      (iZ ≫ pullback.snd f
        (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))) ⁻¹ᵁ V)
    (E : DerivedCategory
      (pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).Modules)
    (hE : Nonempty ((derivedPullback (ofScheme (pullback.snd f
        (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A)) ⁻¹ᵁ V).ι)).obj E ≅
      (derivedPullback (ofScheme (pullback.snd f
        (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A)) ⁻¹ᵁ V).ι)).obj
        ((DerivedCategory.singleFunctor
          (pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).Modules 0).obj
          ((Scheme.Modules.pushforward iZ).obj (SheafOfModules.unit Z.ringCatSheaf))))) :
    IsClosedImmersion (chowDatumMorphism (pullback.fst f _) (pullback.snd f _) iZ U V hb hW) ∧
      AlgebraicGeometry.FinitePresentation
        (chowDatumMorphism (pullback.fst f _) (pullback.snd f _) iZ U V hb hW) ∧
      ∀ K : DerivedCategory X.Modules,
        (∀ n : ℤ, ((DerivedCategory.homologyFunctor X.Modules n).obj K).IsQuasicoherent) →
        Nonempty ((derivedPullback (ofScheme V.ι)).obj
            ((derivedPushforward (ofScheme (pullback.snd f
              (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))))).obj
              (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor
                  (pullback f (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))).sheaf).obj
                ((derivedPullback (ofScheme (pullback.fst f
                  (projectiveSpaceOver m (Spec (.of A)) ↘ Spec (.of A))))).obj K)).obj E)) ≅
          (derivedPushforward (ofScheme
            (chowDatumMorphism (pullback.fst f _) (pullback.snd f _) iZ U V hb hW))).obj
            ((derivedPullback (ofScheme U.ι)).obj K))

Tag 0CSL, a lemma

Tag 0CSL in the Stacks Project.

AlgebraicGeometry.isPseudoCoherent_of_derivedGlobalSectionsOver_tensor_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/PseudoCoherentByPseudoCoherentTwists.lean, line 141.

Let A be a ring, let X be a scheme separated and of finite presentation over A, with structure morphism f : X ⟶ Spec A, and let K ∈ D_QCoh(𝒪_X). If RΓ(X, E ⊗^𝐋 K) is a pseudo-coherent object of D(A) for every pseudo-coherent object E of D(𝒪_X), then K is pseudo-coherent relative to A.

"Separated and of finite presentation over A" is IsSeparated f, QuasiCompact f and LocallyOfFinitePresentation f (quasi-separatedness follows from separatedness); K ∈ D_QCoh(𝒪_X) is quasi-coherence of its cohomology sheaves; RΓ(X, -) is the A-linear AlgebraicGeometry.derivedGlobalSectionsOver f; pseudo-coherence relative to A is AlgebraicGeometry.Scheme.Hom.IsPseudoCoherent f (Stacks 09UI).

theorem isPseudoCoherent_of_derivedGlobalSectionsOver_tensor_isPseudoCoherent
    (f : X ⟶ Spec (.of A)) [IsSeparated f] [QuasiCompact f]
    [LocallyOfFinitePresentation f] (K : DerivedCategory X.Modules)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj K).IsQuasicoherent)
    (hpc : ∀ E : DerivedCategory X.Modules, RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E →
      StacksDraft.PseudoCoherence.IsPseudoCoherent
        ((derivedGlobalSectionsOver f).obj
          (((Stacks.SheafOfModules.derivedTensor X.sheaf).obj E).obj K))) :
    f.IsPseudoCoherent K

Tag 0GES, a lemma

Tag 0GES in the Stacks Project.

AlgebraicGeometry.isPseudoCoherent_of_derivedGlobalSectionsOver_tensor_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/PseudoCoherentByPerfectTwists.lean, line 111.

[Stacks, Tag 0GES]. Let A be a ring, let X be a scheme separated and of finite presentation over A, with structure morphism f : X ⟶ Spec A, and let K ∈ D_QCoh(𝒪_X). If RΓ(X, E ⊗^𝐋 K) is a pseudo-coherent object of D(A) for every perfect object E of D(𝒪_X), then K is pseudo-coherent relative to A.

theorem isPseudoCoherent_of_derivedGlobalSectionsOver_tensor_isPerfect
    (f : X ⟶ Spec (CommRingCat.of A)) [IsSeparated f] [QuasiCompact f]
    [LocallyOfFinitePresentation f]
    (K : DerivedCategory (StructureSheafModules X.sheaf))
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent)
    (hpc : ∀ E : DerivedCategory (StructureSheafModules X.sheaf),
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E →
        StacksDraft.PseudoCoherence.IsPseudoCoherent
          ((derivedGlobalSectionsOver f).obj (((derivedTensor X.sheaf).obj E).obj K))) :
    f.IsPseudoCoherent K

Tag 0GET, a lemma

Tag 0GET in the Stacks Project.

AlgebraicGeometry.eventually_subsingleton_ext_of_derivedGlobalSections_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectDetectedByGlobalSections.lean, line 164. The attribute's comment: “ONLY the vanishing the tag's hypothesis produces: Ext^i_X(G, K) and Hom(G⟦-i⟧, K) vanish for i ≪ 0. That K is Spec(A)-perfect is NOT proved here; it needs Stacks 0GES, the implication (2) ⇒ (1) of Stacks 0GEH, and condition (1) of Stacks 0GEQ, none of which the library carries. See the implementation notes for what is carried.”.

Stacks 0GET, the vanishing that the hypothesis produces. Let A be a ring, let X be a scheme separated, of finite presentation and flat over A, let G be a perfect generator of D_QCoh(𝒪_X) whose dual G^∨ is perfect, and let K be an object of D_QCoh(𝒪_X). If RΓ(X, K ⊗^L_{𝒪_X} E) is a perfect object of D(A) for every perfect object E of D(𝒪_X), then Ext^i_X(G, K) and Hom_{D(𝒪_X)}(G⟦-i⟧, K) vanish for i ≪ 0.

Perfectness of G^∨ is Stacks 08DQ, and is a hypothesis here rather than a consequence of hG; see the implementation notes. It makes the hypothesis on perfect twists apply to G^∨, so that RΓ(X, K ⊗^L_{𝒪_X} G^∨) is the underlying complex of abelian groups of a perfect object of D(A). A perfect object of D(A) has vanishing cohomology in all sufficiently negative degrees and the forgetful functor to abelian groups is exact, so H^i(X, G^∨ ⊗^L_{𝒪_X} K) vanishes for i ≪ 0; that is condition (5) of Stacks 0GEQ, whose equivalence with conditions (3) and (2) gives the two assertions.

Spec(A)-perfectness of K is not proved; see the implementation notes.

public theorem eventually_subsingleton_ext_of_derivedGlobalSections_isPerfect
    (f : X ⟶ Spec (CommRingCat.of A)) [IsSeparated f] [QuasiCompact f] [Flat f]
    [LocallyOfFinitePresentation f]
    (hqc : CompactSpace X) (hqs : QuasiSeparatedSpace X)
    (G K : DerivedCategory (StructureSheafModules X.sheaf))
    (hG : (ringedSite X.sheaf).IsPerfect G)
    (hGdual : (ringedSite X.sheaf).IsPerfect (derivedDual X.sheaf G))
    (hgen : ∀ L : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj L).IsQuasicoherent) →
        (∀ (n : ℤ) (g : G⟦n⟧ ⟶ L), g = 0) → IsZero L)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent)
    (h08I1 : ∀ i : ℤ, IsIso (derivedTensorDualToSheafHom X.sheaf G (K⟦i⟧)))
    (hperf : ∀ E : DerivedCategory (StructureSheafModules X.sheaf),
      (ringedSite X.sheaf).IsPerfect E →
        ∃ M : DerivedCategory (ModuleCat.{u} A), StacksDraft.Perfect.IsPerfect M ∧
          Nonempty ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
              (((derivedTensor X.sheaf).obj K).obj E) ≅
            (forget₂ (ModuleCat.{u} A) AddCommGrpCat.{u}).mapDerivedCategory.obj M)) :
    (∃ N : ℤ, ∀ i ≤ N, Subsingleton (DerivedCategory.Ext G K i)) ∧
      ∃ N : ℤ, ∀ i ≤ N, Subsingleton (G⟦-i⟧ ⟶ K)

AlgebraicGeometry.eventually_subsingleton_ext_of_derivedGlobalSections_isPerfect', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectDetectedByGlobalSectionsDual.lean, line 121. The attribute's comment: “ONLY the vanishing the tag's hypothesis produces: Ext^i_X(G, K) and Hom(G⟦-i⟧, K) vanish for i ≪ 0, for a perfect generator G, with perfectness of the dual and invertibility of the Stacks 08I1 map proved by Stacks 08DQ. That K is Spec(A)-perfect is NOT proved here; it needs Stacks 0GES, the implication (2) ⇒ (1) of Stacks 0GEH, and condition (1) of Stacks 0GEQ.”.

The vanishing of Stacks 0GET, with the duality inputs proved. Let A be a ring, let X be a scheme separated, of finite presentation and flat over A, let G be a perfect generator of D_QCoh(𝒪_X), and let K be an object of D_QCoh(𝒪_X). If RΓ(X, K ⊗^L_{𝒪_X} E) is a perfect object of D(A) for every perfect object E of D(𝒪_X), then Ext^i_X(G, K) and Hom_{D(𝒪_X)}(G⟦-i⟧, K) vanish for i ≪ 0.

This is eventually_subsingleton_ext_of_derivedGlobalSections_isPerfect with its two arguments about G discharged by [Stacks, Tag 08DQ]: the dual G^∨ is perfect by the first assertion, Stacks.SheafOfModules.isPerfect_derivedDual, and the map of [Stacks, Tag 08I1] out of K⟦i⟧ ⊗^L G^∨ is invertible for every i by the third, Stacks.SheafOfModules.isIso_derivedTensorDualToSheafHom_of_isPerfect.

That K is Spec(A)-perfect, the conclusion of the source, is not proved; the implementation notes of StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectDetectedByGlobalSections.lean list the three results it rests on.

public theorem eventually_subsingleton_ext_of_derivedGlobalSections_isPerfect'
    (f : X ⟶ Spec (CommRingCat.of A)) [IsSeparated f] [QuasiCompact f] [Flat f]
    [LocallyOfFinitePresentation f]
    (hqc : CompactSpace X) (hqs : QuasiSeparatedSpace X)
    (G K : DerivedCategory (StructureSheafModules X.sheaf))
    (hG : (ringedSite X.sheaf).IsPerfect G)
    (hgen : ∀ L : DerivedCategory (StructureSheafModules X.sheaf),
      (∀ i : ℤ, ((DerivedCategory.homologyFunctor
          (StructureSheafModules X.sheaf) i).obj L).IsQuasicoherent) →
        (∀ (n : ℤ) (g : G⟦n⟧ ⟶ L), g = 0) → IsZero L)
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent)
    (hperf : ∀ E : DerivedCategory (StructureSheafModules X.sheaf),
      (ringedSite X.sheaf).IsPerfect E →
        ∃ M : DerivedCategory (ModuleCat.{u} A), StacksDraft.Perfect.IsPerfect M ∧
          Nonempty ((derivedModuleGlobalSections (ringedSite X.sheaf)).obj
              (((derivedTensor X.sheaf).obj K).obj E) ≅
            (forget₂ (ModuleCat.{u} A) AddCommGrpCat.{u}).mapDerivedCategory.obj M)) :
    (∃ N : ℤ, ∀ i ≤ N, Subsingleton (DerivedCategory.Ext G K i)) ∧
      ∃ N : ℤ, ∀ i ≤ N, Subsingleton (G⟦-i⟧ ⟶ K)

AlgebraicGeometry.Scheme.Hom.isRelativelyPerfect_of_isPerfect_derivedGlobalSectionsOver_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectFromGlobalSections.lean, line 93.

Stacks 0GET. Let A be a ring and let X be a scheme separated, of finite presentation and flat over A, with structure morphism f : X ⟶ Spec A. Let K be an object of D_QCoh(𝒪_X). If RΓ(X, E ⊗^L K) is a perfect object of D(A) for every perfect object E of D(𝒪_X), then K is Spec(A)-perfect.

RΓ(X, -) is the A-linear derived global sections AlgebraicGeometry.derivedGlobalSectionsOver, perfectness in D(A) is StacksDraft.Perfect.IsPerfect, perfectness of E is Stacks 08CM on the ringed space of X, and Spec(A)-perfectness is AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect (Stacks 0DI0). Of finite presentation is [QuasiCompact f] [LocallyOfFinitePresentation f] together with quasi-separatedness, which separatedness implies.

theorem Scheme.Hom.isRelativelyPerfect_of_isPerfect_derivedGlobalSectionsOver_tensor
    (f : X ⟶ Spec (CommRingCat.of A)) [IsSeparated f] [QuasiCompact f]
    [LocallyOfFinitePresentation f] [Flat f]
    (K : DerivedCategory (StructureSheafModules X.sheaf))
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor
      (StructureSheafModules X.sheaf) i).obj K).IsQuasicoherent)
    (hperf : ∀ E : DerivedCategory (StructureSheafModules X.sheaf),
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.toRingedSpace) E →
        StacksDraft.Perfect.IsPerfect
          ((derivedGlobalSectionsOver f).obj (((derivedTensor X.sheaf).obj E).obj K))) :
    f.IsRelativelyPerfect K

Sources

LeanAlgebraicGeometry.torIndependent_pullback_product_of_flat · AlgebraicGeometry.exists_derivedChowDatum · AlgebraicGeometry.isClosedImmersion_chowDatumMorphism · AlgebraicGeometry.finitePresentation_chowDatumMorphism · AlgebraicGeometry.chowDatum_derivedPushforward_tensor_restrict_iso · AlgebraicGeometry.chowDatum_derivedPushforward_tensor_restrict_iso_of_isDQCoh · AlgebraicGeometry.chowDatum_fourierMukai · AlgebraicGeometry.isPseudoCoherent_of_derivedGlobalSectionsOver_tensor_isPseudoCoherent

Section37.70 Descent finiteness properties of complexes #

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

Tag 0CSN, a lemma

Tag 0CSN in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_derivedPullback_of_mem_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFppfDescentConverse.lean, line 432. The attribute's comment: “both implications, at the source's hypotheses: f locally of finite type, an arbitrary fppf covering of X (Presieve.ofArrows in Scheme.fppfPrecoverage, any index universe), E with quasi-coherent cohomology sheaves, any m”.

Stacks 0CSN. Let f : X ⟶ S be locally of finite type, let {g i : Y i ⟶ X} be an fppf covering of schemes, let E be an object of D(𝒪_X) with quasi-coherent cohomology sheaves and let m be an integer. Then E is m-pseudo-coherent relative to S if and only if every L(g i)^*E is m-pseudo-coherent relative to S.

The forward implication is Stacks 0695 (a member of an fppf covering is flat and locally of finite presentation, hence pseudo-coherent) followed by Stacks 09US, AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_comp_derivedPullback; it needs neither joint surjectivity nor the quasi-coherence of E. The converse is Scheme.Hom.isPseudoCoherentFrom_of_forall_derivedPullback_of_mem_fppfPrecoverage (Stacks 05WN, 0683, 09US, 09UK, 08EU, 09UN and Zariski gluing). The membership of g i ≫ f in the class of morphisms locally of finite type, which the predicate takes as an instance argument, comes from the covering.

public theorem Scheme.Hom.isPseudoCoherentFrom_iff_forall_derivedPullback_of_mem_fppfPrecoverage
    {X S : Scheme.{u}} {ι : Type v} (Y : ι → Scheme.{u}) (g : ∀ i, Y i ⟶ X) (f : X ⟶ S)
    [LocallyOfFiniteType f] (hg : Presieve.ofArrows Y g ∈ Scheme.fppfPrecoverage X)
    (E : DerivedCategory X.Modules)
    (hE : ∀ i : ℤ, ((DerivedCategory.homologyFunctor X.Modules i).obj E).IsQuasicoherent)
    (m : ℤ) :
    f.IsPseudoCoherentFrom E m ↔
      ∀ i, letI : LocallyOfFinitePresentation (g i) :=
          locallyOfFinitePresentation_of_mem_fppfPrecoverage Y g hg i
        (g i ≫ f).IsPseudoCoherentFrom ((derivedPullback (g i).toLRSHom.toShHom).obj E) m

Declarations registered for the tag:

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_derivedPullback_of_mem_fppfPrecoverage', declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFppfDescentPullback.lean, line 101 (StacksFrontier): “THE FORWARD IMPLICATION ONLY, with the Stacks 09US hypothesis DISCHARGED; the tag is an iff and its converse is NOT proved. Base already registers the forward half at PseudoCoherent/RelativeFppfDescent.lean:148, which carries 09US as a hypothesis; that file's own notes say discharging it is what would make the implication unconditional. 09US is now proved (PseudoCoherent/DerivedPullback09US.lean:634), so this restatement carries only 0E23 (DerivedBaseChangeIsoOfTorIndependent), which 09US itself already requires -- strictly fewer hypotheses than the base form. The covering is genuinely fppf (Presieve.ofArrows in Scheme.fppfPrecoverage), not etale or Zariski; no quasi-compactness, finiteness or Noetherian hypothesis is added, and nothing is assumed about E's cohomology sheaves. THE CONVERSE needs exactly two things the library lacks: Stacks 08EU at a GENERAL K (the library has it only at K = O_Y[0], and its docstring says the devissage to general K is not carried out), and the local splitting of O_X -> pi_* O_Y for a surjective finite locally free pi, which is absent entirely.”.

Tag 0CSP, a lemma

Tag 0CSP in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_comp_iff_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFlatBase.lean, line 56.

Stacks 0CSP. Let f : X ⟶ T be locally of finite type, let g : T ⟶ S be flat and locally of finite presentation, let E be an object of D(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent relative to S if and only if it is m-pseudo-coherent relative to T.

public theorem isPseudoCoherentFrom_comp_iff_of_flat
    {X T S : Scheme.{u}} (f : X ⟶ T) (g : T ⟶ S) [LocallyOfFiniteType f] [Flat g]
    [LocallyOfFinitePresentation g] (E : DerivedCategory X.Modules) (m : ℤ) :
    (f ≫ g).IsPseudoCoherentFrom E m ↔ f.IsPseudoCoherentFrom E m

Tag 0CSQ, a lemma

Tag 0CSQ in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_pullback_snd_of_pseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFppfBaseChange.lean, line 101. The attribute's comment: “both directions, for a pseudo-coherent f -- by Stacks 0684 this is every f locally of finite type over a locally Noetherian base; no hypothesis on the cohomology sheaves of E is used”.

Stacks 0CSQ for a pseudo-coherent f. Let f : X ⟶ S be a pseudo-coherent morphism of schemes, let {g i : S i ⟶ S} be an fppf covering, let E be an object of D(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent relative to S if and only if the derived pullback of E to X ×_S S i is m-pseudo-coherent relative to S i for every i.

public theorem Scheme.Hom.isPseudoCoherentFrom_iff_forall_pullback_snd_of_pseudoCoherent
    {X S : Scheme.{u}} (f : X ⟶ S) [PseudoCoherent f] {ι : Type v} (Y : ι → Scheme.{u})
    (g : ∀ i, Y i ⟶ S) (hg : Presieve.ofArrows Y g ∈ Scheme.fppfPrecoverage S)
    (E : DerivedCategory X.Modules) (m : ℤ) :
    f.IsPseudoCoherentFrom E m ↔
      ∀ i, (pullback.snd f (g i)).IsPseudoCoherentFrom
        ((derivedPullback (pullback.fst f (g i)).toLRSHom.toShHom).obj E) m

AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/RelativeFppfBaseChangeGeneral.lean, line 330.

Stacks 0CSQ. Let f : X ⟶ S be locally of finite type, let {g a : Y a ⟶ S} be an fppf covering, let E be an object of D(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent relative to S if and only if the derived pullback of E to X ×_S Y a is m-pseudo-coherent relative to Y a for every a.

The forward direction is Stacks 09UR at the flat morphism g a; the converse is AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_of_forall_pullback_snd. No hypothesis on the cohomology sheaves of E is used.

public theorem Scheme.Hom.isPseudoCoherentFrom_iff_forall_pullback_snd {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] {ι : Type v} (Y : ι → Scheme.{u}) (g : ∀ a, Y a ⟶ S)
    (hg : Presieve.ofArrows Y g ∈ Scheme.fppfPrecoverage S) (E : DerivedCategory X.Modules)
    (m : ℤ) :
    f.IsPseudoCoherentFrom E m ↔
      ∀ a, (pullback.snd f (g a)).IsPseudoCoherentFrom
        ((derivedPullback (pullback.fst f (g a)).toLRSHom.toShHom).obj E) m

Sources

LeanAlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_derivedPullback_of_mem_fppfPrecoverage · AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_derivedPullback_of_mem_fppfPrecoverage' · AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_comp_iff_of_flat · AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_pullback_snd_of_pseudoCoherent · AlgebraicGeometry.Scheme.Hom.isPseudoCoherentFrom_iff_forall_pullback_snd

Section37.71 Relatively perfect objects #

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

Tag 0DJX, a lemma

Tag 0DJX in the Stacks Project.

Stacks.Thickenings.isPseudoCoherent_of_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/Thickening.lean, line 154. The attribute's comment: “the whole statement, unconditionally: pseudo-coherence of K' in D(𝒪_{X'}) from pseudo-coherence of Li^*K', for a finite-order thickening i : X ⟶ X' of schemes, at the standard derived category”. References: SGA 6 I (2.16.2), “(i), special case”.

Pseudo-coherence descends along a finite-order thickening of schemes. Let i : X ⟶ X' be a closed immersion whose kernel ideal sheaf is nilpotent and let K' be an object of D(𝒪_{X'}) such that K = Li^*K' is pseudo-coherent. Then K' is pseudo-coherent.

Pseudo-coherence of K' is a local condition on X', so it is enough to produce it over an affine open U of X'. Over the chart Spec Γ(X', U) the thickening becomes Spec of the surjection i.app U, whose kernel is nilpotent because a power of the kernel ideal sheaf vanishes; the hypothesis travels to that chart because derived pullback preserves pseudo-coherence and the two ways around the square Spec Γ(X', U) ← Spec Γ(X, i⁻¹U) over i agree. The affine case then applies, and its conclusion comes back to U along AlgebraicGeometry.IsAffineOpen.isoSpec, again by preservation of pseudo-coherence under derived pullback, this time along the inverse.

theorem isPseudoCoherent_of_derivedPullback {X X' : Scheme.{u}} (i : X ⟶ X')
    (hi : IsFiniteOrderThickening i)
    (K' : DerivedCategory (OXMod.{u, u} X'.toRingedSpace))
    (hK : AlgebraicGeometry.RingedSpace.IsPseudoCoherent (X := X.toRingedSpace)
      ((derivedPullback i.toLRSHom.toShHom).obj K')) :
    AlgebraicGeometry.RingedSpace.IsPseudoCoherent (X := X'.toRingedSpace) K'

Stacks.Thickenings.isQuasicoherent_homology_of_isPseudoCoherent_derivedPullback_specMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PseudoCoherent/ThickeningQuasicoherent.lean, line 530. The attribute's comment: “the quasi-coherence of the cohomology, in the affine case”.

The quasi-coherence half of [Stacks, Tag 0DJX] in the affine case. Let f : R ⟶ S be a surjection of commutative rings with nilpotent kernel, so that i = Spec f is a finite-order thickening, and let A be an object of D(𝒪_{Spec R}) whose derived pullback Li^*A is pseudo-coherent. Then every cohomology sheaf of A is quasi-coherent, that is, A lies in D_QCoh(𝒪_{Spec R}).

This is the first paragraph of the source's proof. The dévissage is on the kernel ideal I = ker f: writing P for the property of an R-module N that Ñ[0] ⊗ᴸ_{𝒪_{Spec R}} A has quasi-coherent cohomology, Stacks.Thickenings.prop_of_isNilpotent_of_smul_eq_bot reduces P for every module — in particular for R itself, where the unit of the derived tensor product identifies 𝒪_{Spec R}[0] ⊗ᴸ A with A — to P for a module annihilated by I.

The inductive step. P is stable under extensions: a short exact sequence of R-modules becomes a short exact sequence of 𝒪_{Spec R}-modules, M ↦ M̃ being exact (AlgebraicGeometry.tilde.preservesFiniteLimits), hence a distinguished triangle (CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished); the derived tensor product is exact in its left variable, so tensoring with A keeps the triangle distinguished; and the quasi-coherent modules form a weak Serre subcategory ([Stacks, Tag 01LA]), so the middle vertex of a distinguished triangle whose outer vertices lie in D_QCoh lies in D_QCoh.

The base case. A module N annihilated by I is the restriction of scalars of an S-module M (Stacks.Thickenings.exists_restrictScalars_iso_of_smul_eq_bot), and then Ñ ≅ i_*(M̃) (Stacks.Descent.restrictScalarsCompTildeIso). The projection formula for the closed embedding i, in the form exists_iso_derivedPushforward_derivedTensor_obj, produces D in D(𝒪_{Spec S}) with i_*(M̃)[0] ⊗ᴸ_{𝒪_{Spec R}} A ≅ Ri_*D and D ≅ M̃[0] ⊗ᴸ_{𝒪_{Spec S}} Li^*A; the second factor of the latter is in D_QCoh(𝒪_{Spec S}) by [Stacks, Tag 08E5], the first because M̃ is quasi-coherent, so D is by [Stacks, Tag 08DX] in the form isQuasicoherent_homology_specDerivedTensor, and Ri_*D is by [Stacks, Tag 08D5].

Note that i_* = Ri_* here, which is derivedPushforwardQIsoOfIsClosedEmbedding, and that no identification of the isomorphism with the canonical projection-formula morphism of [Stacks, Tag 0B53] is needed: only membership in D_QCoh is transported.

public theorem isQuasicoherent_homology_of_isPseudoCoherent_derivedPullback_specMap
    (hf : Function.Surjective f.hom) (hnil : IsNilpotent (RingHom.ker f.hom))
    (A : DerivedCategory (StrictlyPerfect.OXMod.{u, u} (Spec R).toRingedSpace))
    (hA : AlgebraicGeometry.RingedSpace.IsPseudoCoherent (X := (Spec S).toRingedSpace)
      ((derivedPullback (Spec.map f).toLRSHom.toShHom).obj A)) :
    ∀ n : ℤ, ((DerivedCategory.homologyFunctor (Spec R).Modules n).obj A).IsQuasicoherent

Tag 0DJY, a lemma

Tag 0DJY in the Stacks Project.

Stacks.Thickenings.isPseudoCoherent_of_isPullback_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectThickening.lean, line 535. The attribute's comment: “the pseudo-coherence conjunct of the conclusion; the Tor-dimension conjunct is not proved — see the implementation notes of this module”.

The pseudo-coherence conjunct of Stacks 0DJY. In a cartesian diagram of schemes with i : X ⟶ X', f : X ⟶ Y, f' : X' ⟶ Y' and j : Y ⟶ Y', with j a finite-order thickening, an object E' of D(𝒪_{X'}) whose derived pullback Li^*E' is pseudo-coherent is itself pseudo-coherent.

A base change of a finite-order thickening is a finite-order thickening (Stacks 09ZU), so i is one, and the conclusion is Stacks 0DJX. Neither flatness nor local finite presentation of f' is used, and the family of derived tensor products plays no role, so neither appears.

This is the first of the two conjuncts of the conclusion of Stacks 0DJY. The second, locally finite Tor dimension over f'^{-1}𝒪_{Y'}, is not proved here; its local content is Stacks.Thickenings.hasTorAmplitudeCanonical_derivedStalk_of_isPullback above, and what is missing between the two is recorded in the implementation notes of this file.

public theorem isPseudoCoherent_of_isPullback_of_isFiniteOrderThickening
    {X X' Y Y' : Scheme.{u}} (i : X ⟶ X') (f : X ⟶ Y) (f' : X' ⟶ Y') (j : Y ⟶ Y')
    (hpb : IsPullback i f f' j) (hj : IsFiniteOrderThickening j)
    (E' : DerivedCategory (OXMod.{u, u} X'.toRingedSpace))
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace)
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        i.toLRSHom.toShHom).obj E')) :
    RingedSpace.IsPseudoCoherent (X := X'.toRingedSpace) E'

Stacks.Thickenings.isRelativelyPerfect_of_isPullback_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectThickeningTorDimension.lean, line 252.

Stacks 0DJY at the canonical derived tensor products. Consider a cartesian diagram of schemes with i : X ⟶ X', f : X ⟶ Y, f' : X' ⟶ Y' and j : Y ⟶ Y', in which f' is flat and locally of finite presentation and j is a finite-order thickening. Let E' be an object of D(𝒪_{X'}). If E = Li^*E' is Y-perfect, then E' is Y'-perfect, relative perfectness being AlgebraicGeometry.Scheme.Hom.IsRelativelyPerfect — Stacks 0DI0 read at the canonical derived tensor products — on both sides.

public theorem isRelativelyPerfect_of_isPullback_of_isFiniteOrderThickening
    {X X' Y Y' : Scheme.{u}} {i : X ⟶ X'} {f : X ⟶ Y} {f' : X' ⟶ Y'} {j : Y ⟶ Y'}
    (hpb : IsPullback i f f' j) (hj : IsFiniteOrderThickening j)
    [Flat f'] [LocallyOfFinitePresentation f']
    (E' : DerivedCategory (OXMod.{u, u} X'.toRingedSpace)) :
    haveI : Flat f := MorphismProperty.of_isPullback (P := @Flat) hpb inferInstance
    haveI : LocallyOfFinitePresentation f :=
      MorphismProperty.of_isPullback (P := @LocallyOfFinitePresentation) hpb inferInstance
    f.IsRelativelyPerfect
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
          i.toLRSHom.toShHom).obj E') →
      f'.IsRelativelyPerfect E'

Tag 0DJZ, a lemma

Tag 0DJZ in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.exists_finset_affineOpens_mvPolynomial_surjective_chartHom_of_universallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectJacobsonChart.lean, line 184. The attribute's comment: “the covering step with which the proof opens: for f : X ⟶ Spec R universally closed and locally of finite type, finitely many affine opens cover X and the sections over each are a quotient of a polynomial algebra over R in finitely many variables”. References: EGA I (6.6.3), “special case”; EGA IV (1.5.1), “(a) ⇒ (c), special case”.

The covering step of Stacks 0DJZ. Let R be a ring and let f : X ⟶ Spec R be universally closed and locally of finite type. Then finitely many affine opens cover X, and over each the sections are a quotient of a polynomial algebra R[x_1, …, x_d] in finitely many variables, compatibly with the structure map that f induces.

The source's proof of Stacks 0DJZ opens with this: choose a finite affine open covering X = U_1 ∪ … ∪ U_n; for each i we can choose a closed immersion U_i → 𝐀^{d_i}_S. For an affine U_i, giving a closed immersion into 𝐀^{d_i}_S over S is the same as giving a surjection R[x_1, …, x_{d_i}] ⟶ Γ(X, U_i) of R-algebras, and the surjection is the form the fibrewise criterion of Stacks 0DJH consumes, so it is the form exported here.

Quasi-compactness of X comes from universal closedness of f: the import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed carries an instance making a universally closed morphism quasi-compact, and Spec R is quasi-compact, so AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace applies. Properness is not asked for; universal closedness and local finite type are all the source's proof of this step uses, and they are also the hypotheses under which the sibling module StacksFrontier.AlgebraicGeometry.Perfect.RelativelyPerfectJacobsonSpecialization proves the specialization step.

public theorem exists_finset_affineOpens_mvPolynomial_surjective_chartHom_of_universallyClosed
    [LocallyOfFiniteType f] [UniversallyClosed f] :
    ∃ s : Finset X.affineOpens, (⨆ V ∈ s, (V : X.Opens)) = ⊤ ∧
      ∀ V ∈ s, ∃ (d : ℕ) (ψ : MvPolynomial (Fin d) R →+* Γ(X, V.1)),
        Function.Surjective ψ ∧ ψ.comp MvPolynomial.C = chartHom f V.1

AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_of_isPerfectRelativeTo_closedFibre_of_genuine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectJacobsonDescent.lean, line 218.

Stacks 0DJZ. Let R be a ring and I an ideal contained in its Jacobson radical; set S = Spec R and S₀ = Spec (R/I). Let f : X ⟶ S be proper, flat and locally of finite presentation and let X₀ = S₀ ×_S X. Let E be a pseudo-coherent object of D(𝒪_X). If the derived restriction E₀ of E to X₀ is S₀-perfect, then E is S-perfect.

Relative perfectness is read at families of certified derived tensor products on the open subspaces of the inverse-image ringed spaces, pinned to the tensor product of sheaves of modules, which is the tensor product of the source's definition.

theorem isPerfectRelativeTo_of_isPerfectRelativeTo_closedFibre_of_genuine [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] (hI : I ≤ (⊥ : Ideal R).jacobson)
    (D : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage (Spec (CommRingCat.of R)).toRingedSpace f.base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{u + 1, u}
        ((RingedSpace.inverseImage (Spec (CommRingCat.of R)).toRingedSpace f.base).restrict
          U.isOpenEmbedding))
    (hD : IsGenuineRelativeTensorFamily f D)
    (D₀ : ∀ U : TopologicalSpace.Opens
        (RingedSpace.inverseImage (Spec (CommRingCat.of (R ⧸ I))).toRingedSpace
          (closedFibreToBase f I).base).carrier,
      RingedSpace.CertifiedDerivedSheafTensoring.{u + 1, u}
        ((RingedSpace.inverseImage (Spec (CommRingCat.of (R ⧸ I))).toRingedSpace
          (closedFibreToBase f I).base).restrict U.isOpenEmbedding))
    (hD₀ : IsGenuineRelativeTensorFamily (closedFibreToBase f I) D₀)
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
    (hE₀ : (closedFibreToBase f I).IsPerfectRelativeTo D₀
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (closedFibreToTotal f I).toLRSHom.toShHom).obj E)) :
    f.IsPerfectRelativeTo D E

AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_canonical_of_closedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectJacobsonDescent.lean, line 249.

Stacks 0DJZ at the canonical derived tensor products. Let R be a ring and I an ideal contained in its Jacobson radical; set S = Spec R and S₀ = Spec (R/I). Let f : X ⟶ S be proper, flat and locally of finite presentation and let X₀ = S₀ ×_S X. Let E be a pseudo-coherent object of D(𝒪_X). If the derived restriction E₀ of E to X₀ is S₀-perfect, then E is S-perfect, relative perfectness being read at the canonical derived tensor products on both sides.

theorem isPerfectRelativeTo_canonical_of_closedFibre [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] (hI : I ≤ (⊥ : Ideal R).jacobson)
    (E : DerivedCategory (OXMod.{u, u} X.toRingedSpace))
    (hE : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) E)
    (hE₀ : (closedFibreToBase f I).IsPerfectRelativeTo
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage (Spec (CommRingCat.of (R ⧸ I))).toRingedSpace
          (closedFibreToBase f I).base))
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
        (closedFibreToTotal f I).toLRSHom.toShHom).obj E)) :
    f.IsPerfectRelativeTo
      (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily
        (RingedSpace.inverseImage (Spec (CommRingCat.of R)).toRingedSpace f.base)) E

AlgebraicGeometry.exists_specializes_mem_range_pullback_snd_quotientMk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/RelativelyPerfectJacobsonSpecialization.lean, line 111. The attribute's comment: “the specialization step of the proof: universal closedness of f and I inside the Jacobson radical force every point of X to specialize to a point of X₀ = Spec (R/I) ×_{Spec R} X”.

Stacks 0DJZ, the specialization step. Let I be an ideal of R contained in the Jacobson radical, let f : X ⟶ Spec R be universally closed and let X₀ = Spec (R/I) ×_{Spec R} X. Then every point of X specializes to a point lying in the image of X₀ ⟶ X.

public theorem exists_specializes_mem_range_pullback_snd_quotientMk
    {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    [UniversallyClosed f] {I : Ideal R} (hI : I ≤ (⊥ : Ideal R).jacobson) (x : X) :
    ∃ x₀ : X, x ⤳ x₀ ∧ x₀ ∈
      Set.range (pullback.snd (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) f).base

Sources

LeanStacks.Thickenings.isPseudoCoherent_of_derivedPullback · Stacks.Thickenings.isQuasicoherent_homology_of_isPseudoCoherent_derivedPullback_specMap · Stacks.Thickenings.isPseudoCoherent_of_isPullback_of_isFiniteOrderThickening · Stacks.Thickenings.isRelativelyPerfect_of_isPullback_of_isFiniteOrderThickening · AlgebraicGeometry.Scheme.Hom.exists_finset_affineOpens_mvPolynomial_surjective_chartHom_of_universallyClosed · AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_of_isPerfectRelativeTo_closedFibre_of_genuine · AlgebraicGeometry.Scheme.Hom.isPerfectRelativeTo_canonical_of_closedFibre · AlgebraicGeometry.exists_specializes_mem_range_pullback_snd_quotientMk

Section37.72 Contracting rational curves #

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

Tag 0E7F, a lemma

Tag 0E7F in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_firstCohomologyStructureSheaf_fiber_of_isZero_firstDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreFirstCohomology.lean, line 371. The attribute's comment: “part (1)”. References: EGA III (7.9.10.1), “partial”.

[Stacks, Tag 0E7F], part (1). Let f : X ⟶ Y be proper and let y ∈ Y be a point whose fibre has dimension at most one. If R¹ f_* 𝒪_X = 0, then H¹(X_y, 𝒪_{X_y}) = 0.

[Stacks, Tag 0E7D] part (2) shrinks Y to an affine open V ∋ y above which the higher direct images of quasi-coherent modules vanish in degrees above one, and isZero_firstCohomologyStructureSheaf_fiber_of_vanishing_restrict concludes over V.

theorem isZero_firstCohomologyStructureSheaf_fiber_of_isZero_firstDirectImage
    (f : X ⟶ Y) [IsProper f] (y : Y)
    (hdim : topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hR : IsZero (firstDirectImageStructureSheaf f)) :
    IsZero (firstCohomologyStructureSheaf (f.fiber y))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_firstCohomologyStructureSheaf_fiber_of_isZero_firstDirectImage_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreFirstCohomology.lean, line 391. The attribute's comment: “part (2)”. References: EGA III (7.9.10.1), “partial”.

[Stacks, Tag 0E7F], part (2). Let f : X ⟶ Y be proper and let y ∈ Y be a point whose fibre has dimension at most one. If there is a morphism g : Y' ⟶ Y with y in its image such that the base change f' : X ×_Y Y' ⟶ Y' of f by g has R¹ f'_* 𝒪_{X'} = 0, then H¹(X_y, 𝒪_{X_y}) = 0.

[Stacks, Tag 0E7D] part (2) shrinks Y to an affine open V ∋ y above which the higher direct images of quasi-coherent modules vanish in degrees above one, and isZero_firstCohomologyStructureSheaf_fiber_of_vanishing_restrict_baseChange concludes over V.

theorem isZero_firstCohomologyStructureSheaf_fiber_of_isZero_firstDirectImage_baseChange
    (f : X ⟶ Y) [IsProper f] (y : Y)
    (hdim : topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    {Y' : Scheme.{u}} (g : Y' ⟶ Y) (hy : y ∈ Set.range g)
    (hR : IsZero (firstDirectImageStructureSheaf (pullback.snd f g))) :
    IsZero (firstCohomologyStructureSheaf (f.fiber y))

Tag 0E7G, a lemma

Tag 0E7G in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_isZero_restrict_firstDirectImage_of_isZero_cohomologyOne_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/ContractingRationalCurves.lean, line 215. The attribute's comment: “the clauses of Tags 0EX4 and 0EX3 (b) are the hypotheses hft, hbc”.

[Stacks, Tag 0E7G]. Let f : X ⟶ Y be proper and let y ∈ Y be a point whose fibre has dimension at most one and satisfies H¹(X_y, 𝒪_{X_y}) = 0. Then there is an open V ∋ y with R¹ f_* 𝒪_X|_V = 0, and R¹ f'_* 𝒪_{X'} = 0 for the base change along every g : Y' ⟶ V.

The hypothesis on the fibre makes R¹ (f_y)_* 𝒪_{X_y} vanish over the affine base Spec κ(y), hence by hbc the pullback of R¹ f_* 𝒪_X along Spec κ(y) ⟶ Y; so y misses the support of R¹ f_* 𝒪_X by [Stacks, Tag 056J]. The support is closed because of the finite-type clause hft, which gives the neighbourhood V. Universality after base change is hbc again, applied to g ≫ V.ι and read through the compatibility of pullback with composition.

theorem exists_isOpen_isZero_restrict_firstDirectImage_of_isZero_cohomologyOne_fiber
    (f : X ⟶ Y) [IsProper f] (y : Y)
    (_hdim : topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hft : (firstDirectImageStructureSheaf f).IsFiniteType)
    (hbc : FirstDirectImageCommutesBaseChange f)
    (hH : IsZero (firstCohomologyStructureSheaf (f.fiber y))) :
    ∃ V : Y.Opens, y ∈ V ∧
      IsZero ((Scheme.Modules.restrictFunctor V.ι).obj (firstDirectImageStructureSheaf f)) ∧
      ∀ (Y' : Scheme.{u}) (g : Y' ⟶ V.toScheme),
        IsZero (firstDirectImageStructureSheaf (pullback.snd f (g ≫ V.ι)))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_isZero_restrict_firstDirectImage_of_isPullback_of_isZero_cohomologyOne_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/VanishingNeighbourhood.lean, line 195.

[Stacks, Tag 0E7G]. Let f : X ⟶ Y be proper and let y ∈ Y be a point with dim(X_y) ≤ 1 and H¹(X_y, 𝒪_{X_y}) = 0. Then there is an open neighbourhood V of y such that R¹ f_* 𝒪_X|_V = 0, and the same holds after base change by any Y' ⟶ V: for every cartesian square X' ⟶ X, f' : X' ⟶ Y', g : Y' ⟶ Y over f with g(Y') ⊆ V, R¹ f'_* 𝒪_{X'} = 0.

The source's proof: shrink to an open W ∋ y over which all fibres have dimension at most one ([Stacks, Tag 02FZ]); there R¹ f_* 𝒪_X is of finite type ([Stacks, Tag 0EX4], firstDirectImageFiniteTypeOfFibreDimensionOne) and its pullback to Spec κ(y) is R¹ of the fibre, which vanishes; so y is outside the closed support ([Stacks, Tag 056J]), and V is the complement of the support in W (exists_isOpen_firstDirectImage_vanishes_of_factor). For a base change along g into V, the pullback of R¹ f_* 𝒪_X along g factors through its restriction to V, which is zero, and over W this pullback is R¹ f'_* 𝒪_{X'} (isZero_pullback_firstDirectImage_iff_of_factor_of_isPullback, the vanishing form of [Stacks, Tag 0EX3]).

theorem exists_isOpen_isZero_restrict_firstDirectImage_of_isPullback_of_isZero_cohomologyOne_fiber
    (f : X ⟶ Y) [IsProper f] (y : Y)
    (hdim : topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hH : IsZero (firstCohomologyStructureSheaf (f.fiber y))) :
    ∃ V : Y.Opens, y ∈ V ∧
      IsZero ((Scheme.Modules.restrictFunctor V.ι).obj (firstDirectImageStructureSheaf f)) ∧
      ∀ ⦃X' Y' : Scheme.{u}⦄ {g' : X' ⟶ X} {f' : X' ⟶ Y'} {g : Y' ⟶ Y},
        IsPullback g' f' f g → Set.range g ⊆ V → IsZero (firstDirectImageStructureSheaf f')

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_firstDirectImage_vanishes_universally, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/VanishingNeighbourhood.lean, line 239.

[Stacks, Tag 0E7G]. Let f : X ⟶ Y be proper and let y ∈ Y be a point with dim(X_y) ≤ 1 and H¹(X_y, 𝒪_{X_y}) = 0. Then there is an open neighbourhood V of y such that R¹ f_* 𝒪_X|_V = 0, and R¹ f'_* 𝒪_{X'} = 0 for the base change f' of f along every Y' ⟶ V.

The source's proof: shrink to an open W ∋ y over which all fibres have dimension at most one ([Stacks, Tag 02FZ]); there R¹ f_* 𝒪_X is of finite type ([Stacks, Tag 0EX4]) and its pullback to Spec κ(y) is R¹ of the fibre, which vanishes; so y is outside the closed support ([Stacks, Tag 056J]). This is exists_isOpen_isZero_restrict_firstDirectImage_of_isPullback_of_isZero_cohomologyOne_fiber read on the cartesian square of the chosen pullback along g ≫ V.ι.

theorem exists_isOpen_firstDirectImage_vanishes_universally (f : X ⟶ Y) [IsProper f] (y : Y)
    (hdim : topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hH : IsZero (firstCohomologyStructureSheaf (f.fiber y))) :
    ∃ V : Y.Opens, y ∈ V ∧
      IsZero ((Scheme.Modules.restrictFunctor V.ι).obj (firstDirectImageStructureSheaf f)) ∧
      ∀ (Y' : Scheme.{u}) (g : Y' ⟶ V.toScheme),
        IsZero (firstDirectImageStructureSheaf (pullback.snd f (g ≫ V.ι)))

Tag 0E7H, a lemma

Tag 0E7H in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_higherDirectImage_of_one_lt_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionOneCohomologyVanishing.lean, line 102. The attribute's comment: “clause (1)”.

[Stacks, Tag 0E7H] clause (1). For a proper morphism f : X ⟶ Y all of whose fibres have dimension at most one and a quasi-coherent ℱ on X, Rᵖ f_* ℱ = 0 for every p > 1.

This is [Stacks, Tag 0E7D] at d = 1. The tag's hypothesis H¹(X_y, 𝒪_{X_y}) = 0 is not used for this clause and is not imposed.

theorem isZero_higherDirectImage_of_one_lt_of_isProper {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsProper f] (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (F : X.Modules) [F.IsQuasicoherent] (p : ℤ) (hp : 1 < p) :
    IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F)

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_cohomology_of_notMem_zero_one_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionOneCohomologyVanishing.lean, line 116. The attribute's comment: “clause (3)”.

[Stacks, Tag 0E7H] clause (3). For a proper morphism f : X ⟶ Y onto an affine scheme all of whose fibres have dimension at most one and a quasi-coherent ℱ on X, Hᵖ(X, ℱ) = 0 for every p ∉ {0, 1}.

Negative degrees vanish for formal reasons, and degrees above one by [Stacks, Tag 0E7D] over an affine base. The tag's hypothesis H¹(X_y, 𝒪_{X_y}) = 0 is not used for this clause and is not imposed.

theorem isZero_cohomology_of_notMem_zero_one_of_isAffine {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsProper f] [IsAffine Y]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (F : X.Modules) [F.IsQuasicoherent] (p : ℤ) (hp : p ∉ ({0, 1} : Set ℤ)) :
    IsZero (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerivedPlus p).obj F)

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_cohomology_one_of_generatingSections_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionOneCohomologyVanishing.lean, line 196. The attribute's comment: “clause (4)”.

[Stacks, Tag 0E7H] clause (4). Let f : X ⟶ Y be a proper morphism onto an affine scheme such that dim(X_y) ≤ 1 and H¹(X_y, 𝒪_{X_y}) = 0 for every y ∈ Y, and let ℱ be a quasi-coherent 𝒪_X-module which is globally generated. Then H¹(X, ℱ) = 0.

R¹ f_* 𝒪_X is of finite type by [Stacks, Tag 0EX4] at d = 1 (firstDirectImageFiniteTypeOfFibreDimensionOne), and the rest is isZero_cohomology_one_of_generatingSections_of_isFiniteType.

theorem isZero_cohomology_one_of_generatingSections_of_isAffine {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsProper f] [IsAffine Y]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hfib : ∀ y : Y, IsZero (firstCohomologyStructureSheaf (f.fiber y)))
    (F : X.Modules) [F.IsQuasicoherent] (σ : SheafOfModules.GeneratingSections F) :
    IsZero (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerivedPlus 1).obj F)

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_higherDirectImage_one_of_epi_pullback_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/FibreDimensionOneCohomologyVanishing.lean, line 210. The attribute's comment: “clause (2)”.

[Stacks, Tag 0E7H] clause (2). Let f : X ⟶ Y be a proper morphism such that dim(X_y) ≤ 1 and H¹(X_y, 𝒪_{X_y}) = 0 for every y ∈ Y, let ℱ be a quasi-coherent 𝒪_X-module, and suppose there is a surjection f^*𝒢 ⟶ ℱ with 𝒢 quasi-coherent on Y. Then R¹ f_* ℱ = 0.

theorem isZero_higherDirectImage_one_of_epi_pullback_of_isProper {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsProper f]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hfib : ∀ y : Y, IsZero (firstCohomologyStructureSheaf (f.fiber y)))
    (F : X.Modules) [F.IsQuasicoherent] (G : Y.Modules) [G.IsQuasicoherent]
    (p : (Scheme.Modules.pullback f).obj G ⟶ F) (hp : Epi p) :
    IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus 1).obj F)

Tag 0E7I, a lemma

Tag 0E7I in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.epi_unitToPushforwardUnit_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/SurjectivityAfterBaseChange.lean, line 816.

[Stacks, Tag 0E7I]. Let f : X ⟶ Y be a proper morphism of schemes such that dim(X_y) ≤ 1 and H¹(X_y, 𝒪_{X_y}) = 0 for every y ∈ Y, and suppose 𝒪_Y ⟶ f_* 𝒪_X is surjective. Then 𝒪_{Y'} ⟶ f'_* 𝒪_{X'} is surjective for every base change f' of f.

Surjectivity is local on the base, and around each point of Y' there is an affine open mapping into an affine open of Y; over such a pair the restricted base change is a base change of f ∣_ W along a morphism of affine schemes, which factors as a closed immersion followed by a flat morphism through the spectrum of a polynomial algebra. The flat half is surjective_appTop_of_flat_base, and the closed-immersion half is surjective_appTop_of_closedImmersion_base, where clause (4) of [Stacks, Tag 0E7H] is applied to the ideal sheaf of the closed immersion.

Mathlib's IsProper is separated, universally closed and locally of finite type; universal closedness gives quasi-compactness, so this is Stacks' notion of proper.

theorem epi_unitToPushforwardUnit_of_baseChange
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hfib : ∀ y : Y, IsZero (firstCohomologyStructureSheaf (f.fiber y)))
    (hsurj : Epi (Scheme.Modules.unitToPushforwardUnit f))
    {Y' : Scheme.{u}} (g : Y' ⟶ Y) :
    Epi (Scheme.Modules.unitToPushforwardUnit (pullback.snd f g))

Tag 0E7J, a lemma

Tag 0E7J in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_flat_fibreDimension_vanishing_epi_near_specialFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/SpecialFibreNeighbourhood.lean, line 334.

[Stacks, Tag 0E7J]. Let X --f--> Y --q--> S be morphisms of schemes and let s ∈ S. Write f_s : X_s ⟶ Y_s for the induced morphism of fibres over s (in the two spellings Stacks.Flatness.fiberHom f q s and pullback.snd f (q.fiberι s) of X_s = X ×_Y Y_s). Assume

X ⟶ S is locally of finite presentation and flat at the points of X_s,

f is proper,

the fibres of f_s have dimension at most one and R¹ f_{s,*} 𝒪_{X_s} = 0,

𝒪_{Y_s} ⟶ f_{s,*} 𝒪_{X_s} is surjective.

Then there is an open Y_s ⊆ V ⊆ Y such that (a) f⁻¹(V) is flat over S, (b) dim(X_y) ≤ 1 for y ∈ V, (c) R¹ f_* 𝒪_X|_V = 0, (d) 𝒪_V ⟶ f_* 𝒪_X|_V is surjective, and (b), (c) and (d) remain true after base change of f⁻¹(V) ⟶ V by any Y' ⟶ V.

(a) and (b) are exists_isOpen_flat_and_fibreDimension_le_one; (c) and its persistence are [Stacks, Tag 0E7G] along Y_s (exists_isOpen_firstDirectImage_vanishes_of_factor); (d) is exists_isOpen_notMem_supp_cokernel_unit at every point of Y_s, and its persistence is [Stacks, Tag 0E7I] (epi_unitToPushforwardUnit_of_baseChange), whose hypotheses on the fibres follow from the persistence of (b) and (c).

theorem exists_isOpen_flat_fibreDimension_vanishing_epi_near_specialFibre (f : X ⟶ Y)
    (q : Y ⟶ S) (s : S) [LocallyOfFinitePresentation (f ≫ q)] [IsProper f]
    (hflat : ∀ x : X, (f ≫ q) x = s → IsFlatAt (f ≫ q).toLRSHom.toShHom x)
    (hdim : ∀ y : q.fiber s,
      topologicalKrullDim ((Stacks.Flatness.fiberHom f q s).fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hR : IsZero (firstDirectImageStructureSheaf (pullback.snd f (q.fiberι s))))
    (hsurj : Epi (Scheme.Modules.unitToPushforwardUnit (pullback.snd f (q.fiberι s)))) :
    ∃ V : Y.Opens, (∀ y : Y, q y = s → y ∈ V) ∧
      Flat ((f ⁻¹ᵁ V).ι ≫ (f ≫ q)) ∧
      (∀ y : Y, y ∈ V → topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞)) ∧
      IsZero ((Scheme.Modules.restrictFunctor V.ι).obj (firstDirectImageStructureSheaf f)) ∧
      Epi ((Scheme.Modules.restrictFunctor V.ι).map (Scheme.Modules.unitToPushforwardUnit f)) ∧
      ∀ (Y' : Scheme.{u}) (g : Y' ⟶ V.toScheme),
        (∀ y' : Y', topologicalKrullDim ((pullback.snd (f ∣_ V) g).fiber y') ≤
          ((1 : ℕ) : WithBot ℕ∞)) ∧
        IsZero (firstDirectImageStructureSheaf (pullback.snd (f ∣_ V) g)) ∧
        Epi (Scheme.Modules.unitToPushforwardUnit (pullback.snd (f ∣_ V) g))

Tag 0E7K, a lemma

Tag 0E7K in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isIso_directImageStructureSheafBaseChangeMap_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/DirectImageStructureSheafCommutesBaseChange.lean, line 129. The attribute's comment: “clause (b): formation of f_* 𝒪_X commutes with arbitrary base change S' ⟶ S”.

[Stacks, Tag 0E7K], clause (b). Let X ⟶ Y ⟶ S be a commutative triangle of schemes with X ⟶ S flat, let f : X ⟶ Y be proper with dim(X_y) ≤ 1 for every y ∈ Y, and suppose R¹ f_* 𝒪_X = 0. Then formation of f_* 𝒪_X commutes with arbitrary base change S' ⟶ S: for Y' = Y ×_S S' and X' = X ×_Y Y', the canonical comparison (Y' ⟶ Y)^* f_* 𝒪_X ⟶ f'_* 𝒪_{X'} is an isomorphism.

theorem isIso_directImageStructureSheafBaseChangeMap_of_flat {X Y S : Scheme.{u}} (f : X ⟶ Y)
    (q : Y ⟶ S) [Flat (f ≫ q)] [IsProper f]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hR : IsZero (firstDirectImageStructureSheaf f)) {S' : Scheme.{u}} (h : S' ⟶ S) :
    IsIso (directImageStructureSheafBaseChangeMap f (pullback.fst q h))

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isFlatOver_directImageStructureSheaf_of_fibreDimension_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/DirectImageStructureSheafCommutesBaseChange.lean, line 142. The attribute's comment: “clause (a): f_* 𝒪_X is flat over S”.

[Stacks, Tag 0E7K], clause (a). Let X ⟶ Y ⟶ S be a commutative triangle of schemes with X ⟶ S flat, let f : X ⟶ Y be proper with dim(X_y) ≤ 1 for every y ∈ Y, and suppose R¹ f_* 𝒪_X = 0. Then f_* 𝒪_X is flat over S.

theorem isFlatOver_directImageStructureSheaf_of_fibreDimension_le_one {X Y S : Scheme.{u}}
    (f : X ⟶ Y) (q : Y ⟶ S) [Flat (f ≫ q)] [IsProper f]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hR : IsZero (firstDirectImageStructureSheaf f)) :
    IsFlatOver q.toLRSHom.toShHom (directImageStructureSheaf f)

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isFlatOver_directImageStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/DirectImageStructureSheafFlat.lean, line 107. The attribute's comment: “clause (a): flatness of f_* 𝒪_X over the base”.

Let X ⟶ Y ⟶ S be a commutative triangle of schemes with X ⟶ S flat, let f : X ⟶ Y be proper with dim(X_y) ≤ 1 for every y ∈ Y, and suppose R¹ f_* 𝒪_X = 0. Then f_* 𝒪_X is flat over S.

theorem isFlatOver_directImageStructureSheaf (hcoh : CohomologyVanishesAboveOne.{u})
    {X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S) [Flat (f ≫ q)] [IsProper f]
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞))
    (hR : IsZero (firstDirectImageStructureSheaf f)) :
    IsFlatOver q.toLRSHom.toShHom (directImageStructureSheaf f)

Tag 0E7L, a lemma

Tag 0E7L in the Stacks Project.

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_isIso_unitToPushforwardUnit_of_specialFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeBaseChange/StructureSheafIsoNearSpecialFibreReduction.lean, line 442.

[Stacks, Tag 0E7L]. Let X --f--> Y --q--> S be a commutative triangle of schemes and s ∈ S. Assume 1. X ⟶ S is locally of finite presentation and flat at the points of X_s, 2. Y ⟶ S is locally of finite presentation, 3. f is proper, 4. the fibres of f_s : X_s ⟶ Y_s have dimension ≤ 1 and R¹f_{s,*}𝒪_{X_s} = 0, 5. 𝒪_{Y_s} ⟶ f_{s,*}𝒪_{X_s} is an isomorphism.

Then there is an open Y_s ⊂ V ⊂ Y such that (a) V is flat over S, (b) f⁻¹(V) is flat over S, (c) dim(X_y) ≤ 1 for y ∈ V, (d) R¹f_*𝒪_X|_V = 0, (e) 𝒪_V ⟶ f_*𝒪_X|_V is an isomorphism, and (a) – (e) remain true after base change of f⁻¹(V) ⟶ V by any S' ⟶ S (for the base change X' ⟶ V' of f⁻¹(V) ⟶ V, the open of (a) – (e) being all of V').

In the hypotheses, f_s is the base change of f along Y_s ⟶ Y for (4) on R¹ and for (5), and (f ≫ q).fiber s ⟶ q.fiber s for the dimension bound of (4); these are the same morphism up to the canonical isomorphism X ×_Y Y_s ≅ X_s.

The proof is the source's. Near each y ∈ Y_s one restricts to affine opens of Y and S over which X is flat; the situation is the base change of a Noetherian model (exists_noetherianModel, [Stacks, Tags 01ZM, 081F, 04AI]), the special-fibre hypotheses descend to the image point of the model base along a faithfully flat field extension, and over the Noetherian model the stalk maps of 𝒪_Y ⟶ f_*𝒪_X are bijective near the special fibre (surjective by coherence of the cokernel, [Stacks, Tag 02O5], and Nakayama; injective by the local flatness criterion, [Stacks, Tag 00ME]); this is carried back by [Stacks, Tag 0E7K] (b). Conclusions (a) and (e) and the persistence then follow from [Stacks, Tag 0E7K] on V (conclusions_of_isOpen).

theorem exists_isOpen_isIso_unitToPushforwardUnit_of_specialFibre (f : X ⟶ Y) (q : Y ⟶ S) (s : S)
    [LocallyOfFinitePresentation (f ≫ q)]
    [LocallyOfFinitePresentation q] [IsProper f]
    (hflat : ∀ x : X, (f ≫ q) x = s → IsFlatAt (f ≫ q).toLRSHom.toShHom x)
    (hdim : ∀ y : q.fiber s, topologicalKrullDim ((Stacks.Flatness.fiberHom f q s).fiber y) ≤
      ((1 : ℕ) : WithBot ℕ∞))
    (hR : IsZero (firstDirectImageStructureSheaf (pullback.snd f (q.fiberι s))))
    (hiso : IsIso (Scheme.Modules.unitToPushforwardUnit (pullback.snd f (q.fiberι s)))) :
    ∃ V : Y.Opens, (∀ y : Y, q y = s → y ∈ V) ∧
      Flat (V.ι ≫ q) ∧
      Flat ((f ⁻¹ᵁ V).ι ≫ (f ≫ q)) ∧
      (∀ y : Y, y ∈ V → topologicalKrullDim (f.fiber y) ≤ ((1 : ℕ) : WithBot ℕ∞)) ∧
      IsZero ((Scheme.Modules.restrictFunctor V.ι).obj (firstDirectImageStructureSheaf f)) ∧
      IsIso ((Scheme.Modules.restrictFunctor V.ι).map (Scheme.Modules.unitToPushforwardUnit f)) ∧
      ∀ ⦃S' : Scheme.{u}⦄ (h : S' ⟶ S),
        Flat (pullback.snd (V.ι ≫ q) h) ∧
        Flat (pullback.snd (f ∣_ V) (pullback.fst (V.ι ≫ q) h) ≫ pullback.snd (V.ι ≫ q) h) ∧
        (∀ y' : (pullback (V.ι ≫ q) h : Scheme.{u}), topologicalKrullDim
          ((pullback.snd (f ∣_ V) (pullback.fst (V.ι ≫ q) h)).fiber y') ≤
            ((1 : ℕ) : WithBot ℕ∞)) ∧
        IsZero (firstDirectImageStructureSheaf
          (pullback.snd (f ∣_ V) (pullback.fst (V.ι ≫ q) h))) ∧
        IsIso (Scheme.Modules.unitToPushforwardUnit
          (pullback.snd (f ∣_ V) (pullback.fst (V.ι ≫ q) h)))

Tag 0E24, a lemma

Tag 0E24 in the Stacks Project.

Stacks.PicardFibreTrivial.pullback_injective_and_exists_pullback_iso_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardFibreTrivial/Basic.lean, line 203.

Stacks Project, Tag 0E24. Let f : X ⟶ Y be a proper morphism onto a Noetherian scheme such that f_* 𝒪_X = 𝒪_Y, such that the fibres of f have dimension at most one, and such that H¹(X_y, 𝒪_{X_y}) = 0 for every y ∈ Y. Then f^* : Pic(Y) ⟶ Pic(X) is a bijection onto the subgroup of classes of invertible 𝒪_X-modules ℒ with ℒ|_{X_y} ≅ 𝒪_{X_y} for all y ∈ Y: on isomorphism classes of invertible modules f^* is injective, and an invertible ℒ is isomorphic to a pullback f^* 𝒩 of an invertible 𝒪_Y-module exactly when it is trivial on every fibre.

The source also asks for X to be Noetherian; that follows from the other hypotheses (f is proper over a Noetherian base) and is not needed.

theorem pullback_injective_and_exists_pullback_iso_iff (f : X ⟶ Y) [IsProper f] [IsNoetherian Y]
    (hO : IsIso (SheafOfModules.unitToPushforwardObjUnit f.toRingCatSheafHom))
    (hdim : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ 1)
    (hH1 : ∀ y : Y, IsZero (cohomologyOverField (Y.residueField y) (f.fiberToSpecResidueField y)
      (SheafOfModules.unit (f.fiber y).ringCatSheaf) 1)) :
    (∀ M N : Y.Modules,
      Stacks.SheafOfModules.IsInvertible Y.presheaf
        (structureSheafRing Y.toRingedSpace).property M →
      Stacks.SheafOfModules.IsInvertible Y.presheaf
        (structureSheafRing Y.toRingedSpace).property N →
      Nonempty ((Scheme.Modules.pullback f).obj M ≅ (Scheme.Modules.pullback f).obj N) →
      Nonempty (M ≅ N)) ∧
    ∀ L : X.Modules,
      Stacks.SheafOfModules.IsInvertible X.presheaf
        (structureSheafRing X.toRingedSpace).property L →
      ((∃ M : Y.Modules,
          Stacks.SheafOfModules.IsInvertible Y.presheaf
            (structureSheafRing Y.toRingedSpace).property M ∧
          Nonempty ((Scheme.Modules.pullback f).obj M ≅ L)) ↔
        ∀ y : Y, Nonempty ((Scheme.Modules.pullback (f.fiberι y)).obj L ≅
          SheafOfModules.unit (f.fiber y).ringCatSheaf))

Sources

LeanStacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_firstCohomologyStructureSheaf_fiber_of_isZero_firstDirectImage ·

Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_firstCohomologyStructureSheaf_fiber_of_isZero_firstDirectImage_baseChange

·

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_isZero_restrict_firstDirectImage_of_isZero_cohomologyOne_fiber

·

Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_isZero_restrict_firstDirectImage_of_isPullback_of_isZero_cohomologyOne_fiber

· Stacks.AlgebraicGeometry.TopDegreeBaseChange.exists_isOpen_firstDirectImage_vanishes_universally · Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_higherDirectImage_of_one_lt_of_isProper · Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_cohomology_of_notMem_zero_one_of_isAffine · Stacks.AlgebraicGeometry.TopDegreeBaseChange.isZero_cohomology_one_of_generatingSections_of_isAffine

Section37.73 Affine stratifications #

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

Tag 0F2S, a definition

Tag 0F2S in the Stacks Project.

AlgebraicGeometry.AffineStratification, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/Defs.lean, line 52.

A locally finite stratification of X with affine reduced induced strata and affine inclusions into X.

structure AffineStratification (X : Scheme.{u}) (I : Type v) [PartialOrder I]

Tag 0F2T, a lemma

Tag 0F2T in the Stacks Project.

AlgebraicGeometry.exists_affineStratification_fin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/Reindex.lean, line 457.

A finite affine stratification can be reindexed by the interval from zero to the length of its indexing poset.

theorem exists_affineStratification_fin {X : Scheme.{u}}
    {I : Type v} [PartialOrder I] [Finite I]
    (s : AffineStratification X I) (n : ℕ)
    (hn : (Order.krullDim I = n) ∨ (IsEmpty I ∧ n = 0)) :
    Nonempty (AffineStratification X (Fin (n + 1)))

Tag 0F2U, a lemma

Tag 0F2U in the Stacks Project.

AlgebraicGeometry.hasFiniteAffineStratification_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/FiniteExistence.lean, line 92.

A scheme has an affine stratification indexed by a finite poset if and only if it is quasi-compact and quasi-separated.

theorem hasFiniteAffineStratification_iff (X : Scheme.{u}) :
    HasFiniteAffineStratification.{u, v} X ↔ (CompactSpace X ∧ QuasiSeparatedSpace X)

Tag 0F2V, a definition

Tag 0F2V in the Stacks Project.

AlgebraicGeometry.affineStratificationNumber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/Defs.lean, line 69.

The least n admitting an affine stratification of X with strata indexed by 0, …, n.

noncomputable def affineStratificationNumber (X : Scheme.{u}) : ℕ

Tag 0F2W, a lemma

Tag 0F2W in the Stacks Project.

AlgebraicGeometry.affineStratificationNumber_le_of_isOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/CoverBound.lean, line 148.

[Stacks, Tag 0F2W]. A separated scheme with an open covering by n + 1 affine opens has affine stratification number at most n.

theorem affineStratificationNumber_le_of_isOpenCover (X : Scheme.{u}) [X.IsSeparated] {n : ℕ}
    (U : Fin (n + 1) → X.Opens) (hU : IsOpenCover U) (hUaff : ∀ i, IsAffineOpen (U i)) :
    affineStratificationNumber X ≤ n

Tag 0F2X, a lemma

Tag 0F2X in the Stacks Project.

AlgebraicGeometry.affineStratificationNumber_le_of_topologicalKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/DimensionBound.lean, line 298.

[Stacks, Tag 0F2X]. A Noetherian scheme of finite dimension d has affine stratification number at most d.

theorem affineStratificationNumber_le_of_topologicalKrullDim (X : Scheme.{u}) [IsNoetherian X]
    (d : ℕ) (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) :
    affineStratificationNumber X ≤ d

AlgebraicGeometry.nonempty_affineStratification_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/DimensionStratification.lean, line 44. The attribute's comment: “an affine stratification indexed by 0, …, d exists”.

A Noetherian scheme of dimension at most d has an affine stratification indexed by 0, …, d; that is, its affine stratification number is at most d in the sense of [Stacks, Tag 0F2V].

theorem nonempty_affineStratification_of_topologicalKrullDim_le (X : Scheme.{u})
    [IsNoetherian X] (d : ℕ) (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) :
    Nonempty (AffineStratification X (Fin (d + 1)))

Tag 0F2Y, a proposition

Tag 0F2Y in the Stacks Project.

AlgebraicGeometry.isZero_cohomology_of_affineStratificationNumber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/CohomologyVanishingProof.lean, line 251.

[Stacks, Tag 0F2Y]. Let X be a nonempty quasi-compact quasi-separated scheme with affine stratification number n. Then Hᵖ(X, F) = 0 for every p > n and every quasi-coherent 𝒪_X-module F.

theorem isZero_cohomology_of_affineStratificationNumber (X : Scheme.{u}) [Nonempty X]
    [CompactSpace X] [QuasiSeparatedSpace X] (F : X.Modules) [F.IsQuasicoherent] (p : ℕ)
    (hp : affineStratificationNumber X < p) :
    IsZero (Hgroup X.ringCatSheaf ⊤ p F)

Tag 0F2Z, an example

Tag 0F2Z in the Stacks Project.

AlgebraicGeometry.affineStratificationNumber_proj_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/ProjectiveSpace.lean, line 85. The attribute's comment: “the upper bound”.

[Stacks, Tag 0F2Z], the upper bound. The affine stratification number of ℙⁿ_k is at most n: projective space is separated and the n + 1 standard coordinate charts are an affine open covering.

theorem affineStratificationNumber_proj_le (k : Type u) [Field k] (n : ℕ) :
    affineStratificationNumber (Proj (polyGrading k n)) ≤ n

AlgebraicGeometry.le_affineStratificationNumber_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/ProjectiveSpace.lean, line 154. The attribute's comment: “the lower bound”.

[Stacks, Tag 0F2Z], the lower bound. The affine stratification number of ℙⁿ_k is at least n: Hⁿ(ℙⁿ_k, 𝒪(-n-1)) is nonzero, while [Stacks, Tag 0F2Y] makes the cohomology of a quasi-coherent module vanish above the affine stratification number.

theorem le_affineStratificationNumber_proj (k : Type u) [Field k] (n : ℕ) :
    n ≤ affineStratificationNumber (Proj (polyGrading k n))

AlgebraicGeometry.affineStratificationNumber_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/ProjectiveSpace.lean, line 168. The attribute's comment: “the equality”.

[Stacks, Tag 0F2Z]. The affine stratification number of n-dimensional projective space over a field is exactly n.

theorem affineStratificationNumber_proj (k : Type u) [Field k] (n : ℕ) :
    affineStratificationNumber (Proj (polyGrading k n)) = n

Sources

LeanAlgebraicGeometry.AffineStratification · AlgebraicGeometry.exists_affineStratification_fin · AlgebraicGeometry.hasFiniteAffineStratification_iff · AlgebraicGeometry.affineStratificationNumber · AlgebraicGeometry.affineStratificationNumber_le_of_isOpenCover · AlgebraicGeometry.affineStratificationNumber_le_of_topologicalKrullDim · AlgebraicGeometry.nonempty_affineStratification_of_topologicalKrullDim_le · AlgebraicGeometry.isZero_cohomology_of_affineStratificationNumber

Section37.74 Universally open morphisms #

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

Tag 0F31, a lemma

Tag 0F31 in the Stacks Project.

AlgebraicGeometry.universallyOpen_iff_forall_isOpenMap_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyOpen/Criteria.lean, line 314. The attribute's comment: “parts (1) and (2)”.

A morphism of schemes is universally open if and only if its base change along every morphism locally of finite presentation is an open map.

theorem universallyOpen_iff_forall_isOpenMap_pullback_snd {X S : Scheme.{u}} (f : X ⟶ S) :
    UniversallyOpen f ↔
      ∀ (S' : Scheme.{u}) (g : S' ⟶ S),
        LocallyOfFinitePresentation g → IsOpenMap (pullback.snd f g)

AlgebraicGeometry.universallyOpen_iff_forall_isOpenMap_affineSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyOpen/Criteria.lean, line 325. The attribute's comment: “parts (1) and (3)”.

A morphism of schemes is universally open if and only if the induced morphism of affine n-spaces is an open map for every n.

theorem universallyOpen_iff_forall_isOpenMap_affineSpaceMap {X S : Scheme.{u}} (f : X ⟶ S) :
    UniversallyOpen f ↔
      ∀ n : ℕ, IsOpenMap (AffineSpace.map (ULift.{u} (Fin n)) f)

Tag 0F32, a lemma

Tag 0F32 in the Stacks Project.

AlgebraicGeometry.universallyOpen_of_locallyQuasiFinite_of_dominant_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyOpen/QuasiFiniteDominant.lean, line 417. References: EGA IV (14.4.5), “quasi-finite case”; EGA IV (14.4.2), “quasi-finite, b)=>a)”; EGA IV (14.4.4), “loc. quasi-finite case”; EGA IV (14.5.6), “(d) ⇒ (b)”; EGA IV (14.5.9), “(d) ⇒ (a), special case”; EGA IV (18.10.2), “special case”; SGA 3 VIB (5.6.0), “(i), (ii), special case”.

Stacks Project, Tag 0F32. A locally quasi-finite morphism to a geometrically unibranch, locally Noetherian scheme is universally open as soon as every irreducible component of its source dominates an irreducible component of its target.

theorem universallyOpen_of_locallyQuasiFinite_of_dominant_components
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    [IsLocallyNoetherian Y] (hY : IsGeometricallyUnibranch Y)
    (hcomponents : ∀ C : irreducibleComponents X,
      ∃ D : irreducibleComponents Y, closure (f '' (C : Set X)) = (D : Set Y)) :
    UniversallyOpen f

Tag 0F33, a lemma

Tag 0F33 in the Stacks Project.

AlgebraicGeometry.universallyOpen_iff_isOpen_image_basicOpen_linearCombination, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/UniversallyOpenFinite.lean, line 162.

Universal openness of a finite algebra is detected by the image of the principal open defined by a universal linear combination of module generators.

theorem universallyOpen_iff_isOpen_image_basicOpen_linearCombination
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (d : ℕ) (b : Fin d → B) (hb : Submodule.span A (Set.range b) = ⊤) :
    UniversallyOpen (Spec.map (CommRingCat.ofHom (algebraMap A B))) ↔
      IsOpen (PrimeSpectrum.comap (MvPolynomial.map (σ := Fin d) (algebraMap A B)) ''
        (PrimeSpectrum.basicOpen
          (∑ i : Fin d, MvPolynomial.C (b i) * MvPolynomial.X i) :
            Set (PrimeSpectrum (MvPolynomial (Fin d) B))))

Tag 0F34, a lemma

Tag 0F34 in the Stacks Project.

AlgebraicGeometry.exists_locallyQuasiFinite_universallyOpen_baseChange_of_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/UniversallyOpen.lean, line 829.

Let S be the limit of a cofiltered system of schemes with affine transition morphisms and f₀ : X₀ ⟶ Y₀ a locally finitely presented morphism over a quasi-compact quasi-separated stage S i₀, with X₀, Y₀ quasi-compact and quasi-separated. If the base change of f₀ to the limit is locally of finite type, locally quasi-finite and universally open, then so is its base change to some stage S i.

public theorem exists_locallyQuasiFinite_universallyOpen_baseChange_of_limitBaseChange
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (S : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    (c : Cone S) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (S.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace (S.obj i₀)] [QuasiSeparatedSpace (S.obj i₀)]
    [CompactSpace X₀.left] [QuasiSeparatedSpace X₀.left]
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    [LocallyOfFiniteType ((Over.pullback (c.π.app i₀)).map f₀).left]
    [LocallyQuasiFinite ((Over.pullback (c.π.app i₀)).map f₀).left]
    [UniversallyOpen ((Over.pullback (c.π.app i₀)).map f₀).left] :
    ∃ (i : I) (g : i ⟶ i₀),
      (LocallyOfFiniteType ((Over.pullback (S.map g)).map f₀).left ∧
        LocallyQuasiFinite ((Over.pullback (S.map g)).map f₀).left) ∧
          UniversallyOpen ((Over.pullback (S.map g)).map f₀).left

Tag 0F35, a lemma

Tag 0F35 in the Stacks Project.

AlgebraicGeometry.geometricIrreducibleComponentCount_eq_numGeometricConnectedComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/GeometricFibreCount.lean, line 112. The attribute's comment: “agreement”.

For a locally quasi-finite morphism, the functions counting geometrically irreducible and geometrically connected components of its fibres agree.

theorem geometricIrreducibleComponentCount_eq_numGeometricConnectedComponents
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] :
    geometricIrreducibleComponentCount f =
      numGeometricConnectedComponents f

AlgebraicGeometry.exists_forall_geometricIrreducibleComponentCount_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/GeometricFibreCount.lean, line 162. The attribute's comment: “boundedness”.

The geometric fibre count of a locally quasi-finite morphism whose source is quasi-compact is bounded by a natural number.

theorem exists_forall_geometricIrreducibleComponentCount_le {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] [CompactSpace X] :
    ∃ d : ℕ, ∀ y : Y, geometricIrreducibleComponentCount f y ≤ (d : ℕ∞)

AlgebraicGeometry.exists_isGreatest_range_geometricIrreducibleComponentCount, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/GeometricFibreCount.lean, line 176. The attribute's comment: “maximum, the target is assumed nonempty”.

The geometric fibre count of a locally quasi-finite morphism whose source is quasi-compact and whose target is nonempty attains a finite maximum: its set of values has a greatest element.

theorem exists_isGreatest_range_geometricIrreducibleComponentCount {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] [CompactSpace X] [Nonempty Y] :
    ∃ d : ℕ, IsGreatest (Set.range (geometricIrreducibleComponentCount f)) (d : ℕ∞)

Tag 0F36, a lemma

Tag 0F36 in the Stacks Project.

AlgebraicGeometry.isOpen_geometricIrreducibleComponentCount_ge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyOpen/FibreCountLowerBound.lean, line 414. References: EGA IV (18.10.17.1), “globally univ. open”; SGA 1 I (10.7), “more general”.

Stacks Project, Tag 0F36. For a separated, locally quasi-finite and universally open morphism of schemes, the locus where the number of geometric components of the fibre is at least a fixed natural number is open.

theorem isOpen_geometricIrreducibleComponentCount_ge {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsSeparated f] [LocallyOfFiniteType f] [LocallyQuasiFinite f] [UniversallyOpen f] (d : ℕ) :
    IsOpen {y : Y | (d : ℕ∞) ≤ geometricIrreducibleComponentCount f y}

Tag 0F37, a lemma

Tag 0F37 in the Stacks Project.

AlgebraicGeometry.isOpen_geometricIrreducibleComponentCount_maxLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyOpen/MaximalFibreCount.lean, line 350. The attribute's comment: “openness”.

Stacks Project, Tag 0F37. For a separated, locally quasi-finite and universally open morphism whose geometric fibre count attains the finite maximum d, the locus where the count equals d is open.

theorem isOpen_geometricIrreducibleComponentCount_maxLocus
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f] [LocallyOfFiniteType f]
    [LocallyQuasiFinite f] [UniversallyOpen f] (d : ℕ)
    (hmax : IsGreatest (Set.range (geometricIrreducibleComponentCount f)) (d : ℕ∞)) :
    IsOpen {y : Y | geometricIrreducibleComponentCount f y = (d : ℕ∞)}

AlgebraicGeometry.isFinite_restrict_geometricIrreducibleComponentCount_maxLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/UniversallyOpen/MaximalFibreCount.lean, line 362. The attribute's comment: “finiteness”.

Stacks Project, Tag 0F37. The morphism is finite over the open locus where its geometric fibre count attains the finite maximum.

theorem isFinite_restrict_geometricIrreducibleComponentCount_maxLocus
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f] [LocallyOfFiniteType f]
    [LocallyQuasiFinite f] [UniversallyOpen f] (d : ℕ)
    (hmax : IsGreatest (Set.range (geometricIrreducibleComponentCount f)) (d : ℕ∞)) :
    IsFinite (f ∣_ ⟨{y : Y | geometricIrreducibleComponentCount f y = (d : ℕ∞)},
      isOpen_geometricIrreducibleComponentCount_maxLocus f d hmax⟩)

Sources

LeanAlgebraicGeometry.universallyOpen_iff_forall_isOpenMap_pullback_snd · AlgebraicGeometry.universallyOpen_iff_forall_isOpenMap_affineSpaceMap · AlgebraicGeometry.universallyOpen_of_locallyQuasiFinite_of_dominant_components · AlgebraicGeometry.universallyOpen_iff_isOpen_image_basicOpen_linearCombination · AlgebraicGeometry.exists_locallyQuasiFinite_universallyOpen_baseChange_of_limitBaseChange · AlgebraicGeometry.geometricIrreducibleComponentCount_eq_numGeometricConnectedComponents · AlgebraicGeometry.exists_forall_geometricIrreducibleComponentCount_le · AlgebraicGeometry.exists_isGreatest_range_geometricIrreducibleComponentCount

Section37.75 Weightings #

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

Tag 0F39, a lemma

Tag 0F39 in the Stacks Project.

AlgebraicGeometry.separableDegreeWeightedFiberSum_comp_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/WeightedFibreSum.lean, line 392.

Weighted fibre sums by separable residue degrees commute with cartesian base change.

theorem separableDegreeWeightedFiberSum_comp_of_isPullback
    {U U' V V' : Scheme.{u}} (f : U ⟶ V) (h : U' ⟶ U)
    (f' : U' ⟶ V') (g : V' ⟶ V) (sq : IsPullback h f' f g)
    [LocallyQuasiFinite f] (hfinite : ∀ v, (f ⁻¹' {v}).Finite) (w : U → ℤ) :
    separableDegreeWeightedFiberSum f w ∘ g =
      separableDegreeWeightedFiberSum f' (w ∘ h)

Tag 0F3A, a definition

Tag 0F3A in the Stacks Project.

AlgebraicGeometry.IsWeighting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Weighting.lean, line 56. References: SGA 4 XVII (6.2.4), “condition (*)”.

An integer-valued function w on X is a weighting of f : X ⟶ Y if its separable-degree weighted fibre sum is locally constant on every finite open piece of every étale base change of f.

def IsWeighting {X Y : Scheme.{u}} (f : X ⟶ Y) (w : X → ℤ) : Prop

Tag 0F3B, a lemma

Tag 0F3B in the Stacks Project.

AlgebraicGeometry.IsWeighting.comp_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/BaseChange.lean, line 619. References: SGA 4 XVII (6.2.4), “base change”.

A weighting pulls back to a weighting along an arbitrary base change.

theorem IsWeighting.comp_of_isPullback {X Y X' Y' : Scheme.{u}}
    {f : X ⟶ Y} {p : X' ⟶ X} {f' : X' ⟶ Y'} {g : Y' ⟶ Y}
    {w : X → ℤ} (hw : IsWeighting f w)
    (sq : IsPullback p f' f g) [LocallyOfFiniteType f] [LocallyQuasiFinite f] :
    IsWeighting f' (w ∘ p)

Tag 0GK8, a lemma

Tag 0GK8 in the Stacks Project.

AlgebraicGeometry.IsWeighting.comp_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/Weighting.lean, line 79.

The restriction of a weighting to an open subscheme of the source is a weighting of the restricted morphism.

theorem IsWeighting.comp_isOpenImmersion {X' X Y : Scheme.{u}}
    (j : X' ⟶ X) [IsOpenImmersion j] {f : X ⟶ Y} {w : X → ℤ}
    (hw : IsWeighting f w) : IsWeighting (j ≫ f) (w ∘ j)

Tag 0GK9, a lemma

Tag 0GK9 in the Stacks Project.

AlgebraicGeometry.IsWeighting.mul_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/Composition.lean, line 827. References: SGA 4 XVII (6.2.4), “composite”.

The pointwise product of a weighting of f and the pullback of a weighting of g is a weighting of f ≫ g.

theorem IsWeighting.mul_comp {X Y Z : Scheme.{u}}
    {f : X ⟶ Y} {g : Y ⟶ Z}
    [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    [LocallyOfFiniteType g] [LocallyQuasiFinite g]
    {w_f : X → ℤ} {w_g : Y → ℤ}
    (hw_f : IsWeighting f w_f)
    (hw_g : IsWeighting g w_g) :
    IsWeighting (f ≫ g) (fun x ↦ w_f x * w_g (f x))

Tag 0F3C, a lemma

Tag 0F3C in the Stacks Project.

AlgebraicGeometry.universallyOpen_of_positive_weighting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/UniversallyOpen.lean, line 126.

Stacks Project, Tag 0F3C. A locally quasi-finite morphism carrying an everywhere positive weighting is universally open.

theorem universallyOpen_of_positive_weighting {X Y : Scheme.{u}}
    {f : X ⟶ Y} [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    {w : X → ℤ} (hw : IsWeighting f w) (hpositive : ∀ x : X, 0 < w x) :
    UniversallyOpen f

Tag 0F3D, a lemma

Tag 0F3D in the Stacks Project.

AlgebraicGeometry.flatQuasiFiniteWeight, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FlatLength.lean, line 959. The attribute's comment: “the formula”.

The local-fibre length times the inseparable degree of the residue-field extension at a point of a scheme morphism.

noncomputable def flatQuasiFiniteWeight {X Y : Scheme.{u}} (f : X ⟶ Y) : X → ℤ

AlgebraicGeometry.flatQuasiFiniteWeight_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FlatLength.lean, line 1069. The attribute's comment: “positivity”.

The canonical local-fibre weighting is strictly positive.

theorem flatQuasiFiniteWeight_pos {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyQuasiFinite f] [LocallyOfFinitePresentation f] [Flat f]
    (x : X) : 0 < flatQuasiFiniteWeight f x

AlgebraicGeometry.flatQuasiFiniteWeight_isWeighting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FlatLength.lean, line 1096. The attribute's comment: “weighting”.

The canonical local-fibre function is a weighting.

theorem flatQuasiFiniteWeight_isWeighting {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyQuasiFinite f] [LocallyOfFinitePresentation f] [Flat f] :
    IsWeighting f (flatQuasiFiniteWeight f)

AlgebraicGeometry.flatQuasiFiniteWeight_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FlatLengthBaseChange.lean, line 203. The attribute's comment: “base-change invariance of the function of the formula”.

Stacks Project, Example 0GKI, final claim. Let f : X ⟶ Y be flat, locally quasi-finite and locally of finite presentation and let f' : X' ⟶ Y' be a base change of f along g : Y' ⟶ Y, with p : X' ⟶ X the projection. Then the canonical weighting of f' is the restriction along p of the canonical weighting of f.

The weight at a point is the length of the local ring of the scheme-theoretic fibre through it times the inseparable degree of the residue field extension. The comparison morphism of fibres N is flat, so Tag 02M1 splits the length upstairs as the length downstairs times the length of the local ring of the fibre of N, and Stacks.Chow.length_fiberStalk_mul_finInsepDegree_of_isPullback trades that last length against the two inseparable degrees.

theorem flatQuasiFiniteWeight_of_isPullback {X Y X' Y' : Scheme.{u}} (f : X ⟶ Y)
    {p : X' ⟶ X} {f' : X' ⟶ Y'} {g : Y' ⟶ Y} (sq : IsPullback p f' f g)
    [LocallyQuasiFinite f] [LocallyOfFinitePresentation f] [Flat f] :
    flatQuasiFiniteWeight f' = flatQuasiFiniteWeight f ∘ p

Tag 0F3E, a lemma

Tag 0F3E in the Stacks Project.

AlgebraicGeometry.exists_weighting_genericSeparableDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/GenericSeparableDegree/Weighting.lean, line 437. References: SGA 4 XVII (6.2.6), “n(x) is a weighting”.

The generic-separable-degree weighting. For f : X ⟶ Y locally quasi-finite and locally of finite type over a geometrically unibranch locally Noetherian scheme Y, there is a weighting w of f whose value at x is, for all compatible strict henselizations Rsh of 𝒪_{Y,f(x)} and Ssh of 𝒪_{X,x}, every minimal prime p of Rsh and every algebraic closure Kbar of κ(p), the number of κ(p)-algebra maps κ(p) ⊗[Rsh] Ssh → Kbar.

public theorem exists_weighting_genericSeparableDegree
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    [LocallyQuasiFinite f] [IsLocallyNoetherian Y]
    (hY : IsGeometricallyUnibranch Y) :
    ∃ w : X → ℕ,
      IsWeighting f (fun x ↦ (w x : ℤ)) ∧
      ∀ (x : X)
        (κY : Type u) [Field κY]
        [Algebra (maximalIdeal (Y.presheaf.stalk (f x))).ResidueField κY]
        [IsSepClosure (maximalIdeal (Y.presheaf.stalk (f x))).ResidueField κY]
        (Rsh : Type u) [CommRing Rsh] [IsLocalRing Rsh]
        [Algebra (Y.presheaf.stalk (f x)) Rsh]
        (_hRsh : Stacks.StrictHenselization.IsStrictHenselization
          (Y.presheaf.stalk (f x)) κY Rsh)
        (κX : Type u) [Field κX]
        [Algebra (maximalIdeal (X.presheaf.stalk x)).ResidueField κX]
        [IsSepClosure (maximalIdeal (X.presheaf.stalk x)).ResidueField κX]
        (Ssh : Type u) [CommRing Ssh] [IsLocalRing Ssh]
        [Algebra (X.presheaf.stalk x) Ssh] [Algebra Rsh Ssh]
        [Algebra (Y.presheaf.stalk (f x)) Ssh]
        [IsScalarTower (Y.presheaf.stalk (f x)) Rsh Ssh]
        (_hSsh : Stacks.StrictHenselization.IsStrictHenselization
          (X.presheaf.stalk x) κX Ssh)
        (_hcomp : (algebraMap (Y.presheaf.stalk (f x)) Ssh) =
          (algebraMap (X.presheaf.stalk x) Ssh).comp (f.stalkMap x).hom)
        (p : Ideal Rsh) [p.IsPrime] (_hp : p ∈ minimalPrimes Rsh)
        (Kbar : Type u) [Field Kbar]
        [Algebra p.ResidueField Kbar] [IsAlgClosure p.ResidueField Kbar],
        w x = Nat.card (AlgHom p.ResidueField
          (TensorProduct Rsh p.ResidueField Ssh) Kbar)

Sources

LeanAlgebraicGeometry.separableDegreeWeightedFiberSum_comp_of_isPullback · AlgebraicGeometry.IsWeighting · AlgebraicGeometry.IsWeighting.comp_of_isPullback · AlgebraicGeometry.IsWeighting.comp_isOpenImmersion · AlgebraicGeometry.IsWeighting.mul_comp · AlgebraicGeometry.universallyOpen_of_positive_weighting · AlgebraicGeometry.flatQuasiFiniteWeight · AlgebraicGeometry.flatQuasiFiniteWeight_pos

Section37.76 More on weightings #

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

Tag 0F3G, a lemma

Tag 0F3G in the Stacks Project.

AlgebraicGeometry.isLocallyConstructible_weighting_levelSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/LevelSetConstructible.lean, line 657.

Stacks Project, Tag 0F3G. The level sets of a weighting of a locally quasi-finite morphism are locally constructible in the source.

Quasi-finiteness being local, the hypothesis is AlgebraicGeometry.LocallyQuasiFinite together with AlgebraicGeometry.LocallyOfFiniteType, which is Stacks 01TD's pointwise characterization of a locally quasi-finite morphism.

theorem isLocallyConstructible_weighting_levelSet
    {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    {w : X → ℤ} (hw : IsWeighting f w) (n : ℤ) :
    IsLocallyConstructible {x : X | w x = n}

Tag 0F3H, a lemma

Tag 0F3H in the Stacks Project.

AlgebraicGeometry.isLocallyConstructible_separableDegreeWeightedFiberSum_levelSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FibreSumLevelSetConstructible.lean, line 618.

Stacks Project, Tag 0F3H. Each level set of the weighted fibre sum of a weighting of a locally quasi-finite morphism of finite presentation is locally constructible on the target.

The statement is local on the target, so one restricts to an affine open of it; the restricted morphism is again locally quasi-finite of finite presentation and the restricted weight is again a weighting, by [Stacks, Tag 0F3B], while the weighted fibre sum commutes with the restriction by [Stacks, Tag 0F39].

theorem isLocallyConstructible_separableDegreeWeightedFiberSum_levelSet
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyQuasiFinite f] (hf : FinitePresentation f)
    (w : X → ℤ) (hw : IsWeighting f w) (n : ℤ) :
    Topology.IsLocallyConstructible
      {y : Y | separableDegreeWeightedFiberSum f w y = n}

Tag 0F3I, a lemma

Tag 0F3I in the Stacks Project.

AlgebraicGeometry.IsWeighting.upperSemicontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/Semicontinuity.lean, line 111.

Stacks Project, Tag 0F3I. A positive weighting of a locally quasi-finite morphism is upper semicontinuous on its source.

theorem IsWeighting.upperSemicontinuous
    {X Y : Scheme.{u}} {f : X ⟶ Y} [LocallyOfFiniteType f]
    [LocallyQuasiFinite f] {w : X → ℤ}
    (hw : IsWeighting f w) (hpos : ∀ x, 0 < w x) :
    UpperSemicontinuous w

Tag 0F3J, a lemma

Tag 0F3J in the Stacks Project.

AlgebraicGeometry.lowerSemicontinuous_separableDegreeWeightedFiberSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/Semicontinuity.lean, line 125. References: EGA IV (18.2.8), “semicontinuity of n(y)”.

Stacks Project, Tag 0F3J. The weighted fibre sum of a positive weighting of a separated, locally quasi-finite morphism with finite fibres is lower semicontinuous.

theorem lowerSemicontinuous_separableDegreeWeightedFiberSum
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsSeparated f]
    [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    (hfinite : ∀ y, (f ⁻¹' {y}).Finite) (w : X → ℤ)
    (hw : IsWeighting f w) (hpos : ∀ x, 0 < w x) :
    LowerSemicontinuous (separableDegreeWeightedFiberSum f w)

Tag 0F3K, a lemma

Tag 0F3K in the Stacks Project.

AlgebraicGeometry.exists_isGreatest_range_separableDegreeWeightedFiberSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/FibreSumMaximum.lean, line 376. The attribute's comment: “the target is assumed nonempty”.

Stacks Project, Tag 0F3K. The weighted fibre sum of a weighting of a locally quasi-finite morphism with quasi-compact source attains its maximum: its set of values has a greatest element.

The target is assumed nonempty, which the source does not say and without which the set of values is empty and has no greatest element.

public theorem exists_isGreatest_range_separableDegreeWeightedFiberSum
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    [CompactSpace X] [Nonempty Y] {w : X → ℤ} (hw : IsWeighting f w) :
    ∃ d : ℤ, IsGreatest (Set.range (separableDegreeWeightedFiberSum f w)) d

Tag 0F3L, a lemma

Tag 0F3L in the Stacks Project.

AlgebraicGeometry.exists_isFinite_restrict_separableDegreeWeightedFiberSum_maxLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/MaximalLocus.lean, line 309.

Stacks Project, Tag 0F3L. A separated locally quasi-finite morphism with finite fibres and a positive weighting is finite over the open locus where its weighted fibre sum attains its global maximum.

theorem exists_isFinite_restrict_separableDegreeWeightedFiberSum_maxLocus
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    [LocallyQuasiFinite f] [IsSeparated f]
    (hfinite : ∀ y : Y, (f ⁻¹' {y}).Finite)
    (w : X → ℤ) (hw : IsWeighting f w)
    (hpositive : ∀ x : X, 0 < w x)
    (d : ℤ)
    (hmax : IsGreatest (Set.range (separableDegreeWeightedFiberSum f w)) d) :
    ∃ U : Y.Opens,
      (U : Set Y) = {y | separableDegreeWeightedFiberSum f w y = d} ∧
        IsFinite (f ∣_ U)

Tag 0F3M, a lemma

Tag 0F3M in the Stacks Project.

Algebra.exists_finitePresentation_algebra_universal_for_idempotents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/IdempotentUniversalAlgebra.lean, line 91.

Stacks Project, Tag 0F3M. A finite, finitely presented algebra has a finitely presented weakly universal base change equipped with an idempotent: every idempotent after an arbitrary base change is the image of the universal one under some specialization.

theorem Algebra.exists_finitePresentation_algebra_universal_for_idempotents
    (A : Type u) [CommRing A] (B : Type v) [CommRing B] [Algebra A B]
    [Module.Finite A B] [Algebra.FinitePresentation A B] :
    ∃ (Auniv : Type (max u v)) (_ : CommRing Auniv) (_ : Algebra A Auniv)
      (_ : Algebra.FinitePresentation A Auniv)
      (euniv : B ⊗[A] Auniv),
      IsIdempotentElem euniv ∧
        ∀ (A' : Type w) [CommRing A'] [Algebra A A'] (e : B ⊗[A] A'),
          IsIdempotentElem e →
            ∃ f : Auniv →ₐ[A] A',
              Algebra.TensorProduct.map (AlgHom.id A B) f euniv = e

Tag 0F3N, a lemma

Tag 0F3N in the Stacks Project.

AlgebraicGeometry.exists_universal_finite_open_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/UniversalFiniteOpen.lean, line 242.

Stacks Project, Tag 0F3N. A quasi-finite morphism of finite presentation between affine schemes admits a base change of finite presentation carrying a universal finite open subscheme: every open subscheme of a base change along a morphism of affine schemes that is finite over the new base is the inverse image of this one.

theorem exists_universal_finite_open_subscheme
    {X Y : Scheme.{u}} [IsAffine X] [IsAffine Y] (f : X ⟶ Y)
    [LocallyQuasiFinite f] (hfp : FinitePresentation f) :
    ∃ (Yuniv : Scheme.{u}) (g : Yuniv ⟶ Y)
      (Uuniv : (pullback f g).Opens),
      FinitePresentation g ∧
        IsFinite (Uuniv.ι ≫ pullback.snd f g) ∧
      ∀ (Y' : Scheme.{u}) [IsAffine Y'] (g' : Y' ⟶ Y)
          (U' : (pullback f g').Opens),
          IsFinite (U'.ι ≫ pullback.snd f g') →
            ∃ (h : Y' ⟶ Yuniv) (hh : h ≫ g = g'),
              (pullback.lift (pullback.fst f g')
                (pullback.snd f g' ≫ h)
                (by rw [Category.assoc, hh]; exact pullback.condition)) ⁻¹ᵁ Uuniv = U'

Tag 0F3P, a lemma

Tag 0F3P in the Stacks Project.

AlgebraicGeometry.eventually_exists_weighting_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/LimitDescent/FiniteStage.lean, line 495.

A weighting on the limit base change of a quasi-finite finitely presented morphism of affine schemes comes from a weighting at every sufficiently late stage of the directed inverse system.

theorem eventually_exists_weighting_baseChange
    {I : Type v} [Small.{u} I] [Preorder I] [IsDirected I (· ≤ ·)]
    (D : Iᵒᵖ ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ i : I, IsAffine (D.obj (op i))]
    (i₀ : I) (X₀ : Scheme.{u}) [IsAffine X₀]
    (f₀ : X₀ ⟶ D.obj (op i₀))
    (hfp : FinitePresentation f₀)
    [LocallyQuasiFinite f₀]
    (w : (pullback f₀ (c.π.app (op i₀)) : Scheme.{u}) → ℤ)
    (hw : IsWeighting
      (pullback.snd f₀ (c.π.app (op i₀))) w) :
    ∀ᶠ i in Filter.atTop, ∀ hi : i₀ ≤ i,
      ∃ wᵢ : (pullback f₀ (D.map (homOfLE hi).op) : Scheme.{u}) → ℤ,
        IsWeighting
          (pullback.snd f₀ (D.map (homOfLE hi).op)) wᵢ ∧
        w = wᵢ ∘ pullback.lift
          (pullback.fst f₀ (c.π.app (op i₀)))
          (pullback.snd f₀ (c.π.app (op i₀)) ≫ c.π.app (op i))
          (by
            rw [Category.assoc, c.w (homOfLE hi).op]
            exact pullback.condition)

Sources

LeanAlgebraicGeometry.isLocallyConstructible_weighting_levelSet · AlgebraicGeometry.isLocallyConstructible_separableDegreeWeightedFiberSum_levelSet · AlgebraicGeometry.IsWeighting.upperSemicontinuous · AlgebraicGeometry.lowerSemicontinuous_separableDegreeWeightedFiberSum · AlgebraicGeometry.exists_isGreatest_range_separableDegreeWeightedFiberSum · AlgebraicGeometry.exists_isFinite_restrict_separableDegreeWeightedFiberSum_maxLocus · Algebra.exists_finitePresentation_algebra_universal_for_idempotents · AlgebraicGeometry.exists_universal_finite_open_subscheme

Section37.77 Weightings and affine stratification numbers #

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

Tag 0F3R, a lemma

Tag 0F3R in the Stacks Project.

AlgebraicGeometry.exists_isAffineOpen_separableDegreeWeightedFiberSum_eq_max, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/Weighting/AffineMaxLocus.lean, line 1130.

Stacks Project, Tag 0F3R. Let f : X ⟶ Y be a quasi-finite morphism of finite presentation between affine schemes and let w be an everywhere positive weighting of f. If the weighted fibre sum of w attains a greatest value d, then the locus in Y where that value is attained is an affine open subscheme of Y.

Quasi-finiteness is expressed, as in Tag 01TD, by AlgebraicGeometry.LocallyOfFiniteType together with AlgebraicGeometry.LocallyQuasiFinite; the maximum value exists by Tag 0F3K, and the locus is produced together with its openness rather than assumed open.

theorem exists_isAffineOpen_separableDegreeWeightedFiberSum_eq_max
    {X Y : Scheme.{u}} [IsAffine X] [IsAffine Y] (f : X ⟶ Y)
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] (hfp : FinitePresentation f)
    (w : X → ℤ) (hw : IsWeighting f w) (hpositive : ∀ x, 0 < w x) (d : ℤ)
    (hd : IsGreatest (Set.range (separableDegreeWeightedFiberSum f w)) d) :
    ∃ U : Y.Opens,
      (U : Set Y) = {y | separableDegreeWeightedFiberSum f w y = d} ∧ IsAffineOpen U

Tag 0F3S, a proposition

Tag 0F3S in the Stacks Project.

AlgebraicGeometry.affineStratificationNumber_le_ncard_separableDegreeWeightedFiberSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AffineStratification/WeightingBound.lean, line 208.

Let f : X ⟶ Y be a surjective quasi-finite morphism of schemes and let w : X → ℤ_{>0} be a positive weighting of f. If X is affine and Y is separated, then the affine stratification number of Y is at most the number of distinct values of the weighted fibre integral ∫_f w.

theorem affineStratificationNumber_le_ncard_separableDegreeWeightedFiberSum
    {X Y : Scheme.{u}} [IsAffine X] [Y.IsSeparated] (f : X ⟶ Y)
    [Surjective f] [LocallyOfFiniteType f] [LocallyQuasiFinite f]
    (w : X → ℤ) (hw : IsWeighting f w) (hpositive : ∀ x, 0 < w x) :
    affineStratificationNumber Y ≤
      (Set.range (separableDegreeWeightedFiberSum f w)).ncard

Sources

LeanAlgebraicGeometry.exists_isAffineOpen_separableDegreeWeightedFiberSum_eq_max · AlgebraicGeometry.affineStratificationNumber_le_ncard_separableDegreeWeightedFiberSum

Section37.78 Completely decomposed morphisms #

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

Tag 0GTI, a definition

Tag 0GTI in the Stacks Project.

AlgebraicGeometry.IsCompletelyDecomposed, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CompletelyDecomposed.lean, line 59. The attribute's comment: “morphism”.

A morphism of schemes is completely decomposed if every point of the target is the image of a point at which the induced map on residue fields is an isomorphism.

def IsCompletelyDecomposed {X Y : Scheme.{u}} (f : X ⟶ Y) : Prop

AlgebraicGeometry.IsCompletelyDecomposedFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CompletelyDecomposed.lean, line 65. The attribute's comment: “family”.

A family of morphisms of schemes with a common target is completely decomposed if the induced morphism from the coproduct of the source schemes is completely decomposed.

def IsCompletelyDecomposedFamily {I : Type v} [Small.{u} I]
    {X : I → Scheme.{u}} {Y : Scheme.{u}} (f : ∀ i, X i ⟶ Y) : Prop

Tag 0GTJ, a lemma

Tag 0GTJ in the Stacks Project.

AlgebraicGeometry.isCompletelyDecomposed_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CompletelyDecomposed.lean, line 120. The attribute's comment: “morphisms”.

The composite of two completely decomposed morphisms of schemes is completely decomposed.

lemma isCompletelyDecomposed_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsCompletelyDecomposed f) (hg : IsCompletelyDecomposed g) :
    IsCompletelyDecomposed (f ≫ g)

AlgebraicGeometry.isCompletelyDecomposedFamily_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CompletelyDecomposed.lean, line 132. The attribute's comment: “families”.

Composing a completely decomposed family with a completely decomposed family over each of its sources gives a completely decomposed family indexed by the dependent sum.

lemma isCompletelyDecomposedFamily_comp {I : Type v} [Small.{u} I]
    {J : I → Type w} [∀ i, Small.{u} (J i)] {X : I → Scheme.{u}}
    {X' : ∀ i, J i → Scheme.{u}} {Y : Scheme.{u}} (f : ∀ i, X i ⟶ Y)
    (g : ∀ i j, X' i j ⟶ X i) (hf : IsCompletelyDecomposedFamily f)
    (hg : ∀ i, IsCompletelyDecomposedFamily (g i)) :
    IsCompletelyDecomposedFamily
      (fun ij : Σ i, J i => g ij.1 ij.2 ≫ f ij.1)

Tag 0GTK, a lemma

Tag 0GTK in the Stacks Project.

AlgebraicGeometry.isCompletelyDecomposed_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CompletelyDecomposed.lean, line 197. The attribute's comment: “morphism”.

A completely decomposed morphism remains completely decomposed after arbitrary base change.

lemma isCompletelyDecomposed_pullback
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : IsCompletelyDecomposed f) :
    IsCompletelyDecomposed (pullback.snd f g)

AlgebraicGeometry.isCompletelyDecomposedFamily_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/WeaklyEtale/CompletelyDecomposed.lean, line 208. The attribute's comment: “family”.

A completely decomposed family of morphisms remains completely decomposed after arbitrary base change.

lemma isCompletelyDecomposedFamily_pullback
    {I : Type v} [Small.{u} I] {X : I → Scheme.{u}} {Y Y' : Scheme.{u}}
    (f : ∀ i, X i ⟶ Y) (g : Y' ⟶ Y)
    (hf : IsCompletelyDecomposedFamily f) :
    IsCompletelyDecomposedFamily (fun i ↦ pullback.snd (f i) g)

Tag 0GTL, a lemma

Tag 0GTL in the Stacks Project.

AlgebraicGeometry.exists_finite_immersion_cover_with_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/CompletelyDecomposed/FiniteCover.lean, line 299.

A completely decomposed morphism locally of finite presentation over a quasi-compact, quasi-separated base has a finite surjective cover by immersions of finite presentation on each of which the morphism admits a section.

theorem exists_finite_immersion_cover_with_sections
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : IsCompletelyDecomposed f)
    [LocallyOfFinitePresentation f] [CompactSpace Y] [QuasiSeparatedSpace Y] :
    ∃ (n : ℕ) (Z : Fin n → Scheme.{u}) (g : ∀ i, Z i ⟶ Y),
      Surjective (Sigma.desc g) ∧
        (∀ i, IsImmersion (g i)) ∧
        (∀ i, FinitePresentation (g i)) ∧
        (∀ i, ∃ s : Z i ⟶ pullback f (g i),
          s ≫ pullback.snd f (g i) = 𝟙 (Z i))

Tag 0GTM, a lemma

Tag 0GTM in the Stacks Project.

AlgebraicGeometry.exists_isCompletelyDecomposed_baseChange_of_limitBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Limits/DescendingMorphisms/CompletelyDecomposed.lean, line 236.

Stacks Project, Tag 0GTM. Let a scheme be the limit of a cofiltered inverse system of schemes with affine transition morphisms, and let a locally finitely presented morphism over one stage have quasi-compact, quasi-separated target. If its base change to the limit is completely decomposed, then its base change to some later stage is completely decomposed.

theorem exists_isCompletelyDecomposed_baseChange_of_limitBaseChange
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (S : I ⥤ Scheme.{u})
    [∀ {i j : I} (g : i ⟶ j), IsAffineHom (S.map g)]
    (c : Cone S) (hc : IsLimit c) (i₀ : I)
    (X₀ Y₀ : Over (S.obj i₀)) (f₀ : X₀ ⟶ Y₀)
    [CompactSpace Y₀.left] [QuasiSeparatedSpace Y₀.left]
    [LocallyOfFinitePresentation f₀.left]
    (hf : IsCompletelyDecomposed ((Over.pullback (c.π.app i₀)).map f₀).left) :
    ∃ (i : I) (g : i ⟶ i₀),
      IsCompletelyDecomposed ((Over.pullback (S.map g)).map f₀).left

Sources

LeanAlgebraicGeometry.IsCompletelyDecomposed · AlgebraicGeometry.IsCompletelyDecomposedFamily · AlgebraicGeometry.isCompletelyDecomposed_comp · AlgebraicGeometry.isCompletelyDecomposedFamily_comp · AlgebraicGeometry.isCompletelyDecomposed_pullback · AlgebraicGeometry.isCompletelyDecomposedFamily_pullback · AlgebraicGeometry.exists_finite_immersion_cover_with_sections · AlgebraicGeometry.exists_isCompletelyDecomposed_baseChange_of_limitBaseChange

Section37.79 Families of ample invertible modules #

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

Tag 0GTP, a lemma

Tag 0GTP in the Stacks Project.

Stacks.AmpleFamilyRelativeAmple.exists_isAmpleFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFamilyRelativeAmple/Basic.lean, line 365.

Stacks Tag 0GTP. Let f : X ⟶ Y be a morphism of schemes. If Y has an ample family of invertible modules and there is an invertible 𝒪_X-module ample relative to f, then X has an ample family of invertible modules.

theorem exists_isAmpleFamily {X Y : Scheme.{u}} (f : X ⟶ Y) {I : Type v} (N : I → Y.Modules)
    (hN : Y.IsAmpleFamily N)
    (hL : ∃ (L : X.Modules) (_ : IsInvertibleModule X L),
      Stacks.RelativeAmple.IsRelativelyAmple f L) :
    ∃ (J : Type v) (M : J → X.Modules), X.IsAmpleFamily M

Tag 0GTQ, a lemma

Tag 0GTQ in the Stacks Project.

Stacks.AmpleFamilyRelativeAmple.exists_isAmpleFamily_of_isAffineHom_or_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFamilyRelativeAmple/QuasiAffine.lean, line 61.

Stacks 0GTQ. Let f : X ⟶ Y be an affine or quasi-affine morphism of schemes. If Y has an ample family of invertible modules, then so does X.

theorem exists_isAmpleFamily_of_isAffineHom_or_isQuasiAffineHom {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : IsAffineHom f ∨ IsQuasiAffineHom f) {I : Type v} (N : I → Y.Modules)
    (hN : Y.IsAmpleFamily N) :
    ∃ (J : Type v) (M : J → X.Modules), X.IsAmpleFamily M

Sources

LeanStacks.AmpleFamilyRelativeAmple.exists_isAmpleFamily · Stacks.AmpleFamilyRelativeAmple.exists_isAmpleFamily_of_isAffineHom_or_isQuasiAffineHom

Section37.80 Blowing up and ample families of invertible modules #

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

Tag 0GTS, a lemma

Tag 0GTS in the Stacks Project.

Stacks.AmpleFamilyCartier.exists_isAmpleFamily_of_isAmpleOnComplement_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/AmpleFamilyCartier/AmpleFamily.lean, line 153.

[Stacks, Tag 0GTS]. Let X be a scheme, let D 0, …, D (m-1) be effective Cartier divisors on X and L 0, …, L (m-1) invertible 𝒪_X-modules such that the divisors have empty common intersection (every point lies in the complement of some D i) and L i restricted to X ∖ D i is ample. Then X has an ample family of invertible modules.

theorem exists_isAmpleFamily_of_isAmpleOnComplement_cover {m : ℕ}
    (D : Fin m → X.IdealSheafData) (L : Fin m → X.Modules)
    (hD : ∀ i, Stacks.Divisors.IsEffectiveCartierDivisor (D i))
    (hL : ∀ i, Stacks.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 (L i))
    (hcover : ∀ x : X, ∃ i, x ∈ (D i).support.compl)
    (hample : ∀ i, IsAmpleOnComplement (D i) (L i)) :
    ∃ (J : Type u) (N : J → X.Modules), X.IsAmpleFamily N

Tag 0GTT, a lemma

Tag 0GTT in the Stacks Project.

Stacks.DenseOpenAdmissibleBlowup.exists_isCompact_dense_admissibleBlowup_isAmpleFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/DenseOpenAdmissibleBlowup/AmpleFamily.lean, line 42.

[Stacks, Tag 0GTT]. Let X be a quasi-compact and quasi-separated scheme with finitely many irreducible components. There exist a quasi-compact dense open U ⊆ X and a U-admissible blowup X' ⟶ X such that X' has an ample family of invertible modules.

public theorem exists_isCompact_dense_admissibleBlowup_isAmpleFamily
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    [Finite (irreducibleComponents X)] :
    ∃ U : X.Opens, IsCompact (U : Set X) ∧ Dense (U : Set X) ∧
      ∃ (X' : Scheme.{u}) (f : X' ⟶ X), Stacks.Blowup.IsAdmissibleBlowup U f ∧
        ∃ (J : Type u) (N : J → X'.Modules), X'.IsAmpleFamily N

Tag 0GTU, a proposition

Tag 0GTU in the Stacks Project.

Stacks.BlowupAmpleFamily.exists_finitePresentation_proper_completelyDecomposed_isAmpleFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/BlowupAmpleFamily/Noetherian.lean, line 187.

[Stacks, Tag 0GTU]. Let X be a quasi-compact and quasi-separated scheme. There is a morphism of schemes f : Y ⟶ X which is of finite presentation, proper and completely decomposed ([Stacks, Tag 0GTI]) and such that Y has an ample family of invertible modules.

The reduction to a base of finite type over ℤ is exists_finitePresentation_proper_completelyDecomposed_isAmpleFamily_of_finiteTypeCase, and the case of such a base, which is Noetherian, is exists_finitePresentation_proper_completelyDecomposed_isAmpleFamily_of_isNoetherian.

theorem exists_finitePresentation_proper_completelyDecomposed_isAmpleFamily
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] :
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X), FinitePresentation f ∧ IsProper f ∧
      IsCompletelyDecomposed f ∧ ∃ (J : Type u) (N : J → Y.Modules), Y.IsAmpleFamily N

Sources

LeanStacks.AmpleFamilyCartier.exists_isAmpleFamily_of_isAmpleOnComplement_cover · Stacks.DenseOpenAdmissibleBlowup.exists_isCompact_dense_admissibleBlowup_isAmpleFamily · Stacks.BlowupAmpleFamily.exists_finitePresentation_proper_completelyDecomposed_isAmpleFamily

Section37.81 The extensive criterion for closed immersions #

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

Tag 0H2P, a lemma

Tag 0H2P in the Stacks Project.

AlgebraicGeometry.isClosedImmersion_iff_lifts_injective_specMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedImmersionCriterion/Affine.lean, line 180.

An affine morphism is a closed immersion exactly when maps out of spectra lift against every injective map of commutative rings.

theorem isClosedImmersion_iff_lifts_injective_specMap
    {X Y : Scheme.{u}} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
    IsClosedImmersion f ↔
      ∀ (A B : Type u) [CommRing A] [CommRing B] (ψ : A →+* B),
        Function.Injective ψ →
        ∀ (g : Spec (.of B) ⟶ X) (h : Spec (.of A) ⟶ Y),
          (Spec.map (CommRingCat.ofHom ψ) ≫ h = g ≫ f) →
          ∃ l : Spec (.of A) ⟶ X,
            (Spec.map (CommRingCat.ofHom ψ) ≫ l = g) ∧ (l ≫ f = h)

Tag 0H2Q, a lemma

Tag 0H2Q in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.mem_essImage_of_unit_isSplitMono registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 60 (StacksFrontier): “a retraction of the unit X → Spec Γ(X, 𝒪_X) puts X in Spec's essential image”.
AlgebraicGeometry.Spec.reflective registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 62 (StacksFrontier): “Spec is reflective with unit X.toSpecΓ”.
AlgebraicGeometry.ΓSpec.adjunction_unit_app registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 63 (StacksFrontier): “the unit is X.toSpecΓ”.
AlgebraicGeometry.essImage_Spec registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 64 (StacksFrontier): “the essential image of Spec is the affine schemes”.

Tag 0H2R, a lemma

Tag 0H2R in the Stacks Project.

AlgebraicGeometry.ker_toSpecΓ_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedImmersionCriterion/CanonicalMorphism.lean, line 43. The attribute's comment: “the largest quasi-coherent submodule of ker f^♯ is zero”.

The largest quasi-coherent 𝒪_S-module contained in the kernel of f^♯ : 𝒪_S ⟶ f_* 𝒪_X, for f : X ⟶ S = Spec Γ(X, 𝒪_X) the canonical morphism, is zero.

theorem ker_toSpecΓ_eq_bot : X.toSpecΓ.ker = ⊥

AlgebraicGeometry.eq_bot_of_le_ker_toSpecΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedImmersionCriterion/CanonicalMorphism.lean, line 54. The attribute's comment: “the largest quasi-coherent submodule of ker f^♯ is zero, universal form”.

A quasi-coherent ideal sheaf on S = Spec Γ(X, 𝒪_X) whose sections over every affine open are killed by f^♯ is zero.

theorem eq_bot_of_le_ker_toSpecΓ {I : (Spec Γ(X, ⊤)).IdealSheafData}
    (hI : ∀ U, I.ideal U ≤ RingHom.ker (X.toSpecΓ.app U).hom) : I = ⊥

AlgebraicGeometry.toSpecΓ_app_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedImmersionCriterion/CanonicalMorphism.lean, line 68. The attribute's comment: “if X is quasi-compact then f^♯ is injective”.

If X is quasi-compact then f^♯ : 𝒪_S ⟶ f_* 𝒪_X is injective, for f : X ⟶ S = Spec Γ(X, 𝒪_X) the canonical morphism: it is injective on the sections over every open of S.

theorem toSpecΓ_app_injective [CompactSpace X] (U : (Spec Γ(X, ⊤)).Opens) :
    Function.Injective (X.toSpecΓ.app U)

AlgebraicGeometry.isDominant_toSpecΓ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedImmersionCriterion/CanonicalMorphism.lean, line 74. The attribute's comment: “if X is quasi-compact then f is dominant”.

If X is quasi-compact then the canonical morphism X ⟶ Spec Γ(X, 𝒪_X) is dominant.

theorem isDominant_toSpecΓ [CompactSpace X] : IsDominant X.toSpecΓ

Tag 0H2S, a lemma

Tag 0H2S in the Stacks Project.

AlgebraicGeometry.isClosedImmersion_iff_lifts_injective_specMap_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedImmersionCriterion/QuasiCompact.lean, line 117.

A quasi-compact scheme morphism is a closed immersion exactly when maps out of spectra lift against every injective homomorphism of commutative rings.

public theorem isClosedImmersion_iff_lifts_injective_specMap_of_quasiCompact
    {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] :
    IsClosedImmersion f ↔
      ∀ (A B : Type u) [CommRing A] [CommRing B] (ψ : A →+* B),
      Function.Injective ψ →
      ∀ (g : Spec (.of B) ⟶ X) (h : Spec (.of A) ⟶ Y),
        (Spec.map (CommRingCat.ofHom ψ) ≫ h = g ≫ f) →
        ∃ l : Spec (.of A) ⟶ X,
          (Spec.map (CommRingCat.ofHom ψ) ≫ l = g) ∧ (l ≫ f = h)

Sources

LeanAlgebraicGeometry.isClosedImmersion_iff_lifts_injective_specMap · CategoryTheory.mem_essImage_of_unit_isSplitMono · AlgebraicGeometry.Spec.reflective · AlgebraicGeometry.ΓSpec.adjunction_unit_app · AlgebraicGeometry.essImage_Spec · AlgebraicGeometry.ker_toSpecΓ_eq_bot · AlgebraicGeometry.eq_bot_of_le_ker_toSpecΓ · AlgebraicGeometry.toSpecΓ_app_injective

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

37.68 Relative morphisms to 37.81 The extensive criterion…

Section37.68 Relative morphisms#

Tag 0BL1, an equation

Tag 0BL2, an equation

Tag 05Y6, a lemma

Tag 0BL3, a lemma

Tag 0BL4, a lemma

Tag 0BL5, a lemma

Sources

Section37.69 Characterizing pseudo-coherent complexes, III#

Tag 0CTA, a lemma

Tag 0CSJ, a lemma

Tag 0CSK, a lemma

Tag 0CSL, a lemma

Tag 0GES, a lemma

Tag 0GET, a lemma

Sources

Section37.70 Descent finiteness properties of complexes#

Tag 0CSN, a lemma

Tag 0CSP, a lemma

Tag 0CSQ, a lemma

Sources

Section37.71 Relatively perfect objects#

Tag 0DJX, a lemma

Tag 0DJY, a lemma

Tag 0DJZ, a lemma

Sources

Section37.72 Contracting rational curves#

Tag 0E7F, a lemma

Tag 0E7G, a lemma

Tag 0E7H, a lemma

Tag 0E7I, a lemma

Tag 0E7J, a lemma

Tag 0E7K, a lemma

Tag 0E7L, a lemma

Tag 0E24, a lemma

Sources

Section37.73 Affine stratifications#

Tag 0F2S, a definition

Tag 0F2T, a lemma

Tag 0F2U, a lemma

Tag 0F2V, a definition

Tag 0F2W, a lemma

Tag 0F2X, a lemma

Tag 0F2Y, a proposition

Tag 0F2Z, an example

Sources

Section37.74 Universally open morphisms#

Tag 0F31, a lemma

Tag 0F32, a lemma

Tag 0F33, a lemma

Tag 0F34, a lemma

Tag 0F35, a lemma

Tag 0F36, a lemma

Tag 0F37, a lemma

Sources

Section37.75 Weightings#

Tag 0F39, a lemma

Tag 0F3A, a definition

Tag 0F3B, a lemma

Tag 0GK8, a lemma

Tag 0GK9, a lemma

Tag 0F3C, a lemma

Tag 0F3D, a lemma

Tag 0F3E, a lemma

Sources

Section37.76 More on weightings#

Tag 0F3G, a lemma

Tag 0F3H, a lemma

Tag 0F3I, a lemma

Tag 0F3J, a lemma

Tag 0F3K, a lemma

Tag 0F3L, a lemma

Tag 0F3M, a lemma

Tag 0F3N, a lemma

Tag 0F3P, a lemma

Sources

Section37.77 Weightings and affine stratification numbers#

Tag 0F3R, a lemma

Tag 0F3S, a proposition

Section37.68 Relative morphisms #

Section37.69 Characterizing pseudo-coherent complexes, III #

Section37.70 Descent finiteness properties of complexes #

Section37.71 Relatively perfect objects #

Section37.72 Contracting rational curves #

Section37.73 Affine stratifications #

Section37.74 Universally open morphisms #

Section37.75 Weightings #

Section37.76 More on weightings #

Section37.77 Weightings and affine stratification numbers #

Section37.78 Completely decomposed morphisms #

Section37.79 Families of ample invertible modules #

Section37.80 Blowing up and ample families of invertible modules #

Section37.81 The extensive criterion for closed immersions #