76.49 When is a morphism an… to 76.57 Blowing up and the…

Section76.49 When is a morphism an isomorphism?#

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

Tag 05X8, a lemma

Tag 05X8 in the Stacks Project.

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

Stacks 05X8. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite type and closed, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change of f along it is unramified.

The open subspace is the one cut out, through the correspondence of Stacks 03BZ, by the complement of the image under p of the set of points at which f is not unramified: that set is closed because the unramified locus of part (1) of Stacks 05W2 is open, and its image is closed because p is. Factoring through W is the containment of the image of the points of Z' in that complement, by Stacks 03IE, while unramifiedness of the base change is unramifiedness at each of its points, by Stacks 03ZK; part (2) of Stacks 05W2 identifies the latter with unramifiedness of f at each point of X lying over a point of the image of Z', and the two conditions then agree by a complementation.

theorem exists_isOpenSubspace_forall_factorsThrough_iff_isUnramified_baseChange
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFiniteType B S hS p) (hpc : IsClosedMorphism B S hS p) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsUnramified B S hS (baseChangeOverBase B S hS f p q hfq g)

Tag 05X9, a lemma

Tag 05X9 in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isUnramified_universallyInjective_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UnramifiedLocusOnBase.lean, line 545.

Stacks 05X9. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite type and closed and the morphism X ×_Y X ⟶ Z given by the first projection followed by p is closed, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change of f along it is unramified and universally injective.

The open subspace is cut out, through the correspondence of Stacks 03BZ, by the point set of the open subspace of Stacks 05X8 intersected with the complement of the image under X ×_Y X ⟶ Z of the complement of the image of the relative diagonal of the base change of f over that open subspace; that image is an open subspace of X ×_Y X because the relative diagonal of an unramified morphism is an open immersion by part (1) of Stacks 05W1 and because X ×_Z W₀ sits inside X ×_Y X as a base change of W₀. Factoring through the intersection is, by Stacks 03IE, the conjunction of factoring through the open subspace of Stacks 05X8 and of every point of X ×_Y X over the image of Z' lying in the image of the diagonal, and the second condition is universal injectivity of the base change.

theorem exists_isOpenSubspace_iff_isUnramified_universallyInjective_baseChange
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFiniteType B S hS p) (hpc : IsClosedMorphism B S hS p)
    (hp₂ : IsClosedMorphism B S hS (pullback.fst f f ≫ p)) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsUnramified B S hS (baseChangeOverBase B S hS f p q hfq g) ∧
            UniversallyInjective B S hS (baseChangeOverBase B S hS f p q hfq g)

Tag 05XA, a lemma

Tag 05XA in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isClosedImmersion_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/ClosedImmersionLocusOnBase.lean, line 82.

Stacks 05XA. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite type and universally closed and q is separated, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change of f along it is a closed immersion.

The open subspace is the one of Stacks 05X9 for the same triangle, over which the base change of f is unramified and universally injective: it is available because p is closed and because X ×_Y X ⟶ Z is closed, being a base change of f followed by p. Every base change of f is universally closed, since f is by part (1) of Stacks 04NX, so the three conditions of Stacks 05W8 for the base change reduce to the two cut out by that subspace.

theorem exists_isOpenSubspace_iff_isClosedImmersion_baseChange
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFiniteType B S hS p) (hpuc : UniversallyClosed B S hS p)
    (hq : IsSeparated B S hS q) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsClosedImmersion B S hS (baseChangeOverBase B S hS f p q hfq g)

Tag 05XB, a lemma

Tag 05XB in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatLocusOnBase.lean, line 131. The attribute's comment: “the open subspace of the base over which the morphism becomes flat”.

Stacks 05XB. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite presentation, flat and closed and q is locally of finite type, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change of f along it is flat.

The open subspace is cut out, through the correspondence of Stacks 03BZ, by the complement of the image under p of the set of points of X at which f is not flat, which is closed by the openness half of Stacks 05X3 and whose image is closed because p is. Factoring through it is the containment of the image of the points of Z' in that complement by Stacks 03IE, and flatness of the base change is flatness at each of its points by Stacks 03MM, which the base-change half of Stacks 05X3 reads off from flatness of f over the image of Z'.

theorem exists_isOpenSubspace_iff_isFlat_baseChange
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFinitePresentation B S hS p) (hpflat : IsFlat B S hS p)
    (hpc : IsClosedMorphism B S hS p) (hq : IsLocallyOfFiniteType B S hS q) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsFlat B S hS (baseChangeOverBase B S hS f p q hfq g)

Tag 05XC, a lemma

Tag 05XC in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isSurjective_isFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/FlatLocusOnBase.lean, line 209. The attribute's comment: “the open subspace of the base over which the morphism becomes surjective and flat”.

Stacks 05XC. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite presentation, flat and closed and q is locally of finite type and closed, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change of f along it is surjective and flat.

The open subspace is cut out by the point set of the subspace W₀ of Stacks 05XB intersected with the locus of points of Z whose fibre in |Y| lies in the image of X ×_Z W₀ ⟶ Y. That locus is open because q is closed and because X ×_Z W₀ ⟶ Y is open on points, being the base change of f over W₀ — flat by the choice of W₀ and locally of finite presentation, hence universally open by Stacks 042S — followed by the open immersion Y ×_Z W₀ ⟶ Y. Over W₀ its image coincides with the image of f, and containment of the image of Z' in the locus is surjectivity of the base change.

theorem exists_isOpenSubspace_iff_isSurjective_isFlat_baseChange
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFinitePresentation B S hS p) (hpflat : IsFlat B S hS p)
    (hpc : IsClosedMorphism B S hS p) (hq : IsLocallyOfFiniteType B S hS q)
    (hqc : IsClosedMorphism B S hS q) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsSurjective B S hS (baseChangeOverBase B S hS f p q hfq g) ∧
            IsFlat B S hS (baseChangeOverBase B S hS f p q hfq g)

Tag 05XD, a lemma

Tag 05XD in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/IsomorphismLocusOnBase.lean, line 125. The attribute's comment: “the open subspace of the base over which the morphism becomes an isomorphism”.

Stacks 05XD. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is locally of finite presentation, flat and universally closed and q is locally of finite type, closed and separated, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change of f along it is an isomorphism.

The open subspace is the intersection, formed on point sets through the correspondence of Stacks 03BZ, of the open subspace of Stacks 05XC over which the base change is surjective and flat with that of Stacks 05XA over which it is a closed immersion. A surjective flat closed immersion is an isomorphism, and an isomorphism is surjective, flat and a closed immersion.

theorem exists_isOpenSubspace_iff_isIso_baseChange
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hp : IsLocallyOfFinitePresentation B S hS p) (hpflat : IsFlat B S hS p)
    (hpuc : UniversallyClosed B S hS p) (hq : IsLocallyOfFiniteType B S hS q)
    (hqc : IsClosedMorphism B S hS q) (hqsep : IsSeparated B S hS q) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsIso (baseChangeOverBase B S hS f p q hfq g)

Tag 06CE, a lemma

Tag 06CE in the Stacks Project.

AlgebraicGeometry.Space.koszulLocusOnBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusOnBase.lean, line 152. The attribute's comment: “the open subspace of the base”.

Stacks 06CE. The open subspace W ⊂ Z of a morphism f : X ⟶ Y of algebraic spaces over S whose source is given over Z by p : X ⟶ Z: the subspace of the base cut out by the complement of the image under p of the set of points at which f is not Koszul, so that a point of |Z| lies in W exactly when f is Koszul at every point of |X| above it.

public def koszulLocusOnBase (f : X ⟶ Y) (p : X ⟶ Z) : Subfunctor Z

AlgebraicGeometry.Space.range_pointsMap_ι_koszulLocusOnBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusOnBase.lean, line 159. The attribute's comment: “the point set of the open subspace of the base”.

The point set of W is the complement of the image under p of the non-Koszul locus of f.

public theorem range_pointsMap_ι_koszulLocusOnBase (f : X ⟶ Y) (p : X ⟶ Z) :
    Set.range (pointsMap B S hS (koszulLocusOnBase B S hS f p).toFunctor
        (koszulLocusOnBase B S hS f p).ι) =
      (pointsMap B S hS X p '' {x : points B S hS X | KoszulAt B S hS f x}ᶜ)ᶜ

AlgebraicGeometry.Space.isOpenSubspace_koszulLocusOnBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusOnBase.lean, line 171. The attribute's comment: “the subspace of the base is open”.

Stacks 06CE. W is an open subspace of Z.

The non-Koszul locus of f is closed because the Koszul locus is open by Stacks 06CA, its image under p is closed because p is closed, and the complement of a closed set is open, hence the point set of an open subspace by Stacks 03BZ.

public theorem isOpenSubspace_koszulLocusOnBase (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (p : X ⟶ Z) (hpc : IsClosedMorphism B S hS p) :
    IsOpenSubspace B S hS (koszulLocusOnBase B S hS f p)

AlgebraicGeometry.Space.factorsThrough_koszulLocusOnBase_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusOnBaseUnconditional.lean, line 110. The attribute's comment: “with the open subspace named rather than quantified over”.

Stacks 06CE, with the open subspace named. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is flat, locally of finite presentation and closed and q is flat and locally of finite presentation, then a morphism Z' ⟶ Z from an algebraic space factors through AlgebraicGeometry.Space.koszulLocusOnBase exactly when the base change of f along it is a local complete intersection morphism.

theorem factorsThrough_koszulLocusOnBase_iff
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hpflat : IsFlat B S hS p) (hplfp : IsLocallyOfFinitePresentation B S hS p)
    (hpc : IsClosedMorphism B S hS p) (hqflat : IsFlat B S hS q)
    (hqlfp : IsLocallyOfFinitePresentation B S hS q)
    (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hZ' : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z) :
    (∃ r : Z' ⟶ (koszulLocusOnBase B S hS f p).toFunctor,
        r ≫ (koszulLocusOnBase B S hS f p).ι = g) ↔
      IsLocalCompleteIntersection B S hS (baseChangeOverBase B S hS f p q hfq g)

AlgebraicGeometry.Space.exists_isOpenSubspace_factorsThrough_iff_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/LocalCompleteIntersection/KoszulLocusOnBaseUnconditional.lean, line 135.

Stacks 06CE. Let f : X ⟶ Y be a morphism of algebraic spaces over S whose source and target are given over a third algebraic space Z by morphisms p : X ⟶ Z and q : Y ⟶ Z with f ≫ q = p. If p is flat, locally of finite presentation and closed and q is flat and locally of finite presentation, then there is an open subspace W of Z through which a morphism Z' ⟶ Z from an algebraic space factors exactly when the base change f_{Z'} : X_{Z'} ⟶ Y_{Z'} of f along it is a local complete intersection morphism.

The open subspace is AlgebraicGeometry.Space.koszulLocusOnBase: the complement of the image under p of the non-Koszul locus of f.

theorem exists_isOpenSubspace_factorsThrough_iff_isLocalCompleteIntersection
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z) (hfq : f ≫ q = p)
    (hpflat : IsFlat B S hS p) (hplfp : IsLocallyOfFinitePresentation B S hS p)
    (hpc : IsClosedMorphism B S hS p) (hqflat : IsFlat B S hS q)
    (hqlfp : IsLocallyOfFinitePresentation B S hS q) :
    ∃ W : Subfunctor Z, IsOpenSubspace B S hS W ∧
      ∀ (Z' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_ : IsAlgebraicSpace B S hS Z') (g : Z' ⟶ Z),
        (∃ r : Z' ⟶ W.toFunctor, r ≫ W.ι = g) ↔
          IsLocalCompleteIntersection B S hS (baseChangeOverBase B S hS f p q hfq g)

Sources

LeanAlgebraicGeometry.Space.exists_isOpenSubspace_forall_factorsThrough_iff_isUnramified_baseChange · AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isUnramified_universallyInjective_baseChange · AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isClosedImmersion_baseChange · AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isFlat_baseChange · AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isSurjective_isFlat_baseChange · AlgebraicGeometry.Space.exists_isOpenSubspace_iff_isIso_baseChange · AlgebraicGeometry.Space.koszulLocusOnBase · AlgebraicGeometry.Space.range_pointsMap_ι_koszulLocusOnBase

Section76.51 Characterizing pseudo-coherent complexes, II #

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

Tag 0CTQ, a lemma

Tag 0CTQ in the Stacks Project.

AlgebraicGeometry.Space.torIndependent_baseChange_product_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TorIndependenceFlatBaseChange.lean, line 512.

Let S be a scheme, let
Z' ⟶ Y'
↓     ↓
X' ⟶ B'
be a commutative square of algebraic spaces over S, let Bb ⟶ B' be a morphism and let Xb and Yb be the base changes of X' and Y' to Bb. If Y' ⟶ B' and Z' ⟶ X' are flat, then Xb ×_{Bb} Yb and Z' are Tor independent over X' ×_{B'} Y'.

public theorem torIndependent_baseChange_product_of_isFlat
    {Bb B' X' Y' Z' Xb Yb P P' : AlgebraicSpaces B S hS}
    {bb : Bb ⟶ B'} {x : X' ⟶ B'} {y : Y' ⟶ B'} {zx : Z' ⟶ X'} {zy : Z' ⟶ Y'}
    (hz : zx ≫ x = zy ≫ y)
    {xX' : Xb ⟶ X'} {xB : Xb ⟶ Bb} (sqX : IsPullback xX'.hom xB.hom x.hom bb.hom)
    {yY' : Yb ⟶ Y'} {yB : Yb ⟶ Bb} (sqY : IsPullback yY'.hom yB.hom y.hom bb.hom)
    {pXb : P ⟶ Xb} {pYb : P ⟶ Yb} (sqP : IsPullback pXb.hom pYb.hom xB.hom yB.hom)
    {p'X : P' ⟶ X'} {p'Y : P' ⟶ Y'} (sqP' : IsPullback p'X.hom p'Y.hom x.hom y.hom)
    (pp' : P ⟶ P') (hpp'X : pp' ≫ p'X = pXb ≫ xX') (hpp'Y : pp' ≫ p'Y = pYb ≫ yY')
    (zp' : Z' ⟶ P') (hzp'X : zp' ≫ p'X = zx) (hzp'Y : zp' ≫ p'Y = zy)
    (hy : IsFlat B S hS y.hom) (hzx : IsFlat B S hS zx.hom) :
    TorIndependent P.2 Z'.2 P'.2 pp'.hom zp'.hom

Tag 0CTR, a lemma

Tag 0CTR in the Stacks Project.

AlgebraicGeometry.Space.nonempty_derivedChowDatum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedChow/General.lean, line 576.

Stacks 0CTR (derived Chow lemma). Let A be a ring and X an algebraic space separated and of finite presentation over A. Every point x ∈ |X| carries a datum of the derived Chow lemma: n ≥ 0, a closed subspace Z ⊂ X ×_A ℙⁿ_A of finite presentation, an open V ⊂ ℙⁿ_A, a point of c⁻¹(V) over x and E ∈ D(𝒪_{X ×_A ℙⁿ_A}) with properties (1)–(5) of the source (AlgebraicGeometry.Space.DerivedChowDatum).

theorem nonempty_derivedChowDatum (X : AlgebraicSpaces B (Spec (.of A)) hA)
    (hsep : IsSeparated B (Spec (.of A)) hA (toBase B (Spec (.of A)) hA X).hom)
    (hfp : IsFinitePresentation B (Spec (.of A)) hA (toBase B (Spec (.of A)) hA X).hom)
    (x : points B (Spec (.of A)) hA X.1) :
    Nonempty (DerivedChowDatum X x)

Tag 0CTS, a lemma

Tag 0CTS in the Stacks Project.

AlgebraicGeometry.Space.DerivedChowDatum.isFinitePresentation_overOpenToOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedChow/Restriction.lean, line 179. The attribute's comment: “the closed immersion c|_W : W ⟶ V of the statement is of finite presentation”.

Stacks 0CTS, first assertion. For X of finite presentation over S, the closed immersion c|_W : W ⟶ V is of finite presentation.

theorem isFinitePresentation_overOpenToOpen
    (hfp : IsFinitePresentation B S hS (toBase B S hS X).hom) :
    IsFinitePresentation B S hS (overOpenToOpen D.i D.v).hom

AlgebraicGeometry.Space.DerivedChowDatum.nonempty_restrict_derivedPushforward_tensor_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedChow/Restriction.lean, line 196.

Stacks 0CTS. For a datum (n, Z, z, V, E) of the derived Chow lemma on X and K ∈ D_QCoh(𝒪_X), Rq_*(Lp^*K ⊗^𝐋 E)|_V ≅ R(c|_W)_* K|_W, where p and q are the two projections of X ×_S ℙⁿ_S, c|_W : W ⟶ V is the closed immersion of the datum and K|_W is the derived pullback along the étale morphism b : W ⟶ X.

theorem nonempty_restrict_derivedPushforward_tensor_iso
    (K : DerivedCategory (SheafOfModules.{u} (ringedToposStructureRingSheaf B S hS X)))
    (hK : QcohDerived B S hS X K) :
    Nonempty ((smallEtaleDerivedModulePullback B S hS D.v).obj
        ((derivedModulePushforward B S hS (productSnd X D.n D.contains)).obj
          (((smallEtaleDerivedTensor B S hS (product B S hS X D.n D.contains)).obj
            ((smallEtaleDerivedModulePullback B S hS (productFst X D.n D.contains)).obj K)).obj
              D.E)) ≅
      (derivedModulePushforward B S hS (overOpenToOpen D.i D.v)).obj
        ((smallEtaleDerivedModulePullback B S hS
          (overOpenι D.i D.v ≫ D.i ≫ productFst X D.n D.contains)).obj K))

Tag 0CTT, a lemma

Tag 0CTT in the Stacks Project.

AlgebraicGeometry.Space.isRelativelyPseudoCoherent_of_isPseudoCoherent_derivedSections_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedChow/RelativePseudoCoherent.lean, line 73.

Stacks 0CTT. Let X be an algebraic space separated and of finite presentation over A and K ∈ D_QCoh(𝒪_X) with RΓ(X, E ⊗^𝐋 K) pseudo-coherent over A for every pseudo-coherent E. Then K is pseudo-coherent relative to A.

theorem isRelativelyPseudoCoherent_of_isPseudoCoherent_derivedSections_tensor
    {X : AlgebraicSpaces B (Spec (CommRingCat.of A)) hA}
    (hsep : IsSeparated B _ hA (toBase B _ hA X).hom)
    (hfp : IsFinitePresentation B _ hA (toBase B _ hA X).hom)
    (K : DerivedCategory (Modules.{u, u} B _ hA X.1 X.2)) (hK : QcohDerived B _ hA X K)
    (h : ∀ E : DerivedCategory (Modules.{u, u} B _ hA X.1 X.2),
      (smallEtaleRingedSite B _ hA X.1 X.2).IsPseudoCoherent E →
        StacksDraft.PseudoCoherence.IsPseudoCoherent
          ((representedAffineDerivedSections B _ hA (baseSiteObj B _ hA)).obj
            ((derivedModulePushforward B _ hA (toBase B _ hA X)).obj
              (((smallEtaleDerivedTensor B _ hA X).obj E).obj K)))) :
    IsRelativelyPseudoCoherent B _ hA X.1 X.2 (toBase B _ hA X).hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B _ hA hfp.1) ⟨K, hK⟩

Tag 0GFJ, a lemma

Tag 0GFJ in the Stacks Project.

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

Let X be an algebraic space separated and of finite presentation over A and K ∈ D_QCoh(𝒪_X) with RΓ(X, E ⊗^𝐋 K) pseudo-coherent over A for every perfect E. Then K is pseudo-coherent relative to A.

theorem isRelativelyPseudoCoherent_of_isPseudoCoherent_derivedSections_tensor_perfect
    {X : AlgebraicSpaces B (Spec (CommRingCat.of A)) hA}
    (hsep : IsSeparated B _ hA (toBase B _ hA X).hom)
    (hfp : IsFinitePresentation B _ hA (toBase B _ hA X).hom)
    (K : DerivedCategory (Modules.{u, u} B _ hA X.1 X.2)) (hK : QcohDerived B _ hA X K)
    (h : ∀ E : DerivedCategory (Modules.{u, u} B _ hA X.1 X.2),
      (smallEtaleRingedSite B _ hA X.1 X.2).IsPerfect E →
        StacksDraft.PseudoCoherence.IsPseudoCoherent
          ((representedAffineDerivedSections B _ hA (baseSiteObj B _ hA)).obj
            ((derivedModulePushforward B _ hA (toBase B _ hA X)).obj
              (((smallEtaleDerivedTensor B _ hA X).obj E).obj K)))) :
    IsRelativelyPseudoCoherent B _ hA X.1 X.2 (toBase B _ hA X).hom
      (isLocallyOfFiniteType_of_isLocallyOfFinitePresentation B _ hA hfp.1) ⟨K, hK⟩

Sources

LeanAlgebraicGeometry.Space.torIndependent_baseChange_product_of_isFlat · AlgebraicGeometry.Space.nonempty_derivedChowDatum · AlgebraicGeometry.Space.DerivedChowDatum.isFinitePresentation_overOpenToOpen · AlgebraicGeometry.Space.DerivedChowDatum.nonempty_restrict_derivedPushforward_tensor_iso · AlgebraicGeometry.Space.isRelativelyPseudoCoherent_of_isPseudoCoherent_derivedSections_tensor · AlgebraicGeometry.Space.isRelativelyPseudoCoherent_of_isPseudoCoherent_derivedSections_tensor_perfect

Section76.52 Relatively perfect objects #

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

Tag 0DKN, a definition

Tag 0DKN in the Stacks Project.

AlgebraicGeometry.Space.IsPerfectRelativeTo, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/Relative.lean, line 179. References: SGA 6 III (4.1), “spaces, flat l.f.p.”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, an object E of D(𝒪_X) is perfect relative to Y when E is pseudo-coherent and, read as an object of D(f⁻¹𝒪_Y) through restriction of scalars along f⁻¹𝒪_Y ⟶ 𝒪_X, locally has finite Tor dimension.

Finite Tor dimension on the slice of the small étale site over V is measured against the derived tensor product T V on that slice. The hypotheses _hflat and _hlfp that f is flat and locally of finite presentation do not enter the condition.

abbrev IsPerfectRelativeTo
    (_hflat : IsFlat B S hS f.hom)
    (_hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U))
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) : Prop

AlgebraicGeometry.Space.IsRelativelyPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativelyPerfect.lean, line 101. The attribute's comment: “Y-perfect objects: pseudo-coherent, and locally of finite tor dimension over f⁻¹𝒪_Y for the derived tensor product of 06YU; independent of that choice by isRelativelyPerfect_iff_isPerfectRelativeTo”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat and locally of finite presentation. An object E of D(𝒪_X) is perfect relative to Y, or Y-perfect, if E is pseudo-coherent and E locally has finite Tor dimension as an object of D(f⁻¹𝒪_Y).

E is read as an object of D(f⁻¹𝒪_Y) through restriction of scalars along f⁻¹𝒪_Y ⟶ 𝒪_X, and finite Tor dimension on the slice of (X_étale, f⁻¹𝒪_Y) over U is measured against the derived tensor product of that slice constructed by Stacks 06YU.

def IsRelativelyPerfect
    (_hflat : IsFlat B S hS f.hom)
    (_hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) : Prop

Tag 0DKP, an example

Tag 0DKP in the Stacks Project.

AlgebraicGeometry.Space.isRelativelyPerfect_dualNumberResidueComplex_and_not_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativelyPerfectNotFibrewise.lean, line 383. The attribute's comment: “relative perfectness over a field is not perfectness on the fibres”.

Stacks 0DKP, the closing warning. Over a field, relative perfectness is not perfectness on the fibres: on the algebraic space Spec k[ε] — which is of finite presentation over k (AlgebraicGeometry.Space.isFinitePresentation_dualNumberSpaceMap), and whose only fibre over Spec k is itself — the residue field of the dual numbers, placed in degree zero, is k-perfect and is not a perfect object of D(𝒪_{Spec k[ε]}).

theorem isRelativelyPerfect_dualNumberResidueComplex_and_not_isPerfect :
    IsRelativelyPerfect B S hS (dualNumberSpaceMap B S hS k hk b)
        (isFlat_toFieldSpace B S hS k hk b _)
        (isLocallyOfFinitePresentation_dualNumberSpaceMap B S hS k hk b)
        (dualNumberResidueComplex B S hS k hk b) ∧
      ¬ (smallEtaleRingedSite B S hS (dualNumberSpace B S hS k hk b).1
        (dualNumberSpace B S hS k hk b).2).IsPerfect (dualNumberResidueComplex B S hS k hk b)

AlgebraicGeometry.Space.isPerfectRelativeTo_of_isBounded_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeOverField.lean, line 231. The attribute's comment: “bounded pseudo-coherent objects are perfect relative to a field”.

Let k be a field and let X be an algebraic space locally of finite presentation over k. A bounded pseudo-coherent object of D(𝒪_X) is perfect relative to Spec k, the flatness of X ⟶ Spec k being isFlat_toFieldSpace.

theorem isPerfectRelativeTo_of_isBounded_of_isPseudoCoherent
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U))
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hpc : (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent E)
    (hbdd : DerivedCategoryB.IsBounded E) :
    IsPerfectRelativeTo B S hS f (isFlat_toFieldSpace B S hS k hk b f) hlfp T E

AlgebraicGeometry.Space.isBounded_and_isPseudoCoherent_iff_derivedCategoryBBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeOverFieldCharacterization.lean, line 143. The attribute's comment: “bounded pseudo-coherent objects are the objects of D^b_Coh(X), by Stacks 08IK”.

On a locally Noetherian algebraic space the bounded pseudo-coherent objects of D(𝒪_X) are the objects of D^b_Coh(𝒪_X): an object of D(𝒪_X) is bounded and pseudo-coherent if and only if it is bounded with coherent cohomology sheaves.

This is the bounded case of the final statement of Stacks 08IK, which identifies the pseudo-coherent objects with D⁻_Coh(𝒪_X); quasi-coherence of the cohomology sheaves holds on both sides, on the left by Stacks 08JL.

theorem isBounded_and_isPseudoCoherent_iff_derivedCategoryBBounded
    (E : DerivedCategory (Modules.{u, u} B S hS F hF)) :
    (DerivedCategoryB.IsBounded E ∧ (smallEtaleRingedSite B S hS F hF).IsPseudoCoherent E) ↔
      DerivedCategoryB.derivedCategoryBBounded
        (fun M : Modules.{u, u} B S hS F hF => M.IsCoherentOnSite) E

AlgebraicGeometry.Space.isQuasiCompactSpace_of_isFinitePresentation_fieldSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeOverFieldCharacterization.lean, line 171. The attribute's comment: “in particular, an algebraic space of finite presentation over a field is quasi-compact”.

An algebraic space of finite presentation over a field is quasi-compact.

theorem isQuasiCompactSpace_of_isFinitePresentation_fieldSpace
    (hfp : IsFinitePresentation B S hS f.hom) : IsQuasiCompactSpace B S hS X.1

AlgebraicGeometry.Space.isRelativelyPerfect_iff_isBounded_and_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeOverFieldCharacterization.lean, line 330. The attribute's comment: “k-perfect objects are the bounded pseudo-coherent ones”.

Stacks 0DKP, first equivalence. Let k be a field and let X be an algebraic space of finite presentation over k. An object E of D(𝒪_X) is k-perfect (Stacks 0DKN) if and only if it is bounded and pseudo-coherent.

theorem isRelativelyPerfect_iff_isBounded_and_isPseudoCoherent
    (hfp : IsFinitePresentation B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) :
    IsRelativelyPerfect B S hS f (isFlat_toFieldSpace B S hS k hk b f) hfp.1 E ↔
      (DerivedCategoryB.IsBounded E ∧ (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent E)

AlgebraicGeometry.Space.isRelativelyPerfect_iff_derivedCategoryBBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeOverFieldCharacterization.lean, line 342. The attribute's comment: “the k-perfect objects are exactly the objects of D^b_Coh(X)”.

Stacks 0DKP. Let k be a field and let X be an algebraic space of finite presentation over k. An object E of D(𝒪_X) is k-perfect (Stacks 0DKN) if and only if it lies in D^b_Coh(𝒪_X), that is, if and only if it is bounded with coherent cohomology sheaves.

theorem isRelativelyPerfect_iff_derivedCategoryBBounded
    (hfp : IsFinitePresentation B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) :
    IsRelativelyPerfect B S hS f (isFlat_toFieldSpace B S hS k hk b f) hfp.1 E ↔
      DerivedCategoryB.derivedCategoryBBounded
        (fun M : Modules.{u, u} B S hS X.1 X.2 => M.IsCoherentOnSite) E

Tag 0DKQ, a lemma

Tag 0DKQ in the Stacks Project.

AlgebraicGeometry.Space.isPerfectRelativeToCanonical_tfae_chartDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSchemeCharts.lean, line 380.

Relative perfectness of algebraic spaces read on scheme charts. Let f : X ⟶ Y be a morphism of algebraic spaces which is flat and locally of finite presentation, and let E ∈ D_QCoh(𝒪_X). For a commutative square of étale scheme charts U ⟶ V over f, write E_0 for the object Rε_*(E|_U) of D_QCoh(𝒪_{U_0}) corresponding to E|_U (Stacks 071Q). The following are equivalent: 1. E is Y-perfect; 2. for every such square, E_0 is V_0-perfect in the sense of schemes; 3. for some such square whose chart of X is surjective, E_0 is V_0-perfect; 4. for every such square with U and V affine, RΓ(U, E) is 𝒪_Y(V)-perfect, that is, pseudo-coherent over Γ(U, 𝒪_U) and of finite Tor dimension over Γ(V, 𝒪_V).

theorem isPerfectRelativeToCanonical_tfae_chartDiagram
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) (hE : QcohDerived B S hS X E) :
    List.TFAE
      [IsPerfectRelativeToCanonical.{u, u + 1, u + 1} B S hS f hfl hlfp E,
        ∀ d : ChartDiagram B S hS X.1 Y.1 f.hom,
          haveI := flat_chartDiagram_g f hfl d
          haveI := locallyOfFinitePresentation_chartDiagram_g f hlfp d
          ((BigFppfOver.toScheme B S hS).map d.g).IsPerfectRelativeTo
            (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily.{u + 1, u}
              (RingedSpace.inverseImage
                (representedSchemeRepresentedZariskiRingedToposHom B S hS
                  ((SmallEtale.toOver B S hS Y.1).obj d.V)).toRingedSpace
                ((BigFppfOver.toScheme B S hS).map d.g).base))
            (chartObject d.U E),
        ∃ d : ChartDiagram B S hS X.1 Y.1 f.hom, IsSurjective B S hS d.U.1.hom ∧
          haveI := flat_chartDiagram_g f hfl d
          haveI := locallyOfFinitePresentation_chartDiagram_g f hlfp d
          ((BigFppfOver.toScheme B S hS).map d.g).IsPerfectRelativeTo
            (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily.{u + 1, u}
              (RingedSpace.inverseImage
                (representedSchemeRepresentedZariskiRingedToposHom B S hS
                  ((SmallEtale.toOver B S hS Y.1).obj d.V)).toRingedSpace
                ((BigFppfOver.toScheme B S hS).map d.g).base))
            (chartObject d.U E),
        ∀ (d : ChartDiagram B S hS X.1 Y.1 f.hom)
          [IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS X.1).obj d.U))]
          [IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS Y.1).obj d.V))],
          StacksDraft.PseudoCoherence.IsPseudoCoherent
              ((representedAffineDerivedSections B S hS
                ((SmallEtale.toOver B S hS X.1).obj d.U)).obj
                ((smallEtaleDerivedModulePullback B S hS (chartToSpace B S hS X d.U)).obj E)) ∧
            StacksDraft.TorAmplitude.HasFiniteTorDimensionCanonical
              Γ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS Y.1).obj d.V), ⊤)
              ((ModuleCat.restrictScalars
                ((BigFppfOver.toScheme B S hS).map d.g).appTop.hom).mapDerivedCategory.obj
                ((representedAffineDerivedSections B S hS
                  ((SmallEtale.toOver B S hS X.1).obj d.U)).obj
                  ((smallEtaleDerivedModulePullback B S hS
                    (chartToSpace B S hS X d.U)).obj E)))]

Tag 0DKR, a lemma

Tag 0DKR in the Stacks Project.

AlgebraicGeometry.Space.isClosedUnderIsomorphisms_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 221. The attribute's comment: “isomorphism closure”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) form a strictly full subcategory: relative perfectness is invariant under isomorphism in D(𝒪_X).

theorem isClosedUnderIsomorphisms_isPerfectRelativeTo
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U)) :
    (isPerfectRelativeTo B S hS f hflat hlfp T).IsClosedUnderIsomorphisms

AlgebraicGeometry.Space.isSaturated_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 291. The attribute's comment: “saturation”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) form a saturated (thick) subcategory: both summands of a Y-perfect biproduct are Y-perfect.

theorem isSaturated_isPerfectRelativeTo
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U)) :
    (isPerfectRelativeTo B S hS f hflat hlfp T).IsSaturated

AlgebraicGeometry.Space.containsZero_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 322. The attribute's comment: “contains a zero object”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) contain a zero object.

theorem containsZero_isPerfectRelativeTo
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U)) :
    (isPerfectRelativeTo B S hS f hflat hlfp T).ContainsZero

AlgebraicGeometry.Space.isStableUnderShift_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 339. The attribute's comment: “closure under the shifts”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) are stable under every shift E ↦ E[n].

theorem isStableUnderShift_isPerfectRelativeTo
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U)) :
    (isPerfectRelativeTo B S hS f hflat hlfp T).IsStableUnderShift ℤ

AlgebraicGeometry.Space.isTriangulated_isPerfectRelativeTo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 394. The attribute's comment: “closure under cones: the Y-perfect objects form a triangulated subcategory. The zero object and the shifts are containsZero_isPerfectRelativeTo and isStableUnderShift_isPerfectRelativeTo”. References: SGA 6 I (5.8.4), “5.8.4 a), special case”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) form a triangulated subcategory: the property contains a zero object, is stable under all shifts, and is closed under extensions, for a given family T of derived tensor products on the slices.

theorem isTriangulated_isPerfectRelativeTo
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U)) :
    (isPerfectRelativeTo B S hS f hflat hlfp T).IsTriangulated

AlgebraicGeometry.Space.isClosedUnderIsomorphisms_isPerfectRelativeToCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 460. The attribute's comment: “isomorphism closure, for an actual f”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) form a strictly full subcategory.

theorem isClosedUnderIsomorphisms_isPerfectRelativeToCanonical
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    (isPerfectRelativeToCanonical B S hS f hflat hlfp).IsClosedUnderIsomorphisms

AlgebraicGeometry.Space.isSaturated_isPerfectRelativeToCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 478. The attribute's comment: “saturation, for an actual f”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) form a saturated (thick) subcategory.

theorem isSaturated_isPerfectRelativeToCanonical
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    (isPerfectRelativeToCanonical B S hS f hflat hlfp).IsSaturated

AlgebraicGeometry.Space.containsZero_isPerfectRelativeToCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 496. The attribute's comment: “contains a zero object, for an actual f”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) contain a zero object.

theorem containsZero_isPerfectRelativeToCanonical
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    (isPerfectRelativeToCanonical B S hS f hflat hlfp).ContainsZero

AlgebraicGeometry.Space.isStableUnderShift_isPerfectRelativeToCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 514. The attribute's comment: “closure under the shifts, for an actual f”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) are stable under every shift.

theorem isStableUnderShift_isPerfectRelativeToCanonical
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    (isPerfectRelativeToCanonical B S hS f hflat hlfp).IsStableUnderShift ℤ

AlgebraicGeometry.Space.isTriangulated_isPerfectRelativeToCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeSubcategory.lean, line 528. The attribute's comment: “closure under cones for an actual f: the Y-perfect objects of D(O_X) form a triangulated subcategory. The zero object and the shifts are containsZero_isPerfectRelativeToCanonical and isStableUnderShift_isPerfectRelativeToCanonical”.

For a morphism f : X ⟶ Y of algebraic spaces which is flat and locally of finite presentation, the Y-perfect objects of D(𝒪_X) form a triangulated subcategory: the property contains a zero object, is stable under all shifts, and is closed under extensions.

theorem isTriangulated_isPerfectRelativeToCanonical
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom) :
    (isPerfectRelativeToCanonical B S hS f hflat hlfp).IsTriangulated

Tag 0DKS, a lemma

Tag 0DKS in the Stacks Project.

AlgebraicGeometry.Space.isRelativelyPerfect_of_isPerfect_and_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativelyPerfectDerivedTensor.lean, line 320.

Stacks 0DKS. Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat and locally of finite presentation.

A perfect object of D(𝒪_X) is Y-perfect.

If K, M ∈ D(𝒪_X), then K ⊗^𝐋_{𝒪_X} M is Y-perfect if K is perfect and M is Y-perfect.

Y-perfectness is Stacks 0DKN, AlgebraicGeometry.Space.IsRelativelyPerfect. The derived tensor product is any derived tensor product datum TX of Stacks 06YU on the small étale site of X, for instance the canonical one. The first assertion is AlgebraicGeometry.Space.isRelativelyPerfect_of_isPerfect, the second AlgebraicGeometry.Space.isRelativelyPerfect_derivedTensor.

theorem isRelativelyPerfect_of_isPerfect_and_derivedTensor
    (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (TX : Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, d}
      (smallEtaleRingedSite B S hS X.1 X.2)) :
    (∀ E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2),
        (smallEtaleRingedSite B S hS X.1 X.2).IsPerfect E →
          IsRelativelyPerfect B S hS f hflat hlfp E) ∧
      ∀ K M : DerivedCategory (Modules.{u, u} B S hS X.1 X.2),
        (smallEtaleRingedSite B S hS X.1 X.2).IsPerfect K →
          IsRelativelyPerfect B S hS f hflat hlfp M →
            IsRelativelyPerfect B S hS f hflat hlfp ((TX.tensor.obj K).obj M)

Tag 0DKT, a lemma

Tag 0DKT in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.isPerfectRelativeToCanonical_smallEtaleDerivedModulePullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeBaseChangeTags.lean, line 20 (StacksFrontier).

Tag 0DKU, a situation

Tag 0DKU in the Stacks Project.

AlgebraicGeometry.Space.RelativeDescentSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativelyPerfect.lean, line 39.

A directed inverse system of quasi-compact, quasi-separated algebraic spaces with affine transition morphisms, together with its limit, a flat algebraic space of finite presentation over one chosen stage, and the base changes of that space to every later stage and to the limit.

structure RelativeDescentSituation (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (hZ : B.Contains (⊤_ Scheme.{u})) (I : Type v) [Preorder I]
    [IsDirected I (· ≤ ·)]

Tag 0DKV, a lemma

Tag 0DKV in the Stacks Project.

AlgebraicGeometry.Space.RelativeDescentSituation.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativelyPerfectHomDescent.lean, line 293. The attribute's comment: “the restriction of Situation 0DKU along a flat morphism of finite presentation, a step the tag's proof needs and which this development lacked; stated for flat plus finite presentation rather than étale, which is strictly more general. The tag's own conclusion is not proved here”.

The restriction of a relative descent situation along a flat finitely presented morphism g : U₀ ⟶ X₀: the inverse system, its limit and the chosen stage are unchanged, U₀ replaces X₀ with structure morphism g ≫ p₀, and the base changes are the fibre products Xᵢ ×_{X₀} U₀ and X ×_{X₀} U₀.

def restrict {U₀ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hU₀ : IsAlgebraicSpace B S hS U₀)
    (g : U₀ ⟶ D.X₀) (hgflat : IsFlat B S hS g)
    (hgfp : IsFinitePresentation B S hS g) : RelativeDescentSituation B S hS hZ I

AlgebraicGeometry.Space.RelativeDescentSituation.homDescent_iff_isIso_colimitDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativelyPerfectHomDescent.lean, line 478. The attribute's comment: “the tag's conclusion reformulated: the elementary descent statement holds exactly when the canonical colimit comparison map is invertible”.

HomDescent holds exactly when the canonical map from the colimit of the system of derived homomorphism sets to Hom_{D(𝒪_X)}(K, L) is an isomorphism.

theorem homDescent_iff_isIso_colimitDesc [HasColimit (D.homFunctor P K₀ L₀)] :
    D.HomDescent P K₀ L₀ ↔
      IsIso (colimit.desc (D.homFunctor P K₀ L₀) (D.homCocone P K₀ L₀))

AlgebraicGeometry.Space.RelativeDescentSituation.isIso_colimitDesc_homCocone_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativelyPerfectHomDescentFinal.lean, line 80. The attribute's comment: “the full statement; the condition D.IsSchemeLimit on the limit cone is the meaning of Y = lim Y_i in Situation 0DKU, the limit of algebraic spaces of Stacks 07SF, which the presheaf limit cone of RelativeDescentSituation does not record by itself (see the module documentation of RelativeDescentSchemeLimit for a situation where the presheaf limit is empty and the conclusion fails); it holds automatically for small index sets, see isIso_colimitDesc_homCocone_of_isPseudoCoherent_of_mk_lt and isIso_colimitDesc_homCocone_of_isPseudoCoherent_of_countable”.

Stacks 0DKV. In Situation 0DKU, with Y = lim Yᵢ the limit of algebraic spaces of Stacks 07SF (a limit of schemes on affine charts), let K₀, L₀ be objects of D(𝒪_{X₀}) with K₀ pseudo-coherent and L₀ ∈ D_QCoh(𝒪_{X₀}) locally of finite Tor dimension as an object of D((X₀ → Y₀)⁻¹𝒪_{Y₀}). Then the comparison map colim_{i ≥ 0} Hom_{D(𝒪_{Xᵢ})}(Lf_{i0}^*K₀, Lf_{i0}^*L₀) ⟶ Hom_{D(𝒪_X)}(Lf₀^*K₀, Lf₀^*L₀) is an isomorphism.

theorem isIso_colimitDesc_homCocone_of_isPseudoCoherent
    (D : RelativeDescentSituation B S hS hZ I) (hD : D.IsSchemeLimit)
    (K₀ L₀ : derivedModules B S hS D.initialSource) (hK₀ : IsPseudoCoherentObject K₀)
    (hL₀ : IsInQuasicoherentDerived D.initialSource L₀)
    (hL₀tor : HasLocallyFiniteTorDimensionAlong D.initialStructure L₀) :
    IsIso (colimit.desc (D.homFunctor (DerivedPullbackComposition.canonical B S hS) K₀ L₀)
      (D.homCocone (DerivedPullbackComposition.canonical B S hS) K₀ L₀))

AlgebraicGeometry.Space.RelativeDescentSituation.isIso_colimitDesc_homCocone_of_isPseudoCoherent_of_mk_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativelyPerfectHomDescentFinal.lean, line 101. The attribute's comment: “the full statement for every directed index set I with #I below the cofinality of the size cutoff of the site, with no condition on the limit: the limit of presheaves of RelativeDescentSituation is then the limit of algebraic spaces of Stacks 07SF (isSchemeLimit_of_size)”.

Stacks 0DKV for a small index set. In Situation 0DKU indexed by a directed set with fewer elements than the cofinality of the size cutoff of the site, let K₀, L₀ be objects of D(𝒪_{X₀}) with K₀ pseudo-coherent and L₀ ∈ D_QCoh(𝒪_{X₀}) locally of finite Tor dimension as an object of D((X₀ → Y₀)⁻¹𝒪_{Y₀}). Then the comparison map colim_{i ≥ 0} Hom_{D(𝒪_{Xᵢ})}(Lf_{i0}^*K₀, Lf_{i0}^*L₀) ⟶ Hom_{D(𝒪_X)}(Lf₀^*K₀, Lf₀^*L₀) is an isomorphism. No condition on the limit is needed: for such index sets the limit of presheaves is the limit of algebraic spaces of Stacks 07SF.

theorem isIso_colimitDesc_homCocone_of_isPseudoCoherent_of_mk_lt
    (D : RelativeDescentSituation B S hS hZ I) (hI : #I < B.cutoff.ord.cof)
    (K₀ L₀ : derivedModules B S hS D.initialSource) (hK₀ : IsPseudoCoherentObject K₀)
    (hL₀ : IsInQuasicoherentDerived D.initialSource L₀)
    (hL₀tor : HasLocallyFiniteTorDimensionAlong D.initialStructure L₀) :
    IsIso (colimit.desc (D.homFunctor (DerivedPullbackComposition.canonical B S hS) K₀ L₀)
      (D.homCocone (DerivedPullbackComposition.canonical B S hS) K₀ L₀))

AlgebraicGeometry.Space.RelativeDescentSituation.isIso_colimitDesc_homCocone_of_isPseudoCoherent_of_countable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RelativelyPerfectHomDescentFinal.lean, line 119. The attribute's comment: “the full statement for every countable directed index set, on every big fppf site, with no condition on the limit”.

Stacks 0DKV for a countable index set. In Situation 0DKU indexed by a countable directed set, on any big fppf site, let K₀, L₀ be objects of D(𝒪_{X₀}) with K₀ pseudo-coherent and L₀ ∈ D_QCoh(𝒪_{X₀}) locally of finite Tor dimension as an object of D((X₀ → Y₀)⁻¹𝒪_{Y₀}). Then the comparison map colim_{i ≥ 0} Hom_{D(𝒪_{Xᵢ})}(Lf_{i0}^*K₀, Lf_{i0}^*L₀) ⟶ Hom_{D(𝒪_X)}(Lf₀^*K₀, Lf₀^*L₀) is an isomorphism. The size cutoff of every big fppf site has uncountable cofinality.

theorem isIso_colimitDesc_homCocone_of_isPseudoCoherent_of_countable [Countable I]
    (D : RelativeDescentSituation B S hS hZ I)
    (K₀ L₀ : derivedModules B S hS D.initialSource) (hK₀ : IsPseudoCoherentObject K₀)
    (hL₀ : IsInQuasicoherentDerived D.initialSource L₀)
    (hL₀tor : HasLocallyFiniteTorDimensionAlong D.initialStructure L₀) :
    IsIso (colimit.desc (D.homFunctor (DerivedPullbackComposition.canonical B S hS) K₀ L₀)
      (D.homCocone (DerivedPullbackComposition.canonical B S hS) K₀ L₀))

Tag 0DKW, a lemma

Tag 0DKW in the Stacks Project.

AlgebraicGeometry.Space.RelativeDescentSituation.relativelyPerfectColimit_proved, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/RepresentedHomotopyPullbackCoherenceConsequences.lean, line 56.

In Situation 0DKU (indexed by a directed preorder I in Type u), whose limit is a limit of schemes on affine charts (the standing meaning of Y = lim Yᵢ, AlgebraicGeometry.Space.RelativeDescentSituation.IsSchemeLimit), the category of Y-perfect objects of D(𝒪_X) is the colimit of the categories of Yᵢ-perfect objects of D(𝒪_{Xᵢ}), in the five clauses of AlgebraicGeometry.Space.RelativeDescentSituation.RelativelyPerfectColimit.

theorem relativelyPerfectColimit_proved (D : RelativeDescentSituation B S hS hZ I) :
    D.RelativelyPerfectColimit

Tag 0DKX, a lemma

Tag 0DKX in the Stacks Project.

AlgebraicGeometry.Space.isPerfect_derivedPushforward_and_isIso_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDerivedHomDualProved.lean, line 111.

Stacks 0DKX. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat, proper and of finite presentation, and let E ∈ D(𝒪_X) be Y-perfect (Stacks 0DKN). Then Rf_*E is a perfect object of D(𝒪_Y), and its formation commutes with arbitrary base change: for every cartesian square
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
the base change map Lg^*Rf_*E ⟶ Rf'_*L(g')^*E (Stacks 07A7) is an isomorphism.

theorem isPerfect_derivedPushforward_and_isIso_baseChange
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hproper : IsProper B S hS f.hom)
    (hflat : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (E : derivedModules B S hS X) (hE : IsPerfectRelativeToCanonical B S hS f hflat hfp.1 E) :
    (smallEtaleRingedSite B S hS Y.1 Y.2).IsPerfect ((spaceDerivedPushforward B S hS f).obj E) ∧
      ∀ {X' Y' : AlgebraicSpaces B S hS} (g' : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y)
        (hpb : IsPullback g' f' f g),
        IsIso (smallEtaleDerivedModuleBaseChangeMap B S hS f g f' g' hpb.w E)

Tag 0DKY, a lemma

Tag 0DKY in the Stacks Project.

AlgebraicGeometry.Space.exists_isPseudoCoherent_pushforward_sheafHom_iso_dual, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDerivedHomDualProved.lean, line 153.

Stacks 0DKY. Let f : X ⟶ Y be a morphism of algebraic spaces over S, and let E, K be objects of D(𝒪_X). Assume that Y is quasi-compact and quasi-separated, that f is proper, flat and of finite presentation, that E is Y-perfect (Stacks 0DKN) and that K is pseudo-coherent. Then there is a pseudo-coherent L ∈ D(𝒪_Y) with Rf_* R𝓗om(K, E) ≅ R𝓗om(L, 𝒪_Y), and the same holds after arbitrary base change: for every cartesian square X' = X ×_Y Y' with projections g' : X' ⟶ X and f' : X' ⟶ Y', Rf'_* R𝓗om(L(g')^*K, L(g')^*E) ≅ R𝓗om(Lg^*L, 𝒪_{Y'}).

(hZ says that the site contains Spec ℤ, through which quasi-separatedness of Y is expressed.)

theorem exists_isPseudoCoherent_pushforward_sheafHom_iso_dual
    (hZ : B.Contains (⊤_ Scheme.{u})) {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hqc : IsQuasiCompactSpace B S hS Y.1) (hqs : IsAbsolutelyQuasiSeparated B S hS hZ Y.1)
    (hproper : IsProper B S hS f.hom) (hflat : IsFlat B S hS f.hom)
    (hfp : IsFinitePresentation B S hS f.hom) (K E : derivedModules B S hS X)
    (hE : IsPerfectRelativeToCanonical B S hS f hflat hfp.1 E)
    (hK : (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent K) :
    ∃ L : derivedModules B S hS Y, (smallEtaleRingedSite B S hS Y.1 Y.2).IsPseudoCoherent L ∧
      Nonempty ((spaceDerivedPushforward B S hS f).obj
          (((smallEtaleDerivedSheafHom B S hS X).obj (Opposite.op K)).obj E) ≅
        smallEtaleDerivedDual B S hS Y L) ∧
      ∀ {X' Y' : AlgebraicSpaces B S hS} (g' : X' ⟶ X) (f' : X' ⟶ Y') (g : Y' ⟶ Y),
        IsPullback g' f' f g →
        Nonempty ((spaceDerivedPushforward B S hS f').obj
            (((smallEtaleDerivedSheafHom B S hS X').obj
              (Opposite.op (((smallEtaleDerivedPullbackData B S hS).pull g').obj K))).obj
                (((smallEtaleDerivedPullbackData B S hS).pull g').obj E)) ≅
          smallEtaleDerivedDual B S hS Y'
            (((smallEtaleDerivedPullbackData B S hS).pull g).obj L))

Tag 0GFK, a lemma

Tag 0GFK in the Stacks Project.

AlgebraicGeometry.Space.isPerfectRelativeToCanonical_iff_isLocallyBoundedBelow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeFibrewiseBoundedBelow.lean, line 242.

Stacks 0GFK. Let f : X ⟶ T be a morphism from an algebraic space to a scheme which is flat and locally of finite presentation, and let E ∈ D(𝒪_X) be pseudo-coherent. Then E is T-perfect exactly when E is locally bounded below and, for every point s ∈ T, the derived pullback L(X_s ⟶ X)^*E to the fibre X_s = X ×_T Spec κ(s) is locally bounded below.

theorem isPerfectRelativeToCanonical_iff_isLocallyBoundedBelow (f : X ⟶ representedSpace T)
    (hfl : IsFlat B S hS f.hom) (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent E) :
    IsPerfectRelativeToCanonical.{u, u + 1, u + 1} B S hS f hfl hlfp E ↔
      IsLocallyBoundedBelow X E ∧ ∀ s : (BigFppfOver.toScheme B S hS).obj T,
        IsLocallyBoundedBelow (residueFibre f s)
          ((smallEtaleDerivedModulePullback B S hS (residueFibreι f s)).obj E)

Tag 0GFL, a lemma

Tag 0GFL in the Stacks Project.

AlgebraicGeometry.Space.QuasicoherentDerivedCategory.isPerfectRelativeToCanonical_of_isPerfect_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedChow/RelativePerfect.lean, line 304.

Let A be a ring and X an algebraic space separated, of finite presentation and flat over A. Let K ∈ D_QCoh(𝒪_X). If RΓ(X, E ⊗^𝐋 K) is perfect in D(A) for every perfect E ∈ D(𝒪_X), then K is Spec(A)-perfect.

Here K is an object of the full subcategory D_QCoh(𝒪_X) of D(𝒪_X) (Stacks 071X), and RΓ(X, -) with values in D(A) is RΓ(Spec A, Rf_*(-)) for the structure morphism f : X ⟶ Spec A.

theorem QuasicoherentDerivedCategory.isPerfectRelativeToCanonical_of_isPerfect_derivedSections
    {X : AlgebraicSpaces B (Spec (CommRingCat.of A)) hA}
    (hsep : IsSeparated B _ hA (toBase B _ hA X).hom)
    (hfp : IsFinitePresentation B _ hA (toBase B _ hA X).hom)
    (hfl : IsFlat B _ hA (toBase B _ hA X).hom)
    (K : QuasicoherentDerivedCategory.{u, u} B _ hA X.1 X.2)
    (h : ∀ E : DerivedCategory (Modules.{u, u} B _ hA X.1 X.2),
      (smallEtaleRingedSite B _ hA X.1 X.2).IsPerfect E →
        StacksDraft.Perfect.IsPerfect
          ((representedAffineDerivedSections B _ hA (baseSiteObj B _ hA)).obj
            ((derivedModulePushforward B _ hA (toBase B _ hA X)).obj
              (((smallEtaleDerivedTensor B _ hA X).obj E).obj K.obj)))) :
    IsPerfectRelativeToCanonical.{u, u + 1, u + 1} B _ hA (toBase B _ hA X) hfl hfp.1 K.obj

Sources

Section76.53 Theorem of the cube #

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

Tag 0D23, a lemma

Tag 0D23 in the Stacks Project.

AlgebraicGeometry.Space.exists_isImmersion_isFinitePresentation_factorsThrough_iff_hasDescentAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescentLocus/Theorem.lean, line 294.

Let f : X ⟶ Y be a flat, proper morphism of finite presentation of algebraic spaces over S, and E a finite locally free 𝒪_X-module. Assume that for every g : Y' ⟶ Y, with base change f' : X' = X ×_Y Y' ⟶ Y', the map 𝒪_{Y'} ⟶ f'_*𝒪_{X'} is an isomorphism. Then there is an immersion j : Z ⟶ Y of finite presentation such that a morphism g : Y' ⟶ Y factors through j exactly when there is a finite locally free 𝒪_{Y'}-module N with (f')^*N ≅ (g')^*E (AlgebraicGeometry.Space.HasDescentAt; the source's (g')^*L is a typo for (g')^*E).

theorem exists_isImmersion_isFinitePresentation_factorsThrough_iff_hasDescentAt
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hfl : IsFlat B S hS f.hom)
    (hP : IsProper B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (E : Modules.{u, u} B S hS X.1 X.2) (hE : SheafOfModules.IsFiniteLocallyFree E)
    (hiso : ∀ {Y' : AlgebraicSpaces B S hS} (g : Y' ⟶ Y),
      IsIso (structureSharp B S hS (pullback.snd f g))) :
    ∃ (Z : AlgebraicSpaces B S hS) (j : Z ⟶ Y),
      IsImmersion B S hS j.hom ∧ IsFinitePresentation B S hS j.hom ∧
      ∀ {Y' : AlgebraicSpaces B S hS} (g : Y' ⟶ Y),
        (∃ h : Y' ⟶ Z, h ≫ j = g) ↔ HasDescentAt f E g

Sources

LeanAlgebraicGeometry.Space.exists_isImmersion_isFinitePresentation_factorsThrough_iff_hasDescentAt

Section76.54 Descent of finiteness properties of complexes #

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

Tag 0DL1, a lemma

Tag 0DL1 in the Stacks Project.

AlgebraicGeometry.Space.isPseudoCoherentFrom_iff_forall_fpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/PseudoCoherentFpqcDescent.lean, line 156. The attribute's comment: “carries 08H4 for spaces, the 0D6D comparison and the scheme case as hypotheses”.

Stacks 0DL1. Let {f_i : X_i ⟶ X} be an fpqc covering of algebraic spaces over a scheme S, let E be an object of D_QCoh(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent if and only if every derived pullback Lf_i^*E is.

The forward implication is pullback preservation of m-pseudo-coherence. For the converse, Stacks 0419 refines the covering by morphisms e_i : T_i ⟶ X_i out of schemes of the site with {e_i ≫ f_i} again an fpqc covering; the derived pullback along e_i ≫ f_i is Le_i^* of Lf_i^*E, which is m-pseudo-coherent by pullback preservation, and the refined covering has scheme sources, so the case of schemes applies.

theorem isPseudoCoherentFrom_iff_forall_fpqcCovering
    (hL : BottomRankStratum.HasDerivedModulePullbacks B S hS)
    (hpull : DerivedPullbackPreservesPseudoCoherence B S hS hL)
    (hcomp : HasDerivedModulePullbackCompIso B S hS hL)
    (hschemes : FpqcDescentOfPseudoCoherenceOnSchemes.{u, v} B S hS hL)
    {I : Type v} {X : AlgebraicSpaces B S hS} {Xi : I → AlgebraicSpaces B S hS}
    (f : ∀ i, Xi i ⟶ X) (hf : IsFpqcCovering B S hS fun i => (f i).hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : ∀ n : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS X.1 X.2) n).obj E).IsQuasicoherentOnSite)
    (m : ℤ) :
    (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherentFrom E m ↔
      ∀ i, haveI := hL (f i)
        (smallEtaleRingedSite B S hS (Xi i).1 (Xi i).2).IsPseudoCoherentFrom
          ((smallEtaleDerivedModulePullback B S hS (f i)).obj E) m

AlgebraicGeometry.Space.isPseudoCoherentFrom_iff_forall_derivedPullback_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PseudoCoherent/FpqcDescent.lean, line 461.

Stacks 0DL1. Let {f_i : X_i ⟶ X} be an fpqc covering of algebraic spaces over a scheme S, let E be an object of D_QCoh(𝒪_X) and let m be an integer. Then E is m-pseudo-coherent if and only if each Lf_i^*E is m-pseudo-coherent.

The forward implication is AlgebraicGeometry.Space.isPseudoCoherentFrom_smallEtaleDerivedModulePullback. For the converse, Stacks 0419 refines the covering by morphisms e_i : T_i ⟶ X_i out of schemes of the site with {e_i ≫ f_i} again an fpqc covering; L(e_i ≫ f_i)^*E ≅ Le_i^*(Lf_i^*E) (Stacks 0D6D) is m-pseudo-coherent by the forward implication, as Lf_i^*E has quasi-coherent cohomology (Stacks 08F4), and AlgebraicGeometry.Space.isPseudoCoherentFrom_of_isFpqcCovering_representable applies.

theorem isPseudoCoherentFrom_iff_forall_derivedPullback_of_isFpqcCovering {I : Type v}
    {X : AlgebraicSpaces B S hS} {Xi : I → AlgebraicSpaces B S hS}
    (f : ∀ i, Xi i ⟶ X) (hf : IsFpqcCovering B S hS fun i => (f i).hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : ∀ n : ℤ, ((DerivedCategory.homologyFunctor
      (Modules.{u, u} B S hS X.1 X.2) n).obj E).IsQuasicoherentOnSite)
    (m : ℤ) :
    (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherentFrom E m ↔
      ∀ i, (smallEtaleRingedSite B S hS (Xi i).1 (Xi i).2).IsPseudoCoherentFrom
        ((smallEtaleDerivedModulePullback B S hS (f i)).obj E) m

Tag 0DL2, a lemma

Tag 0DL2 in the Stacks Project.

AlgebraicGeometry.Space.hasTorAmplitudeCanonical_etaleStalk_iff_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeTorAmplitudeFpqcDescent.lean, line 365. The attribute's comment: “tor amplitude in [a, b], at a geometric point”.

Stacks 0DL2, the clause on Tor amplitude in [a, b], at a geometric point.

Let
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
be a cartesian square of algebraic spaces whose two morphisms to the base are Tor independent, let x̄' be a geometric point of the upper-left corner, with images x̄ in X, ȳ' in Y' and ȳ in Y, and suppose that the canonical homomorphism 𝒪_{Y, ȳ} → 𝒪_{Y', ȳ'} of étale local rings of Stacks 04NG is faithfully flat — which for a member of an fpqc covering it is, being flat by Stacks 04NG and local. Then an object E of D(𝒪_{X, x̄}) has Tor amplitude in [a, b] over 𝒪_{Y, ȳ} if and only if its derived base change to 𝒪_{X, x̄} ⊗_{𝒪_{Y, ȳ}} 𝒪_{Y', ȳ'} has Tor amplitude in [a, b] over 𝒪_{Y', ȳ'}.

This is the source's own proof read at the geometric stalks, where the source reads it: a relative Tor-amplitude bound is a bound on the stalk complexes over the étale local rings of the base (Stacks 0DJJ and 04K5), the stalk of L(g')^* E is the derived base change of the stalk of E, Tor independence identifies that derived base change over 𝒪_{X, x̄} with the derived base change over 𝒪_{Y, ȳ} by Stacks 0661, and the bound descends along the faithfully flat 𝒪_{Y, ȳ} → 𝒪_{Y', ȳ'} by Stacks 068S. The forward implication is Stacks 0DKD (1) at the tensor product.

theorem hasTorAmplitudeCanonical_etaleStalk_iff_of_cartesian
    {X' X Y' Y : AlgebraicSpaces B S hS} (g' : X' ⟶ X) (f' : X' ⟶ Y')
    (f : X ⟶ Y) (g : Y' ⟶ Y) (hpb : IsPullback g' f' f g)
    (htor : TorIndependent X.2 Y'.2 Y.2 f.hom g.hom)
    (x' : GeometricPoint B S hS X'.1)
    (E : DerivedCategory (ModuleCat.{u + 1}
      ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x')))) (a b : ℤ) :
    letI : Algebra
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x')) :=
      (etaleLocalRingMap X.2 f.hom (geometricPointMap g'.hom x')).toAlgebra
    letI : Algebra
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) :=
      ((eqToHom (congrArg (etaleLocalRing B S hS Y.1)
          (congrArg (fun k : X' ⟶ Y => geometricPointMap k.hom x') hpb.w)) ≫
        CommRingCat.ofHom
          (etaleLocalRingMap Y'.2 g.hom (geometricPointMap f'.hom x'))).hom).toAlgebra
    Module.FaithfullyFlat
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) →
    letI T := TensorProduct
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x'))
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x'))
    letI : Algebra ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) T :=
      Algebra.TensorProduct.rightAlgebra
    (HasTorAmplitudeCanonical
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ((ModuleCat.restrictScalars
          (etaleLocalRingMap X.2 f.hom
            (geometricPointMap g'.hom x'))).mapDerivedCategory.obj E) a b ↔
      HasTorAmplitudeCanonical ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x'))
        ((ModuleCat.restrictScalars (algebraMap
            ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) T)).mapDerivedCategory.obj
          ((totalDerivedExtensionScalars.{u + 1, u + 1, u + 1} (algebraMap
            ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x')) T)).functor.obj E))
        a b)

AlgebraicGeometry.Space.hasFiniteTorDimensionCanonical_etaleStalk_iff_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeTorAmplitudeFpqcDescent.lean, line 448. The attribute's comment: “finite tor dimension, at a geometric point”.

Stacks 0DL2, the clause on finite Tor dimension, at a geometric point.

Under the hypotheses of hasTorAmplitudeCanonical_etaleStalk_iff_of_cartesian, an object E of D(𝒪_{X, x̄}) has finite Tor dimension over 𝒪_{Y, ȳ} if and only if its derived base change to 𝒪_{X, x̄} ⊗_{𝒪_{Y, ȳ}} 𝒪_{Y', ȳ'} has finite Tor dimension over 𝒪_{Y', ȳ'}. Finite Tor dimension is Tor amplitude in some interval, so this is the previous statement for each interval separately — the "elementary topology" with which the source reduces the second clause of the lemma to the first.

theorem hasFiniteTorDimensionCanonical_etaleStalk_iff_of_cartesian
    {X' X Y' Y : AlgebraicSpaces B S hS} (g' : X' ⟶ X) (f' : X' ⟶ Y')
    (f : X ⟶ Y) (g : Y' ⟶ Y) (hpb : IsPullback g' f' f g)
    (htor : TorIndependent X.2 Y'.2 Y.2 f.hom g.hom)
    (x' : GeometricPoint B S hS X'.1)
    (E : DerivedCategory (ModuleCat.{u + 1}
      ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x')))) :
    letI : Algebra
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x')) :=
      (etaleLocalRingMap X.2 f.hom (geometricPointMap g'.hom x')).toAlgebra
    letI : Algebra
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) :=
      ((eqToHom (congrArg (etaleLocalRing B S hS Y.1)
          (congrArg (fun k : X' ⟶ Y => geometricPointMap k.hom x') hpb.w)) ≫
        CommRingCat.ofHom
          (etaleLocalRingMap Y'.2 g.hom (geometricPointMap f'.hom x'))).hom).toAlgebra
    Module.FaithfullyFlat
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) →
    letI T := TensorProduct
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x'))
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x'))
    letI : Algebra ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) T :=
      Algebra.TensorProduct.rightAlgebra
    (HasFiniteTorDimensionCanonical
        ↥(etaleLocalRing B S hS Y.1 (geometricPointMap f.hom (geometricPointMap g'.hom x')))
        ((ModuleCat.restrictScalars
          (etaleLocalRingMap X.2 f.hom
            (geometricPointMap g'.hom x'))).mapDerivedCategory.obj E) ↔
      HasFiniteTorDimensionCanonical
        ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x'))
        ((ModuleCat.restrictScalars (algebraMap
            ↥(etaleLocalRing B S hS Y'.1 (geometricPointMap f'.hom x')) T)).mapDerivedCategory.obj
          ((totalDerivedExtensionScalars.{u + 1, u + 1, u + 1} (algebraMap
            ↥(etaleLocalRing B S hS X.1 (geometricPointMap g'.hom x')) T)).functor.obj E)))

AlgebraicGeometry.Space.locallyHasFiniteTorDimension_derivedScalarRestriction_iff_forall_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeTorAmplitudeFpqcDescentLocal.lean, line 658. The attribute's comment: “locally finite tor dimension”.

Stacks 0DL2, locally finite Tor dimension.

theorem locallyHasFiniteTorDimension_derivedScalarRestriction_iff_forall_of_isFpqcCovering
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) :
    LocallyHasFiniteTorDimension.{u + 1, u, u, u + 1}
      (fun U => Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u + 1, u, u + 1}
        ((inverseImageRingedSite B S hS f).over U))
      ((derivedScalarRestriction B S hS f).obj E) ↔
      ∀ i, LocallyHasFiniteTorDimension.{u + 1, u, u, u + 1}
      (fun U => Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u + 1, u, u + 1}
        ((inverseImageRingedSite B S hS (f' i)).over U))
      ((derivedScalarRestriction B S hS (f' i)).obj
        ((smallEtaleDerivedModulePullback B S hS (g' i)).obj E))

AlgebraicGeometry.Space.hasTorAmplitude_derivedScalarRestriction_iff_forall_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativeTorAmplitudeFpqcDescentSheaf.lean, line 228. The attribute's comment: “tor amplitude in [a, b]”.

Let {g_i : Y_i ⟶ Y} be an fpqc covering of algebraic spaces over S, let f : X ⟶ Y be a morphism of algebraic spaces and let X_i = Y_i ×_Y X, with projections f_i : X_i ⟶ Y_i and g'_i : X_i ⟶ X. An object E of D(𝒪_X) has Tor amplitude in [a, b] as an object of D(f⁻¹𝒪_Y) if and only if every L(g'_i)^* E has Tor amplitude in [a, b] as an object of D(f_i⁻¹𝒪_{Y_i}), both measured against the derived tensor product of Stacks 06YU.

theorem hasTorAmplitude_derivedScalarRestriction_iff_forall_of_isFpqcCovering
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2)) (a b : ℤ) :
    Stacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitude.{u + 1, u, u, u + 1}
        (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u + 1, u, u + 1}
          (inverseImageRingedSite B S hS f)) ((derivedScalarRestriction B S hS f).obj E) a b ↔
      ∀ i, Stacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitude.{u + 1, u, u, u + 1}
        (Stacks.SheafOfModules.canonicalDerivedTensorProduct.{u + 1, u, u + 1}
          (inverseImageRingedSite B S hS (f' i)))
        ((derivedScalarRestriction B S hS (f' i)).obj
          ((smallEtaleDerivedModulePullback B S hS (g' i)).obj E)) a b

Tag 0DL3, a lemma

Tag 0DL3 in the Stacks Project.

AlgebraicGeometry.Space.isPseudoCoherent_of_derivedPullback_of_isFiniteOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PseudoCoherent/Thickening.lean, line 135.

Stacks 0DL3. Let S be a scheme and let i : Z ⟶ X' be a finite-order thickening of algebraic spaces over S. Let K' be an object of D(𝒪_{X'}) such that K = Li^*K' is pseudo-coherent. Then K' is pseudo-coherent.

The thickening is the inclusion AlgebraicGeometry.Space.subspaceInclusion of a closed subspace Z of X' which is a finite-order thickening (Stacks 05ZK), Li^* is the derived pullback of Stacks 06YY along it, and pseudo-coherence is Stacks 08FT on the small étale ringed sites.

theorem isPseudoCoherent_of_derivedPullback_of_isFiniteOrderThickening
    {X' : AlgebraicSpaces B S hS} (Z : ClosedSubspaces B S hS X'.1)
    (hZ : IsFiniteOrderThickening B S hS X' Z.1)
    (K' : DerivedCategory (Modules.{u, u} B S hS X'.1 X'.2))
    (hK :
      haveI := hasLeftDerivedFunctor_smallEtaleModulePullbackOnHomotopy B S hS
        (subspaceInclusion B S hS X' Z)
      (smallEtaleRingedSite B S hS Z.1.toFunctor Z.2.1).IsPseudoCoherent
        ((smallEtaleDerivedModulePullback B S hS (subspaceInclusion B S hS X' Z)).obj K')) :
    (smallEtaleRingedSite B S hS X'.1 X'.2).IsPseudoCoherent K'

Tag 0DL4, a lemma

Tag 0DL4 in the Stacks Project.

AlgebraicGeometry.Space.isPerfectRelativeToCanonical_of_pull_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ComplexesStackThickeningPerfectProved.lean, line 130.

Consider a cartesian square
X --i--> X'
|f       |f'
v        v
Y --j--> Y'
of algebraic spaces over S. Assume f' is flat and locally of finite presentation and j is a finite-order thickening: j is an isomorphism onto its range, which is a finite-order thickening of Y' (Stacks 05ZK). Let E' ∈ D(𝒪_{X'}). If E = Li^*E' is Y-perfect (Stacks 0DKN), then E' is Y'-perfect.

theorem isPerfectRelativeToCanonical_of_pull_of_isThickeningHom
    {X X' Y Y' : AlgebraicSpaces B S hS} {i : X ⟶ X'} {f : X ⟶ Y} {f' : X' ⟶ Y'} {j : Y ⟶ Y'}
    (hpb : IsPullback i f f' j) (hj : IsThickeningHom B S hS j)
    (hjfin : IsFiniteOrderThickening B S hS Y' (Subfunctor.range j.hom))
    (hflat : IsFlat B S hS f'.hom) (hlfp : IsLocallyOfFinitePresentation B S hS f'.hom)
    (E' : derivedModules B S hS X')
    (hE : IsPerfectRelativeToCanonical B S hS f
      ((isFlat_isStableUnderBaseChange B S hS).of_isPullback hpb hflat)
      ((isLocallyOfFinitePresentation_isStableUnderBaseChange B S hS).of_isPullback hpb
        hlfp)
      (((smallEtaleDerivedPullbackData B S hS).pull i).obj E')) :
    IsPerfectRelativeToCanonical B S hS f' hflat hlfp E'

Tag 0DL5, a lemma

Tag 0DL5 in the Stacks Project.

AlgebraicGeometry.Space.isRelativelyPerfect_of_isRelativelyPerfect_closedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativelyPerfectClosedFibre.lean, line 638.

Stacks 0DL5. Let (R, I) be a ring with an ideal contained in its Jacobson radical, let 𝒮 = Spec R and 𝒮₀ = Spec (R/I), and let f : X ⟶ 𝒮 be a proper and flat morphism of algebraic spaces, locally of finite presentation (hence of finite presentation, f being proper). Let X₀ = 𝒮₀ ×_𝒮 X, with projections i : X₀ ⟶ X and f₀ : X₀ ⟶ 𝒮₀. If a pseudo-coherent object E of D(𝒪_X) has 𝒮₀-perfect derived restriction Li^*E to X₀, then E is 𝒮-perfect.

On an affine étale chart Spec A ⟶ X, presented by d variables over R, E is ε^*(P~) for a bounded above complex P of finite free A-modules, and Li^*E is ε^*((P ⊗_R R/I)~) on the closed fibre of the chart. One interval [a, b] bounds the Tor amplitude of the geometric stalks of Li^*E on the quasi-compact X₀, and then [a - d, b] bounds those of E over the stalks of f⁻¹𝒪_𝒮 (hasTorAmplitudeCanonical_geometricStalk_of_closedFibre); a uniform bound at the geometric stalks gives locally finite Tor dimension (Stacks 0DJJ, 04K5).

X₀ is the fibre product in the category of algebraic spaces; flatness and local finite presentation of f₀, the preconditions of 𝒮₀-perfectness (Stacks 0DKN), are those of f by base change.

theorem isRelativelyPerfect_of_isRelativelyPerfect_closedFibre
    (hI : I ≤ (⊥ : Ideal R).jacobson) (i : X₀ ⟶ X)
    (hpb : IsPullback i f₀ f (representedSpaceMap B S hS (quotientSpecMap B S hS hR gR I hR₀)))
    (hproper : IsProper B S hS f.hom) (hflat : IsFlat B S hS f.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent E)
    (hE₀ : haveI := hasLeftDerivedFunctor_smallEtaleModulePullbackOnHomotopy B S hS i
      IsRelativelyPerfect B S hS f₀ (isFlat_snd_of_isPullback B S hS hpb hflat)
        (isLocallyOfFinitePresentation_snd_of_isPullback B S hS hpb hlfp)
        ((smallEtaleDerivedModulePullback B S hS i).obj E)) :
    IsRelativelyPerfect B S hS f hflat hlfp E

AlgebraicGeometry.Space.isPerfectRelativeTo_of_isPerfectRelativeTo_closedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/RelativelyPerfectJacobsonFibre.lean, line 258. The attribute's comment: “the pseudo-coherence clause and the specialization step; Tor clause carried”.

Stacks 0DL5. Let (R, I) be a ring with an ideal contained in its Jacobson radical, let 𝒮 = Spec R and 𝒮₀ = Spec (R/I), let f : X ⟶ 𝒮 be a proper, flat, locally finitely presented morphism of algebraic spaces and let X₀ = 𝒮₀ ×_𝒮 X. A pseudo-coherent object E of D(𝒪_X) whose derived restriction to X₀ is 𝒮₀-perfect is 𝒮-perfect.

The pseudo-coherence clause of the conclusion is the hypothesis on E. For the Tor clause, properness makes |X| → |𝒮| closed and the ideal I lying in the Jacobson radical makes every nonempty closed subset of |𝒮| meet |𝒮₀|, so every point of |X| specializes into the closed fibre; from there the bound is hTor.

theorem isPerfectRelativeTo_of_isPerfectRelativeTo_closedFibre (i : X₀ ⟶ X) (j : 𝒮₀ ⟶ 𝒮)
    [(smallEtaleModulePullbackOnHomotopy B S hS i).HasLeftDerivedFunctor
      (smallEtaleModuleQuasiIso B S hS X)]
    (hflat : IsFlat B S hS f.hom) (hlfp : IsLocallyOfFinitePresentation B S hS f.hom)
    (hflat₀ : IsFlat B S hS f₀.hom) (hlfp₀ : IsLocallyOfFinitePresentation B S hS f₀.hom)
    (T : ∀ U : (inverseImageRingedSite B S hS f).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f).over U))
    (T₀ : ∀ U : (inverseImageRingedSite B S hS f₀).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, u, e}
        ((inverseImageRingedSite B S hS f₀).over U))
    {R : Type u} [CommRing R] {I : Ideal R} (hI : I ≤ (⊥ : Ideal R).jacobson)
    (eR : points B S hS 𝒮.1 ≃ₜ PrimeSpectrum R)
    (hj : Set.range (pointsMap B S hS 𝒮₀.1 j.hom) =
      eR ⁻¹' PrimeSpectrum.zeroLocus (I : Set R))
    (hproper : IsProper B S hS f.hom) (_hpb : IsPullback i f₀ f j)
    (hTor : LocallyFiniteTorDimensionFromClosedFibre B S hS f f₀ i j hflat₀ hlfp₀ T T₀)
    (E : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hE : (smallEtaleRingedSite B S hS X.1 X.2).IsPseudoCoherent E)
    (hE₀ : IsPerfectRelativeTo B S hS f₀ hflat₀ hlfp₀ T₀
      ((smallEtaleDerivedModulePullback B S hS i).obj E)) :
    IsPerfectRelativeTo B S hS f hflat hlfp T E

Sources

Section76.55 Families of nodal curves #

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

Tag 0DSE, a definition

Tag 0DSE in the Stacks Project.

AlgebraicGeometry.Space.IsAtWorstNodalOfRelativeDimensionOne, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Nodal.lean, line 71.

Stacks 0DSE. A morphism of algebraic spaces over S is at-worst-nodal of relative dimension one when every commuting square of étale scheme charts induces a scheme morphism which is at-worst-nodal of relative dimension one.

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

Tag 0DSF, a lemma

Tag 0DSF in the Stacks Project.

AlgebraicGeometry.Space.isAtWorstNodalOfRelativeDimensionOne_isStableUnderBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Nodal.lean, line 80.

Stacks 0DSF. Being at-worst-nodal of relative dimension one is preserved by base change of morphisms of algebraic spaces over S.

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

Tag 0DSG, a lemma

Tag 0DSG in the Stacks Project.

AlgebraicGeometry.Space.isAtWorstNodalOfRelativeDimensionOne_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/PseudoCoherent/Nodal.lean, line 97.

Stacks 0DSG. Eight criteria for a morphism of algebraic spaces over S to be at-worst-nodal of relative dimension one: the condition may be tested after base change to every scheme or to every affine scheme, on one surjective étale chart of the target, on the composite with one surjective étale chart of the source, in every or in one surjective commuting square of étale charts, or over a pair of Zariski coverings.

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

Tag 0DSH, a lemma

Tag 0DSH in the Stacks Project.

AlgebraicGeometry.Space.exists_isGreatest_isNodalOpen_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/NodalOpenSubspace.lean, line 558.

Stacks 0DSH. Let S be a scheme and let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat and locally of finite presentation. Then there is a maximal open subspace X' ⊆ X such that the restriction of f to X' is at-worst-nodal of relative dimension one, and formation of X' commutes with arbitrary base change.

The maximal open subspace is AlgebraicGeometry.Space.nodalOpenSubspace; it is an open subspace on which the restriction of f is at-worst-nodal of relative dimension one, and it contains every open subspace with that property, which is the content of the IsGreatest assertion. The second assertion is that for an arbitrary morphism g : Y' ⟶ Y of algebraic spaces over S, the locus of the base change X ×_Y Y' ⟶ Y' of f along g is the inverse image of the locus of f under the projection to X.

theorem exists_isGreatest_isNodalOpen_baseChange {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hflat : IsFlat B S hS f) (hfp : IsLocallyOfFinitePresentation B S hS f) :
    IsGreatest {W : Subfunctor X | IsNodalOpen B S hS f W} (nodalOpenSubspace B S hS f) ∧
      ∀ Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS Y' →
        ∀ g : Y' ⟶ Y, nodalOpenSubspace B S hS (pullback.snd f g) =
          (nodalOpenSubspace B S hS f).preimage (pullback.fst f g)

Sources

LeanAlgebraicGeometry.Space.IsAtWorstNodalOfRelativeDimensionOne · AlgebraicGeometry.Space.isAtWorstNodalOfRelativeDimensionOne_isStableUnderBaseChange · AlgebraicGeometry.Space.isAtWorstNodalOfRelativeDimensionOne_tfae · AlgebraicGeometry.Space.exists_isGreatest_isNodalOpen_baseChange

Section76.56 The resolution property #

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

Tag 0GUY, a situation

Tag 0GUY in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_isSurjective_isEtale_of_isQuasiCompactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyDescentSituation.lean, line 111. The attribute's comment: “the existence of the affine surjective étale chart of the situation”.

Stacks 0GUY, the existence of the chart V → X. A quasi-compact algebraic space over S admits a surjective étale morphism from an affine scheme of the site, surjectivity being the point-set notion of Stacks 03ME.

This is the parenthetical claim of the source that such a chart exists: Stacks 03H6 gives a chart whose every represented base change is a surjective morphism of schemes, and Stacks 03H5 identifies that with surjectivity on points.

theorem exists_affine_isSurjective_isEtale_of_isQuasiCompactSpace
    (X : AlgebraicSpaces B S hS) (hX : IsQuasiCompactSpace B S hS X.1) :
    ∃ (V : BigFppfOver B S hS) (φ : yoneda.obj V ⟶ X.1),
      IsAffine ((BigFppfOver.toScheme B S hS).obj V) ∧
        IsSurjective B S hS φ ∧ IsEtale B S hS φ

AlgebraicGeometry.Space.ResolutionPropertyDescentSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyDescentSituation.lean, line 130. The attribute's comment: “the data chosen in the situation, and the conditions imposed on it”.

Stacks 0GUY. The choices fixed in the situation of the source for a quasi-compact and quasi-separated algebraic space X over S: an affine scheme V of the site with a surjective étale morphism φ : V → X, a factorization of φ into an open immersion j : V → Y into an algebraic space Y followed by a finite morphism π : Y → X, and a finite type quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_Y with |V(ℐ)| = |Y| ∖ |j(V)|.

A chart V as in the first clause exists by AlgebraicGeometry.Space.exists_affine_isSurjective_isEtale_of_isQuasiCompactSpace.

structure ResolutionPropertyDescentSituation (X : AlgebraicSpaces B S hS)
    (hqc : IsQuasiCompactSpace B S hS X.1)
    (hqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)

Tag 0GUZ, a lemma

Tag 0GUZ in the Stacks Project.

AlgebraicGeometry.Space.exists_epi_biproduct_idealSheafPowPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ResolutionPropertySurjection.lean, line 218.

Stacks 0GUZ. In the situation of Stacks 0GUY — a quasi-compact and quasi-separated algebraic space X, a surjective étale φ : V ⟶ X from an affine scheme factored as an open immersion j : V ⟶ Y followed by a finite π : Y ⟶ X, and a finite type quasi-coherent sheaf of ideals ℐ ⊆ 𝒪_Y with V(ℐ) = Y ∖ j(V) — assume X Noetherian. Then every coherent 𝒪_X-module ℱ admits, for some r ≥ 0 and integers n_1, …, n_r ≥ 0, a surjection

⨁_{i = 1}^{r} π_*(ℐ^{n_i}) ⟶ ℱ

of 𝒪_X-modules. This is AlgebraicGeometry.Space.exists_epi_biproduct_idealSheafPowPushforward_of_le at N = 0.

theorem exists_epi_biproduct_idealSheafPowPushforward (hX : IsNoetherian B S hS hZ X.1)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F) :
    ∃ (r : ℕ) (n : Fin r → ℕ)
      (_ : HasBiproduct fun i =>
        idealSheafPowPushforward B S hS (D.piHom B S hS hZ X hqc hqs) D.I (n i))
      (σ : (⨁ fun i => idealSheafPowPushforward B S hS (D.piHom B S hS hZ X hqc hqs) D.I (n i)) ⟶
        F), Epi σ

Tag 0GV0, a lemma

Tag 0GV0 in the Stacks Project.

AlgebraicGeometry.Space.exists_isFiniteLocallyFreeOnSite_epi_modulePushforwardIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyDescentIdealQuotient.lean, line 134. The attribute's comment: “the direction from the resolution property: π_*ℐ is coherent by Stacks 07UH, so the resolution property of the Noetherian X exhibits it as the quotient of a finite locally free module. The converse direction is not claimed; its input Stacks 0GUZ, the powers ℐ^n of a quasi-coherent sheaf of ideals on an algebraic space, and the closure of finite local freeness under tensor powers and finite direct sums are all absent from the library, as the module documentation records”.

Stacks 0GV0, the direction from the resolution property. In the situation of Stacks 0GUY with X Noetherian, if X has the resolution property then π_*ℐ is the quotient of a finite locally free 𝒪_X-module: there are a finite locally free 𝒪_X-module E and an epimorphism E ⟶ π_*ℐ.

theorem exists_isFiniteLocallyFreeOnSite_epi_modulePushforwardIdeal
    (hX : IsNoetherian B S hS hZ X.1)
    (hRP : HasResolutionProperty.{u, u} B S hS X.1 X.2) :
    ∃ (E : Modules.{u, u} B S hS X.1 X.2)
      (_ : SheafOfModules.IsFiniteLocallyFreeOnSite E)
      (p : E ⟶ modulePushforwardIdeal B S hS hZ X hqc hqs D), Epi p

AlgebraicGeometry.Space.hasResolutionProperty_iff_exists_epi_modulePushforwardIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyNoetherianIdealCriterion.lean, line 90. The attribute's comment: “the whole statement, both directions”.

Let X be a quasi-compact and quasi-separated algebraic space, φ : V ⟶ X a surjective étale morphism from an affine scheme factored as an open immersion j : V ⟶ Y followed by a finite π : Y ⟶ X, and ℐ ⊆ 𝒪_Y a finite type quasi-coherent sheaf of ideals with V(ℐ) = Y ∖ j(V), and assume X is Noetherian. Then X has the resolution property if and only if π_*ℐ is the quotient of a finite locally free 𝒪_X-module.

theorem hasResolutionProperty_iff_exists_epi_modulePushforwardIdeal
    (hX : IsNoetherian B S hS hZ X.1) :
    HasResolutionProperty.{u, u} B S hS X.1 X.2 ↔
      ∃ (E : Modules.{u, u} B S hS X.1 X.2) (_ : SheafOfModules.IsFiniteLocallyFreeOnSite E)
        (p : E ⟶ modulePushforwardIdeal B S hS hZ X hqc hqs D), Epi p

Tag 0GV1, a lemma

Tag 0GV1 in the Stacks Project.

AlgebraicGeometry.Space.ResolutionPropertyDescentSituation.exists_isFiniteLocallyFreeOnSite_epi_idealDirectImage_of_hasResolutionProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyIdealDirectImage.lean, line 141. The attribute's comment: “the implication from the resolution property of X to π_*ℐ being the quotient of a finite locally free 𝒪_X-module; the reverse implication, whose proof in the source reduces to the Noetherian case Stacks 0GV0, is not proved — see the module documentation for the inputs it needs”.

Stacks 0GV1, the implication from the resolution property. In the situation of Stacks 0GUY, if the algebraic space X has the resolution property then π_*ℐ is the quotient of a finite locally free 𝒪_X-module.

theorem exists_isFiniteLocallyFreeOnSite_epi_idealDirectImage_of_hasResolutionProperty
    (hX : HasResolutionProperty.{u, u} B S hS X.1 X.2) :
    ∃ (E : Modules.{u, u} B S hS X.1 X.2)
      (_ : SheafOfModules.IsFiniteLocallyFreeOnSite E)
      (f : E ⟶ idealDirectImage B S hS hZ sit), Epi f

AlgebraicGeometry.Space.hasResolutionProperty_iff_exists_epi_idealDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyIdealDirectImageConverse.lean, line 269.

In the situation of Stacks 0GUY — X a quasi-compact and quasi-separated algebraic space over S, V an affine scheme with a surjective étale φ : V ⟶ X factored as an open immersion j : V ⟶ Y followed by a finite π : Y ⟶ X, and ℐ ⊆ 𝒪_Y a finite type quasi-coherent sheaf of ideals with |V(ℐ)| = |Y| ∖ |j(V)| — the algebraic space X has the resolution property if and only if π_*ℐ is the quotient of a finite locally free 𝒪_X-module.

theorem hasResolutionProperty_iff_exists_epi_idealDirectImage
    (sit : ResolutionPropertyDescentSituation B S hS hZ X hqc hqs) :
    HasResolutionProperty.{u, u} B S hS X.1 X.2 ↔
      ∃ (E : Modules.{u, u} B S hS X.1 X.2) (_ : SheafOfModules.IsFiniteLocallyFreeOnSite E)
        (p : E ⟶ sit.idealDirectImage B S hS hZ), Epi p

Tag 0GV2, a lemma

Tag 0GV2 in the Stacks Project.

AlgebraicGeometry.Space.hasResolutionProperty_limitAlgebraicSpace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyLimitIff.lean, line 77.

Stacks 0GV2. Let X = lim X_i be the limit of a cofiltered system of quasi-compact and quasi-separated algebraic spaces over S with affine transition morphisms. Then X has the resolution property if and only if some X_i has it.

The system is indexed by a cofiltered category, which contains the directed systems of the source; the bounds hSize and hHomSize on the index are those under which the limit of the presheaves D is an algebraic space of the big fppf site (limitAlgebraicSpace, Stacks 07SF).

If X_i has the resolution property, so does X, by the affine case of Stacks 0GUU along the affine projection X ⟶ X_i. Conversely, the proof is the source's; see the module documentation.

theorem hasResolutionProperty_limitAlgebraicSpace_iff
    (hqc : ∀ i, IsQuasiCompactSpace B S hS (D.obj i))
    (hqs : ∀ i, IsAbsolutelyQuasiSeparated B S hS hZ (D.obj i)) :
    HasResolutionProperty.{u, u} B S hS
        (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine).1
        (limitAlgebraicSpace B S hS D hSize hHomSize hD hAffine).2 ↔
      ∃ i, HasResolutionProperty.{u, u} B S hS (D.obj i) (hD i)

Tag 0GV3, a lemma

Tag 0GV3 in the Stacks Project.

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

Stacks 0GV3. Let X be a quasi-compact and quasi-separated algebraic space over a scheme S with the resolution property. Then X has affine diagonal over ℤ: the diagonal of X viewed as an algebraic space over Spec ℤ is an affine morphism.

theorem isAffineHom_viewOverIntegers_diag_of_hasResolutionProperty
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXqc : IsQuasiCompactSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X)
    (hXres : HasResolutionProperty.{u, u} B S hS X hX) :
    IsAffineHom B (⊤_ Scheme.{u}) hZ (diag (viewOverIntegers B S hS hZ X))

Sources

LeanAlgebraicGeometry.Space.exists_affine_isSurjective_isEtale_of_isQuasiCompactSpace · AlgebraicGeometry.Space.ResolutionPropertyDescentSituation · AlgebraicGeometry.Space.exists_epi_biproduct_idealSheafPowPushforward · AlgebraicGeometry.Space.exists_isFiniteLocallyFreeOnSite_epi_modulePushforwardIdeal · AlgebraicGeometry.Space.hasResolutionProperty_iff_exists_epi_modulePushforwardIdeal ·

AlgebraicGeometry.Space.ResolutionPropertyDescentSituation.exists_isFiniteLocallyFreeOnSite_epi_idealDirectImage_of_hasResolutionProperty

· AlgebraicGeometry.Space.hasResolutionProperty_iff_exists_epi_idealDirectImage · AlgebraicGeometry.Space.hasResolutionProperty_limitAlgebraicSpace_iff

Section76.57 Blowing up and the resolution property #

Section 76.57 of the Stacks Project, Tag 0GV4. 2 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GV5, a lemma

Tag 0GV5 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.exists_isQuasiCompact_dense_isAdmissibleBlowup_hasResolutionProperty, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyAfterAdmissibleBlowup.lean, line 24 (StacksFrontier).

Tag 0GV6, a lemma

Tag 0GV6 in the Stacks Project.

AlgebraicGeometry.Space.exists_closedFiltration_admissibleBlowups_resolutionProperty_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/ResolutionPropertyDenseBlowupUnconditional.lean, line 679.

Stacks 0GV6 for an algebraic space over an arbitrary base scheme, with no hypothesis beyond the tag's own. For a quasi-compact, quasi-separated algebraic space X over a scheme S of the site there are closed subspaces Z₀ ⊇ Z₁ ⊇ ⋯ ⊇ Z_t of X, each of finite presentation over X, with Z₀ ⊆ X a thickening, with Z_t carrying no points, and with a (Z_i ∖ Z_{i+1})-admissible blowing up of Z_i whose source has the resolution property for every i < t.

This is AlgebraicGeometry.Space.exists_closedFiltration_admissibleBlowups_resolutionProperty with its hypothesis h0GV5 discharged by AlgebraicGeometry.Space.forall_exists_isQuasiCompact_dense_isAdmissibleBlowup_ hasResolutionProperty, read over the terminal scheme.

The index direction, and an erratum in the source. The tag's statement reads "for each i = 0, …, t - 1 there exists a (Z_i ∖ Z_{i - 1})-admissible blowing up", with the chain X ⊃ Z_0 ⊃ Z_1 ⊃ ⋯ ⊃ Z_t = ∅. That index cannot be meant. The chain gives Z_i ⊆ Z_{i - 1}, so Z_i ∖ Z_{i - 1} is empty for every i ≥ 1, and at i = 0 it names a Z_{-1} the statement never introduces. A ∅-admissible blowing up is one whose centre is disjoint from ∅, that is any blowing up at all, so the literal reading collapses the clause to "some blowing up of Z_i has the resolution property" — strictly weaker than intended. The tag's own proof settles it: its induction produces blowing ups admissible with respect to Z_{1, i} ∖ Z_{1, i + 1}. So the sets meant are the strata Z_i ∖ Z_{i + 1}, which partition Z_0, and that is what is proved here.

theorem exists_closedFiltration_admissibleBlowups_resolutionProperty_unconditional
    (X : AlgebraicSpaces B S hS) (hqc : IsQuasiCompactSpace B S hS X.1)
    (hqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X.1) :
    ∃ (t : ℕ) (Z : ℕ → Subfunctor X.1) (hZ : ∀ i, IsClosedSubspace B S hS (Z i)),
      (∀ i, IsFinitePresentation B S hS (Z i).ι) ∧
      (∀ i, Z (i + 1) ≤ Z i) ∧
      IsThickening B S hS X (Z 0) ∧
      IsEmpty (points B S hS (Z t).toFunctor) ∧
      ∀ i < t, ∃ (U : OpenSubspaces B S hS (Z i).toFunctor) (Y : AlgebraicSpaces B S hS)
          (f : Y ⟶ (⟨(Z i).toFunctor, (hZ i).1⟩ : AlgebraicSpaces B S hS)),
        Set.range (pointsMap B S hS U.1.toFunctor (U.1.ι ≫ (Z i).ι)) =
            subspacePointSet B S hS X.1 (Z i) \ subspacePointSet B S hS X.1 (Z (i + 1)) ∧
          IsAdmissibleBlowup B S hS U f ∧
          HasResolutionProperty.{u, u} B S hS Y.1 Y.2

Sources

LeanAlgebraicGeometry.Space.exists_isQuasiCompact_dense_isAdmissibleBlowup_hasResolutionProperty · AlgebraicGeometry.Space.exists_closedFiltration_admissibleBlowups_resolutionProperty_unconditional

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

76.49 When is a morphism an… to 76.57 Blowing up and the…

Section76.49 When is a morphism an isomorphism?#

Tag 05X8, a lemma

Tag 05X9, a lemma

Tag 05XA, a lemma

Tag 05XB, a lemma

Tag 05XC, a lemma

Tag 05XD, a lemma

Tag 06CE, a lemma

Sources

Section76.51 Characterizing pseudo-coherent complexes, II#

Tag 0CTQ, a lemma

Tag 0CTR, a lemma

Tag 0CTS, a lemma

Tag 0CTT, a lemma

Tag 0GFJ, a lemma

Sources

Section76.52 Relatively perfect objects#

Tag 0DKN, a definition

Tag 0DKP, an example

Tag 0DKQ, a lemma

Tag 0DKR, a lemma

Tag 0DKS, a lemma

Tag 0DKT, a lemma

Tag 0DKU, a situation

Tag 0DKV, a lemma

Tag 0DKW, a lemma

Tag 0DKX, a lemma

Tag 0DKY, a lemma

Tag 0GFK, a lemma

Tag 0GFL, a lemma

Sources

Section76.53 Theorem of the cube#

Tag 0D23, a lemma

Sources

Section76.54 Descent of finiteness properties of complexes#

Tag 0DL1, a lemma

Tag 0DL2, a lemma

Tag 0DL3, a lemma

Tag 0DL4, a lemma

Tag 0DL5, a lemma

Sources

Section76.55 Families of nodal curves#

Tag 0DSE, a definition

Tag 0DSF, a lemma

Tag 0DSG, a lemma

Tag 0DSH, a lemma

Sources

Section76.56 The resolution property#

Tag 0GUY, a situation

Tag 0GUZ, a lemma

Tag 0GV0, a lemma

Tag 0GV1, a lemma

Tag 0GV2, a lemma

Tag 0GV3, a lemma

Sources

Section76.57 Blowing up and the resolution property#

Tag 0GV5, a lemma

Tag 0GV6, a lemma

Sources

Section76.51 Characterizing pseudo-coherent complexes, II #

Section76.52 Relatively perfect objects #

Section76.53 Theorem of the cube #

Section76.54 Descent of finiteness properties of complexes #

Section76.55 Families of nodal curves #

Section76.56 The resolution property #

Section76.57 Blowing up and the resolution property #