48.12 Right adjoint of… to 48.21 Dimension functions

Section48.12 Right adjoint of pushforward for proper flat morphisms #

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

Tag 0E4I, a lemma

Tag 0E4I in the Stacks Project.

Stacks.Duality.preservesColimitsOfShape_rightAdjoint_quasiCoherentDerivedPushforward_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/RightAdjointDirectSumsFlat.lean, line 52.

Let Y be a quasi-compact and quasi-separated scheme, let f : X ⟶ Y be proper, flat and of finite presentation, and let a be a right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y). Then a commutes with direct sums.

theorem preservesColimitsOfShape_rightAdjoint_quasiCoherentDerivedPushforward_of_flat
    {a : quasiCoherentDerivedCategory Y ⥤ quasiCoherentDerivedCategory X}
    (adj : quasiCoherentDerivedPushforward f
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ⊣ a) (J : Type u) :
    PreservesColimitsOfShape (Discrete J) a

Tag 0E4J, a lemma

Tag 0E4J in the Stacks Project.

Stacks.Duality.isIso_twistedInverseImageRestrictionMap_app_of_flat_of_unbounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/ProperFlatSupport.lean, line 44. The attribute's comment: “(2)”.

Let Y be a quasi-compact and quasi-separated scheme, f : X ⟶ Y proper, flat and of finite presentation, and j : V ⟶ Y the inclusion of a quasi-compact open, with base change j' : U ⟶ X. The map (j')^* ∘ a ⟶ a' ∘ j^* of [Stacks, Tag 0A9L] is an isomorphism at every K ∈ D_QCoh(𝒪_Y).

theorem isIso_twistedInverseImageRestrictionMap_app_of_flat_of_unbounded
    (sq : IsPullback j' f' f j) (K : quasiCoherentDerivedCategory Y) :
    haveI : IsOpenImmersion j' := MorphismProperty.of_isPullback sq.flip inferInstance
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : CompactSpace V := QuasiCompact.compactSpace_of_compactSpace j
    haveI : CompactSpace U := compactSpace_of_isPullback sq
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : QuasiSeparatedSpace V := j.isOpenEmbedding.quasiSeparatedSpace
    haveI : QuasiSeparatedSpace U := j'.isOpenEmbedding.quasiSeparatedSpace
    IsIso ((twistedInverseImageRestrictionMap j' f' f j
      (isQuasicoherent_homology_derivedPushforward_of_qcqs j')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs j)
      (isQuasicoherent_homology_derivedRestrict j) (isQuasicoherent_homology_derivedRestrict j')
      sq).app K)

Stacks.Duality.isZero_derivedRestrict_twistedInverseImage_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/ProperFlatSupport.lean, line 128. The attribute's comment: “(1)”.

Let Y be a quasi-compact and quasi-separated scheme and f : X ⟶ Y proper, flat and of finite presentation, with a the right adjoint of Rf_* on D_QCoh. For every closed T ⊆ Y, if Q ∈ D_QCoh(𝒪_Y) is supported on T then a(Q) is supported on f⁻¹(T). Here T is the complement of the open W, and "supported on T" is "restricts to zero on W".

theorem isZero_derivedRestrict_twistedInverseImage_of_flat (W : Y.Opens)
    (Q : quasiCoherentDerivedCategory Y) (hQ : IsZero ((derivedRestrict W.ι).obj Q.obj)) :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    IsZero ((derivedRestrict (f ⁻¹ᵁ W).ι).obj
      ((twistedInverseImage f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj Q).obj)

Tag 0E4K, a lemma

Tag 0E4K in the Stacks Project.

Stacks.Duality.isIso_twistedInverseImageCompareWithPullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonFlat.lean, line 164.

[Stacks, Tag 0E4K]. Let Y be a quasi-compact and quasi-separated scheme and f : X ⟶ Y proper, flat and of finite presentation. The map Lf^*K ⊗ᴸ a(𝒪_Y) ⟶ a(K) of Equation 48.8.0.1 is an isomorphism for every K ∈ D_QCoh(𝒪_Y).

theorem isIso_twistedInverseImageCompareWithPullback_of_flat (K : quasiCoherentDerivedCategory Y) :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    IsIso (twistedInverseImageCompareWithPullback f
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (quasiCoherentDerivedPullbackTensorIso f).hom
      (quasiCoherentDerivedTensorRightUnitor Y) K)

Tag 0AAB, a lemma

Tag 0AAB in the Stacks Project.

Stacks.Duality.isIso_twistedInverseImageBaseChangeMap_app_of_isProper_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/AffineBaseChangeLocal.lean, line 426.

[Stacks, Tag 0AAB]. Let g : Y' ⟶ Y be a morphism of quasi-compact and quasi-separated schemes and f : X ⟶ Y proper, flat and of finite presentation, with base change f' : X' ⟶ Y'. Then the base change map L(g')^* a(K) ⟶ a'(Lg^*K) of [Stacks, Tag 0AA6] is an isomorphism for every K ∈ D_QCoh(𝒪_Y).

theorem isIso_twistedInverseImageBaseChangeMap_app_of_isProper_of_flat {X' X Y' Y : Scheme.{u}}
    [CompactSpace Y'] [QuasiSeparatedSpace Y'] [CompactSpace Y] [QuasiSeparatedSpace Y]
    {g' : X' ⟶ X} {f' : X' ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f] (K : quasiCoherentDerivedCategory Y) :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : QuasiCompact f' := MorphismProperty.of_isPullback sq inferInstance
    haveI : QuasiSeparated f' := MorphismProperty.of_isPullback sq inferInstance
    haveI : CompactSpace X' := QuasiCompact.compactSpace_of_compactSpace f'
    haveI : QuasiSeparatedSpace X' := quasiSeparatedSpace_of_quasiSeparated f'
    haveI := isIso_twistedInverseImagePushforwardBaseChange_of_torIndependent sq
      (torIndependent_of_flat_left f g)
    IsIso ((twistedInverseImageBaseChangeMap g' f' f g
      (isQuasicoherent_homology_derivedPushforward_of_qcqs g')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs g)
      sq).app K)

Tag 0B6S, a remark

Tag 0B6S in the Stacks Project.

Stacks.Duality.relativeDualizingComplexStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/RelativeDualizingComplexStructureSheaf.lean, line 104. The attribute's comment: “the relative dualizing complex omega^bullet_{X/Y} = a(O_Y) that the Remark names, the right adjoint of Tag 0A9E applied to the structure sheaf; defined for every quasi-compact quasi-separated morphism to a quasi-compact scheme, so in particular under the Remark's hypotheses”.

The relative dualizing complex ω_{X/Y}^• = a(𝒪_Y) of [Stacks, Tag 0B6S], for a = f^× the right adjoint of [Stacks, Tag 0A9E]: the twisted inverse image of the structure sheaf of the base, placed in degree zero.

Over Y = Spec k for a field k this is Stacks.Duality.dualizingComplexOverField, the dualizing complex of [Stacks, Tag 0BS2].

def relativeDualizingComplexStructureSheaf : quasiCoherentDerivedCategory X

Stacks.Duality.relativeDualizingTraceStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DerivedPushforward/RelativeDualizingComplexStructureSheaf.lean, line 116. The attribute's comment: “the trace map Tr_{f,O_Y} : Rf_* omega^bullet_{X/Y} to O_Y that the Remark displays, the counit of the adjunction of Tag 0A9E at the structure sheaf of the base”.

The trace map Tr_{f, 𝒪_Y} : Rf_* ω_{X/Y}^• ⟶ 𝒪_Y of [Stacks, Tag 0AWG], displayed in [Stacks, Tag 0B6S]: the counit of Rf_* ⊣ f^× at the structure sheaf of the base.

That it induces the trace map Tr_{f, K} for every K in D_QCoh(𝒪_Y) — the commuting square of the Remark — is Stacks.Duality.map_relativeDualizingTensorIso_hom_app_comp_trace.

def relativeDualizingTraceStructureSheaf :
    (quasiCoherentDerivedPushforward f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
      (relativeDualizingComplexStructureSheaf f) ⟶
    Stacks.Duality.DerivedPushforward.derivedStructureSheaf Y

Stacks.Duality.relativeDualizingTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexTensorDescription.lean, line 142. The attribute's comment: “the functorial isomorphism a(K) = Lf^*K ⊗^L omega^bullet_{X/Y} for K in D_QCoh(O_Y), omega^bullet_{X/Y} = a(O_Y), for Y quasi-compact quasi-separated and f proper flat of finite presentation: an isomorphism of functors whose components are the map of Equation 48.8.0.1, invertible by Tag 0E4K”.

The functorial isomorphism a(K) = Lf^*K ⊗ᴸ ω^•_{X/Y} of [Stacks, Tag 0B6S], for Y quasi-compact and quasi-separated and f : X ⟶ Y proper, flat and of finite presentation: an isomorphism of functors D_QCoh(𝒪_Y) ⥤ D_QCoh(𝒪_X) from K ↦ Lf^*K ⊗ᴸ_{𝒪_X} ω^•_{X/Y}, where ω^•_{X/Y} = a(𝒪_Y) is the relative dualizing complex, to the right adjoint a of [Stacks, Tag 0A9E]. Its components are the map of Equation 48.8.0.1 ([Stacks, Tag 0A9S]), which is invertible by [Stacks, Tag 0E4K].

def relativeDualizingTensorIso :
    quasiCoherentDerivedPullback' f ⋙ (quasiCoherentDerivedTensor X).flip.obj
        ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
          (derivedStructureSheaf Y)) ≅
      twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)

Stacks.Duality.map_relativeDualizingTensorIso_hom_app_comp_trace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexTensorDescription.lean, line 175. The attribute's comment: “the trace compatibility: Tr_{f,K} composed with Rf_ of the isomorphism a(K) = Lf^K ⊗^L omega^bullet_{X/Y} is the projection formula of Tag 08EU followed by id_K ⊗ Tr_{f,O_Y} and K ⊗^L O_Y = K, the Remark's commuting square, for Y quasi-compact quasi-separated and f proper flat of finite presentation”.

The trace map Tr_{f, 𝒪_Y} induces the trace map Tr_{f, K} for every K, the commuting square of [Stacks, Tag 0B6S]: Rf_* of the isomorphism Lf^*K ⊗ᴸ ω^•_{X/Y} ≅ a(K) followed by the trace Tr_{f, K} : Rf_* a(K) ⟶ K of [Stacks, Tag 0AWG] is the projection formula Rf_*(Lf^*K ⊗ᴸ ω^•_{X/Y}) ≅ K ⊗ᴸ Rf_* ω^•_{X/Y} of [Stacks, Tag 08EU], followed by id_K ⊗ Tr_{f, 𝒪_Y} : K ⊗ᴸ Rf_* ω^•_{X/Y} ⟶ K ⊗ᴸ 𝒪_Y and the identification K ⊗ᴸ 𝒪_Y = K.

theorem map_relativeDualizingTensorIso_hom_app_comp_trace (K : quasiCoherentDerivedCategory Y) :
    (quasiCoherentDerivedPushforward f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).map
        ((relativeDualizingTensorIso f).hom.app K) ≫
      (twistedInverseImageAdjunction f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).counit.app K =
    (relativeDualizingProjectionFormulaIso f K).inv ≫
      ((quasiCoherentDerivedTensor Y).obj K).map (relativeDualizingTraceStructureSheaf f) ≫
      quasiCoherentRightUnitor.hom.app K

Stacks.Duality.relativeDualizingBaseChangeIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexTensorDescription.lean, line 257. The attribute's comment: “the base change of the relative dualizing complex in the Remark's last sentence: for g : Y' to Y a morphism of quasi-compact quasi-separated schemes and X' = Y' x_Y X, the base change map L(g')^ a(O_Y) to a'(Lg^ O_Y) of Tag 0AA6 is an isomorphism (Tag 0AAB), so omega^bullet_{X'/Y'} = L(g')^ omega^bullet_{X/Y} through it and a'(Lg^ O_Y = O_{Y'})”.

ω^•_{X'/Y'} = L(g')^* ω^•_{X/Y}, the first assertion of the last sentence of [Stacks, Tag 0B6S]: the base change map of [Stacks, Tag 0AA6] at 𝒪_Y is an isomorphism ([Stacks, Tag 0AAB]), and composed with a'(Lg^*𝒪_Y ≅ 𝒪_{Y'}) it is the isomorphism relativeDualizingBaseChangeIso.

theorem relativeDualizingBaseChangeIso_hom :
    haveI := quasiCompact_of_isPullback_relativeDualizing f sq
    haveI := quasiSeparated_of_isPullback_relativeDualizing f sq
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace X' := QuasiCompact.compactSpace_of_compactSpace f'
    haveI : QuasiSeparatedSpace X' := quasiSeparatedSpace_of_quasiSeparated f'
    haveI := isIso_twistedInverseImagePushforwardBaseChange_of_torIndependent sq
      (torIndependent_of_flat_left f g)
    IsIso ((twistedInverseImageBaseChangeMap g' f' f g
        (isQuasicoherent_homology_derivedPushforward_of_qcqs g')
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
        (isQuasicoherent_homology_derivedPushforward_of_qcqs g) sq).app
          (derivedStructureSheaf Y)) ∧
      (relativeDualizingBaseChangeIso f sq).hom =
        (twistedInverseImageBaseChangeMap g' f' f g
          (isQuasicoherent_homology_derivedPushforward_of_qcqs g')
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
          (isQuasicoherent_homology_derivedPushforward_of_qcqs g) sq).app
            (derivedStructureSheaf Y) ≫
          (twistedInverseImage f' (isQuasicoherent_homology_derivedPushforward_of_qcqs f')).map
            (quasiCoherentDerivedPullbackDerivedStructureSheafIsoOfIsQuasicoherent g
        (isQuasicoherent_homology_derivedPullback' g)).hom

Stacks.Duality.map_trace_comp_eq_baseChange_comp_trace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexTensorDescription.lean, line 294. The attribute's comment: “the base change of the trace in the Remark's last sentence: Tr_{f',O_{Y'}} is the base change of Tr_{f,O_Y} via the base change isomorphism, i.e. Lg^ Tr_{f,O_Y} followed by Lg^ O_Y = O_{Y'} equals the base change map of Rf_ at omega^bullet_{X/Y} followed by Rf'_ of L(g')^* omega^bullet_{X/Y} = omega^bullet_{X'/Y'} and Tr_{f',O_{Y'}} (Tag 0B6J)”.

The trace map of f' is the base change of the trace map of f, the second assertion of the last sentence of [Stacks, Tag 0B6S], by [Stacks, Tag 0B6J]: Lg^* of Tr_{f, 𝒪_Y} : Rf_* ω^•_{X/Y} ⟶ 𝒪_Y, followed by Lg^*𝒪_Y ≅ 𝒪_{Y'}, is the base change map β : Lg^* Rf_* ⟶ Rf'_* L(g')^* at ω^•_{X/Y} (invertible, [Stacks, Tag 08IB]), followed by Rf'_* of the base change isomorphism L(g')^* ω^•_{X/Y} ≅ ω^•_{X'/Y'} and Tr_{f', 𝒪_{Y'}} : Rf'_* ω^•_{X'/Y'} ⟶ 𝒪_{Y'}.

theorem map_trace_comp_eq_baseChange_comp_trace :
    haveI := quasiCompact_of_isPullback_relativeDualizing f sq
    haveI := quasiSeparated_of_isPullback_relativeDualizing f sq
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace X' := QuasiCompact.compactSpace_of_compactSpace f'
    haveI : QuasiSeparatedSpace X' := quasiSeparatedSpace_of_quasiSeparated f'
    IsIso (quasiCoherentDerivedBaseChange g' f' f g
          (isQuasicoherent_homology_derivedPushforward_of_qcqs g')
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
          (isQuasicoherent_homology_derivedPushforward_of_qcqs g)
          (isQuasicoherent_homology_derivedPullback' g)
          (isQuasicoherent_homology_derivedPullback' g') sq.w).natTrans ∧
    (quasiCoherentDerivedPullback' g).map
        ((twistedInverseImageAdjunction f
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).counit.app
          (derivedStructureSheaf Y)) ≫
      (quasiCoherentDerivedPullbackDerivedStructureSheafIsoOfIsQuasicoherent g
        (isQuasicoherent_homology_derivedPullback' g)).hom =
    (quasiCoherentDerivedBaseChange g' f' f g
          (isQuasicoherent_homology_derivedPushforward_of_qcqs g')
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
          (isQuasicoherent_homology_derivedPushforward_of_qcqs g)
          (isQuasicoherent_homology_derivedPullback' g)
          (isQuasicoherent_homology_derivedPullback' g') sq.w).natTrans.app
        ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
          (derivedStructureSheaf Y)) ≫
      (quasiCoherentDerivedPushforward f'
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f')).map
        (relativeDualizingBaseChangeIso f sq).hom ≫
      (twistedInverseImageAdjunction f'
          (isQuasicoherent_homology_derivedPushforward_of_qcqs f')).counit.app
        (derivedStructureSheaf Y')

Tag 0G81, a remark

Tag 0G81 in the Stacks Project.

Stacks.Duality.isIso_homEquiv_symm_relativeCupProduct_comp_trace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingCupProduct.lean, line 206.

Stacks Project, Tag 0G81. Let Y be a quasi-compact quasi-separated scheme and f : X ⟶ Y a proper, flat morphism of finite presentation; let a be the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) of [Stacks, Tag 0A9E], ω^•_{X/Y} = a(𝒪_Y) the relative dualizing complex and Tr_{f, 𝒪_Y} : Rf_*ω^•_{X/Y} ⟶ 𝒪_Y the trace of [Stacks, Tag 0B6S]. Let K ∈ D(𝒪_X) and M ∈ D_QCoh(𝒪_X) with M pseudo-coherent, and let φ : K ⊗^L_{𝒪_X} M ⟶ ω^•_{X/Y} be a map whose transpose K ⟶ R𝓗om_{𝒪_X}(M, ω^•_{X/Y}) under the tensor–internal-Hom bijection of [Stacks, Tag 08DI] is an isomorphism. Then the map Rf_*K ⟶ R𝓗om_{𝒪_Y}(Rf_*M, 𝒪_Y) corresponding under that bijection on Y to

Rf_*K ⊗^L_{𝒪_Y} Rf_*M ⟶ Rf_*(K ⊗^L_{𝒪_X} M) ⟶ Rf_*ω^•_{X/Y} ⟶ 𝒪_Y

(the relative cup product of [Stacks, Tag 0B68], Rf_*φ and Tr_{f, 𝒪_Y}) is an isomorphism.

The source asks K to lie in D_QCoh(𝒪_X); that is not used. The instance arguments CompactSpace X and QuasiSeparatedSpace X restrict nothing: they hold for every proper f over a quasi-compact quasi-separated Y (AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace and AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated), and are arguments only because the right adjoint a of [Stacks, Tag 0A9E] at this model is found by instance search from them.

theorem isIso_homEquiv_symm_relativeCupProduct_comp_trace (K : DerivedCategory X.Modules)
    (M : quasiCoherentDerivedCategory X)
    (hM : RingedSpace.IsPseudoCoherent (X := X.toRingedSpace) M.obj)
    (φ : ((derivedTensorProductFunctor X.sheaf).obj K).obj M.obj ⟶
      (relativeDualizingComplex f (StandardModel.isQuasicoherent_homology_derivedPushforward f)
        (derivedStructureSheafInDegree Y 0)).obj)
    (hφ : IsIso (((derivedTensorHomAdjunction (Stacks.SheafOfModules.ringedSite X.sheaf)).homEquiv
      K M.obj (relativeDualizingComplex f
        (StandardModel.isQuasicoherent_homology_derivedPushforward f)
        (derivedStructureSheafInDegree Y 0)).obj).symm φ)) :
    IsIso (((derivedTensorHomAdjunction (Stacks.SheafOfModules.ringedSite Y.sheaf)).homEquiv
      ((derivedPushforward f).obj K) ((derivedPushforward f).obj M.obj)
      (derivedStructureSheafInDegree Y 0).obj).symm
        (relativeCupProduct f.toLRSHom.toShHom K M.obj ≫ (derivedPushforward f).map φ ≫
          (ι _).map (relativeDualizingComplexTrace f
            (StandardModel.isQuasicoherent_homology_derivedPushforward f)
            (derivedStructureSheafInDegree Y 0))))

Tag 0E4L, a lemma

Tag 0E4L in the Stacks Project.

Stacks.Duality.StandardModel.isIso_derivedSheafHomothety_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperFlatDualizing/Endomorphisms.lean, line 213. The attribute's comment: “(3)”.

Let Y be a quasi-compact and quasi-separated scheme and f : X ⟶ Y a proper, flat morphism of finite presentation, with relative dualizing complex ω_{X/Y} = a(𝒪_Y) ([Stacks, Remark 0B6S]). Then the homothety 𝒪_X ⟶ R𝓗om_{𝒪_X}(ω_{X/Y}, ω_{X/Y}) is an isomorphism.

theorem isIso_derivedSheafHomothety_relativeDualizingComplex :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    IsIso (Stacks.SheafOfModules.derivedSheafHomothety X.sheaf
      (relativeDualizingComplex f).obj)

Stacks.Duality.StandardModel.isZero_homology_derivedPushforward_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperFlatDualizing/PushforwardVanishing.lean, line 58. The attribute's comment: “(2)”.

[Stacks, Tag 0E4L] (2). Let Y be a quasi-compact and quasi-separated scheme and f : X ⟶ Y a proper, flat morphism of finite presentation, with relative dualizing complex ω_{X/Y} = a(𝒪_Y) ([Stacks, Remark 0B6S]). Then Rf_*ω_{X/Y} has vanishing cohomology sheaves in positive degrees.

theorem isZero_homology_derivedPushforward_relativeDualizingComplex (i : ℤ) (hi : 0 < i) :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    IsZero ((DerivedCategory.homologyFunctor Y.Modules i).obj
      ((derivedPushforward f).obj (relativeDualizingComplex f).obj))

Stacks.Duality.StandardModel.isRelativelyPerfect_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProperFlatDualizing/RelativelyPerfect.lean, line 119. The attribute's comment: “(1)”. References: SGA 6 III (4.9.1), “Case S = Y and F = O_Y”; SGA 6 IV (3.3.2), “3.3.2.4”.

[Stacks, Tag 0E4L] (1). Let Y be a quasi-compact and quasi-separated scheme and f : X ⟶ Y a proper, flat morphism of finite presentation, with relative dualizing complex ω_{X/Y} = a(𝒪_Y) ([Stacks, Remark 0B6S]). Then ω_{X/Y} is a Y-perfect object of D(𝒪_X).

Over an affine open V ⊆ Y, with Spec Γ(V) ⟶ Y the inclusion, the base change of ω_{X/Y} to f⁻¹V ⟶ Spec Γ(V) is the relative dualizing complex of the base change (Stacks.Duality.StandardModel.pullbackRelativeDualizingComplexIso), which is Spec Γ(V)-perfect (isRelativelyPerfect_relativeDualizingComplex_of_spec); relative perfectness is local on the source and on the base.

theorem isRelativelyPerfect_relativeDualizingComplex {X Y : Scheme.{u}} (f : X ⟶ Y)
    [CompactSpace Y] [QuasiSeparatedSpace Y] [IsProper f] [Flat f]
    [LocallyOfFinitePresentation f] :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    f.IsRelativelyPerfect (relativeDualizingComplex f).obj

Tag 0E2P, a lemma

Tag 0E2P in the Stacks Project.

Stacks.Duality.relativeDualizingComplexRigidity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/Rigidity.lean, line 135.

Rigidity, [Stacks, Tag 0E2P]. Let Y be a quasi-compact and quasi-separated scheme and f : X ⟶ Y proper, flat and of finite presentation, with relative dualizing complex ω = a(𝒪_Y) ([Stacks, Tag 0B6S]), and let c be the right adjoint of RΔ_* on D_QCoh for the diagonal Δ : X ⟶ X ×_Y X ([Stacks, Tag 0A9E]). There are canonical isomorphisms 𝒪_X ≅ c(Lpr₁^*ω), 𝒪_X ≅ c(Lpr₂^*ω) (Equation 0E2Q) and ω ≅ c(Lpr₁^*ω ⊗ᴸ Lpr₂^*ω) (Equation 0E2R).

def relativeDualizingComplexRigidity {X Y : Scheme.{u}} [CompactSpace Y] [QuasiSeparatedSpace Y]
    (f : X ⟶ Y) [IsProper f] [Flat f] [LocallyOfFinitePresentation f] :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace (pullback f f : Scheme.{u}) :=
      QuasiCompact.compactSpace_of_compactSpace (pullback.snd f f)
    haveI : QuasiSeparatedSpace (pullback f f : Scheme.{u}) :=
      quasiSeparatedSpace_of_quasiSeparated (pullback.snd f f)
    ((DerivedPushforward.derivedStructureSheaf X ≅
        (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
          ((quasiCoherentDerivedPullback' (pullback.fst f f)).obj
            ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
            (DerivedPushforward.derivedStructureSheaf Y)))) ×
      (DerivedPushforward.derivedStructureSheaf X ≅
        (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
          ((quasiCoherentDerivedPullback' (pullback.snd f f)).obj
            ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
            (DerivedPushforward.derivedStructureSheaf Y))))) ×
      (((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
          (DerivedPushforward.derivedStructureSheaf Y)) ≅
        (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
          (((quasiCoherentDerivedTensor (pullback f f)).obj
            ((quasiCoherentDerivedPullback' (pullback.fst f f)).obj
              ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
              (DerivedPushforward.derivedStructureSheaf Y)))).obj
            ((quasiCoherentDerivedPullback' (pullback.snd f f)).obj
              ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
              (DerivedPushforward.derivedStructureSheaf Y)))))

Tag 0E2Q, an equation

Tag 0E2Q in the Stacks Project.

Stacks.Duality.structureSheafIsoDiagonalTwistedInverseImagePullbackFst, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexRigidity.lean, line 200. The attribute's comment: “first projection: 𝒪_X ≅ c(L pr₁^* ω_{X/Y}^•)”.

[Stacks, Tag 0E2Q], first projection: 𝒪_X ≅ c(L pr₁^* ω_{X/Y}^•); this is the first isomorphism of [Stacks, Tag 0E2P], where ω_{X/Y}^• = a(𝒪_Y) is the relative dualizing complex and c the twisted inverse image of the diagonal Δ : X ⟶ X ×_Y X. With b' the twisted inverse image of pr₂, 𝒪_X = c(b'(𝒪_X)) as pr₂ ∘ Δ = id, and b'(𝒪_X) = L pr₁^* a(𝒪_Y) by flat base change.

def structureSheafIsoDiagonalTwistedInverseImagePullbackFst :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace (pullback f f : Scheme.{u}) :=
      QuasiCompact.compactSpace_of_compactSpace (pullback.fst f f)
    haveI : QuasiSeparatedSpace (pullback f f : Scheme.{u}) := quasiSeparatedSpace_of_quasiSeparated
      (pullback.fst f f)
    derivedStructureSheaf X ≅
      (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
        ((quasiCoherentDerivedPullback' (pullback.fst f f)).obj
          ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
            (derivedStructureSheaf Y)))

Stacks.Duality.structureSheafIsoDiagonalTwistedInverseImagePullbackSnd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexRigidity.lean, line 229. The attribute's comment: “second projection: 𝒪_X ≅ c(L pr₂^* ω_{X/Y}^•)”.

[Stacks, Tag 0E2Q], second projection: 𝒪_X ≅ c(L pr₂^* ω_{X/Y}^•); this is the second isomorphism of [Stacks, Tag 0E2P]. With b the twisted inverse image of pr₁, 𝒪_X = c(b(𝒪_X)) as pr₁ ∘ Δ = id, and b(𝒪_X) = L pr₂^* a(𝒪_Y) by flat base change.

def structureSheafIsoDiagonalTwistedInverseImagePullbackSnd :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace (pullback f f : Scheme.{u}) :=
      QuasiCompact.compactSpace_of_compactSpace (pullback.fst f f)
    haveI : QuasiSeparatedSpace (pullback f f : Scheme.{u}) := quasiSeparatedSpace_of_quasiSeparated
      (pullback.fst f f)
    derivedStructureSheaf X ≅
      (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
        ((quasiCoherentDerivedPullback' (pullback.snd f f)).obj
          ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
            (derivedStructureSheaf Y)))

Stacks.Duality.nonempty_twistedInverseImage_diagonal_pullback_relativeDualizingComplex_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/DiagonalRigidity.lean, line 146.

Equation (0E2Q) of [Stacks, Tag 0E2P]. Let Y be quasi-compact and quasi-separated and f : X ⟶ Y proper, flat and of finite presentation, with relative dualizing complex ω_{X/Y}^• = a(𝒪_Y) ([Stacks, Remark 0B6S]). Then, c being the right adjoint of RΔ_* for the diagonal Δ : X ⟶ X ×_Y X ([Stacks, Tag 0A9E]),

𝒪_X ≅ c(L pr₁^* ω_{X/Y}^•) and 𝒪_X ≅ c(L pr₂^* ω_{X/Y}^•).

theorem nonempty_twistedInverseImage_diagonal_pullback_relativeDualizingComplex_iso :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI := QuasiCompact.compactSpace_of_compactSpace (pullback.snd f f)
    haveI := quasiSeparatedSpace_of_quasiSeparated (pullback.snd f f)
    Nonempty (DerivedPushforward.derivedStructureSheaf X ≅
      (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
        ((quasiCoherentDerivedPullback' (pullback.fst f f)).obj
          (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
            (DerivedPushforward.derivedStructureSheaf Y)))) ∧
    Nonempty (DerivedPushforward.derivedStructureSheaf X ≅
      (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
        ((quasiCoherentDerivedPullback' (pullback.snd f f)).obj
          (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
            (DerivedPushforward.derivedStructureSheaf Y))))

Tag 0E2R, an equation

Tag 0E2R in the Stacks Project.

Stacks.Duality.relativeDualizingComplexRigidityIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexRigidity.lean, line 261.

[Stacks, Tag 0E2R], the rigidity isomorphism; this is the isomorphism of [Stacks, Tag 0E2P] in Equation 0E2R: ω_{X/Y}^• ≅ c(L pr₁^* ω_{X/Y}^• ⊗ᴸ_{𝒪_{X ×_Y X}} L pr₂^* ω_{X/Y}^•), where ω_{X/Y}^• = a(𝒪_Y) is the relative dualizing complex of [Stacks, Tag 0B6S] and c the twisted inverse image of the diagonal Δ : X ⟶ X ×_Y X. With b the twisted inverse image of pr₁: ω = c(b(ω)) as pr₁ ∘ Δ = id, b(ω) = L pr₁^*ω ⊗ᴸ b(𝒪_X) by [Stacks, Tag 0E4K], and b(𝒪_X) = L pr₂^* a(𝒪_Y) by [Stacks, Tag 0AAB].

def relativeDualizingComplexRigidityIso :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    haveI : CompactSpace (pullback f f : Scheme.{u}) :=
      QuasiCompact.compactSpace_of_compactSpace (pullback.fst f f)
    haveI : QuasiSeparatedSpace (pullback f f : Scheme.{u}) := quasiSeparatedSpace_of_quasiSeparated
      (pullback.fst f f)
    (twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
        (derivedStructureSheaf Y) ≅
      (twistedInverseImage (pullback.diagonal f)
        (isQuasicoherent_homology_derivedPushforward_of_qcqs (pullback.diagonal f))).obj
        (((quasiCoherentDerivedTensor (pullback f f : Scheme.{u})).obj
          ((quasiCoherentDerivedPullback' (pullback.fst f f)).obj
            ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
              (derivedStructureSheaf Y)))).obj
          ((quasiCoherentDerivedPullback' (pullback.snd f f)).obj
            ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
              (derivedStructureSheaf Y))))

Tag 0BRU, a remark

Tag 0BRU in the Stacks Project.

Declarations registered for the tag:

Stacks.Duality.relativeDualizingComplexRigidityIso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizingComplexRigidity.lean, line 313 (StacksFrontier): “the rigidity isomorphism ω_{X/Y}^• ≅ c(L pr₁^ ω_{X/Y}^• ⊗ᴸ L pr₂^ ω_{X/Y}^•) of Equation 0E2R”.

Sources

LeanStacks.Duality.preservesColimitsOfShape_rightAdjoint_quasiCoherentDerivedPushforward_of_flat · Stacks.Duality.isIso_twistedInverseImageRestrictionMap_app_of_flat_of_unbounded · Stacks.Duality.isZero_derivedRestrict_twistedInverseImage_of_flat · Stacks.Duality.isIso_twistedInverseImageCompareWithPullback_of_flat · Stacks.Duality.isIso_twistedInverseImageBaseChangeMap_app_of_isProper_of_flat · Stacks.Duality.relativeDualizingComplexStructureSheaf · Stacks.Duality.relativeDualizingTraceStructureSheaf · Stacks.Duality.relativeDualizingTensorIso

Section48.13 Right adjoint of pushforward for perfect proper morphisms #

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

Tag 0A9R, a lemma

Tag 0A9R in the Stacks Project.

Stacks.Duality.preservesCoproducts_rightAdjoint_of_isCompactObject_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/RightAdjointDirectSums.lean, line 167. The attribute's comment: “a commutes with direct sums: for every right adjoint a of the restricted Rf_ and every index type in Type u, a preserves coproducts of that shape. The source's hypotheses on f — perfect, proper, Noetherian source and target — are not binders here; they enter its proof only to make Rf_E perfect, hence compact, and that is the hypothesis hpushE. Carried: hpushE, compactness of Rf_E, which is Tag 0B6G (Rf_ of a perfect complex along a perfect proper morphism is perfect) together with Tag 09M1 (compact iff perfect in D_QCoh) — both in this tree, at StacksFrontier/AlgebraicGeometry/MoreMorphisms/PerfectMorphism/ProperDirectImage.lean and StacksFrontier/AlgebraicGeometry/Perfect/QuasiCoherentDerived/CompactAndPerfect.lean; 09M1 is unconditional in the affine case, but 0B6G is still conditional there, on Tag 02O5 and on the Tor-dimension half of Tag 08EV, which is why hpushE is carried; E, hEc, hE, a compact weak generator of D_QCoh(O_X), Tag 09IS, unproved in this repository and carried in this shape by every consumer here; hpush, quasi-coherence of the cohomology of Rf_*, Tag 08D5; and adj, the existence of the right adjoint, Tag 0A9E, which this repository proves only conditionally in Stacks.Duality.isLeftAdjoint_quasiCoherentDerivedPushforward. No PreservesColimitsOfShape instance for a, or for any functor out of D_QCoh(O_Y), is assumed”.

[Stacks, Tag 0A9R]. Let f : X ⟶ Y be a morphism of schemes along which derived direct image preserves quasi-coherence of cohomology, and let a be a right adjoint of the restriction Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y). Suppose D_QCoh(𝒪_X) has a compact weak generator E whose image Rf_*E is compact in D_QCoh(𝒪_Y). Then a commutes with direct sums.

In the source E is the perfect generator of [Stacks, Tag 09IS] and compactness of Rf_*E is [Stacks, Tag 0B6G] together with [Stacks, Tag 09M1]; those are the only places the source's hypotheses on f — perfect, proper, Noetherian — are used, and they appear here only through hpushE. The formal half of the argument is CategoryTheory.Pretriangulated.preservesCoproducts_of_isCompactObject_map, read with Rf_* as the left adjoint and a as the right one.

theorem preservesCoproducts_rightAdjoint_of_isCompactObject_pushforward
    {a : quasiCoherentDerivedCategory Y ⥤ quasiCoherentDerivedCategory X}
    (adj : quasiCoherentDerivedPushforward f hpush ⊣ a)
    (E : quasiCoherentDerivedCategory X) (hEc : IsCompactObject.{u} E)
    (hE : (ObjectProperty.singleton E).IsWeakTriangulatedGenerator)
    (hpushE : IsCompactObject.{u} ((quasiCoherentDerivedPushforward f hpush).obj E)) :
    ∀ J : Type u, PreservesColimitsOfShape (Discrete J) a

Stacks.Duality.preservesCoproducts_twistedInverseImage_of_isCompactObject_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/RightAdjointDirectSums.lean, line 191. The attribute's comment: “the same conclusion at the source's own right adjoint, Stacks.Duality.twistedInverseImage, the f^× of Tag 0A9E. Carries everything Stacks.Duality.preservesCoproducts_rightAdjoint_of_isCompactObject_pushforward carries — hpushE, which is Tag 0B6G with Tag 09M1, neither of them available to this file; E, hEc, hE, the compact weak generator of Tag 09IS; hpush, Tag 08D5 — with the existence of the right adjoint now the instance binder Functor.IsLeftAdjoint rather than an adjunction argument, that binder being Tag 0A9E”.

[Stacks, Tag 0A9R] at the source's own right adjoint. When the restricted derived direct image is a left adjoint, Stacks.Duality.twistedInverseImage is the right adjoint a of [Stacks, Tag 0A9E] that Lemma 48.13.1 of the source speaks about, and it commutes with direct sums under the same hypotheses as Stacks.Duality.preservesCoproducts_rightAdjoint_of_isCompactObject_pushforward.

theorem preservesCoproducts_twistedInverseImage_of_isCompactObject_pushforward
    [(quasiCoherentDerivedPushforward f hpush).IsLeftAdjoint]
    (E : quasiCoherentDerivedCategory X) (hEc : IsCompactObject.{u} E)
    (hE : (ObjectProperty.singleton E).IsWeakTriangulatedGenerator)
    (hpushE : IsCompactObject.{u} ((quasiCoherentDerivedPushforward f hpush).obj E)) :
    ∀ J : Type u, PreservesColimitsOfShape (Discrete J) (twistedInverseImage f hpush)

Stacks.Duality.preservesColimitsOfShape_rightAdjoint_quasiCoherentDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/RightAdjointDirectSumsPerfectProper.lean, line 111.

Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes and let a be a right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y). Then a commutes with direct sums.

theorem preservesColimitsOfShape_rightAdjoint_quasiCoherentDerivedPushforward [IsNoetherian X]
    [IsNoetherian Y] [Perfect f] [IsProper f]
    {a : quasiCoherentDerivedCategory Y ⥤ quasiCoherentDerivedCategory X}
    (adj : quasiCoherentDerivedPushforward f
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f) ⊣ a) (J : Type u) :
    PreservesColimitsOfShape (Discrete J) a

Stacks.Duality.preservesColimitsOfShape_twistedInverseImage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/RightAdjointDirectSumsPerfectProper.lean, line 123.

For a perfect proper morphism of Noetherian schemes f : X ⟶ Y, the twisted inverse image f^× : D_QCoh(𝒪_Y) ⥤ D_QCoh(𝒪_X), the right adjoint twistedInverseImage f of Rf_*, commutes with direct sums.

instance preservesColimitsOfShape_twistedInverseImage [IsNoetherian X] [IsNoetherian Y]
    [Perfect f] [IsProper f] (J : Type u) :
    PreservesColimitsOfShape (Discrete J)
      (twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f))

Stacks.Duality.preservesCoproducts_twistedInverseImage_of_perfect_proper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/RightAdjointDirectSumsUnconditional.lean, line 70.

[Stacks, Tag 0A9R]. Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes. The twisted inverse image a = f^×, the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) ([Stacks, Tag 0A9E]), commutes with direct sums.

theorem preservesCoproducts_twistedInverseImage_of_perfect_proper (J : Type u) :
    PreservesColimitsOfShape (Discrete J)
      (twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f))

Tag 0AAA, a lemma

Tag 0AAA in the Stacks Project.

Stacks.Duality.isIso_twistedInverseImageRestrictionMap_app_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/ProperPerfectSupport.lean, line 69. The attribute's comment: “(2) variant: for a supplied cartesian square with open immersion j; the tag is isIso_qcqsTwistedInverseImageRestrictionMap_app_of_perfect”.

[Stacks, Tag 0AAA] (2), for a supplied cartesian square. Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes and j : V ⟶ Y an open immersion, with base change j' : U ⟶ X and f' : U ⟶ V. The map (j')^* ∘ a ⟶ a' ∘ j^* of [Stacks, Tag 0A9L] is an isomorphism at every K ∈ D_QCoh(𝒪_Y). The invertibility of ξ : Rj'_* ∘ a' ⟶ a ∘ Rj_* that the map contains is the open-immersion case of [Stacks, Tag 0A9K], Stacks.Duality.isIso_twistedInverseImagePushforwardBaseChange_of_isOpenImmersion. The tag, for every open V ⊆ Y, is Stacks.Duality.isIso_qcqsTwistedInverseImageRestrictionMap_app_of_perfect.

theorem isIso_twistedInverseImageRestrictionMap_app_of_perfect (sq : IsPullback j' f' f j)
    (K : quasiCoherentDerivedCategory Y) :
    haveI : IsOpenImmersion j' := MorphismProperty.of_isPullback sq.flip inferInstance
    haveI : IsProper f' := MorphismProperty.of_isPullback sq inferInstance
    haveI := isNoetherian_of_isOpenImmersion j
    haveI := isNoetherian_of_isProper f'
    haveI := isIso_twistedInverseImagePushforwardBaseChange_of_isOpenImmersion j' f' f j
      (isQuasicoherent_homology_derivedPushforward_of_qcqs j')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs j) sq
    IsIso ((twistedInverseImageRestrictionMap j' f' f j
      (isQuasicoherent_homology_derivedPushforward_of_qcqs j')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f')
      (isQuasicoherent_homology_derivedPushforward_of_qcqs j)
      (isQuasicoherent_homology_derivedRestrict j) (isQuasicoherent_homology_derivedRestrict j')
      sq).app K)

Stacks.Duality.isIso_qcqsTwistedInverseImageRestrictionMap_app_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/ProperPerfectSupport.lean, line 101. The attribute's comment: “(2)”.

[Stacks, Tag 0AAA] (2). Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes and V ⊆ Y an open, with U = f⁻¹(V). The map (j')^* ∘ a ⟶ a' ∘ j^* of [Stacks, Tag 0A9L], Stacks.Duality.OpenImmersion.qcqsTwistedInverseImageRestrictionMap, is an isomorphism at every K ∈ D_QCoh(𝒪_Y). The schemes X, Y are quasi-compact and quasi-separated and V is quasi-compact because they are Noetherian.

theorem isIso_qcqsTwistedInverseImageRestrictionMap_app_of_perfect (V : Y.Opens)
    (K : quasiCoherentDerivedCategory Y) :
    haveI := isNoetherian_of_isOpenImmersion V.ι
    IsIso ((qcqsTwistedInverseImageRestrictionMap f V).app K)

Stacks.Duality.isZero_derivedRestrict_twistedInverseImage_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/ProperPerfectSupport.lean, line 149. The attribute's comment: “(1)”.

[Stacks, Tag 0AAA] (1). Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes, with a the right adjoint of Rf_* on D_QCoh. For every closed T ⊆ Y, if Q ∈ D_QCoh(𝒪_Y) is supported on T then a(Q) is supported on f⁻¹(T). Here T is the complement of the open W, and "supported on T" is "restricts to zero on W". The functor a exists by [Stacks, Tag 0A9E], Stacks.Duality.DerivedPushforward.isLeftAdjoint_quasiCoherentDerivedPushforward_of_qcqs.

theorem isZero_derivedRestrict_twistedInverseImage_of_perfect (W : Y.Opens)
    (Q : quasiCoherentDerivedCategory Y) (hQ : IsZero ((derivedRestrict W.ι).obj Q.obj)) :
    haveI := DerivedPushforward.isLeftAdjoint_quasiCoherentDerivedPushforward_of_qcqs f
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
    IsZero ((derivedRestrict (f ⁻¹ᵁ W).ι).obj
      ((twistedInverseImage f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj Q).obj)

Tag 0A9U, a lemma

Tag 0A9U in the Stacks Project.

Stacks.Duality.isIso_compareWithPullbackTensor_of_isIso_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonGeneral.lean, line 227. The attribute's comment: “the two-variable comparison map for an arbitrary object of D_QCoh(O_Y), by dévissage along a compact generating family. Carried: hgen, the perfect case Stacks 0A9T, asked for only at the generators — held by Stacks.Duality.isIso_compareWithPullbackTensor_of_isPerfect of StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonPerfect.lean; E, hEc, hE, the compact generation of D_QCoh(O_Y) by a perfect object, Stacks 09IS, unproved in this repository and carried the same way by every other consumer here; the instance binder PreservesColimitsOfShape (Discrete J) (quasiCoherentDerivedTensorRight Y L ⋙ a), which is Stacks 0A9R, the commutation of a with direct sums, unproved in this repository; the instance binders Functor.CommShift, Functor.IsTriangulated and NatTrans.CommShift for the two sides and for the comparison map, the triangulated structure PullbackComparison.lean records as unavailable for this repository's derived tensor product; and, inherited from Stacks.Duality.compareWithPullbackTensor, the oplax monoidality α of derived pullback and the invertibility of the projection formula, Stacks 08EU”.

[Stacks, Tag 0A9U]. Let f : X ⟶ Y be a morphism of schemes, let a be a right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y), and let L ∈ D_QCoh(𝒪_Y). Suppose D_QCoh(𝒪_Y) is generated by a family E of compact objects, suppose both sides of the two-variable comparison map of [Stacks, Tag 0A9S] are exact and commute with direct sums as functors of K, suppose the comparison map commutes with the shift, and suppose it is invertible at each E i. Then it is invertible at every K ∈ D_QCoh(𝒪_Y).

This is the source's Lemma 48.13.3. The hypothesis hgen is [Stacks, Tag 0A9T], the perfect case, asked for only at the generators; E, hEc and hE are the compact generation of [Stacks, Tag 09IS]; the direct-sum preservation of quasiCoherentDerivedTensorRight Y L ⋙ a is [Stacks, Tag 0A9R], that a commutes with direct sums. The dévissage is StacksDraft.CompactDevissage.isIso_app_of_isCompactlyGenerated.

theorem isIso_compareWithPullbackTensor_of_isIso_generators {ι : Type u}
    (E : ι → quasiCoherentDerivedCategory Y) (hEc : ∀ i, IsCompactObject.{u} (E i))
    (hE : ∀ Z : quasiCoherentDerivedCategory Y,
      ((ofObj E).shiftClosure ℤ).rightOrthogonal Z → IsZero Z)
    (hgen : ∀ i, IsIso (compareWithPullbackTensor f hpush α adj (E i) L))
    (K : quasiCoherentDerivedCategory Y) :
    IsIso (compareWithPullbackTensor f hpush α adj K L)

Stacks.Duality.isIso_compareWithPullback_of_isIso_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonGeneral.lean, line 297. The attribute's comment: “the structure-sheaf specialization, the map the source displays. Carried: everything Stacks.Duality.isIso_compareWithPullbackTensor_of_isIso_generators carries, at L = 𝒪_Y — hgen, the perfect case Stacks 0A9T held by Stacks.Duality.isIso_compareWithPullbackTensor_of_isPerfect of StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonPerfect.lean; E, hEc, hE, compact generation, Stacks 09IS; the direct-sum preservation of quasiCoherentDerivedTensorRight Y (derivedStructureSheaf Y) ⋙ a, which is Stacks 0A9R; the CommShift/IsTriangulated/NatTrans.CommShift binders; α and Stacks 08EU — and in addition the right unitor of the derived tensor product as the hypothesis ρ, which Stacks.Duality.compareWithPullback already carries because this repository's derived tensor product has no unit”.

[Stacks, Tag 0A9U], the map the source displays. Equation 48.8.0.1 of [Stacks, Tag 0A9S], the map Lf^*K ⊗ᴸ_{𝒪_X} a(𝒪_Y) ⟶ a(K), is an isomorphism for every K ∈ D_QCoh(𝒪_Y): it is the two-variable comparison map at L = 𝒪_Y, which is an isomorphism by Stacks.Duality.isIso_compareWithPullbackTensor_of_isIso_generators, followed by a applied to the right unitor K ⊗ᴸ_{𝒪_Y} 𝒪_Y ≅ K.

theorem isIso_compareWithPullback_of_isIso_generators {ι : Type u}
    (E : ι → quasiCoherentDerivedCategory Y) (hEc : ∀ i, IsCompactObject.{u} (E i))
    (hE : ∀ Z : quasiCoherentDerivedCategory Y,
      ((ofObj E).shiftClosure ℤ).rightOrthogonal Z → IsZero Z)
    (hgen : ∀ i, IsIso (compareWithPullbackTensor f hpush α adj (E i)
      (derivedStructureSheaf Y)))
    (K : quasiCoherentDerivedCategory Y) :
    IsIso (compareWithPullback f hpush α adj ρ K)

Stacks.Duality.isIso_twistedInverseImageCompareWithPullback_of_perfect_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonPerfectProper.lean, line 62.

Stacks Project, Tag 0A9U (Lemma 48.13.3). Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes. The map Lf^*K ⊗ᴸ_{𝒪_X} a(𝒪_Y) ⟶ a(K) of [Stacks, Tag 0A9S] is an isomorphism for every object K of D_QCoh(𝒪_Y).

theorem isIso_twistedInverseImageCompareWithPullback_of_perfect_of_isProper
    (K : quasiCoherentDerivedCategory Y) :
    IsIso (twistedInverseImageCompareWithPullback f
      (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (quasiCoherentDerivedPullbackTensorIso f).hom
      (quasiCoherentDerivedTensorRightUnitor Y) K)

Stacks.Duality.isIso_compareWithPullback_twistedInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/PullbackComparisonUnconditional.lean, line 204.

Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes and let a = f^× be the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) ([Stacks, Tag 0A9E]). The map Lf^*K ⊗ᴸ_{𝒪_X} a(𝒪_Y) ⟶ a(K) of Equation 48.8.0.1 ([Stacks, Tag 0A9S]) is an isomorphism for every object K of D_QCoh(𝒪_Y).

The same holds at any right adjoint of Rf_*, by Stacks.Duality.isIso_compareWithPullback_of_perfect_of_isProper.

theorem isIso_compareWithPullback_twistedInverseImage [IsNoetherian X] [IsNoetherian Y]
    [IsProper f] [AlgebraicGeometry.Perfect f] (K : quasiCoherentDerivedCategory Y) :
    IsIso (compareWithPullback f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
      (pullbackCotensorator f)
      (twistedInverseImageAdjunction f (isQuasicoherent_homology_derivedPushforward_of_qcqs f))
      quasiCoherentRightUnitor K)

Tag 0BZG, a lemma

Tag 0BZG in the Stacks Project.

Stacks.Duality.isIso_torIndependentTwistedInverseImageBaseChange_app_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/PerfectBaseChange.lean, line 157.

[Stacks, Tag 0BZG]. Let f : X ⟶ Y be a perfect proper morphism of Noetherian schemes and g : Y' ⟶ Y a morphism with Y' Noetherian, and let X' = X ×_Y Y', with projections g' : X' ⟶ X and f' : X' ⟶ Y'. If X and Y' are Tor independent over Y, then the base change map L(g')^* a(K) ⟶ a'(Lg^*K) of [Stacks, Tag 0AA6] is an isomorphism for every K ∈ D_QCoh(𝒪_Y), where a and a' are the right adjoints of Rf_* and Rf'_* on D_QCoh ([Stacks, Tag 0A9E]).

theorem isIso_torIndependentTwistedInverseImageBaseChange_app_of_perfect {X' X Y' Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y] [IsNoetherian Y'] {g' : X' ⟶ X} {f' : X' ⟶ Y'}
    {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback g' f' f g) [IsProper f]
    [AlgebraicGeometry.Perfect f] (hTor : TorIndependent f g)
    (K : quasiCoherentDerivedCategory Y) :
    haveI : QuasiCompact f' := MorphismProperty.of_isPullback sq inferInstance
    haveI : QuasiSeparated f' := MorphismProperty.of_isPullback sq inferInstance
    haveI : CompactSpace X' := QuasiCompact.compactSpace_of_compactSpace f'
    haveI : QuasiSeparatedSpace X' := quasiSeparatedSpace_of_quasiSeparated f'
    IsIso ((torIndependentTwistedInverseImageBaseChange sq hTor).app K)

Sources

LeanStacks.Duality.preservesCoproducts_rightAdjoint_of_isCompactObject_pushforward · Stacks.Duality.preservesCoproducts_twistedInverseImage_of_isCompactObject_pushforward · Stacks.Duality.preservesColimitsOfShape_rightAdjoint_quasiCoherentDerivedPushforward · Stacks.Duality.preservesColimitsOfShape_twistedInverseImage · Stacks.Duality.preservesCoproducts_twistedInverseImage_of_perfect_proper · Stacks.Duality.isIso_twistedInverseImageRestrictionMap_app_of_perfect · Stacks.Duality.isIso_qcqsTwistedInverseImageRestrictionMap_app_of_perfect · Stacks.Duality.isZero_derivedRestrict_twistedInverseImage_of_perfect

Section48.14 Right adjoint of pushforward for effective Cartier divisors #

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

Tag 0B4B, a lemma

Tag 0B4B in the Stacks Project.

Stacks.Divisors.normalSheafShiftIsoDerivedSheafHomExactSupport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/EffectiveCartierDerivedSheafHomIso.lean, line 527. The attribute's comment: “the isomorphism 𝒩[-1] ≅ R ℰom(𝒪_D, 𝒪_X), which is what the tag asserts; it is not identified with the canonical comparison morphism Stacks.Divisors.normalSheafShiftToDerivedSheafHomExactSupport”.

[Stacks, Tag 0B4B]. For X a scheme and D ⊆ X an effective Cartier divisor with closed immersion i : D ⟶ X and normal sheaf 𝒩 = 𝒩_{D/X}, there is an isomorphism

𝒩[-1] ≅ R ℰom(𝒪_D, 𝒪_X) in D(𝒪_D),

where R ℰom(𝒪_D, -) is the right adjoint of derived pushforward of [Stacks, Tag 0A76].

This is Stacks.Divisors.derivedSheafHomExactSupportIsoNormalShift precomposed with the normal-sheaf clause of [Stacks, Tag 0B3P] (Stacks.Divisors.normalSheafIsoInvertibleSheaf), which identifies 𝒩_{D/X} with i^* 𝒪_X(D) — the description of 𝒩 the source fixes before stating the lemma. See the module documentation for the proof.

This isomorphism is constructed independently of the canonical comparison morphism Stacks.Divisors.normalSheafShiftToDerivedSheafHomExactSupport; that the comparison morphism is itself invertible is Stacks.Divisors.isIso_normalSheafShiftToDerivedSheafHomExactSupport.

def normalSheafShiftIsoDerivedSheafHomExactSupport :
    (DerivedCategory.singleFunctor D.subscheme.Modules 1).obj (normalSheaf D.subschemeι) ≅
      (closedQuotient D).derivedSheafHomExactSupport.obj
        ((DerivedCategory.singleFunctor X.Modules 0).obj (structureModule X))

Stacks.Divisors.isIso_normalSheafShiftToDerivedSheafHomExactSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/EffectiveCartierDualTriangleFirstMapSectionsCore.lean, line 186.

[Stacks, Tag 0B4B]. For an effective Cartier divisor D ⊆ X the canonical comparison morphism

𝒩_{D/X}[-1] ⟶ R ℰom_{𝒪_X}(𝒪_D, 𝒪_X)

in D(𝒪_D) is an isomorphism.

This is Stacks.Divisors.isIso_normalSheafShiftToDerivedSheafHomExactSupport_of_sectionsCore with its hypothesis supplied by …ClosedQuotientMorphismOfRingedSpaces.sheafHomPushforwardSectionsCore.

theorem isIso_normalSheafShiftToDerivedSheafHomExactSupport :
    IsIso (normalSheafShiftToDerivedSheafHomExactSupport D)

Tag 0B4C, an equation

Tag 0B4C in the Stacks Project.

RingedSpaceModuleAdjunction.ClosedQuotientMorphismOfRingedSpaces.derivedPullbackTensorSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointLemmas/ExactSupportDerivedTensorHomMap.lean, line 201. The attribute's comment: “the canonical map, unconditionally; not functoriality in the complex and not compatibility with distinguished triangles”.

Stacks Project, Tag 0B4C. The canonical map

Li^*K ⊗^L_{𝒪_Z} R ℰom(𝒪_Z, 𝒪_X) ⟶ R ℰom(𝒪_Z, K)

in D(𝒪_Z): the map corresponding to derivedPullbackTensorSheafHomMateMap under the adjunction i_* ⊣ R ℰom(𝒪_Z, -) of [Stacks, Tag 0A76].

def derivedPullbackTensorSheafHomMap
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing S.X))) :
    S.derivedPullbackTensorSheafHom.obj K ⟶ S.derivedSheafHomExactSupport.obj K

RingedSpaceModuleAdjunction.ClosedQuotientMorphismOfRingedSpaces.derivedPullbackTensorSheafHomMap_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointLemmas/ExactSupportDerivedTensorHomMap.lean, line 210. The attribute's comment: “the adjunction equation characterizing the canonical map”.

Stacks Project, Tag 0B4C. The adjunction equation characterizing the canonical map: pushing it forward and composing with the counit of [Stacks, Tag 0A76] gives the displayed composite. This is what "adjoint to" means in the source.

theorem derivedPullbackTensorSheafHomMap_mate
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing S.X))) :
    (modulePushforward S.i).mapDerivedCategory.map
          (S.derivedPullbackTensorSheafHomMap K) ≫
        S.derivedSheafHomAdjunction.counit.app K =
      S.derivedPullbackTensorSheafHomMateMap K

RingedSpaceModuleAdjunction.ClosedQuotientMorphismOfRingedSpaces.derivedPullbackTensorSheafHomMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointLemmas/ExactSupportDerivedTensorHomMap.lean, line 225. The attribute's comment: “uniqueness of the canonical map subject to the adjunction equation”.

Stacks Project, Tag 0B4C. The adjunction equation determines the canonical map: no other morphism of that type satisfies it. Together with derivedPullbackTensorSheafHomMap_mate this is the canonicality the source asserts.

theorem derivedPullbackTensorSheafHomMap_unique
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing S.X)))
    (τ : S.derivedPullbackTensorSheafHom.obj K ⟶ S.derivedSheafHomExactSupport.obj K)
    (hτ : (modulePushforward S.i).mapDerivedCategory.map τ ≫
        S.derivedSheafHomAdjunction.counit.app K =
      S.derivedPullbackTensorSheafHomMateMap K) :
    τ = S.derivedPullbackTensorSheafHomMap K

Tag 0AA4, a lemma

Tag 0AA4 in the Stacks Project.

Stacks.Divisors.normalTensorDerivedSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/EffectiveCartierDerivedSheafHom.lean, line 270. The attribute's comment: “the canonical map Li^*K ⊗ᴸ 𝒩[-1] ⟶ R ℰom(𝒪_D, K) only, unconditionally; that the map is an isomorphism is not proved, since that needs the isomorphism assertion of Tag 0B4B, which this file states only as a map, and functoriality in K is not proved either”.

[Stacks, Tag 0AA4], the canonical map

Li^*K ⊗^L_{𝒪_D} 𝒩[-1] ⟶ R ℰom(𝒪_D, K) in D(𝒪_D),

for K in D(𝒪_X): the canonical map (48.14.1.1) of [Stacks, Tag 0B4C] precomposed with the comparison morphism 𝒩[-1] ⟶ R ℰom(𝒪_D, 𝒪_X) of [Stacks, Tag 0B4B] tensored with Li^*K. This is the composite the source forms; that it is an isomorphism is Stacks.Divisors.isIso_normalTensorDerivedSheafHomMap, and that it is natural in K is Stacks.Divisors.normalTensorDerivedSheafHomMap_natural.

def normalTensorDerivedSheafHomMap
    (K : DerivedCategory X.Modules) :
    (normalTensorDerivedPullback D).obj K ⟶
      (closedQuotient D).derivedSheafHomExactSupport.obj K

Stacks.Divisors.normalTensorDerivedSheafHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/EffectiveCartierNormalTensorIso.lean, line 155.

[Stacks, Tag 0AA4]. Let X be a scheme and D ⊆ X an effective Cartier divisor, with closed immersion i : D ⟶ X and normal sheaf 𝒩. Then the map (48.14.1.1) of [Stacks, Tag 0B4C] combined with the isomorphism R ℰom(𝒪_D, 𝒪_X) ≅ 𝒩[-1] of [Stacks, Tag 0B4B] defines an isomorphism

Li^*K ⊗^L_{𝒪_D} 𝒩[-1] ⟶ R ℰom(𝒪_D, K)

functorial in K in D(𝒪_X).

The isomorphism of functors D(𝒪_X) ⥤ D(𝒪_D) below has as component at K exactly the composite Stacks.Divisors.normalTensorDerivedSheafHomMap the source forms (Stacks.Divisors.normalTensorDerivedSheafHomIso_hom_app): the comparison morphism 𝒩[-1] ⟶ R ℰom(𝒪_D, 𝒪_X) of [Stacks, Tag 0B4B] tensored with Li^*K, followed by the map of [Stacks, Tag 0B4C]. Here 𝒩 is the normal sheaf Stacks.Divisors.normalSheaf of the closed immersion, R ℰom(𝒪_D, -) is the right adjoint of derived pushforward of [Stacks, Tag 0A76], and Li^* and ⊗^L are the derived pullback and derived tensor product of the library.

def normalTensorDerivedSheafHomIso :
    normalTensorDerivedPullback D ≅ (closedQuotient D).derivedSheafHomExactSupport

Sources

LeanStacks.Divisors.normalSheafShiftIsoDerivedSheafHomExactSupport · Stacks.Divisors.isIso_normalSheafShiftToDerivedSheafHomExactSupport · RingedSpaceModuleAdjunction.ClosedQuotientMorphismOfRingedSpaces.derivedPullbackTensorSheafHomMap · RingedSpaceModuleAdjunction.ClosedQuotientMorphismOfRingedSpaces.derivedPullbackTensorSheafHomMap_mate · RingedSpaceModuleAdjunction.ClosedQuotientMorphismOfRingedSpaces.derivedPullbackTensorSheafHomMap_unique · Stacks.Divisors.normalTensorDerivedSheafHomMap · Stacks.Divisors.normalTensorDerivedSheafHomIso

Section48.15 Right adjoint of pushforward in examples #

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

Tag 0A9W, a lemma

Tag 0A9W in the Stacks Project.

Stacks.Duality.ProjectiveBundleDualizing.nonempty_dualizingObject_iso_twistedInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProjectiveBundle/TwistedInverseImage.lean, line 471. The attribute's comment: “the projective bundle P(E) is the relative Proj of Sym(E) with twists O(d) of a twist datum D, and f^L(-n-1) is written O(-n-1) ⊗ π^(∧^(n+1) E); the special case E = O^(n+1) on projectiveSpaceOver is nonempty_twistedInverseImage_derivedStructureSheaf_iso_of_qcqs”.

[Stacks, Tag 0A9W]. Let S be a quasi-compact and quasi-separated scheme, ℰ a finite locally free 𝒪_S-module of rank n + 1 with determinant 𝓛 = ⋀ⁿ⁺¹ ℰ, π : 𝐏(ℰ) ⟶ S the projection and a the right adjoint of R π_* : D_QCoh(𝒪_{𝐏(ℰ)}) ⥤ D_QCoh(𝒪_S) of [Stacks, Tag 0A9E]. Then π^*𝓛(-n-1)[n] ≅ a(𝒪_S), for every n ≥ 0; the isomorphism is the transpose dualizingComparison of the trace R π_*(π^*𝓛(-n-1)[n]) ≅ 𝒪_S.

For ℰ = 𝒪_S^{⊕ n+1} and projective space in the model projectiveSpaceOver, the statement a(𝒪_S) ≅ 𝒪(-n-1)[n] is Stacks.Duality.ProjectiveSpace.nonempty_twistedInverseImage_derivedStructureSheaf_iso_of_qcqs.

theorem nonempty_dualizingObject_iso_twistedInverseImage :
    haveI := quasiCompact_proj E hqc hfree
    haveI := AlgebraicGeometry.isLeftAdjoint_qcqsQuasiCoherentDerivedPushforward (proj E hqc)
    Nonempty (dualizingObject E hqc D hfree ≅ (twistedInverseImage (proj E hqc)
      (isQuasicoherent_homology_derivedPushforward_of_qcqs (proj E hqc))).obj
        (DerivedPushforward.derivedStructureSheaf S))

Tag 0AAC, an example

Tag 0AAC in the Stacks Project.

Stacks.Duality.BlowupBaseChange.baseChange_example, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/BlowupBaseChange/Example.lean, line 238.

[Stacks, Example 0AAC]: the base change map (48.5.0.1) is not an isomorphism for a perfect proper f and a perfect g. Let k be a field, f : X ⟶ Y = 𝐀²_k the blowup of the origin, g : Y' = Spec k ⟶ Y the origin and X' = E = 𝐏¹_k the exceptional divisor, with g' : X' ⟶ X its inclusion and f' : X' ⟶ Y' its structure morphism; let a, a' be the right adjoints of Rf_*, Rf'_* on D_QCoh ([Stacks, Tag 0A9E]). Then f is proper and perfect, g is perfect, the square is cartesian, f and g are not Tor independent, and no morphism L(g')^* a(𝒪_Y) ⟶ a'(Lg^* 𝒪_Y) — in particular no base change map — is an isomorphism.

theorem baseChange_example :
    IsProper (f k) ∧ Perfect (f k) ∧ Perfect (g k) ∧
      IsPullback (g' k) (projToSpecCoeff k 1) (f k) (g k) ∧ ¬ TorIndependent (f k) (g k) ∧
      ∀ φ : (twistedInverseImage (f k)
          (isQuasicoherent_homology_derivedPushforward_of_qcqs (f k)) ⋙
            quasiCoherentDerivedPullback' (g' k)).obj (structureSheaf k) ⟶
        (quasiCoherentDerivedPullback' (g k) ⋙
          twistedInverseImage (projToSpecCoeff k 1)
            (isQuasicoherent_homology_derivedPushforward_of_qcqs (projToSpecCoeff k 1))).obj
            (structureSheaf k), ¬ IsIso φ

Tag 0BQW, a lemma

Tag 0BQW in the Stacks Project.

Stacks.Duality.normalSheafToSheafExtOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Sweep/NormalSheafAsSheafExt.lean, line 415. The attribute's comment: “the canonical map c itself; isIso_normalSheafToSheafExtOne is the assertion that it is an isomorphism”.

The canonical map c of [Stacks, Tag 0BQW]. The normal sheaf 𝒩 = 𝓗om_{𝒪_Y}(ℐ/ℐ², 𝒪_X) maps canonically to 𝓔xt¹_{𝒪_Y}(𝒪_X, 𝒪_X): precompose with ℐ ↠ ℐ/ℐ² to land in 𝓗om_{𝒪_Y}(ℐ, 𝒪_X), identify that with the degree-zero cohomology of 𝓗om_{𝒪_Y}(ℐ, J) for the injective resolution J of 𝒪_X that the derived functor uses, and take the degree-one connecting map of sheafHomComplexSequence. On a local section of 𝒩 this is the class of the pushout of the second-order thickening sequence of [Stacks, Tag 0BQX] along it, which is how the source constructs c.

public def normalSheafToSheafExtOne :
    normalSheafOfIdealSheaf Y I ⟶
      Stacks.RingedSpace.sheafExt Y (quotientByIdealSheaf Y I) (quotientByIdealSheaf Y I) 1

Stacks.Duality.isIso_normalSheafToSheafExtOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Sweep/NormalSheafAsSheafExt.lean, line 815.

Stacks Project, Tag 0BQW. Let Y be a ringed space, let ℐ ⊆ 𝒪_Y be a sheaf of ideals, put 𝒪_X = 𝒪_Y/ℐ and let 𝒩 = 𝓗om_{𝒪_Y}(ℐ/ℐ², 𝒪_X) be the normal sheaf. The canonical map c : 𝒩 ⟶ 𝓔xt¹_{𝒪_Y}(𝒪_X, 𝒪_X) of normalSheafToSheafExtOne is an isomorphism.

All four inputs of the source's proof are proved here: isIso_internalHomMapLeft_cokernelπ_idealSquareInclusion (every 𝒪_Y-linear map ℐ ⟶ 𝒪_X factors uniquely through ℐ/ℐ²), internalHomMapLeft_ι_app_quotient_eq_zero (the degree-zero map vanishes, because ℐ annihilates 𝒪_X), sheafHomComplexSequence_shortExact ([Stacks, Tag 01DR] for sheaves of modules) and Stacks.RingedSpace.isZero_sheafExt_unit_succ (𝓔xt¹_{𝒪_Y}(𝒪_Y, 𝒪_X) = 0).

public theorem isIso_normalSheafToSheafExtOne :
    IsIso (normalSheafToSheafExtOne Y I)

Tag 0BQX, an equation

Tag 0BQX in the Stacks Project.

Stacks.Duality.secondOrderThickening_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Sweep/SecondOrderThickening.lean, line 89.

Stacks Project, Tag 0BQX. For an ideal sheaf I on a ringed space, the canonical sequence 0 ⟶ I / I² ⟶ 𝒪_Y / I² ⟶ 𝒪_Y / I ⟶ 0 is short exact. The displayed equations say that its arrows are induced by the inclusion I ⟶ 𝒪_Y and the identity of 𝒪_Y, respectively.

public theorem secondOrderThickening_shortExact (Y : RingedSpace.{u, u})
    (I : (SheafOfModules.unit (structureSheafRing Y)).Submodule) :
    let I2 := idealSquare Y I
    ∃ (j : I2.toSheafOfModules ⟶ I.toSheafOfModules)
      (_hj : j ≫ I.ι = I2.ι)
      (f : cokernel j ⟶ cokernel I2.ι)
      (g : cokernel I2.ι ⟶ cokernel I.ι)
      (hzero : f ≫ g = 0),
      (cokernel.π j ≫ f = I.ι ≫ cokernel.π I2.ι) ∧
        (cokernel.π I2.ι ≫ g = cokernel.π I.ι) ∧
          (ShortComplex.mk f g hzero).ShortExact

Tag 0BQY, a lemma

Tag 0BQY in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isIso_desc_app_isKoszulRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularSequence/KoszulSelfExtKoszulRegular.lean, line 148.

Let Y be a ringed space, 𝓘 ⊆ O_Y a Koszul-regular sheaf of ideals and O_X = O_Y/𝓘. Let A be, with its degree-one generator ι, the exterior algebra over O_X of Ext¹_{O_Y}(O_X, O_X). Then the homomorphism of sheaves of graded algebras that the identity of Ext¹_{O_Y}(O_X, O_X) induces out of A — the comparison

⋀ⁿ(Ext¹_{O_Y}(O_X, O_X)) ⟶ Extⁿ_{O_Y}(O_X, O_X)

that composition makes — is an isomorphism in every degree n.

theorem isIso_desc_app_isKoszulRegularIdealSheaf (hJ : IsKoszulRegularIdealSheaf Y J)
    (A : _root_.SheafOfModules.GradedAlgebra.{u, u}
      (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} (quotientRingSheaf.{u, u, u} J)))
    (ι : (koszulRegularSelfExtAlgebra J hJ).piece 1 ⟶ A.piece 1)
    (hA : _root_.SheafOfModules.GradedAlgebra.IsExteriorAlgebra A ι) (n : ℤ) :
    IsIso ((hA.desc (koszulRegularSelfExtAlgebra J hJ)
      (𝟙 ((koszulRegularSelfExtAlgebra J hJ).piece 1))
      (squareZero_id_koszulRegularSelfExtAlgebra J hJ)).app n)

Tag 0BQZ, a lemma

Tag 0BQZ in the Stacks Project.

Stacks.RegularSequence.KoszulChainData.isZero_derivedSheafExt_unit_of_notMem_Icc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularSequence/KoszulExtStructureSheaf.lean, line 190. The attribute's comment: “ONLY the degrees outside 0, …, r of the vanishing half of the tag: the Ext sheaves Ext^i_{O_Y}(O_Y/I, O_Y) are zero for i < 0 and for i > r. Carried: the ideal sheaf is presented GLOBALLY by a Koszul-regular sequence of r sections -- a Koszul chain datum for φ : (O_Y)^r ⟶ O_Y whose augmentation is a quasi-isomorphism -- where the tag assumes only the local condition that I be Koszul-regular, so the opening reduction of its proof is not performed and the tag's locally varying r is here constant. NOT covered: the degrees 0, …, r - 1, the identification of Ext^r with the top exterior power of the normal sheaf, and the derived-category isomorphism RHom(O_X, O_Y) = (top exterior power of N)[-r]”.

The Ext sheaves of a Koszul-regular quotient into the structure sheaf vanish outside the degrees 0, …, r. For an ideal sheaf ℐ ⊂ O_Y generated by a Koszul-regular sequence of r global sections, with quotient O_X = O_Y/ℐ,

𝓔xt^n_{O_Y}(O_X, O_Y) = 0 for n < 0 and for n > r.

This is part of the vanishing half of [Stacks, Tag 0BQZ], whose conclusion R𝓗om_{O_Y}(O_X, O_Y) = ⋀^r 𝒩 [-r] says that these Ext sheaves vanish in every degree other than r and that the r-th one is the top exterior power of the normal sheaf. The degrees 0, …, r - 1 and the degree r itself are not treated: they are where the differential of the Hom complex, which is not zero, has to be computed.

theorem isZero_derivedSheafExt_unit_of_notMem_Icc (K : KoszulChainData.{u, u, u} A φ)
    [QuasiIso K.augmentation] {n : ℤ} (hn : n < 0 ∨ (r : ℤ) < n) :
    IsZero (derivedSheafExt Rc
      (DerivedCategory.Q.obj
        ((single (StructureSheafModules Rc) (ComplexShape.up ℤ) 0).obj
          (quotient Rc (φ := φ))))
      (DerivedCategory.Q.obj (unitSingleComplex Rc)) n)

Stacks.AlgebraicGeometry.RegularIdealSheaf.nonempty_derivedSheafHom_iso_rankExterior, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularSequence/KoszulRegularDerivedDual.lean, line 806.

Stacks Project, Tag 0BQZ. Let Y be a ringed space, 𝓘 ⊆ O_Y a sheaf of ideals, O_X = O_Y/𝓘 and 𝒩 = 𝓗om_{O_Y}(𝓘/𝓘², O_X). If 𝓘 is Koszul-regular, then

R𝓗om_{O_Y}(O_X, O_Y) ≅ ⋀^r 𝒩 [-r]

in D(O_Y), where r : Y → ℕ sends y to the minimal number of generators of 𝓘 needed in a neighbourhood of y (localGeneratorCount). The right-hand side is the complex with zero differential whose degree-n term is the n-th exterior power of 𝒩 over O_X (the exterior algebra SheafOfModules.algebras of normalSheafQuotient) on the locus where r = n, extended by zero (rankExteriorTerm): r is locally constant on the support of O_X, and every term of the formula vanishes off it. See the module docstring for the codomain of r.

theorem nonempty_derivedSheafHom_iso_rankExterior (hJ : IsKoszulRegularIdealSheaf Y J) :
    Nonempty (((derivedSheafHom Y.sheaf).obj (op (DerivedCategory.Q.obj
        ((single (StructureSheafModules Y.sheaf) (ComplexShape.up ℤ) 0).obj (cokernel J.ι))))).obj
        (DerivedCategory.Q.obj ((single (StructureSheafModules Y.sheaf) (ComplexShape.up ℤ) 0).obj
          (_root_.SheafOfModules.unit (structureSheaf Y.sheaf)))) ≅
      DerivedCategory.Q.obj (CochainComplex.zeroDifferentialComplex (rankExteriorTerm (J := J)
        (_root_.SheafOfModules.algebras (Opens.grothendieckTopology Y.carrier)
          (normalSheafQuotient J)).exterior)))

Tag 0BR0, a lemma

Tag 0BR0 in the Stacks Project.

Stacks.Duality.KoszulRegular.nonempty_normalExteriorComplex_iso_rightAdjoint_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/KoszulRegularRightAdjoint.lean, line 135.

Stacks Project, Tag 0BR0. Let Y be a quasi-compact and quasi-separated scheme, let i : X ⟶ Y be a Koszul-regular closed immersion, and let a be the right adjoint of Ri_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) of [Stacks, Tag 0A9E]. Then there is an isomorphism

⋀^r 𝒩 [-r] ≅ a(𝒪_Y),

where 𝒩 = 𝓗om_{𝒪_X}(𝒞_{X/Y}, 𝒪_X) is the normal sheaf of i (Stacks.Divisors.normalSheaf) and r is its rank, a locally constant function on X (normalRank). Since r is only locally constant, ⋀^r 𝒩 [-r] is the complex with zero differential whose degree-n term is ⋀ⁿ𝒩 on the open and closed locus where r = n, extended by zero (normalExteriorComplex): on that locus it is ⋀ⁿ𝒩[-n].

The right adjoint a is quantified over together with its adjunction, which determines it up to unique isomorphism; the derived categories are the locally small models AlgebraicGeometry.Scheme.Modules.hasDerivedCategory, at which [Stacks, Tag 0A9E] produces a. The isomorphism is one of objects of D(𝒪_X); D_QCoh(𝒪_X) being a full subcategory, it is an isomorphism there.

The proof is the source's. By [Stacks, Tags 0A9X and 0A77], a(𝒪_Y) is R ℰom(𝒪_X, 𝒪_Y) and its pushforward is R𝓗om_{𝒪_Y}(i_*𝒪_X, 𝒪_Y), which [Stacks, Tag 0BQZ] computes: its cohomology sheaves are ⋀ⁿ𝒩 on the locus where r = n, extended by zero (Stacks.AlgebraicGeometry.RegularIdealSheaf.extIsoRankExteriorTerm). As i_* is exact and fully faithful on modules ([Stacks, Tag 08KS]), the cohomology sheaves of a(𝒪_Y) are the terms of ⋀^r 𝒩 [-r]; they are concentrated in one degree on each member of the disjoint open cover of X by the rank loci, so a(𝒪_Y) is isomorphic to the complex of its cohomology sheaves with zero differential (Stacks.SheafOfModules.nonempty_iso_zeroDifferentialComplex_homology_of_cover).

theorem nonempty_normalExteriorComplex_iso_rightAdjoint_structureSheaf
    [CompactSpace Y] [QuasiSeparatedSpace Y] (hi : IsKoszulRegularImmersion i)
    (a : quasiCoherentDerivedCategory Y ⥤ quasiCoherentDerivedCategory X)
    (adj : DerivedPushforward.qcqsRestrictedDerivedPushforward i ⊣ a) :
    Nonempty ((DerivedCategory.Q (C := X.Modules)).obj (normalExteriorComplex i hi) ≅
      (a.obj (DerivedPushforward.derivedStructureSheaf Y)).obj)

Tag 0BRT, a lemma

Tag 0BRT in the Stacks Project.

Stacks.Duality.singleFunctorExteriorPowerIsoRelativeDualizingComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/SmoothProper/RelativeDualizingComplex.lean, line 40.

[Stacks, Tag 0BRT]. Let S be a Noetherian scheme and f : X ⟶ S a smooth proper morphism of relative dimension d, and let a be the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_S) ([Stacks, Tag 0A9E]). Then there is an isomorphism ∧^d Ω_{X/S}[d] ≅ a(𝒪_S) in D(𝒪_X).

def singleFunctorExteriorPowerIsoRelativeDualizingComplex {X S : Scheme.{u}} [IsNoetherian S]
    (f : X ⟶ S) (d : ℕ) [SmoothOfRelativeDimension d f] [IsProper f] :
    haveI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    haveI : QuasiSeparatedSpace X := quasiSeparatedSpace_of_quasiSeparated f
    (DerivedCategory.singleFunctor X.Modules (-d)).obj
        (Scheme.Modules.exteriorPower (Scheme.Hom.relativeDifferentials f) d) ≅
      (relativeDualizingComplex f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)
        (DerivedPushforward.derivedStructureSheaf S)).obj

Sources

LeanStacks.Duality.ProjectiveBundleDualizing.nonempty_dualizingObject_iso_twistedInverseImage · Stacks.Duality.BlowupBaseChange.baseChange_example · Stacks.Duality.normalSheafToSheafExtOne · Stacks.Duality.isIso_normalSheafToSheafExtOne · Stacks.Duality.secondOrderThickening_shortExact · Stacks.AlgebraicGeometry.RegularIdealSheaf.isIso_desc_app_isKoszulRegularIdealSheaf · Stacks.RegularSequence.KoszulChainData.isZero_derivedSheafExt_unit_of_notMem_Icc · Stacks.AlgebraicGeometry.RegularIdealSheaf.nonempty_derivedSheafHom_iso_rankExterior

Section48.16 Upper shriek functors #

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

Tag 0A9Y, the section

Tag 0A9Y in the Stacks Project.

Stacks.Duality.upperShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/Basic.lean, line 192.

Stacks Project, Tag 0A9Y. The upper shriek functor of a compactification. Let S be a quasi-compact quasi-separated scheme (in the source, a Noetherian one), let f : X ⟶ Y be a morphism of schemes separated and of finite type over S and let j be a compactification of X over Y, with open immersion j.immersion : X ⟶ X̄ and proper structure morphism f̄ = j.toBase : X̄ ⟶ Y. Let ā be the right adjoint of Rf̄_* : D_QCoh(𝒪_X̄) ⥤ D_QCoh(𝒪_Y) of [Stacks, Tag 0A9E]. Then f^! K = ā(K)|_X, that is f^! = j^* ∘ ā.

def upperShriek :
    quasiCoherentDerivedCategory Y.left ⥤ quasiCoherentDerivedCategory X.left

Tag 0F42, a situation

Tag 0F42 in the Stacks Project.

AlgebraicGeometry.isSeparatedFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/SeparatedFiniteTypeCategory.lean, line 67. The attribute's comment: “the condition on the objects”. References: SGA 4 Vbis (5.3.1); SGA 4 XVII (7.0.1).

A morphism of schemes is separated and of finite type when it is separated, locally of finite type and quasi-compact.

abbrev isSeparatedFiniteType : MorphismProperty Scheme.{u}

AlgebraicGeometry.FTS, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/SeparatedFiniteTypeCategory.lean, line 80. The attribute's comment: “the category”. References: SGA 4 Vbis (5.3.1).

The category of schemes separated and of finite type over S: its objects are the schemes over S whose structure morphism is separated and of finite type, and its morphisms are the morphisms of schemes over S between them.

abbrev FTS (S : Scheme.{u}) : Type (u + 1)

Tag 0AA0, a lemma

Tag 0AA0 in the Stacks Project.

Stacks.Duality.compactificationUpperShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Compactification/ShriekIndependence.lean, line 203. The attribute's comment: “the canonical isomorphism f^!_j = f^!_k between the upper shriek functors (Stacks.Duality.compactificationUpperShriek, which is Stacks.Duality.upperShriek of Stacks 0A9Y, read on D^+_QCoh(O_Y) as in the source) of any two compactifications j, k of a morphism f : X -> Y of FTS S over a Noetherian S: the source's alpha_{g_1}^{-1} then alpha_{g_2} for the two projections of the common refinement with dense interior of Stacks 0ATU. Nothing is carried: alpha_g needs Stacks 0A9K for the square of g, which is Stacks.Duality.isIso_refinementXi, and Stacks 0A9P (2) for it (G proper, Xbar_2 Noetherian), which is Stacks.Duality.isIso_refinementBaseChangePlus, both instances. Its value on the diagonal is the identity (Stacks.Duality.compactificationUpperShriekIso_refl), it is transitive (Stacks.Duality.compactificationUpperShriekIso_trans) and it is the source's alpha_g for an interior-preserving g (Stacks.Duality.compactificationUpperShriekIso_eq_iso); Stacks.Duality.exists_coherent_compactificationUpperShriekIso collects these. The compactifications are arguments; that one exists is Stacks 0F41”.

[Stacks, Tag 0AA0]: the canonical comparison of the upper shriek functors of two compactifications. It is α_{g₁}⁻¹ ≫ α_{g₂} for the two projections of the common refinement with dense interior of [Stacks, Tag 0ATU], as an isomorphism of functors out of D⁺_QCoh(𝒪_Y).

def compactificationUpperShriekIso (j k : CompactificationOf (Over.mk f.left)) :
    compactificationUpperShriek f j ≅ compactificationUpperShriek f k

Stacks.Duality.exists_coherent_compactificationUpperShriekIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Compactification/ShriekIndependence.lean, line 328. The attribute's comment: “the upper shriek functor of a compactification (Stacks.Duality.compactificationUpperShriek, which is Stacks.Duality.upperShriek of Stacks 0A9Y) on D^+_QCoh(O_Y), the source's own domain for it, is independent of the compactification up to canonical isomorphism: a family of isomorphisms between the functors of any two compactifications that is the identity on the diagonal, transitive, and equal to the source's alpha_g (Stacks.Duality.refinementIso) whenever the two compactifications are joined by an interior-preserving morphism g. Nothing is carried; the family is Stacks.Duality.compactificationUpperShriekIso”.

[Stacks, Tag 0AA0]: the upper shriek functor is independent of the compactification, by a coherent family of isomorphisms. There is a family of isomorphisms e j k : f^!_j ≅ f^!_k of functors out of D⁺_QCoh(𝒪_Y), indexed by pairs of compactifications of X over Y, which is the identity on the diagonal, composes transitively, and agrees with the source's comparison α_g whenever j and k are joined by an interior-preserving morphism g. So the isomorphism class of f^! does not depend on the compactification, the identifications of three compactifications are compatible, and the family is the source's.

The family is Stacks.Duality.compactificationUpperShriekIso itself; reflexivity is Stacks.Duality.compactificationUpperShriekIso_refl, transitivity is Stacks.Duality.compactificationUpperShriekIso_trans, and the agreement with α_g is Stacks.Duality.compactificationUpperShriekIso_eq_iso.

theorem exists_coherent_compactificationUpperShriekIso :
    ∃ e : ∀ j k : CompactificationOf (Over.mk f.left),
        compactificationUpperShriek f j ≅ compactificationUpperShriek f k,
      (∀ j, e j j = Iso.refl _) ∧ (∀ j k l, e j k ≪≫ e k l = e j l) ∧
        ∀ (j k : CompactificationOf (Over.mk f.left)) (g : j ⟶ k)
          (hg : CompactificationOf.PreservesInterior g), e j k = refinementIso f g hg

Tag 0ATX, a lemma

Tag 0ATX in the Stacks Project.

Stacks.Duality.upperShriekCompIsoAtModel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Compactification/ShriekComposition.lean, line 1073. The attribute's comment: “the canonical isomorphism (g o f)^! = f^! o g^! of upper shriek functors for composable morphisms f : X -> Y, g : Y -> Z of FTS S over a Noetherian S, at arbitrary compactifications k of g o f, j of f and i of g, as functors out of D^+_QCoh(O_Z), with g^! read in D^+_QCoh(O_Y) (Stacks 0A9I) and each f^! the functor Stacks.Duality.compactificationUpperShriek of Stacks 0A9Y/0AA0. It is the source's construction for a choice of compactifications through i: (j' o j)^ a b = j^ (j')^ a b -> j^ a' i^* b via the base change map of Stacks 0AA6, invertible by Stacks 0A9P (2), read through the canonical comparisons of Stacks 0AA0. Canonicity is proved, not assumed: Stacks.Duality.upperShriekCompIsoAtModel_choice says it is the source's isomorphism for every choice (the second half of the source's proof: the chase of squares A..F through Stacks 0ATQ and 0ATR, and a dominating choice from Stacks 0ATU), and Stacks.Duality.upperShriekCompIsoAtModel_naturality says it is compatible with the comparisons of Stacks 0AA0 in all three compactifications. The compactifications are arguments, as in Stacks 0AA0; that they exist is Stacks 0F41”.

[Stacks, Tag 0ATX]: the canonical isomorphism (g ∘ f)^! ≅ f^! ∘ g^!, for any compactifications k of g ∘ f, j of f and i of g. It is the source's construction for a choice of compactifications whose compactification of Y is i (that one exists is [Stacks, Tag 0A9Z]), read through the canonical comparisons of [Stacks, Tag 0AA0].

def upperShriekCompIsoAtModel (k : CompactificationOf (Over.mk (f ≫ g).left))
    (j : CompactificationOf (Over.mk f.left)) (i : CompactificationOf (Over.mk g.left)) :
    compactificationUpperShriek (f ≫ g) k ≅
      upperShriekPlusAtModel i ⋙ compactificationUpperShriek f j

Stacks.Duality.exists_canonical_upperShriekCompIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Compactification/ShriekComposition.lean, line 1136. The attribute's comment: “existence and canonicity of the isomorphism (g o f)^! = f^! o g^! for composable morphisms of FTS S over a Noetherian S, the upper shriek functors being those of Stacks 0AA0 on D^+_QCoh and g^! read in D^+_QCoh(O_Y): a family of isomorphisms indexed by compactifications of g o f, f and g that equals the source's construction for every choice of compactifications (Stacks.Duality.CompositionData.compIsoAPI) and is compatible with the comparisons of Stacks 0AA0 in all three compactifications. Nothing is assumed beyond the compactifications themselves, which are arguments as in Stacks 0AA0 (their existence is Stacks 0F41)”.

[Stacks, Tag 0ATX]: there is a canonical isomorphism (g ∘ f)^! → f^! ∘ g^!. For composable morphisms f : X ⟶ Y, g : Y ⟶ Z of AlgebraicGeometry.FTS S over a Noetherian S there is a family of isomorphisms (g ∘ f)^!_k ≅ f^!_j ∘ g^!_i, indexed by compactifications k of g ∘ f, j of f and i of g, which is the source's construction for every choice of compactifications, and which is compatible with the canonical comparisons of [Stacks, Tag 0AA0] in all three compactifications — so it is independent of the choices made. The family is Stacks.Duality.upperShriekCompIsoAtModel.

theorem exists_canonical_upperShriekCompIso :
    ∃ e : ∀ (k : CompactificationOf (Over.mk (f ≫ g).left))
        (j : CompactificationOf (Over.mk f.left)) (i : CompactificationOf (Over.mk g.left)),
        compactificationUpperShriek (f ≫ g) k ≅ upperShriekPlusAtModel i ⋙
            compactificationUpperShriek f j,
      (∀ D : CompositionData f g, e D.outer D.inner D.base = D.compIsoAPI) ∧
      ∀ k k' j j' i i', compactificationUpperShriekIso (f ≫ g) k k' ≪≫ e k' j' i' =
        e k j i ≪≫ NatIso.hcomp (basePlusIsoAPI i i') (compactificationUpperShriekIso f j j')

Tag 0ATY, a lemma

Tag 0ATY in the Stacks Project.

Stacks.Duality.exists_upperShriekPseudofunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Compactification/ShriekPseudofunctor/Pseudofunctor.lean, line 222. The attribute's comment: “the full statement: Stacks.Duality.upperShriekPseudofunctor is a pseudofunctor LocallyDiscrete (FTS S)^op -> Cat (Mathlib's Pseudofunctor, i.e. Categories 003N with conditions (a) invertibility, (b), (c) unit laws and (d) cocycle condition as its axioms) over a Noetherian S, with object X |-> D^+_QCoh(O_X), morphism f |-> f^! of Stacks 0AA0 (the functor Stacks.Duality.compactificationUpperShriek of a compactification of f, read in D^+_QCoh, Stacks 0A9I; compactifications exist by Stacks 0F41) and compositor the canonical isomorphism (g o f)^! = f^! o g^! of Stacks 0ATX (Stacks.Duality.upperShriekCompIsoAtModel). The cocycle condition (d) is the source's proof, Stacks.Duality.upperShriekCompIsoAtModel_cocycle: a choice Zbar over T, Ybar over Zbar, Xbar over Ybar (0F41, 0A9Z), the squares A, B, C, and gamma_{A+B} = gamma_A o gamma_B (0ATR), gamma_{B+C} = gamma_C o gamma_B (0ATQ), gamma_A and gamma_C commuting by naturality. The unit (1_X)^! = id, which the source does not specify, is the one determined by the compositor of 1_X, and (b), (c) follow from (d). Nothing is assumed”.

[Stacks, Tag 0ATY]: in Situation 0F42 the constructions of [Stacks, Tag 0AA0] and [Stacks, Tag 0ATX] define a pseudofunctor from FTS S into the 2-category of categories: there is a pseudofunctor (FTS S)ᵒᵖ ⥤ᵖ Cat whose value at X is D⁺_QCoh(𝒪_X), whose value at f is the upper shriek functor f^! of [Stacks, Tag 0AA0] (at a compactification of f, which exists by More on Flatness, Theorem 0F41; by [Stacks, Tag 0AA0] the choice does not matter up to canonical isomorphism), and whose compositor at f, g is the canonical isomorphism (g ∘ f)^! ≅ f^! ∘ g^! of [Stacks, Tag 0ATX]. It is Stacks.Duality.upperShriekPseudofunctor; the axioms of a pseudofunctor are the conditions (a)–(d) of Categories, Definition 003N.

theorem exists_upperShriekPseudofunctor :
    ∃ P : LocallyDiscrete (FTS S)ᵒᵖ ⥤ᵖ Cat.{u, u + 1},
      ∃ hobj : ∀ X : (FTS S)ᵒᵖ,
          P.obj ⟨X⟩ = Cat.of (quasiCoherentDerivedCategoryPlusAtModel X.unop.left),
        (∀ {X Y : (FTS S)ᵒᵖ} (f : X ⟶ Y),
          eqToHom (hobj X).symm ≫ P.map ⟨f⟩ ≫ eqToHom (hobj Y) =
            (upperShriekPlusAtModel (cc f.unop)).toCatHom) ∧
        (∀ {X Y Z : (FTS S)ᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
          HEq (Cat.Hom.toNatIso (P.mapComp ⟨f⟩ ⟨g⟩))
            (upperShriekCompIsoAtModelPlus (cc (g.unop ≫ f.unop)) (cc g.unop) (cc f.unop)))

Tag 0B6T, a lemma

Tag 0B6T in the Stacks Project.

Stacks.Duality.upperShriekCompareWithPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPullbackComparison.lean, line 175. The attribute's comment: “the map mu_{f,K} of Lemma 48.16.5, at the compactification j from which Stacks.Duality.upperShriek computes f^!”.

Stacks Project, Tag 0B6T (Lemma 48.16.5). Let f : X ⟶ Y be a morphism of AlgebraicGeometry.FTS S and let j be a compactification of X over Y, with ambient scheme X̄, open immersion j.immersion and proper structure morphism f̄ = j.toBase. The map

μ_{f,K} : Lf^*K ⊗ᴸ_{𝒪_X} f^!𝒪_Y ⟶ f^!K

is the restriction to X of the comparison map Lf̄^*K ⊗ᴸ_{𝒪_X̄} ā(𝒪_Y) ⟶ ā(K) of Equation 48.8.0.1 ([Stacks, Tag 0A9S]), the source being read through the composition formula Lf^* ≅ Lf̄^* ⋙ Lj^* and the monoidality of Lj^* of [Stacks, Tag 079U].

public def upperShriekCompareWithPullback (K : quasiCoherentDerivedCategory Y.left) :
    ((quasiCoherentDerivedTensor X.left).obj
        ((quasiCoherentDerivedPullback' f.left).obj K)).obj
        ((upperShriek f j).obj (derivedStructureSheaf Y.left)) ⟶
      (upperShriek f j).obj K

Stacks.Duality.upperShriekCompareWithPullback_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPullbackComparison.lean, line 206. The attribute's comment: “functoriality of mu_{f,K} in K”.

The map μ_{f,K} of [Stacks, Tag 0B6T] is functorial in K. Each of its three factors is natural: the composition formula for derived pullback, the monoidality of Lj^*, and Equation 48.8.0.1 by Stacks.Duality.compareWithPullback_naturality.

public theorem upperShriekCompareWithPullback_naturality
    {K K' : quasiCoherentDerivedCategory Y.left} (h : K ⟶ K') :
    ((quasiCoherentDerivedTensor X.left).map
          ((quasiCoherentDerivedPullback' f.left).map h)).app
          ((upperShriek f j).obj (derivedStructureSheaf Y.left)) ≫
        upperShriekCompareWithPullback f j αBar αImm ρ K' =
      upperShriekCompareWithPullback f j αBar αImm ρ K ≫
        (upperShriek f j).map h

Stacks.Duality.upperShriekCompareWithPullback_comp_upperShriekPlusIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPullbackComparisonCanonical.lean, line 670. The attribute's comment: “independence of the compactification”.

[Stacks, Tag 0B6T]: μ_{f,K} does not depend on the compactification. For two compactifications j₁, j₂ of X over Y and K ∈ D⁺_QCoh(𝒪_Y), μ_{f,K} for j₁, followed by the isomorphism f^!_{j₁} ≅ f^!_{j₂} of [Stacks, Tag 0AA0] at K, is Lf^*K tensored with that isomorphism at 𝒪_Y, followed by μ_{f,K} for j₂.

theorem upperShriekCompareWithPullback_comp_upperShriekPlusIso
    (j₁ j₂ : CompactificationOf (Over.mk f.left))
    (K : quasiCoherentDerivedCategoryPlusOfModel Y.left) :
    upperShriekCompareWithPullbackCanonical f j₁ K.obj ≫
        ((upperShriekPlusIso f j₁ j₂).hom.app K).hom =
      ((quasiCoherentDerivedTensor X.left).obj
        ((quasiCoherentDerivedPullback' f.left).obj K.obj)).map
          ((upperShriekPlusIso f j₁ j₂).hom.app (derivedStructureSheafPlus Y.left)).hom ≫
        upperShriekCompareWithPullbackCanonical f j₂ K.obj

Stacks.Duality.upperShriekCompareWithPullbackCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPullbackComparisonCanonicalMaps.lean, line 85. The attribute's comment: “the maps μ_{f,K}”.

Stacks Project, Tag 0B6T (Lemma 48.16.5). Let f : X ⟶ Y be a morphism of AlgebraicGeometry.FTS S and let j be a compactification of X over Y, with ambient scheme X̄, open immersion j.immersion and proper structure morphism f̄ = j.toBase. The map

μ_{f,K} : Lf^*K ⊗ᴸ_{𝒪_X} f^!𝒪_Y ⟶ f^!K

is the restriction to X of the comparison map Lf̄^*K ⊗ᴸ_{𝒪_X̄} ā(𝒪_Y) ⟶ ā(K) of Equation 48.8.0.1 ([Stacks, Tag 0A9S]), the source being read through the composition formula Lf^* ≅ Lf̄^* ⋙ Lj^* and the monoidality of Lj^* of [Stacks, Tag 079U].

public def upperShriekCompareWithPullbackCanonical (K : quasiCoherentDerivedCategory Y.left) :
    ((quasiCoherentDerivedTensor X.left).obj
        ((quasiCoherentDerivedPullback' f.left).obj K)).obj
        ((upperShriek f j).obj (derivedStructureSheaf Y.left)) ⟶
      (upperShriek f j).obj K

Stacks.Duality.upperShriekCompareWithPullbackCanonical_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPullbackComparisonCanonicalMaps.lean, line 108. The attribute's comment: “functoriality of μ_{f,K} in K”.

The map μ_{f,K} of [Stacks, Tag 0B6T] is functorial in K. Each of its three factors is natural: the composition formula for derived pullback, the monoidality of Lj^*, and Equation 48.8.0.1 by Stacks.Duality.compareWithPullback_naturality.

public theorem upperShriekCompareWithPullbackCanonical_naturality
    {K K' : quasiCoherentDerivedCategory Y.left} (h : K ⟶ K') :
    ((quasiCoherentDerivedTensor X.left).map
          ((quasiCoherentDerivedPullback' f.left).map h)).app
          ((upperShriek f j).obj (derivedStructureSheaf Y.left)) ≫
        upperShriekCompareWithPullbackCanonical f j K' =
      upperShriekCompareWithPullbackCanonical f j K ≫
        (upperShriek f j).map h

Stacks.Duality.upperShriekCompareWithPullback_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPullbackComparisonComp.lean, line 549. The attribute's comment: “compatibility with composition”.

Stacks Project, Tag 0B6T (Lemma 48.16.5), compatibility with composition. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of AlgebraicGeometry.FTS S with S Noetherian, and let cf, cg, cfg be compactifications of f, g and g ∘ f, computing f^!, g^! and (g ∘ f)^!. For K ∈ D⁺_QCoh(𝒪_Z), the map μ_f at Lg^*K ⊗ g^!𝒪_Z followed by f^!μ_{g,K} equals: the identification Lf^*(Lg^*K ⊗ g^!𝒪_Z) ⊗ f^!𝒪_Y = Lf^*Lg^*K ⊗ (Lf^*g^!𝒪_Z ⊗ f^!𝒪_Y) (the tensor structure of Lf^* and the associator), Lf^*Lg^*K ⊗ μ_f at g^!𝒪_Z, the identifications Lf^*Lg^*K = L(g ∘ f)^*K and f^!g^!𝒪_Z = (g ∘ f)^!𝒪_Z of [Stacks, Tag 0ATX] (Stacks.Duality.upperShriekCompIso), μ_{g ∘ f} at K, and (g ∘ f)^!K = f^!g^!K. The tensor products are Stacks.Duality.quasiCoherentDerivedTensor, read through Stacks.Duality.quasiCoherentDerivedTensorIsoCurriedTensor where the monoidal structure of D_QCoh is used.

theorem upperShriekCompareWithPullback_comp (cf : CompactificationOf (Over.mk f.left))
    (cg : CompactificationOf (Over.mk g.left)) (cfg : CompactificationOf (Over.mk (f ≫ g).left))
    (K : quasiCoherentDerivedCategoryPlusOfModel Z.left) :
    upperShriekCompareWithPullbackCanonical f cf
        (((quasiCoherentDerivedTensor Y.left).obj
          ((quasiCoherentDerivedPullback' g.left).obj K.obj)).obj
          ((upperShriek g cg).obj (DerivedPushforward.derivedStructureSheaf Z.left))) ≫
        (upperShriek f cf).map (upperShriekCompareWithPullbackCanonical g cg K.obj) =
      ((quasiCoherentDerivedTensorIsoCurriedTensor X.left).hom.app
          ((quasiCoherentDerivedPullback' f.left).obj
            (((quasiCoherentDerivedTensor Y.left).obj
              ((quasiCoherentDerivedPullback' g.left).obj K.obj)).obj
              ((upperShriek g cg).obj (DerivedPushforward.derivedStructureSheaf Z.left))))).app
          ((upperShriek f cf).obj (DerivedPushforward.derivedStructureSheaf Y.left)) ≫
        (quasiCoherentDerivedPullback' f.left).map
          (((quasiCoherentDerivedTensorIsoCurriedTensor Y.left).hom.app
            ((quasiCoherentDerivedPullback' g.left).obj K.obj)).app
            ((upperShriek g cg).obj (DerivedPushforward.derivedStructureSheaf Z.left))) ▷ _ ≫
        Functor.OplaxMonoidal.δ (quasiCoherentDerivedPullback' f.left)
          ((quasiCoherentDerivedPullback' g.left).obj K.obj)
          ((upperShriek g cg).obj (DerivedPushforward.derivedStructureSheaf Z.left)) ▷ _ ≫
        (α_ _ _ _).hom ≫
        (quasiCoherentDerivedPullback' f.left).obj
            ((quasiCoherentDerivedPullback' g.left).obj K.obj) ◁
          (((quasiCoherentDerivedTensorIsoCurriedTensor X.left).inv.app
            ((quasiCoherentDerivedPullback' f.left).obj
              ((upperShriek g cg).obj (DerivedPushforward.derivedStructureSheaf Z.left)))).app
            ((upperShriek f cf).obj (DerivedPushforward.derivedStructureSheaf Y.left)) ≫
          upperShriekCompareWithPullbackCanonical f cf
            ((upperShriek g cg).obj (DerivedPushforward.derivedStructureSheaf Z.left))) ≫
        ((quasiCoherentDerivedPullbackCompIso f.left g.left).hom.app K.obj ⊗ₘ
          ((upperShriekCompIso f g cf cg cfg).inv.app (derivedStructureSheafPlus Z.left)).hom) ≫
        ((quasiCoherentDerivedTensorIsoCurriedTensor X.left).inv.app
            ((quasiCoherentDerivedPullback' (f ≫ g).left).obj K.obj)).app
          ((upperShriek (f ≫ g) cfg).obj (DerivedPushforward.derivedStructureSheaf Z.left)) ≫
        upperShriekCompareWithPullbackCanonical (f ≫ g) cfg K.obj ≫
        ((upperShriekCompIso f g cf cg cfg).hom.app K).hom

Sources

LeanStacks.Duality.upperShriek · AlgebraicGeometry.isSeparatedFiniteType · AlgebraicGeometry.FTS · Stacks.Duality.compactificationUpperShriekIso · Stacks.Duality.exists_coherent_compactificationUpperShriekIso · Stacks.Duality.upperShriekCompIsoAtModel · Stacks.Duality.exists_canonical_upperShriekCompIso · Stacks.Duality.exists_upperShriekPseudofunctor

Section48.17 Properties of upper shriek functors #

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

Tag 0AU0, a lemma

Tag 0AU0 in the Stacks Project.

Stacks.Duality.upperShriekIsoRestrictOfOpenImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekAffineComparison/OpenImmersionRestriction.lean, line 87. The attribute's comment: “j^! = j^ with j^ the restriction to the open X, j^! computed at the compactification X-bar = Y that the source's proof chooses; over a quasi-compact quasi-separated base and on the unbounded D_QCoh”.

Stacks Project, Tag 0AU0 (Lemma 48.17.1). Let j : X ⟶ Y be a morphism of AlgebraicGeometry.FTS S whose underlying morphism of schemes is an open immersion. Then the exceptional inverse image of j is restriction to X:

j^! ≅ j^* : D_QCoh(𝒪_Y) ⥤ D_QCoh(𝒪_X).

Here j^! is computed at the compactification X̄ = Y of Stacks.Duality.openCompactification, the one the source's proof chooses. The isomorphism is the source's: the right adjoint of R(𝟙_Y)_* is the identity (Stacks.Duality.upperShriekIsoDerivedPullbackOfOpenImmersion), and Lj^* is restriction along an open immersion (Stacks.Duality.restrictedDerivedRestrictIsoQuasiCoherentDerivedPullback).

def upperShriekIsoRestrictOfOpenImmersion :
    upperShriek j (openCompactification j) ≅ OpenImmersion.restrictedDerivedRestrict j.left

Tag 0G4J, a lemma

Tag 0G4J in the Stacks Project.

Stacks.Duality.upperShriekRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/OpenImmersionSquare.lean, line 54.

Stacks Project, Tag 0G4J (Lemma 48.17.2). In Situation 48.16.1 let j : U ⟶ X, j' : V ⟶ Y be open immersions and f : X ⟶ Y, g : U ⟶ V morphisms of FTS S with j ≫ f = g ≫ j'. Then j^* ∘ f^! ≅ g^! ∘ (j')^* as functors on D⁺_QCoh(𝒪_Y), for arbitrary compactifications cf of f and cg of g computing f^! and g^!; here j^*, (j')^* are the restrictions to the opens.

This is also the first assertion of [Stacks, Tag 0BV2] (Remark 48.17.5): for open U ⊆ X, V ⊆ Y with f(U) ⊆ V and g the restriction of f, (f^!E)|_U = g^!(E|_V) for E ∈ D⁺_QCoh(𝒪_Y), stated here for arbitrary open immersions and compactifications.

def upperShriekRestrictIso :
    (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙ upperShriek f cf ⋙
        OpenImmersion.restrictedDerivedRestrict j.left ≅
      (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙
        OpenImmersion.restrictedDerivedRestrict j'.left ⋙ upperShriek g cg

Tag 0AA1, a lemma

Tag 0AA1 in the Stacks Project.

Stacks.Duality.nonempty_upperShriekPlus_affineLineProj_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekAffineLine.lean, line 295.

Stacks Project, Tag 0AA1 (Lemma 48.17.3). In Situation 48.16.1 let Y be an object of FTS S and let f : X = 𝔸¹_Y ⟶ Y be the projection. Then there is a (noncanonical) isomorphism f^!(-) ≅ Lf^*(-)[1] of functors on D⁺_QCoh(𝒪_Y), with f^! computed at any compactification j of f.

The proof is through the isomorphisms μ_{f,K} : Lf^*K ⊗ᴸ f^!𝒪_Y ≅ f^!K of [Stacks, Tag 0B6U] (e), f being smooth, together with f^!𝒪_Y ≅ 𝒪_X[1]: the source's 𝒪_{ℙ¹_Y}(-2)|_X ≅ 𝒪_X is replaced by the fundamental class of [Stacks, Tag 0E9Z] for X ⊆ ℙ¹_Y ⟶ Y and the triviality of Ω_{X/Y}.

theorem nonempty_upperShriekPlus_affineLineProj_iso :
    Nonempty (upperShriekPlus (affineLineProj Y) j ⋙ ObjectProperty.ι _ ≅
      ObjectProperty.ι _ ⋙ quasiCoherentDerivedPullback' (affineLineProj Y).left ⋙
        shiftFunctor (quasiCoherentDerivedCategory (affineLineFTS Y).left) (1 : ℤ))

Tag 0AA2, a lemma

Tag 0AA2 in the Stacks Project.

Stacks.Duality.LocallySmall.upperShriek_closedImmersion_of_fts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ClosedImmersionTwistedInverseImageQcqs.lean, line 160. The attribute's comment: “at the locally small derived categories, the model at which the coherator and the right adjoint of Ri_* are built; i^! is constructed here”.

Stacks Project, Tag 0AA2 (Lemma 48.17.4). In Situation 48.16.1 — S a Noetherian scheme and FTS S the schemes separated and of finite type over S — let i : X ⟶ Y be a morphism of FTS S whose underlying morphism of schemes is a closed immersion. Then i^!(-) = R𝓗om(𝒪_X, -):

Ri_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) has a right adjoint;

the upper shriek i^! = j^* ∘ a of [Stacks, Tag 0A9Y] at the compactification X̄ = X that a proper morphism is (Stacks.Duality.properCompactification), with its right adjoint a produced by (1) and its quasi-coherence inputs discharged, agrees with R𝓗om(𝒪_X, -) on D⁺_QCoh(𝒪_Y);

for every right adjoint a of Ri_* the canonical comparison a(K) ⟶ R𝓗om(𝒪_X, K) — the mate of the counit of a under [Stacks, Tag 0A76] — is an isomorphism for every K in D⁺_QCoh(𝒪_Y).

The existence (1) is Stacks.Duality.LocallySmall.isLeftAdjoint_affineHomQuasiCoherentDerivedPushforward, which builds the right adjoint as DQ_X ∘ R𝓗om(𝒪_X, -) from the coherator of [Stacks, Tag 0CR0]; X is quasi-compact and quasi-separated, being of finite type over a Noetherian scheme. The identification (2), (3) is [Stacks, Tag 0A9X] at this model (Stacks.Duality.LocallySmall.isIso_rightAdjointToDerivedSheafHom_app), whose hypotheses — pseudo-coherence of i — hold in Situation 48.16.1.

theorem upperShriek_closedImmersion_of_fts {S : Scheme.{u}} [IsNoetherian S] {X Y : FTS S}
    (i : X ⟶ Y) [IsClosedImmersion i.left] :
    (affineHomQuasiCoherentDerivedPushforward i.left).IsLeftAdjoint ∧
      IsDerivedSheafHomRightAdjoint i.left
        (upperShriek i (properCompactification i)) ∧
      ∀ (a : quasiCoherentDerivedCategory Y.left ⥤ quasiCoherentDerivedCategory X.left)
        (adj : affineHomQuasiCoherentDerivedPushforward i.left ⊣ a)
        (K : (isBoundedBelowQuasiCoherent Y.left).FullSubcategory),
        IsIso ((rightAdjointToDerivedSheafHom i.left
          (isQuasicoherent_homology_derivedPushforward_of_isAffineHom i.left) a adj).app
            K.obj)

Tag 0BV2, a remark

Tag 0BV2 in the Stacks Project.

Stacks.Duality.upperShriekRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/OpenImmersionSquare.lean, line 54. The attribute's comment: “part (a): (f^!E)|_U ≅ g^!(E|_V) for E in D^+_QCoh, every open square and every pair of compactifications”.

Stacks Project, Tag 0G4J (Lemma 48.17.2). In Situation 48.16.1 let j : U ⟶ X, j' : V ⟶ Y be open immersions and f : X ⟶ Y, g : U ⟶ V morphisms of FTS S with j ≫ f = g ≫ j'. Then j^* ∘ f^! ≅ g^! ∘ (j')^* as functors on D⁺_QCoh(𝒪_Y), for arbitrary compactifications cf of f and cg of g computing f^! and g^!; here j^*, (j')^* are the restrictions to the opens.

This is also the first assertion of [Stacks, Tag 0BV2] (Remark 48.17.5): for open U ⊆ X, V ⊆ Y with f(U) ⊆ V and g the restriction of f, (f^!E)|_U = g^!(E|_V) for E ∈ D⁺_QCoh(𝒪_Y), stated here for arbitrary open immersions and compactifications.

def upperShriekRestrictIso :
    (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙ upperShriek f cf ⋙
        OpenImmersion.restrictedDerivedRestrict j.left ≅
      (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙
        OpenImmersion.restrictedDerivedRestrict j'.left ⋙ upperShriek g cg

Stacks.Duality.restrictedUpperShriekIsoOfOpenSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekAffineComparison/OpenSquare.lean, line 171. The attribute's comment: “clause (a) only, the restriction formula (f^!E)|_U = g^!(E|_V) for an open square; clause (b), the affine formula phi^!(K) = RHom(A, K ⊗^L_R P)[n], is NOT claimed, because Stacks 0AA1 (f^! = Lf^*[1] for A^1_V -> V) is absent from this repository. Carried: h0ATXf and h0ATXi, the two instances of Stacks 0ATX for the two factorisations of the diagonal of the square. Stacks 0AU0 is NOT carried: it is proved by Stacks.Duality.upperShriekIsoDerivedPullbackOfOpenImmersion, and supplying it is the only content this statement adds to its hypotheses. Stated for open immersions rather than affine opens, and on the unbounded D_QCoh rather than D^+_QCoh”.

Stacks Project, Tag 0BV2 (Remark 48.17.5), clause (a). Let f : X ⟶ Y and g : U ⟶ V be morphisms of AlgebraicGeometry.FTS S and let j : U ⟶ X, i : V ⟶ Y be morphisms of FTS S whose underlying morphisms of schemes are open immersions, with j ≫ f = g ≫ i. Then restricting an exceptional inverse image to U computes the exceptional inverse image of the restriction to V:

f^! ⋙ Lj^* ≅ Li^* ⋙ g^!,

that is (f^!E)|_U ≅ g^!(E|_V) naturally in E ∈ D_QCoh(𝒪_Y).

The source's proof is reproduced. The two hypotheses h0ATXf and h0ATXi are the two instances of [Stacks, Tag 0ATX] that it cites, for the two factorisations j ≫ f and g ≫ i of the diagonal d : U ⟶ Y of the square. The passage from j^! and i^! to the restrictions Lj^* and Li^* is [Stacks, Tag 0AU0], which is not assumed here but proved in Stacks.Duality.upperShriekIsoDerivedPullbackOfOpenImmersion; it is the whole of the content this statement adds to its hypotheses.

Clause (b) of Tag 0BV2, the affine formula φ^!(K) = RHom(A, K ⊗^L_R P)[n], is not claimed: it needs [Stacks, Tag 0AA1], which this repository does not have.

def restrictedUpperShriekIsoOfOpenSquare (_hdj : j ≫ f = d) (_hdi : g ≫ i = d) :
    upperShriek f cf ⋙ quasiCoherentDerivedPullback' j.left ≅
      quasiCoherentDerivedPullback' i.left ⋙ upperShriek g cg

Stacks.Duality.upperShriekCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekStructureSheafCharts.lean, line 679. The attribute's comment: “part (b): (f^!E)|_U corresponds to phi^!(K) = RHom(A, K (x)^L_R P)[n] for every pair of affine opens U, V with f(U) in V, every presentation A = P/I and every K in D(R) with E|_V = K~, E in D^+_QCoh, every compactification”.

Stacks Project, Tag 0BV2 (Remark 48.17.5), second assertion. In Situation 48.16.1 let f : X ⟶ Y be a morphism of FTS S, j any compactification computing f^!, and E ∈ D⁺_QCoh(𝒪_Y). For affine opens U = Spec A ⊆ f⁻¹(V), V = Spec R, every presentation A = P/I with P = R[x_1, …, x_n] and every K ∈ D(R) with E|_V ≅ K~, the restriction (f^!E)|_U is the sheaf associated to φ^!(K) = RHom_P(A, K ⊗ᴸ_R P)[n].

theorem upperShriekCharts
    {S : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S]
    {X Y : FTS S} (f : X ⟶ Y) (j : CompactificationOf (Over.mk f.left))
    (E : quasiCoherentDerivedCategory Y.left) (hE : DerivedCategoryB.IsBoundedBelow E.obj) :
    UpperShriekCharts f j E

Tag 0AU1, a lemma

Tag 0AU1 in the Stacks Project.

Stacks.Duality.derivedCategoryBPlus_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekCoherent.lean, line 210.

Stacks Project, Tag 0AU1 (Lemma 48.17.6). In Situation 48.16.1 let f : X ⟶ Y be a morphism of FTS S. Then f^! maps D⁺_Coh(𝒪_Y) into D⁺_Coh(𝒪_X). Here f^! is computed at an arbitrary compactification j.

theorem derivedCategoryBPlus_upperShriek
    {S : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S] {X Y : FTS S} (f : X ⟶ Y)
    (j : CompactificationOf (Over.mk f.left)) (E : quasiCoherentDerivedCategory Y.left)
    (hE : DerivedCategoryB.derivedCategoryBPlus
      (fun M : Y.left.Modules ↦ _root_.SheafOfModules.IsCoherent M) E.obj) :
    DerivedCategoryB.derivedCategoryBPlus
      (fun M : X.left.Modules ↦ _root_.SheafOfModules.IsCoherent M)
      ((upperShriek f j).obj E).obj

Tag 0AA3, a lemma

Tag 0AA3 in the Stacks Project.

Stacks.Divisors.isDualizingModule_homologyOne_derivedSheafHomExactSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/EffectiveCartierDualizingModule.lean, line 118. The attribute's comment: “for the inclusion i : D to X of an effective Cartier divisor into a locally Noetherian scheme, read on a module: if omega placed in some degree is a dualizing complex on X then H^1(a(omega)) — which clause (7) of Tag 0AU3 identifies with the degree-one cohomology of i^!omega, namely the normal sheaf twist N tensor i^*omega of the restriction — is a dualizing module on D. Nothing is carried; see the Tag 0AU3 clause string above for the three inputs, all of them proved in the library. The general finite-type case is Stacks.Duality.isDualizingComplex_upperShriek_of_fts”.

[Stacks, Tag 0AA3] for the inclusion of an effective Cartier divisor, read on a module. Let D ⊆ X be an effective Cartier divisor on a locally Noetherian scheme, with closed immersion i : D ⟶ X, and let a(-) be the right adjoint of derived pushforward along i of [Stacks, Tag 0A76]. If a quasi-coherent 𝒪_X-module ω placed in some degree is a dualizing complex on X, then the 𝒪_D-module H¹(a(ω)) is a dualizing module on D.

Degree one is the degree [Stacks, Remark 0B4R] selects, and Stacks.Divisors.nonempty_homologyOne_derivedSheafHomExactSupport_iso identifies H¹(a(ω)) with the normal sheaf twist 𝒩 ⊗ i^*ω of the restriction.

theorem isDualizingModule_homologyOne_derivedSheafHomExactSupport (ω : X.Modules)
    [ω.IsQuasicoherent] (n : ℤ) (hω : Stacks.Duality.IsDualizingComplex
      ((DerivedCategory.singleFunctor X.Modules n).obj ω)) :
    letI : IsLocallyNoetherian D.subscheme := D.isLocallyNoetherian_subscheme
    Stacks.Duality.IsDualizingModule
      ((DerivedCategory.homologyFunctor D.subscheme.Modules 1).obj
        ((closedQuotient D).derivedSheafHomExactSupport.obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj ω)))

Stacks.Duality.isDualizingComplex_upperShriek_of_fts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekDualizingComplex.lean, line 148. The attribute's comment: “granted the conclusion of Tag 0A86 (dualizing may be checked on one affine cover) and the affine-chart description of f^! of Tag 0AA1 together with Tag 0BV2, carried as the explicit hypotheses h0A86 and h0AA1; f^! itself is an explicit parameter fShriek characterised by h0AA1, not a constructed or chosen functor. What is proved is the rest of the source argument: the affine charts of X lying over affine opens of Y cover X, the dualizing model of K over each such V comes from hK, Tag 0BZL upgrades its algebraic upper shriek to a dualizing complex over the chart ring of X, and h0A86 glues the local models. Neither carried hypothesis asserts that anything is dualizing”.

Stacks Project, Tag 0AA3 (Lemma 48.17.7). In Situation 48.16.1, let f : X ⟶ Y be a morphism of FTS S and let f^! be an exceptional inverse image functor D⁺_QCoh(𝒪_Y) ⥤ D⁺_QCoh(𝒪_X) for it, in the sense that on affine charts it is the algebraic upper shriek of a polynomial presentation of the chart ring map. If K is a dualizing complex for Y, then f^!K is a dualizing complex for X.

theorem isDualizingComplex_upperShriek_of_fts {S : Scheme.{u}} [IsNoetherian S] {X Y : FTS S}
    (f : X ⟶ Y)
    (fShriek : quasiCoherentDerivedCategoryPlus Y.left ⥤ quasiCoherentDerivedCategoryPlus X.left)
    (K : quasiCoherentDerivedCategoryPlus Y.left)
    (h0A86 : ∀ L : DerivedCategory X.left.Modules,
      (∀ x : X.left, ∃ (U : X.left.Opens) (hU : IsAffineOpen U),
        x ∈ U ∧ HasDualizingModelOn L U hU) → IsDualizingComplex L)
    (h0AA1 : ∀ (U : X.left.Opens) (hU : IsAffineOpen U) (V : Y.left.Opens)
      (hV : IsAffineOpen V) (hUV : U ≤ f.left ⁻¹ᵁ V)
      (ω : DerivedCategory (ModuleCat.{u} Γ(Y.left, V))),
      IsTildeModelOn K.obj.obj V hV ω →
      ∃ p : Dualizing.PolynomialPresentation (f.left.appLE V U hUV).hom,
        IsTildeModelOn (fShriek.obj K).obj.obj U hU (p.upperShriekFunctor.{u, u}.obj ω))
    (hK : IsDualizingComplex K.obj.obj) :
    IsDualizingComplex (fShriek.obj K).obj.obj

Declarations registered for the tag:

Stacks.Duality.isDualizingComplex_upperShriek_obj, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekDualizingComplexOfChartsRegistration.lean, line 15 (StacksFrontier).

Tag 0AU2, a lemma

Tag 0AU2 in the Stacks Project.

Stacks.Duality.UpperShriekDuality.upperShriekDualityIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekDuality.lean, line 272.

Stacks Project, Tag 0AU2. In Situation [Stacks, Tag 0F42] — S Noetherian — let f : X ⟶ Y be a morphism of schemes separated and of finite type over S, let j be a compactification of X over Y, and let K be a dualizing complex on Y. Set D_Y(M) = R𝓗om(M, K) and D_X(E) = R𝓗om(E, f^!K). Then there is a canonical isomorphism

f^!M ≅ D_X(Lf^* D_Y(M)),

natural in M ∈ D^+_Coh(𝒪_Y).

def upperShriekDualityIso :
    upperShriekStd f j ≅
      (plusCoh Y.left).ι ⋙ ((sheafHom Y.left).flip.obj K).rightOp ⋙ (pull f.left).op ⋙
        (sheafHom X.left).flip.obj (upperShriekDualizing f j hK)

Tag 0B6U, a lemma

Tag 0B6U in the Stacks Project.

Stacks.Duality.derivedCategoryBBounded_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekCoherent.lean, line 237. The attribute's comment: “part (d)”.

Stacks Project, Tag 0B6U (Lemma 48.17.9), part (d). In Situation 48.16.1 let f : X ⟶ Y be a perfect morphism of FTS S. Then f^! maps D^b_Coh(𝒪_Y) into D^b_Coh(𝒪_X). Here f^! is computed at an arbitrary compactification j.

theorem derivedCategoryBBounded_upperShriek {S : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S]
    {X Y : FTS S} (f : X ⟶ Y) (j : CompactificationOf (Over.mk f.left)) [Perfect f.left]
    (E : quasiCoherentDerivedCategory Y.left)
    (hE : DerivedCategoryB.derivedCategoryBBounded
      (fun M : Y.left.Modules ↦ _root_.SheafOfModules.IsCoherent M) E.obj) :
    DerivedCategoryB.derivedCategoryBBounded
      (fun M : X.left.Modules ↦ _root_.SheafOfModules.IsCoherent M)
      ((upperShriek f j).obj E).obj

Stacks.Duality.derivedCategoryBBounded_upperShriek_derivedStructureSheaf_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPerfect.lean, line 63. The attribute's comment: “part (a)”.

Stacks Project, Tag 0B6U (Lemma 48.17.9), part (a). In Situation 48.16.1 let f : X ⟶ Y be a perfect morphism of FTS S. Then f^!𝒪_Y lies in D^b_Coh(𝒪_X): it is cohomologically bounded and its cohomology sheaves are coherent. Here f^! is computed at an arbitrary compactification j.

theorem derivedCategoryBBounded_upperShriek_derivedStructureSheaf_of_perfect [Perfect f.left] :
    DerivedCategoryB.derivedCategoryBBounded
      (fun M : X.left.Modules ↦ _root_.SheafOfModules.IsCoherent M)
      (((upperShriek f j).obj (derivedStructureSheaf Y.left)).obj)

Stacks.Duality.hasFiniteTorDimension_derivedScalarRestriction_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPerfect.lean, line 81. The attribute's comment: “part (b)”.

Stacks Project, Tag 0B6U (Lemma 48.17.9), part (b). In Situation 48.16.1 let f : X ⟶ Y be a perfect morphism of FTS S. Then f^!𝒪_Y has finite tor dimension in D(f⁻¹𝒪_Y): read on the ringed space (X, f⁻¹𝒪_Y), it has Tor amplitude in some interval. Here f^! is computed at an arbitrary compactification j.

theorem hasFiniteTorDimension_derivedScalarRestriction_upperShriek [Perfect f.left] :
    Stacks.Cohomology.TorAmplitude.HasFiniteTorDimension
      (RingedSpace.inverseImage Y.left.toRingedSpace f.left.base)
      ((Scheme.Hom.derivedScalarRestriction f.left).obj (relativeDualizingComplexObj f j))

Stacks.Duality.isIso_derivedSheafHomothety_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPerfect.lean, line 109. The attribute's comment: “part (c)”.

Stacks Project, Tag 0B6U (Lemma 48.17.9), part (c). In Situation 48.16.1 let f : X ⟶ Y be a perfect morphism of FTS S. Then the homothety 𝒪_X ⟶ R𝓗om_{𝒪_X}(f^!𝒪_Y, f^!𝒪_Y) is an isomorphism. Here f^! is computed at an arbitrary compactification j.

theorem isIso_derivedSheafHomothety_upperShriek [Perfect f.left] :
    IsIso (Stacks.SheafOfModules.derivedSheafHomothety X.left.sheaf
      (relativeDualizingComplexObj f j))

Stacks.Duality.isIso_upperShriekCompareWithPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekPerfectComparison.lean, line 46. The attribute's comment: “part (e)”.

Let S be a Noetherian scheme and f : X ⟶ Y a perfect morphism of FTS S. Then the map μ_{f,K} : Lf^*K ⊗ᴸ_{𝒪_X} f^!𝒪_Y ⟶ f^!K, Stacks.Duality.upperShriekCompareWithPullbackCanonical, is an isomorphism for all K ∈ D⁺_QCoh(𝒪_Y). Here f^! and μ_{f,K} are computed at an arbitrary compactification j.

theorem isIso_upperShriekCompareWithPullback [Perfect f.left]
    (j : CompactificationOf (Over.mk f.left)) (K : quasiCoherentDerivedCategory Y.left)
    (hK : DerivedCategoryB.IsBoundedBelow K.obj) :
    IsIso (upperShriekCompareWithPullbackCanonical f j K)

Tag 0E9T, a lemma

Tag 0E9T in the Stacks Project.

Stacks.Duality.upperShriek_structureSheaf_isPerfectRelativeTo_and_isIso_homothety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFlatDualizing.lean, line 122.

Stacks Project, Tag 0E9T (Lemma 48.17.10). In Situation 48.16.1 (S Noetherian), let f : X ⟶ Y be a flat morphism of FTS S, with f^! computed at any compactification j. Then f^!𝒪_Y is a Y-perfect object of D(𝒪_X) and 𝒪_X ⟶ R𝓗om_{𝒪_X}(f^!𝒪_Y, f^!𝒪_Y) is an isomorphism.

theorem upperShriek_structureSheaf_isPerfectRelativeTo_and_isIso_homothety :
    (letI := locallyOfFinitePresentation_left f;
      Scheme.Hom.IsPerfectRelativeTo.{u + 1, u + 1} f.left
        (RingedSpace.canonicalCertifiedDerivedSheafTensoringFamily _)
        (relativeDualizingComplexObj f j)) ∧
      IsIso (Stacks.SheafOfModules.derivedSheafHomothety X.left.sheaf
        (relativeDualizingComplexObj f j))

Stacks.Duality.isPseudoCoherent_of_isShriekOfStructureSheafOnCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekRelativePerfection.lean, line 193. The attribute's comment: “the pseudo-coherence half of the first assertion: f^! O_Y is a pseudo-coherent object of D(O_X), which is the first of the two conjuncts of Y-perfectness (Tag 0DI0). NOT claimed: the Tor-dimension conjunct of the first assertion, and the whole of the second assertion that O_X -> R SheafHom(f^! O_Y, f^! O_Y) is an isomorphism. Both rest on Stacks 0BZW, whose parts (1)(a), (1)(b) and (1)(c) are all proved in this repository at the level of rings -- (1)(b) as Dualizing.PolynomialPresentation.relativeDualizingComplex_hasFiniteTorDimension_of_isPerfectRingMap and (1)(c) as Dualizing.upperShriekFunctor_unit_isIso_derivedHomothety_of_isPerfectModule -- but what is absent is the affine-locality assembly for Tor dimension that Stacks 0DI2 would need, and there is no map O_X -> R SheafHom(K, K) on a scheme in this repository at all, so the sheaf-level second assertion cannot even be stated. Neither is carried as a hypothesis, since either would be the assertion itself. One hypothesis IS carried, hw: the affine-chart description of f^! O_Y, which is Stacks 0AA1 together with clause (b) of Stacks 0BV2; it asserts only an isomorphism, and it is the same hypothesis carried by Tag 0B6U part (a) and Tag 0AA3. Everything asserted about pseudo-coherence is proved, from Tag 0BZK (2) chart by chart -- whose perfect-ring-map hypothesis is discharged, not carried, from Flat and LocallyOfFinitePresentation through Tag 068A -- and Tag 08E8. f^! O_Y enters as an object of D+_QCoh(O_X) at CategoryTheory.HasDerivedCategory.standard characterised by hw, the idiom of Tag 0AA3, rather than as a value of Stacks.Duality.upperShriek, which is defined at the locally small model that Tag 08E8 is not available at”.

Stacks Project, Tag 0E9T, the pseudo-coherence half of the first assertion. In Situation 48.16.1, let f : X ⟶ Y be a flat morphism of finite presentation of FTS S. Then the relative dualizing complex ω^•_{X/Y} = f^!𝒪_Y is a pseudo-coherent object of D(𝒪_X).

Over each chart the model of f^!𝒪_Y lies in D^b_Coh of the chart ring by Tag 0BZK (2); the chart bounds glue, and on a Noetherian scheme a bounded object with coherent cohomology is pseudo-coherent by Tag 08E8.

theorem isPseudoCoherent_of_isShriekOfStructureSheafOnCharts
    [Flat f.left] [LocallyOfFinitePresentation f.left]
    (ω : quasiCoherentDerivedCategory.{u + 1, u} X.left)
    (hw : IsShriekOfStructureSheafOnCharts f ω.obj) :
    RingedSpace.IsPseudoCoherent (X := X.left.toRingedSpace) ω.obj

Tag 0B6V, a lemma

Tag 0B6V in the Stacks Project.

Stacks.Duality.isInvertible_and_isPerfect_upperShriek_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekLocalCompleteIntersection.lean, line 214.

Stacks Project, Tag 0B6V (Lemma 48.17.11). In Situation 48.16.1 let f : X ⟶ Y be a local complete intersection morphism of FTS S. Then 1. f^!𝒪_Y is an invertible object of D(𝒪_X), and 2. f^! maps perfect complexes to perfect complexes.

Here f^! is computed at an arbitrary compactification j.

theorem isInvertible_and_isPerfect_upperShriek_of_isLocalCompleteIntersection
    (hf : IsLocalCompleteIntersectionMorphism f.left) :
    (letI := Scheme.Modules.derivedMonoidal X.left;
      MonoidalCategory.IsInvertible (relativeDualizingComplexObj f j)) ∧
    ∀ K : quasiCoherentDerivedCategory Y.left,
      Stacks.Cohomology.PerfectComplexes.IsPerfect (X := Y.left.toRingedSpace) K.obj →
        Stacks.Cohomology.PerfectComplexes.IsPerfect (X := X.left.toRingedSpace)
          ((upperShriek f j).obj K).obj

Sources

LeanStacks.Duality.upperShriekIsoRestrictOfOpenImmersion · Stacks.Duality.upperShriekRestrictIso · Stacks.Duality.nonempty_upperShriekPlus_affineLineProj_iso · Stacks.Duality.LocallySmall.upperShriek_closedImmersion_of_fts · Stacks.Duality.restrictedUpperShriekIsoOfOpenSquare · Stacks.Duality.upperShriekCharts · Stacks.Duality.derivedCategoryBPlus_upperShriek · Stacks.Divisors.isDualizingModule_homologyOne_derivedSheafHomExactSupport

Section48.18 Base change for upper shriek #

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

Tag 0E9U, a lemma

Tag 0E9U in the Stacks Project.

Stacks.Duality.upperShriekFlatBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFlatBaseChangeIso.lean, line 91.

Flat base change for f^!. Let S be Noetherian and let X' ⟶ X over Y' ⟶ Y be a cartesian square of FTS S with g flat. Then L(g')^* ∘ f^! ≅ (f')^! ∘ Lg^* on D^+_QCoh(𝒪_Y), with f^! computed at any compactification j of f and (f')^! at any compactification c' of f'. It is the base change map L(g')^* j^* ā ≅ (j')^* L(ḡ')^* ā ⟶ (j')^* ā' Lg^* of the base change j' of j, followed by the comparison (f')^!_{j'} ≅ (f')^!_{c'} of [Stacks, Tag 0AA0] at Lg^*K ∈ D^+_QCoh(𝒪_{Y'}).

def upperShriekFlatBaseChangeIso (c' : CompactificationOf (Over.mk f'.left)) :
    (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙
        upperShriek f c ⋙ quasiCoherentDerivedPullback' g'.left ≅
      (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙
        quasiCoherentDerivedPullback' g.left ⋙ upperShriek f' c'

Tag 0FWI, a lemma

Tag 0FWI in the Stacks Project.

Stacks.Duality.upperShriekIsoPullbackOfEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekEtale.lean, line 99.

Stacks Project, Tag 0FWI. In Situation 48.16.1 let f : X ⟶ Y be an étale morphism of FTS S. Then f^! ≅ f^* as functors on D^+_QCoh(𝒪_Y), for f^! computed at any compactification j. The isomorphism at K is Lf^*K ≅ Lf^*K ⊗ᴸ 𝒪_X ≅ Lf^*K ⊗ᴸ f^!𝒪_Y ≅ f^!K, the last map being μ_{f,K} of [Stacks, Tag 0B6U] (e).

def upperShriekIsoPullbackOfEtale [Etale f.left] :
    (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙ upperShriek f j ≅
      (ObjectProperty.ι _ : quasiCoherentDerivedCategoryPlusOfModel Y.left ⥤ _) ⋙
        quasiCoherentDerivedPullback' f.left

Tag 0BZY, a lemma

Tag 0BZY in the Stacks Project.

Stacks.Duality.nonempty_restrict_derivedPullback_upperShriek_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingBaseChange/MakeshiftBaseChange.lean, line 307.

[Stacks, Tag 0BZY] (makeshift base change). In Situation 48.16.1 let X' = X ×_Y Y' be a cartesian square of FTS S with f flat, let E ∈ D⁺_QCoh(𝒪_Y) with Lg^*E bounded below, and let j, j' be compactifications computing f^! and f'^!. For an affine open U' ⊆ X' mapping into affine opens U ⊆ X, V' ⊆ Y', V ⊆ Y of the square (g'(U') ⊆ U, f'(U') ⊆ V', f(U) ⊆ V, g(V') ⊆ V), the restrictions to U' of L(g')^*f^!E and (f')^!Lg^*E are isomorphic.

The reading of "mapping into affine opens". The source asks for U' ⊂ X' "affine open mapping into affine opens of Y, Y', and X", and its proof begins "we immediately reduce to the case where X, Y, Y', and X' are affine", which needs the four affine opens to form a cartesian square of affines; so the opens are a compatible quadruple, f(U) ⊆ V and g(V') ⊆ V. Three independently chosen affine opens containing the images of U' need not form such a square: U ∩ f⁻¹(V) need not be affine (the base S is not assumed separated), so no single affine chart of f need contain g'(U').

The proof is the source's: on the charts both sides are the sheaves associated to the algebraic base change Dualizing.nonempty_totalDerivedExtensionScalars_upperShriekFunctor_iso_of_isOpenImmersion, by the chart description Stacks.Duality.upperShriekCharts of [Stacks, Tag 0BV2].

theorem nonempty_restrict_derivedPullback_upperShriek_iso
    {X X' Y Y' : AlgebraicGeometry.FTS S} (f : X ⟶ Y) (f' : X' ⟶ Y') (g : Y' ⟶ Y) (g' : X' ⟶ X)
    (sq : IsPullback g'.left f'.left f.left g.left) [Flat f.left]
    (j : AlgebraicGeometry.CompactificationOf (Over.mk f.left))
    (j' : AlgebraicGeometry.CompactificationOf (Over.mk f'.left))
    (E : quasiCoherentDerivedCategory Y.left) (hE : DerivedCategoryB.IsBoundedBelow E.obj)
    (hE' : DerivedCategoryB.IsBoundedBelow ((quasiCoherentDerivedPullback' g.left).obj E).obj)
    {U' : X'.left.Opens} (hU' : IsAffineOpen U') {U : X.left.Opens} (hU : IsAffineOpen U)
    {V' : Y'.left.Opens} (hV' : IsAffineOpen V') {V : Y.left.Opens} (hV : IsAffineOpen V)
    (hU'U : U' ≤ g'.left ⁻¹ᵁ U) (hU'V' : U' ≤ f'.left ⁻¹ᵁ V') (hUV : U ≤ f.left ⁻¹ᵁ V)
    (hV'V : V' ≤ g.left ⁻¹ᵁ V) :
    Nonempty ((Scheme.Modules.restrictFunctor U'.ι).mapDerivedCategory.obj
        ((quasiCoherentDerivedPullback' g'.left).obj ((upperShriek f j).obj E)).obj ≅
      (Scheme.Modules.restrictFunctor U'.ι).mapDerivedCategory.obj
        ((upperShriek f' j').obj ((quasiCoherentDerivedPullback' g.left).obj E)).obj)

Tag 0BZZ, a lemma

Tag 0BZZ in the Stacks Project.

Stacks.Duality.isDualizingComplex_derivedPullback_fibreι_upperShriek_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingBaseChange/FibreDualizingCharts.lean, line 440.

Stacks Project, Tag 0BZZ (Lemma 48.18.4). In Situation 48.16.1 let f : X ⟶ Y be a flat morphism of FTS S and set ω^•_{X/Y} = f^!𝒪_Y, for any compactification j defining f^!. For y ∈ Y let h : X_y ⟶ X be the projection from the fibre. Then Lh^*ω^•_{X/Y} is a dualizing complex on X_y.

The fibre charts over the affine charts of f cover X_y; on each, by Stacks.Duality.upperShriekStructureSheafCharts and [Stacks, Tag 08DW], Lh^*ω^•_{X/Y} is the sheaf associated to ω^•_{A/R} ⊗ᴸ_A (A ⊗_R κ(y)), which is dualizing by [Stacks, Tag 0BZW]; [Stacks, Tag 0A86] glues.

theorem isDualizingComplex_derivedPullback_fibreι_upperShriek_unconditional [Flat f.left]
    (y : Y.left) :
    IsDualizingComplex
      ((derivedPullback (f.left.fiberι y)).obj (relativeDualizingComplexObj f j))

Sources

LeanStacks.Duality.upperShriekFlatBaseChangeIso · Stacks.Duality.upperShriekIsoPullbackOfEtale · Stacks.Duality.nonempty_restrict_derivedPullback_upperShriek_iso · Stacks.Duality.isDualizingComplex_derivedPullback_fibreι_upperShriek_unconditional

Section48.19 A duality theory #

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

Tag 0AU3, the section

Tag 0AU3 in the Stacks Project.

Stacks.Duality.isDerivedSheafHomRightAdjoint_of_fts_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ClosedImmersionTwistedInverseImage.lean, line 244. The attribute's comment: “clause (5) of Section 48.19: for a closed immersion f^! is derived sheaf Hom out of the structure sheaf, with the conclusion of Tag 0A9X discharged by Stacks.Duality.tag0A9XHypothesis; i^! is the explicit parameter a with its adjunction, the existence statement being Tag 0A9E”.

Stacks Project, Tag 0AA2 (Lemma 48.17.4), with nothing about Tag 0A9X assumed. In Situation 48.16.1, let i : X ⟶ Y be a morphism of FTS S whose underlying morphism of schemes is a closed immersion, and let a be a right adjoint of Ri_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y). Then a, which is i^!, is derived sheaf Hom out of 𝒪_X: i^!(-) = R𝓗om_{𝒪_Y}(𝒪_X, -) on bounded-below complexes with quasi-coherent cohomology.

This is Stacks.Duality.isDerivedSheafHomRightAdjoint_of_fts with its hypothesis h0A9X discharged by Stacks.Duality.tag0A9XHypothesis, which is the content of [Stacks, Tag 0A9X] (Stacks.Duality.tag0A9X) read at the canonical restriction of Ri_* to the quasi-coherent derived categories. Two of the three things the tag's proof needs are therefore not hypotheses: the conclusion of [Stacks, Tag 0A9X], and the preservation of quasi-coherent cohomology by Ri_* (part (1) of [Stacks, Tag 08D5], a closed immersion being affine).

What remains a parameter is i^! itself, the functor a together with the adjunction adj characterising it, exactly as in Stacks.Duality.isDerivedSheafHomRightAdjoint_of_pseudoCoherent ([Stacks, Tag 0A9X]) and in Stacks.Duality.sheafyTrace. Its existence is [Stacks, Tag 0A9E], which is not proved unconditionally in this tree — Stacks.Duality.DerivedPushforward.isLeftAdjoint_qcqsRestrictedDerivedPushforward carries [Stacks, Tag 08DZ] at the locally small model and [Stacks, Tag 09IS]; a right adjoint being unique up to canonical isomorphism, the statement about an arbitrary one says the same thing as the statement about the one that tag produces.

This declaration is not registered as [Stacks, Tag 0AA2]: the full statement, with i^! produced for every object of FTS S and no affineness or quasi-affineness hypothesis, is Stacks.Duality.LocallySmall.upperShriek_closedImmersion_of_fts in StacksFrontier/AlgebraicGeometry/Duality/ClosedImmersionTwistedInverseImageQcqs.lean.

theorem isDerivedSheafHomRightAdjoint_of_fts_closedImmersion
    {S : Scheme.{u}} [IsNoetherian S] {X Y : FTS S} (i : X ⟶ Y)
    [IsClosedImmersion i.left]
    (a : quasiCoherentDerivedCategory Y.left ⥤ quasiCoherentDerivedCategory X.left)
    (adj : affineHomQuasiCoherentDerivedPushforward i.left ⊣ a) :
    IsDerivedSheafHomRightAdjoint i.left a

Stacks.Duality.LocallySmall.upperShriek_closedImmersion_of_fts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ClosedImmersionTwistedInverseImageQcqs.lean, line 160. The attribute's comment: “clause (5): for a closed immersion f^! = RHom(O_X, -), at the locally small derived categories”.

Stacks Project, Tag 0AA2 (Lemma 48.17.4). In Situation 48.16.1 — S a Noetherian scheme and FTS S the schemes separated and of finite type over S — let i : X ⟶ Y be a morphism of FTS S whose underlying morphism of schemes is a closed immersion. Then i^!(-) = R𝓗om(𝒪_X, -):

Ri_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) has a right adjoint;

the upper shriek i^! = j^* ∘ a of [Stacks, Tag 0A9Y] at the compactification X̄ = X that a proper morphism is (Stacks.Duality.properCompactification), with its right adjoint a produced by (1) and its quasi-coherence inputs discharged, agrees with R𝓗om(𝒪_X, -) on D⁺_QCoh(𝒪_Y);

for every right adjoint a of Ri_* the canonical comparison a(K) ⟶ R𝓗om(𝒪_X, K) — the mate of the counit of a under [Stacks, Tag 0A76] — is an isomorphism for every K in D⁺_QCoh(𝒪_Y).

The existence (1) is Stacks.Duality.LocallySmall.isLeftAdjoint_affineHomQuasiCoherentDerivedPushforward, which builds the right adjoint as DQ_X ∘ R𝓗om(𝒪_X, -) from the coherator of [Stacks, Tag 0CR0]; X is quasi-compact and quasi-separated, being of finite type over a Noetherian scheme. The identification (2), (3) is [Stacks, Tag 0A9X] at this model (Stacks.Duality.LocallySmall.isIso_rightAdjointToDerivedSheafHom_app), whose hypotheses — pseudo-coherence of i — hold in Situation 48.16.1.

theorem upperShriek_closedImmersion_of_fts {S : Scheme.{u}} [IsNoetherian S] {X Y : FTS S}
    (i : X ⟶ Y) [IsClosedImmersion i.left] :
    (affineHomQuasiCoherentDerivedPushforward i.left).IsLeftAdjoint ∧
      IsDerivedSheafHomRightAdjoint i.left
        (upperShriek i (properCompactification i)) ∧
      ∀ (a : quasiCoherentDerivedCategory Y.left ⥤ quasiCoherentDerivedCategory X.left)
        (adj : affineHomQuasiCoherentDerivedPushforward i.left ⊣ a)
        (K : (isBoundedBelowQuasiCoherent Y.left).FullSubcategory),
        IsIso ((rightAdjointToDerivedSheafHom i.left
          (isQuasicoherent_homology_derivedPushforward_of_isAffineHom i.left) a adj).app
            K.obj)

Stacks.Divisors.isDualizingModule_homologyOne_derivedSheafHomExactSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/EffectiveCartierDualizingModule.lean, line 118. The attribute's comment: “clauses (4)(a) and (7) for the inclusion i : D to X of an effective Cartier divisor into a locally Noetherian scheme, read on a module: clause (7) identifies i^! with Li^(-) tensor N[-1], so for a module omega the degree-one cohomology of i^!omega is N tensor i^omega, which is H^1(a(omega)) for a the right adjoint of Tag 0A76; clause (4)(a) is that this is dualizing on D. Nothing is carried: the reduction to affine charts of D lying over affine opens of X on which the ideal of D is principal on a nonzerodivisor is Tag 0A86, the chart-level input is Tag 0AX0 at the surjection Gamma(X,U) to Gamma(D, i^-1 U) whose kernel that nonzerodivisor generates, and the identification of H^1(a(omega)) with the twist is Tag 0AA4 at the level of modules. The general finite-type case of clause (4)(a) is Stacks.Duality.isDualizingComplex_upperShriek_of_fts, stated for an unconstructed f^!”.

[Stacks, Tag 0AA3] for the inclusion of an effective Cartier divisor, read on a module. Let D ⊆ X be an effective Cartier divisor on a locally Noetherian scheme, with closed immersion i : D ⟶ X, and let a(-) be the right adjoint of derived pushforward along i of [Stacks, Tag 0A76]. If a quasi-coherent 𝒪_X-module ω placed in some degree is a dualizing complex on X, then the 𝒪_D-module H¹(a(ω)) is a dualizing module on D.

Degree one is the degree [Stacks, Remark 0B4R] selects, and Stacks.Divisors.nonempty_homologyOne_derivedSheafHomExactSupport_iso identifies H¹(a(ω)) with the normal sheaf twist 𝒩 ⊗ i^*ω of the restriction.

theorem isDualizingModule_homologyOne_derivedSheafHomExactSupport (ω : X.Modules)
    [ω.IsQuasicoherent] (n : ℤ) (hω : Stacks.Duality.IsDualizingComplex
      ((DerivedCategory.singleFunctor X.Modules n).obj ω)) :
    letI : IsLocallyNoetherian D.subscheme := D.isLocallyNoetherian_subscheme
    Stacks.Duality.IsDualizingModule
      ((DerivedCategory.homologyFunctor D.subscheme.Modules 1).obj
        ((closedQuotient D).derivedSheafHomExactSupport.obj
          ((DerivedCategory.singleFunctor X.Modules 0).obj ω)))

Stacks.Duality.isNormalTensorPullbackRightAdjoint_of_fts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/DualityTheoryDivisor.lean, line 174. The attribute's comment: “clause (7) of Section 48.19: for the inclusion of an effective Cartier divisor into an object of FTS S, f^! is derived pullback tensored with the shifted normal sheaf i^*O_Y(D)[-1]. Both inputs are proved unconditionally: clause (5) of the same section (Tag 0AA2) as Stacks.Duality.isDerivedSheafHomRightAdjoint_of_fts_closedImmersion, and Tag 0AA4 as Stacks.Divisors.normalTensorDerivedSheafHomIso. As in clause (5), i^! is the explicit parameter a with its adjunction, the existence statement being Tag 0A9E”.

Stacks Project, Section 0AU3, clause (7). Let S be a Noetherian scheme, let Y be an object of AlgebraicGeometry.FTS S — a scheme separated and of finite type over S — and let D ⊆ Y be an effective Cartier divisor, with closed immersion i : D ⟶ Y and normal sheaf 𝒩 = i^*𝒪_Y(D). Let a be a right adjoint of Ri_* : D_QCoh(𝒪_D) ⥤ D_QCoh(𝒪_Y). Then a, which is i^!, is Li^*(-) ⊗^L_{𝒪_D} 𝒩[-1] on bounded-below complexes with quasi-coherent cohomology:

i^!(-) = Li^*(-) ⊗_{𝒪_D} i^*𝒪_Y(D)[-1].

The proof is the section's own: clause (5) of the section, which is [Stacks, Tag 0AA2] and is formalized as Stacks.Duality.isDerivedSheafHomRightAdjoint_of_fts_closedImmersion, identifies i^! with R𝓗om_{𝒪_Y}(𝒪_D, -); and [Stacks, Tag 0AA4], Stacks.Divisors.normalTensorDerivedSheafHomIso, identifies that with Li^*(-) ⊗^L_{𝒪_D} 𝒩[-1].

theorem isNormalTensorPullbackRightAdjoint_of_fts
    (a : quasiCoherentDerivedCategory Y.left ⥤ quasiCoherentDerivedCategory D.subscheme)
    (adj : affineHomQuasiCoherentDerivedPushforward D.subschemeι ⊣ a) :
    IsNormalTensorPullbackRightAdjoint D a

Stacks.Duality.upperShriek_isRightAdjointOnBoundedBelow_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImage/DualityTheoryProper.lean, line 117. The attribute's comment: “clause (2), first assertion: for a proper morphism f^! is a right adjoint of Rf_ and carries the bounded-below part of D_QCoh into the bounded-below part, so it is the restriction of that right adjoint to D^+_QCoh. The f^! is Stacks.Duality.upperShriek at the identity compactification, which is the one the source uses for a proper morphism; independence of the compactification is Tag 0AA0, which in this repository still carries the Tag 0A9L invertibility of Tag 0A9P. The SECOND assertion of clause (2), the duality isomorphism Rf_ RHom(K, f^! M) = RHom(Rf_* K, M), is not claimed: its map is Stacks.Duality.sheafyTrace and its invertibility is Tag 0GEW, which is open here”.

Stacks Project, Section 0AU3, clause (2), first assertion. Let S be a quasi-compact quasi-separated scheme (in the source, a Noetherian one) and let f : X ⟶ Y be a morphism of AlgebraicGeometry.FTS S, the schemes separated and of finite type over S, whose underlying morphism of schemes is proper. Then f^! is the restriction of the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) to D⁺_QCoh(𝒪_Y): the upper shriek functor of [Stacks, Tag 0A9Y] is a right adjoint of Rf_*, and it carries D⁺_QCoh(𝒪_Y) into D⁺_QCoh(𝒪_X).

Both conjuncts are needed for the clause: the first says f^! is the right adjoint, the second says the restriction of that right adjoint to the bounded-below parts is defined.

theorem upperShriek_isRightAdjointOnBoundedBelow_of_isProper :
    Nonempty (DerivedPushforward.qcqsRestrictedDerivedPushforward f.left ⊣
        upperShriek f (properCompactification f)) ∧
      ∀ K : quasiCoherentDerivedCategory Y.left, DerivedCategoryB.IsBoundedBelow K.obj →
        DerivedCategoryB.IsBoundedBelow
          ((upperShriek f (properCompactification f)).obj K).obj

Stacks.Duality.isDualizingComplex_upperShriek_of_fts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekDualizingComplex.lean, line 148. The attribute's comment: “clause (4)(a) of Section 48.19: the normalized complex f^! of a dualizing complex is dualizing, under the same carried hypotheses as the Tag 0AA3 key below”.

Stacks Project, Tag 0AA3 (Lemma 48.17.7). In Situation 48.16.1, let f : X ⟶ Y be a morphism of FTS S and let f^! be an exceptional inverse image functor D⁺_QCoh(𝒪_Y) ⥤ D⁺_QCoh(𝒪_X) for it, in the sense that on affine charts it is the algebraic upper shriek of a polynomial presentation of the chart ring map. If K is a dualizing complex for Y, then f^!K is a dualizing complex for X.

theorem isDualizingComplex_upperShriek_of_fts {S : Scheme.{u}} [IsNoetherian S] {X Y : FTS S}
    (f : X ⟶ Y)
    (fShriek : quasiCoherentDerivedCategoryPlus Y.left ⥤ quasiCoherentDerivedCategoryPlus X.left)
    (K : quasiCoherentDerivedCategoryPlus Y.left)
    (h0A86 : ∀ L : DerivedCategory X.left.Modules,
      (∀ x : X.left, ∃ (U : X.left.Opens) (hU : IsAffineOpen U),
        x ∈ U ∧ HasDualizingModelOn L U hU) → IsDualizingComplex L)
    (h0AA1 : ∀ (U : X.left.Opens) (hU : IsAffineOpen U) (V : Y.left.Opens)
      (hV : IsAffineOpen V) (hUV : U ≤ f.left ⁻¹ᵁ V)
      (ω : DerivedCategory (ModuleCat.{u} Γ(Y.left, V))),
      IsTildeModelOn K.obj.obj V hV ω →
      ∃ p : Dualizing.PolynomialPresentation (f.left.appLE V U hUV).hom,
        IsTildeModelOn (fShriek.obj K).obj.obj U hU (p.upperShriekFunctor.{u, u}.obj ω))
    (hK : IsDualizingComplex K.obj.obj) :
    IsDualizingComplex (fShriek.obj K).obj.obj

Sources

LeanStacks.Duality.isDerivedSheafHomRightAdjoint_of_fts_closedImmersion · Stacks.Duality.LocallySmall.upperShriek_closedImmersion_of_fts · Stacks.Divisors.isDualizingModule_homologyOne_derivedSheafHomExactSupport · Stacks.Duality.isNormalTensorPullbackRightAdjoint_of_fts · Stacks.Duality.upperShriek_isRightAdjointOnBoundedBelow_of_isProper · Stacks.Duality.isDualizingComplex_upperShriek_of_fts

Section48.20 Glueing dualizing complexes #

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

Tag 0AU4, a situation

Tag 0AU4 in the Stacks Project.

Stacks.Duality.DualizingBase, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GlueingDualizingComplexes.lean, line 141. The attribute's comment: “the Situation: a Noetherian scheme with a chosen dualizing complex”.

Stacks Project, Tag 0AU4. The standing situation of the section on glueing dualizing complexes: a Noetherian scheme S together with a dualizing complex ω_S^• on it, in the sense of [Stacks, Tag 0A87].

structure DualizingBase

Tag 0AU6, an item

Tag 0AU6 in the Stacks Project.

Stacks.Duality.UpperShriek.overlapCompareRestrict_cocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingCocycle.lean, line 249. The attribute's comment: “item (3) of the discussion before Definition 0AUA: the cocycle condition phi_ik = phi_jk after phi_ij for the canonical comparisons of the local models, restricted to the triple overlap U_i cap U_j cap U_k. RESTRICTED only in that the upper-shriek formalism of Stacks 0A9Y/0ATX/0ATY is the parameter UpperShriek, as in 0AUB and 0AUC; the coherence 0ATY, which the source cites for item (3), is its factorIso_assoc field”.

Stacks Project, Tag 0AU6. In Situation [Stacks, Tag 0AU4] let X be of finite type over S and let 𝒰 : X = ⋃ U_i be a finite covering of X by opens separated and of finite type over S. Let ω_i^• be the local models and φ_{ij} : ω_i^•|_{U_i ∩ U_j} ≅ ω_j^•|_{U_i ∩ U_j} the canonical comparisons of the discussion preceding Definition [Stacks, Tag 0AUA]. Then for all i, j, k

φ_{ik}|_{U_i ∩ U_j ∩ U_k} = φ_{jk}|_{U_i ∩ U_j ∩ U_k} ∘ φ_{ij}|_{U_i ∩ U_j ∩ U_k}

in D(𝒪_{U_i ∩ U_j ∩ U_k}). Composition is written left to right, so the right hand side below reads φ_{ij} followed by φ_{jk}.

The restrictions are Stacks.Duality.UpperShriek.overlapCompareRestrict, i.e. the conjugation of Stacks.Duality.UpperShriek.restrictCompare; the proof identifies all three with comparisons built directly on the triple overlap (Stacks.Duality.UpperShriek.overlapCompareRestrict_eq, which is the coherence [Stacks, Tag 0ATY]) and then cancels (Stacks.Duality.UpperShriek.localCompare_trans).

theorem overlapCompareRestrict_cocycle (𝒰 : SeparatedCovering p ι) (i j k : ι) :
    A.overlapCompareRestrict hp ωS 𝒰 i k (𝒰.U i ⊓ 𝒰.U j ⊓ 𝒰.U k)
        (le_inf (inf_le_left.trans inf_le_left) inf_le_right) =
      A.overlapCompareRestrict hp ωS 𝒰 i j (𝒰.U i ⊓ 𝒰.U j ⊓ 𝒰.U k) inf_le_left ≪≫
        A.overlapCompareRestrict hp ωS 𝒰 j k (𝒰.U i ⊓ 𝒰.U j ⊓ 𝒰.U k)
          (le_inf (inf_le_left.trans inf_le_right) inf_le_right)

Tag 0AU7, a lemma

Tag 0AU7 in the Stacks Project.

Stacks.Duality.Normalized.existsUnique_iso_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedExistenceNagata.lean, line 55.

[Stacks, Tag 0AU7] In Situation 0AU4, let X be of finite type over S and 𝒰 a finite open covering of X by schemes separated over S. A dualizing complex normalized relative to ω_S^• and 𝒰 is unique up to unique isomorphism: for two of them, (K, α_i) and (K', α'_i), exactly one isomorphism K ≅ K' carries α_i to α'_i on every member.

theorem existsUnique_iso_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) {ι : Type w}
    {𝒰 : SeparatedCovering p ι} (𝒩 𝒩' : Normalized UpperShriek.nagata hp ωS 𝒰) :
    ∃! e : 𝒩.complex ≅ 𝒩'.complex, ∀ i,
      (UpperShriek.nagata.shriek (𝒰.U i).ι (hp.isShriekable_ι _)).mapIso e ≪≫
        𝒩'.localIso i = 𝒩.localIso i

Tag 0AU8, a lemma

Tag 0AU8 in the Stacks Project.

Stacks.Duality.Normalized.exists_existsUnique_iso_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedExistenceNagata.lean, line 69.

[Stacks, Tag 0AU8] In Situation 0AU4, let X be of finite type over S and 𝒰, 𝒱 two finite open coverings of X by schemes separated over S. If (K, α_i) is a dualizing complex normalized relative to ω_S^• and 𝒰, there is a dualizing complex (K', α'_j) normalized relative to ω_S^• and 𝒱, and the two are canonically isomorphic: exactly one isomorphism K ≅ K' carries the restriction of α_i to U_i ∩ V_j to that of α'_j, for all i, j.

theorem exists_existsUnique_iso_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    {ι J : Type w} {𝒰 : SeparatedCovering p ι} (𝒱 : SeparatedCovering p J)
    (𝒩 : Normalized UpperShriek.nagata hp ωS 𝒰) :
    ∃ 𝒩' : Normalized UpperShriek.nagata hp ωS 𝒱,
      (haveI := hp.source_noetherian; IsDualizingComplex 𝒩'.complex.obj.obj) ∧
      ∃! e : 𝒩.complex ≅ 𝒩'.complex, ∀ i j,
        (UpperShriek.nagata.shriek (𝒰.U i ⊓ 𝒱.U j).ι (hp.isShriekable_ι _)).mapIso e ≪≫
          UpperShriek.nagata.restrictLocalIso hp ωS 𝒩'.complex
            (inf_le_right : 𝒰.U i ⊓ 𝒱.U j ≤ 𝒱.U j) (𝒱.shriekable j) (𝒩'.localIso j) =
        UpperShriek.nagata.restrictLocalIso hp ωS 𝒩.complex
          (inf_le_left : 𝒰.U i ⊓ 𝒱.U j ≤ 𝒰.U i) (𝒰.shriekable i) (𝒩.localIso i)

Tag 0AU9, a lemma

Tag 0AU9 in the Stacks Project.

Stacks.Duality.Normalized.exists_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedExistenceNagata.lean, line 87.

[Stacks, Tag 0AU9] In Situation 0AU4, let X be of finite type over S and 𝒰 a finite open covering of X by schemes separated over S. Then there exists a dualizing complex normalized relative to ω_S^• and 𝒰.

theorem exists_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    {ι : Type w} (𝒰 : SeparatedCovering p ι) :
    ∃ 𝒩 : Normalized UpperShriek.nagata hp ωS 𝒰,
      haveI := hp.source_noetherian; IsDualizingComplex 𝒩.complex.obj.obj

Tag 0AUA, a definition

Tag 0AUA in the Stacks Project.

Stacks.Duality.isDualizingComplex_normalizedDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingComplexNagata.lean, line 55. The attribute's comment: “ω_X^• is a dualizing complex on X”.

[Stacks, Tag 0AUA], ω_X^• is a dualizing complex. Let S be Noetherian with a dualizing complex ω_S^• and X of finite type over S. The dualizing complex ω_X^• normalized relative to ω_S^• is a dualizing complex on X.

theorem isDualizingComplex_normalizedDualizingComplex :
    haveI := hp.source_noetherian
    IsDualizingComplex (normalizedDualizingComplex hp ωS hωS).complex.obj.obj

Stacks.Duality.existsUnique_iso_normalizedDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingComplexNagata.lean, line 66. The attribute's comment: “the pair (ω_X^•, α_U) is unique up to unique isomorphism”.

[Stacks, Tag 0AUA], uniqueness up to unique isomorphism. Let S be Noetherian with a dualizing complex ω_S^• and X of finite type over S. For any complex K on X with isomorphisms β_U : K|_U ≅ (U → S)^! ω_S^• for the opens U ⊆ X separated over S, compatible with restriction, exactly one isomorphism K ≅ ω_X^• carries β_U to the isomorphism α_U of ω_X^• for every such U.

theorem existsUnique_iso_normalizedDualizingComplex
    (𝒦 : NormalizedOnOpens UpperShriek.nagata hp ωS) :
    ∃! e : 𝒦.complex ≅ (normalizedDualizingComplex hp ωS hωS).complex,
      ∀ (W : X.Opens) (hW : IsShriekable (W.ι ≫ p)),
        (UpperShriek.nagata.shriek W.ι (hp.isShriekable_ι W)).mapIso e ≪≫
          (normalizedDualizingComplex hp ωS hωS).localIso W hW = 𝒦.localIso W hW

Stacks.Duality.existsUnique_iso_normalizedDualizingComplex_toNormalized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingComplexNagata.lean, line 82. The attribute's comment: “(ω_X^•, α_{U_i}) is normalized relative to ω_S^• and every finite covering by opens separated over S”.

[Stacks, Tag 0AUA], normalized relative to every covering. Let S be Noetherian with a dualizing complex ω_S^•, X of finite type over S and 𝒰 : X = ⋃ U_i a finite open covering by opens separated over S. Then (ω_X^•, α_{U_i}) is a dualizing complex normalized relative to ω_S^• and 𝒰 (Stacks.Duality.NormalizedOnOpens.toNormalized), and it is the one up to unique isomorphism: for every dualizing complex (K, β_i) normalized relative to ω_S^• and 𝒰, exactly one isomorphism K ≅ ω_X^• carries β_i to α_{U_i} for all i.

theorem existsUnique_iso_normalizedDualizingComplex_toNormalized {ι : Type w}
    (𝒰 : SeparatedCovering p ι) (𝒩 : Normalized UpperShriek.nagata hp ωS 𝒰) :
    ∃! e : 𝒩.complex ≅ ((normalizedDualizingComplex hp ωS hωS).toNormalized 𝒰).complex,
      ∀ i, (UpperShriek.nagata.shriek (𝒰.U i).ι (hp.isShriekable_ι _)).mapIso e ≪≫
          ((normalizedDualizingComplex hp ωS hωS).toNormalized 𝒰).localIso i = 𝒩.localIso i

Stacks.Duality.normalizedDualizingComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedExistenceNagata.lean, line 104.

[Stacks, Tag 0AUA] Let S be Noetherian with a dualizing complex ω_S^• and X of finite type over S. The dualizing complex ω_X^• normalized relative to ω_S^•: a complex on X with isomorphisms α_W : ω_X^•|_W ≅ (W → S)^! ω_S^• for every open W separated over S, compatible with restriction. It is unique up to unique isomorphism (Stacks.Duality.NormalizedOnOpens.existsUnique_iso_ofCompactifications) and normalized relative to ω_S^• and every finite covering of X by opens separated over S (Stacks.Duality.NormalizedOnOpens.toNormalized).

def normalizedDualizingComplex {X S : Scheme.{u}} {p : X ⟶ S}
    (hp : IsFiniteTypeOverNoetherian p) (ωS : quasiCoherentDerivedCategoryPlusOfModel S)
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) :
    NormalizedOnOpens UpperShriek.nagata hp ωS

Tag 0AUB, a lemma

Tag 0AUB in the Stacks Project.

Stacks.Duality.exists_normalized_of_normalized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingTransitivity.lean, line 592. The attribute's comment: “assuming the upper-shriek formalism of Stacks 0A9E/0ATX/0ATY as the parameter UpperShriek, pending its landing”.

[Stacks, Tag 0AUB] Let S be a Noetherian scheme carrying ω_S^•, let q : Y ⟶ S and p = f ≫ q : X ⟶ S be of finite type, and let 𝒱 and 𝒰 be coverings of Y and of X by opens separated and of finite type over S, with each U_k carried by f into V_{idx k}. If ω_X^• is normalized relative to ω_S^• and 𝒰, and ω_Y^• is normalized relative to ω_S^• and 𝒱, then ω_X^• is normalized relative to ω_Y^• and 𝒰 read over Y.

Normalization here is the primitive notion of the text of [Stacks, Tag 0AU5] -- the pair (K, α_i) -- rather than the covering-free Definition [Stacks, Tag 0AUA], and it is the notion the proof of 0AUB manipulates. That ω_X^• is again dualizing is not part of the statement because Normalized does not record dualizing-ness; it is [Stacks, Tag 0AU8].

theorem exists_normalized_of_normalized {𝒟 : Scheme.{u} → Type v}
    [∀ X : Scheme.{u}, Category.{v'} (𝒟 X)] (A : UpperShriek 𝒟) {X Y S : Scheme.{u}}
    {f : X ⟶ Y} {q : Y ⟶ S} {p : X ⟶ S} (hpe : f ≫ q = p)
    (hp : IsFiniteTypeOverNoetherian p) (hq : IsFiniteTypeOverNoetherian q) (ωS : 𝒟 S)
    {ι : Type w} {J : Type w'} (𝒰 : SeparatedCovering p ι) (𝒱 : SeparatedCovering q J)
    (idx : ι → J) (hle : ∀ k, 𝒰.U k ≤ f ⁻¹ᵁ 𝒱.U (idx k)) (𝒩X : Normalized A hp ωS 𝒰)
    (𝒩Y : Normalized A hq ωS 𝒱) :
    ∃ 𝒩 : Normalized A (hp.of_comp' hq hpe) 𝒩Y.complex (𝒰.overMid 𝒱 hp hq hpe idx hle),
      𝒩.complex = 𝒩X.complex

Stacks.Duality.NormalizedOnOpens.exists_relative_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedProperNagata.lean, line 59.

[Stacks, Tag 0AUB] In Situation 0AU4, let f : X ⟶ Y be a morphism of schemes of finite type over S and ω_X^•, ω_Y^• dualizing complexes normalized relative to ω_S^•. Then ω_X^• is a dualizing complex normalized relative to ω_Y^•: ω_Y^• and ω_X^• are dualizing, so (Y, ω_Y^•) is again as in Situation 0AU4, and ω_X^• carries isomorphisms ω_X^•|_W ≅ (W → Y)^! ω_Y^• for every open W separated over Y, compatible with restriction.

theorem exists_relative_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    (haveI := hq.source_noetherian; IsDualizingComplex 𝒦Y.complex.obj.obj) ∧
    (haveI := hp.source_noetherian; IsDualizingComplex 𝒦X.complex.obj.obj) ∧
    ∃ 𝒦 : NormalizedOnOpens UpperShriek.nagata (hp.of_comp' hq hpe) 𝒦Y.complex,
      𝒦.complex = 𝒦X.complex

Tag 0AUC, a lemma

Tag 0AUC in the Stacks Project.

Stacks.Duality.Normalized.restrictOverBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingOpenImmersion.lean, line 227. The attribute's comment: “the restriction of a normalized complex is itself normalized, which is the whole content of the tag; RESTRICTED in that the upper-shriek formalism is the parameter UpperShriek of Stacks 0A9E/0ATX/0ATY and normalization is the covering-indexed notion of the text of Tag 0AU5”.

Stacks Project, Tag 0AUC, part one: ω_Y^•|_X is normalized relative to ω_S^•.

Let (S, ω_S^•) be as in Situation [Stacks, Tag 0AU4], let f : X ⟶ Y be a morphism of schemes of finite type over S and let ω_Y^• be normalized relative to ω_S^• and the covering 𝒱 of Y. Then f^!ω_Y^• is normalized relative to ω_S^• and any covering 𝒰 of X whose members are carried by f into members of 𝒱.

The normalization on U_k is the composite (U_k → X)^!f^!ω_Y^• ≅ (U_k → Y)^!ω_Y^• ≅ (U_k → S)^!ω_S^•: the tautological comparison Stacks.Duality.UpperShriek.shriekRestrictIso followed by the inverse of the transport of β_{idx k} along U_k → V_{idx k}. The compatibility on overlaps splits by Stacks.Duality.UpperShriek.restrictLocalIso_trans into Stacks.Duality.UpperShriek.restrictLocalIso_shriekRestrictIso for the first halves and Stacks.Duality.Normalized.transport_localIso_eq for the second.

For f = j an open immersion j^!ω_Y^• is the restriction ω_Y^•|_X, by [Stacks, Tag 0AU0], and this is the statement [Stacks, Tag 0AUC] needs in order to apply the uniqueness [Stacks, Tag 0AU7]. It is proved for an arbitrary f, since nothing in the argument uses more than shriekability.

def restrictOverBase (hf : IsShriekable f) : Normalized A hp ωS 𝒰

Stacks.Duality.exists_normalizedIso_restrict_of_openImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingOpenImmersion.lean, line 306. The attribute's comment: “RESTRICTED: the upper-shriek formalism is the parameter UpperShriek of Stacks 0A9E/0ATX/0ATY, normalization is the covering-indexed notion of the text of Tag 0AU5, and the uniqueness of a normalized complex on a fixed covering (Tag 0AU7, not proved here) is the hypothesis h0AU7. What is proved is that omega_Y restricted to X is itself normalized relative to omega_S, which is the second normalized structure h0AU7 is applied to”.

Stacks Project, Tag 0AUC. Let (S, ω_S^•) be as in Situation [Stacks, Tag 0AU4]. Let j : X ⟶ Y be an open immersion of schemes of finite type over S. Let ω_X^• and ω_Y^• be dualizing complexes normalized relative to ω_S^•. Then there is a canonical isomorphism ω_X^• = ω_Y^•|_X, where the restriction ω_Y^•|_X is j^!ω_Y^• by [Stacks, Tag 0AU0].

The isomorphism produced is compatible with the normalizations on every member of the covering 𝒰 of X, which is what makes it canonical rather than an arbitrary isomorphism of complexes.

The content is Stacks.Duality.Normalized.restrictOverBase: ω_Y^•|_X is itself normalized relative to ω_S^• and 𝒰. Uniqueness of a complex normalized relative to ω_S^• and a given covering is [Stacks, Tag 0AU7], a separate lemma whose proof needs the invertible objects of [Stacks, Tag 0ATP]; it is not proved in this library and is the hypothesis h0AU7. See the module documentation for why that hypothesis leaves the statement with content.

theorem exists_normalizedIso_restrict_of_openImmersion {𝒟 : Scheme.{u} → Type v}
    [∀ X : Scheme.{u}, Category.{v'} (𝒟 X)] (A : UpperShriek 𝒟) {X Y S : Scheme.{u}}
    {j : X ⟶ Y} {q : Y ⟶ S} {p : X ⟶ S} (hpe : j ≫ q = p) (hj : IsShriekable j)
    (hp : IsFiniteTypeOverNoetherian p) (hq : IsFiniteTypeOverNoetherian q) {ωS : 𝒟 S}
    {ι : Type w} {J : Type w'} {𝒰 : SeparatedCovering p ι} {𝒱 : SeparatedCovering q J}
    (idx : ι → J) (hle : ∀ k, 𝒰.U k ≤ j ⁻¹ᵁ 𝒱.U (idx k))
    (𝒩X : Normalized A hp ωS 𝒰) (𝒩Y : Normalized A hq ωS 𝒱)
    (h0AU7 : ∀ 𝒩 𝒩' : Normalized A hp ωS 𝒰, ∃ e : 𝒩.complex ≅ 𝒩'.complex,
      ∀ k, (A.shriek (𝒰.U k).ι (hp.isShriekable_ι (𝒰.U k))).mapIso e ≪≫ 𝒩'.localIso k =
        𝒩.localIso k) :
    ∃ e : 𝒩X.complex ≅ (A.shriek j hj).obj 𝒩Y.complex,
      ∀ k, (A.shriek (𝒰.U k).ι (hp.isShriekable_ι (𝒰.U k))).mapIso e ≪≫
          (Normalized.restrictOverBase hpe hp hq idx hle 𝒩Y hj).localIso k =
        𝒩X.localIso k

Stacks.Duality.NormalizedOnOpens.existsUnique_iso_shriekOfIsOpenImmersion_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedOnOpensOpenImmersion.lean, line 170.

[Stacks, Tag 0AUC], canonicity. In Situation 0AU4, let j : X ⟶ Y be an open immersion of schemes of finite type over S and ω_X^•, ω_Y^• dualizing complexes normalized relative to ω_S^•. Exactly one isomorphism ω_X^• ≅ j^! ω_Y^• carries the normalization α_W of ω_X^• to that of j^! ω_Y^• (shriekOfIsOpenImmersion) for every open W ⊆ X separated over S.

theorem existsUnique_iso_shriekOfIsOpenImmersion_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    ∃! e : 𝒦X.complex ≅
        (UpperShriek.nagata.shriek j (hq.isShriekable_of_isOpenImmersion j)).obj 𝒦Y.complex,
      ∀ (W : X.Opens) (hW : IsShriekable (W.ι ≫ p)),
        (UpperShriek.nagata.shriek W.ι (hp.isShriekable_ι W)).mapIso e ≪≫
          (𝒦Y.shriekOfIsOpenImmersion hpe hp).localIso W hW = 𝒦X.localIso W hW

Stacks.Duality.NormalizedOnOpens.isoDerivedRestrictNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedOnOpensOpenImmersion.lean, line 189.

[Stacks, Tag 0AUC] In Situation 0AU4, let j : X ⟶ Y be an open immersion of schemes of finite type over S and ω_X^•, ω_Y^• dualizing complexes normalized relative to ω_S^•. The canonical isomorphism ω_X^• ≅ ω_Y^•|_X in D(𝒪_X): the unique isomorphism ω_X^• ≅ j^! ω_Y^• compatible with the normalizations (existsUnique_iso_shriekOfIsOpenImmersion_nagata), followed by j^! = j^* ([Stacks, Tag 0AU0]).

def isoDerivedRestrictNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    𝒦X.complex.obj.obj ≅
      (Scheme.Modules.restrictFunctor j).mapDerivedCategory.obj 𝒦Y.complex.obj.obj

Stacks.Duality.NormalizedOnOpens.isoDerivedRestrictNagata_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedOnOpensOpenImmersion.lean, line 204.

[Stacks, Tag 0AUC], the canonical isomorphism is characterised by the normalizations: for any isomorphism e : ω_X^• ≅ j^! ω_Y^• compatible with the normalizations on every open of X separated over S, isoDerivedRestrictNagata is e followed by j^! = j^*.

theorem isoDerivedRestrictNagata_eq
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (e : 𝒦X.complex ≅
      (UpperShriek.nagata.shriek j (hq.isShriekable_of_isOpenImmersion j)).obj 𝒦Y.complex)
    (he : ∀ (W : X.Opens) (hW : IsShriekable (W.ι ≫ p)),
      (UpperShriek.nagata.shriek W.ι (hp.isShriekable_ι W)).mapIso e ≪≫
        (𝒦Y.shriekOfIsOpenImmersion hpe hp).localIso W hW = 𝒦X.localIso W hW) :
    isoDerivedRestrictNagata hpe hωS 𝒦X 𝒦Y =
      (ObjectProperty.ι _ ⋙ ObjectProperty.ι _).mapIso e ≪≫
        UpperShriek.shriekObjIsoDerivedRestrict nagataCompactification j
          (hq.isShriekable_of_isOpenImmersion j) 𝒦Y.complex

Tag 0AUD, a lemma

Tag 0AUD in the Stacks Project.

Stacks.Duality.dualizingIsoRightAdjointObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GlueingDualizingComplexes.lean, line 404. The attribute's comment: “RESTRICTED: the upper shriek formalism is a parameter, normalization is taken in the separated form omega_X = p^! omega_S, and the identification of f^! with the right adjoint, which is the only place properness is used, is a hypothesis”.

Stacks Project, Tag 0AUD. Let f : X ⟶ Y be a morphism of schemes of finite type over the base of [Stacks, Tag 0AU4], with structure morphisms q : Y ⟶ S and p : X ⟶ S and f ≫ q = p. Let a be the right adjoint of Rf_* of [Stacks, Tag 0A9E]. If ω_X^• and ω_Y^• are normalized relative to ω_S^•, there is a canonical isomorphism a(ω_Y^•) ≅ ω_X^•.

This is the argument of the source in the case where the schemes are separated over S: there ω_X^• = p^!ω_S^• and ω_Y^• = q^!ω_S^•, the properness of f enters only through the identification of f^! with a, and the composition comparison f^! ∘ q^! ≅ p^! — the factorIso field of Stacks.Duality.UpperShriek — finishes it.

def dualizingIsoRightAdjointObj (A : UpperShriek 𝒟) {X Y S : Scheme.{u}}
    {f : X ⟶ Y} {q : Y ⟶ S} {p : X ⟶ S} (hfq : f ≫ q = p)
    (hf : IsShriekable f) (hq : IsShriekable q) (hp : IsShriekable p)
    {a : 𝒟 Y ⥤ 𝒟 X} (hfa : A.shriek f hf ≅ a)
    (ωS : 𝒟 S) {ωX : 𝒟 X} {ωY : 𝒟 Y}
    (nX : ωX ≅ (A.shriek p hp).obj ωS) (nY : ωY ≅ (A.shriek q hq).obj ωS) :
    a.obj ωY ≅ ωX

Stacks.Duality.NormalizedOnOpens.twistedInverseImageObjIsoNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedProperNagata.lean, line 92.

[Stacks, Tag 0AUD] In Situation 0AU4, let f : X ⟶ Y be a proper morphism of schemes of finite type over S, ω_X^•, ω_Y^• the dualizing complexes normalized relative to ω_S^•, and a the right adjoint of Rf_* ([Stacks, Tag 0A9E]). Then there is a canonical isomorphism a(ω_Y^•) ≅ ω_X^•.

def twistedInverseImageObjIsoNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    (twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
        𝒦Y.complex.obj ≅ 𝒦X.complex.obj

Tag 0AUE, a lemma

Tag 0AUE in the Stacks Project.

Stacks.Duality.normalizedUpperShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/DualizingModuleOverField.lean, line 167. The attribute's comment: “the closing remark, first half only: for X separated over the base the complex p^! omega_S^bullet is normalized relative to omega_S^bullet. The second half of the remark, f_new^! K = f^! K, is NOT carried, and neither are parts (1), (3), (5), (6); parts (2) and (4) are elsewhere. RESTRICTED: the upper-shriek formalism of Stacks 0A9Y/0ATX/0ATY is the parameter UpperShriek, pending its landing”.

[Stacks, Tag 0AUE], the closing remark on the separated case. Let X be separated and of finite type over a Noetherian scheme S with structure morphism p, and let ω_S^• be a complex on S. Then p^!ω_S^• is normalized relative to ω_S^•: its restriction to each member of a covering of X by opens separated over S is canonically the local model there, compatibly on overlaps.

def normalizedUpperShriek {ι : Type w} (𝒰 : SeparatedCovering p ι) : Normalized A hp ωS 𝒰

Stacks.Duality.fNewShriekObjIsoDualizing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NewShriekNormalizedComplex.lean, line 131. The attribute's comment: “part (4): omega_X is f_new^! of omega_Y for a finite-type morphism over the base. RESTRICTED: the closed monoidal structure on the derived categories is an instance argument, and the two inputs the source names are hypotheses -- the identification R Hom(omega_Y, omega_Y) = O_Y coming from omega_Y being dualizing, and the unit half Lf^* O_Y = O_X of the monoidality of the derived pullback”.

Stacks Project, Tag 0AUE, part (4). Let f : X ⟶ Y be a morphism of schemes of finite type over the base of [Stacks, Tag 0AU4] and let ω_X^• and ω_Y^• be the complexes normalized relative to ω_S^•, [Stacks, Tag 0AU5]. Then

f_new^! ω_Y^• ≅ ω_X^•.

The computation is the source's: D_Y(ω_Y^•) ≅ 𝒪_Y because ω_Y^• is dualizing, Lf^* carries the unit to the unit, and D_X(𝒪_X) ≅ ω_X^• by Stacks.Duality.relativeDualObjUnit. The statement is not an identity by definition: Stacks.Duality.fNewShriek unfolds the left hand side to R𝓗om(Lf^* R𝓗om(ω_Y^•, ω_Y^•), ω_X^•), and the three steps above are what turn that into ω_X^•.

def fNewShriekObjIsoDualizing (f : X ⟶ Y) (ωX : DerivedCategory X.Modules)
    (ωY : DerivedCategory Y.Modules)
    (eY : (relativeDual ωY).obj (op ωY) ≅ 𝟙_ (DerivedCategory Y.Modules))
    (ef : (derivedPullback f).obj (𝟙_ (DerivedCategory Y.Modules)) ≅
      𝟙_ (DerivedCategory X.Modules)) :
    (fNewShriek f ωX ωY).obj ωY ≅ ωX

Stacks.Duality.fNewShriekStructureObjIsoDualizing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NewShriekNormalizedComplex.lean, line 163. The attribute's comment: “part (2): omega_X is the new twisted inverse image of omega_S along the structure morphism. RESTRICTED: the closed monoidal structure on the derived categories is an instance argument, and the identification R Hom(omega_S, omega_S) = O_S implied by B.isDualizing together with the unit half Lpi^* O_S = O_X of the monoidality of the derived pullback are hypotheses”.

Stacks Project, Tag 0AUE, part (2). For a scheme X of finite type over the base of [Stacks, Tag 0AU4], with structure morphism π : X ⟶ S, the complex normalized relative to ω_S^• is what π_new^! does to ω_S^•:

ω_X^• ≅ (X → S)_new^! ω_S^•.

This is Stacks.Duality.fNewShriekObjIsoDualizing at the structure morphism, read in the vocabulary of the Situation: the two inputs become D_S(ω_S^•) ≅ 𝒪_S, which is the homothety condition of the dualizing complex B.isDualizing names, and Lπ^* 𝒪_S ≅ 𝒪_X.

def fNewShriekStructureObjIsoDualizing
    (eS : (relativeDual B.dualizing).obj (op B.dualizing) ≅
      𝟙_ (DerivedCategory B.scheme.Modules))
    (ep : (derivedPullback Xb.str).obj (𝟙_ (DerivedCategory B.scheme.Modules)) ≅
      𝟙_ (DerivedCategory Xb.scheme.Modules)) :
    (fNewShriek Xb.str Xb.dualizing B.dualizing).obj B.dualizing ≅ Xb.dualizing

Stacks.Duality.existsUnique_iso_upperShriekPlus_of_isSeparated_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 135. The attribute's comment: “the closing remark, first half: omega_X = (X -> S)^! omega_S for X separated over S”.

[Stacks, Tag 0AUE], the closing remark, first half. In Situation 0AU4, if X is separated over S, with structure morphism p, the dualizing complex ω_X^• normalized relative to ω_S^• is canonically isomorphic to p^! ω_S^•, for the upper shriek functor p^! of any compactification j of p ([Stacks, Tag 0A9Y]): exactly one isomorphism ω_X^• ≅ p^!_j ω_S^• carries the normalization α_W of ω_X^• to the canonical (p^! ω_S^•)|_W ≅ (W → S)^! ω_S^• for every open W separated over S.

theorem existsUnique_iso_upperShriekPlus_of_isSeparated_nagata {X S : Scheme.{u}} {p : X ⟶ S}
    {hp : IsFiniteTypeOverNoetherian p} {ωS : quasiCoherentDerivedCategoryPlusOfModel S}
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsSeparated p]
    (𝒦 : NormalizedOnOpens UpperShriek.nagata hp ωS) (j : CompactificationOf (Over.mk p)) :
    haveI := hp.base_noetherian
    ∃! e : 𝒦.complex ≅ (upperShriekPlus (ftsHomOf p
        (isShriekable_of_isSeparated_of_isFiniteTypeOverNoetherian hp).separatedFiniteType
        (isSeparatedFiniteType_id S) (Category.comp_id p)) j).obj ωS,
      ∀ (W : X.Opens) (hW : IsShriekable (W.ι ≫ p)),
        (UpperShriek.nagata.shriek W.ι (hp.isShriekable_ι W)).mapIso
            (e ≪≫ (DominatingCompactification.upperShriekPlusIso (ftsHomOf p
              (isShriekable_of_isSeparated_of_isFiniteTypeOverNoetherian hp).separatedFiniteType
              (isSeparatedFiniteType_id S) (Category.comp_id p)) j
              (nagataCompactification p
                (isShriekable_of_isSeparated_of_isFiniteTypeOverNoetherian hp))).app ωS) ≪≫
          upperShriekLocalIso UpperShriek.nagata hp
            (isShriekable_of_isSeparated_of_isFiniteTypeOverNoetherian hp) ωS hW =
        𝒦.localIso W hW

Stacks.Duality.NormalizedOnOpens.fNewShriekObjIsoNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 167. The attribute's comment: “part (4)”.

[Stacks, Tag 0AUE] part (4). In Situation 0AU4, let f : X ⟶ Y be a morphism of schemes of finite type over S and ω_X^•, ω_Y^• the dualizing complexes normalized relative to ω_S^• (for the upper shriek functors of Nagata compactifications). Then ω_X^• ≅ f_new^! ω_Y^•.

def fNewShriekObjIsoNagata (f : X ⟶ Y)
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    stdComplex nagataCompactification 𝒦X ≅
      (fNewShriekStd f (stdComplex nagataCompactification 𝒦X)
        (stdComplex nagataCompactification 𝒦Y)).obj (stdComplex nagataCompactification 𝒦Y)

Stacks.Duality.NormalizedOnOpens.fNewShriekStructureObjIsoNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 187. The attribute's comment: “part (2)”.

[Stacks, Tag 0AUE] part (2). In Situation 0AU4, for X of finite type over S with structure morphism p : X ⟶ S and ω_X^• the dualizing complex normalized relative to ω_S^•, ω_X^• ≅ (X → S)_new^! ω_S^•, where (X → S)_new^! is formed with ω_S^• itself as the normalized complex of S.

def fNewShriekStructureObjIsoNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS) :
    stdComplex nagataCompactification 𝒦X ≅
      (fNewShriekStd p (stdComplex nagataCompactification 𝒦X) (baseStdComplex ωS)).obj
        (baseStdComplex ωS)

Stacks.Duality.NormalizedOnOpens.coherentDuality_spec_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 203. The attribute's comment: “part (3)”.

[Stacks, Tag 0AUE] part (3). In Situation 0AU4, for X of finite type over S and ω_X^• normalized relative to ω_S^•, the duality D_X = R𝓗om(-, ω_X^•) is an involution of D_Coh(𝒪_X): it carries D_Coh(𝒪_X) into itself, is an anti-equivalence of it with id ≅ D_X ∘ D_X given by biduality, exchanges D^+_Coh and D^-_Coh, and is an anti-equivalence of D^b_Coh(𝒪_X).

theorem coherentDuality_spec_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦 : NormalizedOnOpens UpperShriek.nagata hp ωS) :
    haveI := hp.source_noetherian
    cohStd X (stdComplex nagataCompactification 𝒦) ∧
    (∀ M : Std X, cohStd X M →
      cohStd X ((dualInto (stdComplex nagataCompactification 𝒦)).obj (op M))) ∧
    (coherentDuality X
      (isDualizing_stdComplex nagataCompactification (Category.id_comp p) hωS 𝒦)).IsEquivalence ∧
    IsIso (coherentBiduality X
      (isDualizing_stdComplex nagataCompactification (Category.id_comp p) hωS 𝒦)) ∧
    (∀ M : Std X, cohStd X M →
      (plusCoh X M ↔
        minusCoh X ((dualInto (stdComplex nagataCompactification 𝒦)).obj (op M))) ∧
      (minusCoh X M ↔
        plusCoh X ((dualInto (stdComplex nagataCompactification 𝒦)).obj (op M)))) ∧
    (boundedCoherentDuality X
      (isDualizing_stdComplex nagataCompactification (Category.id_comp p) hωS 𝒦)).IsEquivalence

Stacks.Duality.NormalizedOnOpens.fNewShriekPlusCohNagata_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 245. The attribute's comment: “part (5)”.

[Stacks, Tag 0AUE] part (5). In Situation 0AU4, for a morphism f : X ⟶ Y of schemes of finite type over S, f_new^! is a functor D^+_Coh(𝒪_Y) ⥤ D^+_Coh(𝒪_X) and f_new^! M = D_X(Lf^* D_Y(M)) for M ∈ D^+_Coh(𝒪_Y): for such M the complex D_X(Lf^* D_Y(M)) lies in D^+_Coh(𝒪_X), and it is the value of f_new^! at M.

theorem fNewShriekPlusCohNagata_obj (f : X ⟶ Y)
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) (M : (plusCoh Y).FullSubcategory) :
    plusCoh X ((dualInto (stdComplex nagataCompactification 𝒦X)).obj (op ((pull f).obj
        ((dualInto (stdComplex nagataCompactification 𝒦Y)).obj (op M.obj))))) ∧
      ((fNewShriekPlusCohNagata f hωS 𝒦X 𝒦Y).obj M).obj =
        (dualInto (stdComplex nagataCompactification 𝒦X)).obj (op ((pull f).obj
          ((dualInto (stdComplex nagataCompactification 𝒦Y)).obj (op M.obj))))

Stacks.Duality.NormalizedOnOpens.fNewShriekIsoRightAdjointNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 263. The attribute's comment: “part (6), first assertion”.

[Stacks, Tag 0AUE] part (6), first assertion. In Situation 0AU4, for a proper morphism f : X ⟶ Y of schemes of finite type over S and the dualizing complexes ω_X^•, ω_Y^• normalized relative to ω_S^•, f_new^! is isomorphic to the restriction to D^+_Coh(𝒪_Y) of the right adjoint a of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) ([Stacks, Tag 0A9E]).

def fNewShriekIsoRightAdjointNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    (plusCoh Y).ι ⋙ fNewShriekStd f (stdComplex nagataCompactification 𝒦X)
        (stdComplex nagataCompactification 𝒦Y) ≅
      ObjectProperty.ιOfLE plusCoh_le_qcoh ⋙ rightAdjointStd f

Stacks.Duality.NormalizedOnOpens.fNewShriekSheafHomIsoNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 279. The attribute's comment: “part (6), the isomorphism Rf_ RHom(K, f_new^! M) = RHom(Rf_ K, M)”.

[Stacks, Tag 0AUE] part (6), the duality isomorphism. In Situation 0AU4, for a proper morphism f : X ⟶ Y of schemes of finite type over S, K ∈ D^-_Coh(𝒪_X) and M ∈ D^+_Coh(𝒪_Y), there is a canonical isomorphism Rf_* R𝓗om(K, f_new^! M) ≅ R𝓗om(Rf_* K, M).

def fNewShriekSheafHomIsoNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (K : Std X) (hK : haveI := hp.source_noetherian; minusCoh X K)
    (M : (plusCoh Y).FullSubcategory) :
    (push f).obj (((sheafHom X).obj (op K)).obj
        ((fNewShriekStd f (stdComplex nagataCompactification 𝒦X)
          (stdComplex nagataCompactification 𝒦Y)).obj M.obj)) ≅
      ((sheafHom Y).obj (op ((push f).obj K))).obj M.obj

Stacks.Duality.NormalizedOnOpens.sheafHomDualizingIsoOfMinusCohNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 295. The attribute's comment: “part (6), the isomorphism Rf_ RHom(K, omega_X) = RHom(Rf_ K, omega_Y)”.

[Stacks, Tag 0AUE] part (6), the duality for the dualizing complexes. In Situation 0AU4, for a proper morphism f : X ⟶ Y of schemes of finite type over S and K ∈ D^-_Coh(𝒪_X), Rf_* R𝓗om(K, ω_X^•) ≅ R𝓗om(Rf_* K, ω_Y^•).

def sheafHomDualizingIsoOfMinusCohNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (K : Std X) (hK : haveI := hp.source_noetherian; minusCoh X K) :
    (push f).obj (((sheafHom X).obj (op K)).obj (stdComplex nagataCompactification 𝒦X)) ≅
      ((sheafHom Y).obj (op ((push f).obj K))).obj (stdComplex nagataCompactification 𝒦Y)

Stacks.Duality.NormalizedOnOpens.upperShriekStdIsoFNewShriekNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekNormalizedNagata.lean, line 310. The attribute's comment: “the closing remark, second half: f_new^! K = f^! K for K in D^+_Coh”.

[Stacks, Tag 0AUE], the closing remark, f_new^! = f^!. In Situation 0AU4, let f : X ⟶ Y be a separated morphism of schemes of finite type over S (for instance a morphism between schemes separated over S) and ω_X^•, ω_Y^• the dualizing complexes normalized relative to ω_S^•. For every compactification j of f, the upper shriek functor f^! of j ([Stacks, Tag 0A9Y]) satisfies f^! K ≅ f_new^! K, naturally in K ∈ D^+_Coh(𝒪_Y).

def upperShriekStdIsoFNewShriekNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsSeparated f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (j : CompactificationOf (Over.mk f)) :
    haveI := hq.source_noetherian
    UpperShriekDuality.upperShriekStd (ftsHomSelf (isShriekable_of_isSeparated hpe hp hq)) j ≅
      (plusCoh Y).ι ⋙ fNewShriekStd f (stdComplex nagataCompactification 𝒦X)
        (stdComplex nagataCompactification 𝒦Y)

Stacks.Duality.newShriekPseudofunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekPseudofunctorNagata.lean, line 337. The attribute's comment: “part (1)”.

In Situation [Stacks, Tag 0AU4], let ω_X^• be the dualizing complex normalized relative to ω_S^• of each scheme X of finite type over S. The functors f_new^! = D_X ∘ Lf^* ∘ D_Y : D^+_Coh(𝒪_Y) ⥤ D^+_Coh(𝒪_X) and the arrows (g ∘ f)_new^! ⟶ f_new^! ∘ g_new^! turn D^+_Coh into a pseudofunctor from the category of schemes of finite type over S to the 2-category of categories: X ↦ D^+_Coh(𝒪_X), f ↦ f_new^!, with mapComp the inverse of the comparison f_new^! ∘ g_new^! ⟶ (g ∘ f)_new^! given by the biduality η_Y ([Stacks, Tag 0A89]) and mapId the inverse of η_X : id ⟶ (id_X)_new^! (Stacks.Duality.NewShriekPseudofunctor.comp, Stacks.Duality.NewShriekPseudofunctor.unit, Stacks.Duality.newShriekPseudofunctor_map_obj_obj).

def newShriekPseudofunctor {S : Scheme.{u}} [IsNoetherian S]
    (ωS : quasiCoherentDerivedCategoryPlusOfModel S) (hωS : IsDualizingComplex ωS.obj.obj) :
    Pseudofunctor (LocallyDiscrete (SchemesOfFiniteTypeOver S)ᵒᵖ) Cat

Tag 0BV3, a remark

Tag 0BV3 in the Stacks Project.

Stacks.Duality.fNewShriekTwistIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/GlueingDualizingComplexes.lean, line 304. The attribute's comment: “RESTRICTED: the closed symmetric monoidal structure on the derived categories is an instance argument; the invertible twist with a chosen two-sided inverse, the identification of the twisted normalized complexes, and the compatibility of the derived pullback with the twist are hypotheses”.

Stacks Project, Tag 0BV3. f_new^! does not depend on the choice of the dualizing complex on the base.

Let f : X ⟶ Y be a morphism of schemes of finite type over the base of [Stacks, Tag 0AU4]. Replacing ω_S^• by a second dualizing complex replaces it by ω_S^• ⊗ ℒ for an invertible ℒ in D(𝒪_S) ([Stacks, Tag 0ATP]), and the complexes normalized relative to it by the twists ω_X^• ⊗ Lπ_X^*ℒ and ω_Y^• ⊗ Lπ_Y^*ℒ ([Stacks, Tag 0A9T]). This says that the two resulting functors f_new^! are canonically isomorphic — an isomorphism of functors, not merely a family of isomorphisms of objects.

The computation is the one sketched in the source. The twist passes through the target variable of R𝓗om by Stacks.Duality.relativeDualTwistTargetIso, is carried across Lf^* by tw, and cancels against the outer twist by Stacks.Duality.relativeDualTwistCancelIso; each of those is natural in the contravariant variable because it comes from Stacks.Duality.parametrizedRightAdjointUniq. The source's p^! does not appear: it is one route to the middle step and is not needed.

def fNewShriekTwistIso (f : X ⟶ Y)
    {ωX ωX' : DerivedCategory X.Modules} {ωY ωY' : DerivedCategory Y.Modules}
    {LX : DerivedCategory X.Modules} (hX : HasInverse LX)
    {LY : DerivedCategory Y.Modules} (hY : HasInverse LY)
    (eX : ωX' ≅ ωX ⊗ LX) (eY : ωY' ≅ ωY ⊗ LY)
    (tw : tensorRight LY ⋙ derivedPullback f ≅ derivedPullback f ⋙ tensorRight LX) :
    fNewShriek f ωX' ωY' ≅ fNewShriek f ωX ωY

Stacks.Duality.NormalizedOnOpens.fNewShriekIndependenceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedTwist.lean, line 916.

Stacks Project, Tag 0BV3. Let S be a Noetherian scheme with a dualizing complex ω_S^• and let f : X ⟶ Y be a morphism of schemes of finite type over S. Then the functor

f_new^! = D_X ∘ Lf^* ∘ D_Y : D^+_Coh(𝒪_Y) ⥤ D(𝒪_X)

of [Stacks, Tag 0AUE], formed with the dualizing complexes ω_X^•, ω_Y^• normalized relative to ω_S^•, does not depend on ω_S^• up to canonical isomorphism: for a second dualizing complex ω_S'^• on S, with ω_X'^•, ω_Y'^• normalized relative to it, the two functors are isomorphic. (It takes values in D^+_Coh(𝒪_X), Stacks.Duality.plusCoh_fNewShriek.)

The proof: ω_X'^• ≅ f_new^! ω_Y'^• (stdComplexIsoFNewShriek), and then Stacks.Duality.fNewShriekStdIsoOfIso, which uses that R𝓗om(ω_Y'^•, ω_Y^•) is invertible ([Stacks, Tag 0ATP]).

def fNewShriekIndependenceIso (hpe : f ≫ q = p)
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj)
    (hωS' : haveI := hp.base_noetherian; IsDualizingComplex ωS'.obj.obj)
    (𝒦X : NormalizedOnOpens (UpperShriek.ofCompactifications c) hp ωS)
    (𝒦Y : NormalizedOnOpens (UpperShriek.ofCompactifications c) hq ωS)
    (𝒦X' : NormalizedOnOpens (UpperShriek.ofCompactifications c) hp ωS')
    (𝒦Y' : NormalizedOnOpens (UpperShriek.ofCompactifications c) hq ωS') :
    (plusCoh Y).ι ⋙ fNewShriekStd f (stdComplex c 𝒦X') (stdComplex c 𝒦Y') ≅
      (plusCoh Y).ι ⋙ fNewShriekStd f (stdComplex c 𝒦X) (stdComplex c 𝒦Y)

Tag 0B6X, an example

Tag 0B6X in the Stacks Project.

Stacks.Duality.NormalizedOnOpens.sheafHomDualizingIsoNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekProperQCohNagata.lean, line 51.

[Stacks, Tag 0B6X], the second isomorphism. In Situation 0AU4, for a proper f : X ⟶ Y of schemes of finite type over S, the dualizing complexes ω_X^•, ω_Y^• normalized relative to ω_S^• and every L in D_QCoh(𝒪_X), Rf_* R𝓗om(L, ω_X^•) ≅ R𝓗om(Rf_* L, ω_Y^•): the sheafy trace map at ω_Y^• composed with a(ω_Y^•) ≅ ω_X^• ([Stacks, Tag 0AUD]).

def sheafHomDualizingIsoNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (L : Std X) (hL : qcoh X L) :
    (push f).obj (((sheafHom X).obj (op L)).obj (stdComplex nagataCompactification 𝒦X)) ≅
      ((sheafHom Y).obj (op ((push f).obj L))).obj (stdComplex nagataCompactification 𝒦Y)

Stacks.Duality.NormalizedOnOpens.traceNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedProperNagata.lean, line 107.

[Stacks, Tag 0B6X], the trace map. In Situation 0AU4, for a proper f : X ⟶ Y of schemes of finite type over S and the dualizing complexes ω_X^•, ω_Y^• normalized relative to ω_S^•, the canonical arrow Tr_f : Rf_* ω_X^• ⟶ ω_Y^•: the trace map of [Stacks, Section 0AWG] read through a(ω_Y^•) ≅ ω_X^• ([Stacks, Tag 0AUD]).

def traceNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    (quasiCoherentDerivedPushforward f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
        𝒦X.complex.obj ⟶ 𝒦Y.complex.obj

Stacks.Duality.NormalizedOnOpens.homEquivNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedProperNagata.lean, line 122.

[Stacks, Tag 0B6X], the first isomorphism. In Situation 0AU4, for a proper f : X ⟶ Y of schemes of finite type over S, the dualizing complexes ω_X^•, ω_Y^• normalized relative to ω_S^• and L in D_QCoh(𝒪_X), Hom_X(L, ω_X^•) = Hom_Y(Rf_* L, ω_Y^•); it sends u to Tr_f ∘ Rf_* u (homEquivNagata_apply).

def homEquivNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (L : quasiCoherentDerivedCategory X) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    (L ⟶ 𝒦X.complex.obj) ≃
      ((quasiCoherentDerivedPushforward f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj L ⟶ 𝒦Y.complex.obj)

Stacks.Duality.NormalizedOnOpens.homEquivNagata_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedProperNagata.lean, line 137.

[Stacks, Tag 0B6X], the first isomorphism is produced by the trace map: homEquivNagata sends u : L ⟶ ω_X^• to Tr_f ∘ Rf_* u.

theorem homEquivNagata_apply
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS)
    (L : quasiCoherentDerivedCategory X) (u : L ⟶ 𝒦X.complex.obj) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    homEquivNagata hpe hωS 𝒦X 𝒦Y L u =
      (quasiCoherentDerivedPushforward f
        (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).map u ≫
        traceNagata hpe hωS 𝒦X 𝒦Y

Tag 0AX4, a remark

Tag 0AX4 in the Stacks Project.

Stacks.Duality.NormalizedOnOpens.exists_finitePushforwardIso_trace_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RightAdjointPushforward/FiniteDualizingComplexNagata.lean, line 54.

[Stacks, Tag 0AX4] Let S be Noetherian with a dualizing complex ω_S^•, f : X ⟶ Y a finite morphism of schemes of finite type over S, and ω_X^•, ω_Y^• the dualizing complexes normalized relative to ω_S^•. Then R𝓗om(f_* 𝒪_X, ω_Y^•) lies in D⁺_QCoh(f_* 𝒪_X) and f_* ω_X^• ≅ R𝓗om(f_* 𝒪_X, ω_Y^•) there, by an isomorphism through which the trace map Tr_f : Rf_* ω_X^• ⟶ ω_Y^• of [Stacks, Tag 0B6X] is Rf_* ω_X^• = f_* ω_X^• = R𝓗om(f_* 𝒪_X, ω_Y^•) ⟶ ω_Y^•, evaluation at 1 (the counit of res ⊣ R𝓗om(f_* 𝒪_X, -)).

theorem exists_finitePushforwardIso_trace_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsFinite f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    DerivedCategoryB.derivedCategoryBPlus
        (SheafOfModules.isQuasicoherent (pushforwardRing f.base X.ringCatSheaf))
        (((structureSheafModelEquiv Y).inverse ⋙ derivedHomSheaf f ⋙
          (pushforwardRingModelEquiv f).functor).obj 𝒦Y.complex.obj.obj) ∧
      ∃ e : ((derivedQuasicoherentPushforwardOverRingEquivalence f).functor.obj
          𝒦X.complex.obj).obj ≅ ((structureSheafModelEquiv Y).inverse ⋙ derivedHomSheaf f ⋙
            (pushforwardRingModelEquiv f).functor).obj 𝒦Y.complex.obj.obj,
        (ObjectProperty.ι _).map (traceOfCompactifications nagataCompactification hpe hωS 𝒦X 𝒦Y) =
          (derivedPushforwardOverRingCompRestrictScalarsIso.{u} f).hom.app
              𝒦X.complex.obj.obj ≫
            (scalarRestriction f).mapDerivedCategory.map e.hom ≫
            (scalarRestrictionAdjunctionLS f).counit.app 𝒦Y.complex.obj.obj

Tag 0B6W, a remark

Tag 0B6W in the Stacks Project.

Stacks.Duality.NormalizedOnOpens.twistedInverseImageObjIsoPullbackTensorOfFlat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedFlatProperPullbackTensor.lean, line 63. The attribute's comment: “the second canonical isomorphism a(ω_Y^•) = Lf^* ω_Y^• ⊗ ω_{X/Y}^•”.

[Stacks, Remark 0B6W], the second canonical isomorphism. For a flat proper morphism f : X ⟶ Y of schemes of finite type over a Noetherian S, with a the right adjoint of Rf_*, there is a canonical isomorphism a(K) ≅ Lf^* K ⊗ᴸ a(𝒪_Y) for K ∈ D⁺_QCoh(𝒪_Y): through a = f^! (at the Nagata compactification of f) it is the inverse of μ_{f,K} ([Stacks, Tag 0B6U] (e)).

def twistedInverseImageObjIsoPullbackTensorOfFlat [IsProper f] [Flat f]
    (K : quasiCoherentDerivedCategoryPlusOfModel Y) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    (twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj K.obj ≅
      ((quasiCoherentDerivedTensor X).obj ((quasiCoherentDerivedPullback' f).obj K.obj)).obj
        ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
          (DerivedPushforward.derivedStructureSheaf Y))

Stacks.Duality.NormalizedOnOpens.isoPullbackTensorOfFlatNagata, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedFlatProperPullbackTensor.lean, line 99. The attribute's comment: “ω_X^• = a(ω_Y^•) = Lf^* ω_Y^• ⊗ ω_{X/Y}^• in D(O_X)”.

[Stacks, Remark 0B6W]. Let f : X ⟶ Y be a flat proper morphism of schemes of finite type over S, where S is Noetherian with a dualizing complex ω_S^•, and ω_X^•, ω_Y^• the dualizing complexes normalized relative to ω_S^•. With a the right adjoint of Rf_* and ω_{X/Y}^• = a(𝒪_Y) the relative dualizing complex, the canonical isomorphism ω_X^• ≅ a(ω_Y^•) ≅ Lf^* ω_Y^• ⊗ᴸ ω_{X/Y}^• in D(𝒪_X): the inverse of Stacks.Duality.twistedInverseImageObjIsoNagata ([Stacks, Tag 0AUD]) followed by twistedInverseImageObjIsoPullbackTensorOfFlat.

def isoPullbackTensorOfFlatNagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f] [Flat f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    𝒦X.complex.obj ≅ ((quasiCoherentDerivedTensor X).obj
        ((quasiCoherentDerivedPullback' f).obj 𝒦Y.complex.obj)).obj
          ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
            (DerivedPushforward.derivedStructureSheaf Y))

Stacks.Duality.NormalizedOnOpens.nonempty_iso_pullback_tensor_of_flat_nagata, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NormalizedCohenMacaulayNagata.lean, line 51.

[Stacks, Tag 0B6W] Let f : X ⟶ Y be a flat proper morphism of schemes of finite type over S, where S is Noetherian with a dualizing complex ω_S^•, and ω_X^•, ω_Y^• the dualizing complexes normalized relative to ω_S^•. With a the right adjoint of Rf_* and ω_{X/Y}^• = a(𝒪_Y) the relative dualizing complex, ω_X^• ≅ a(ω_Y^•) ≅ Lf^* ω_Y^• ⊗ᴸ ω_{X/Y}^• in D(𝒪_X).

theorem nonempty_iso_pullback_tensor_of_flat_nagata
    (hωS : haveI := hp.base_noetherian; IsDualizingComplex ωS.obj.obj) [IsProper f] [Flat f]
    (𝒦X : NormalizedOnOpens UpperShriek.nagata hp ωS)
    (𝒦Y : NormalizedOnOpens UpperShriek.nagata hq ωS) :
    haveI := hq.source_noetherian
    haveI := hp.source_noetherian
    Nonempty (𝒦X.complex.obj ≅ ((quasiCoherentDerivedTensor X).obj
        ((quasiCoherentDerivedPullback' f).obj 𝒦Y.complex.obj)).obj
          ((twistedInverseImage f (isQuasicoherent_homology_derivedPushforward_of_qcqs f)).obj
            (DerivedPushforward.derivedStructureSheaf Y)))

Sources

LeanStacks.Duality.DualizingBase · Stacks.Duality.UpperShriek.overlapCompareRestrict_cocycle · Stacks.Duality.Normalized.existsUnique_iso_nagata · Stacks.Duality.Normalized.exists_existsUnique_iso_nagata · Stacks.Duality.Normalized.exists_nagata · Stacks.Duality.isDualizingComplex_normalizedDualizingComplex · Stacks.Duality.existsUnique_iso_normalizedDualizingComplex · Stacks.Duality.existsUnique_iso_normalizedDualizingComplex_toNormalized

Section48.21 Dimension functions #

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

Tag 0AWL, a lemma

Tag 0AWL in the Stacks Project.

Stacks.Duality.isNormalizedDualizingComplex_derivedStalkOfComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/NormalizedAtClosedPointCharts.lean, line 78.

Stacks Project, Tag 0AWL (Lemma 48.21.1). Let S be a Noetherian scheme with a dualizing complex ω_S^•, let p : X ⟶ S be of finite type, and let ω_X^• be normalized relative to ω_S^•: every point has an affine open neighbourhood U with ω_X^•|_U ≅ (U ⟶ S)^! ω_S^• for a compactification of U over S. Let x ∈ X be a closed point and s = p x. If ω_{S,s}^• is a normalized dualizing complex over 𝒪_{S,s}, then ω_{X,x}^• is a normalized dualizing complex over 𝒪_{X,x}. The source also asks that s be closed; this is not needed.

theorem isNormalizedDualizingComplex_derivedStalkOfComplex
    {S X : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S] (p : X ⟶ S) [LocallyOfFiniteType p]
    (ωS : quasiCoherentDerivedCategory S) (hωS : IsDualizingComplex ωS.obj)
    (ωX : DerivedCategory X.Modules)
    (hωX : ∀ x : X, ∃ (U : X.Opens) (_ : IsAffine U.toScheme) (_ : x ∈ U)
      (j : CompactificationOf (Over.mk (ftsHomToBase (U.ι ≫ p)).left)),
      Nonempty ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj ωX ≅
        ((upperShriek (ftsHomToBase (U.ι ≫ p)) j).obj ωS).obj))
    (x : X) (hx : IsClosed ({x} : Set X))
    (hωSs : ∃ E : CochainComplex S.Modules ℤ, Nonempty (DerivedCategory.Q.obj E ≅ ωS.obj) ∧
      Dualizing.IsNormalizedDualizingComplex.{u, u} (derivedStalkOfComplex (p x) E)) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian p
    ∀ E : CochainComplex X.Modules ℤ, Nonempty (DerivedCategory.Q.obj E ≅ ωX) →
      Dualizing.IsNormalizedDualizingComplex.{u, u} (derivedStalkOfComplex x E)

Stacks.Duality.isNormalizedDualizingComplex_derivedStalkOfComplex_normalizedDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/NormalizedDualizingComplexNagataCharts.lean, line 98.

[Stacks, Tag 0AWL]. Let S be a Noetherian scheme with a dualizing complex ω_S^•, let X be of finite type over S and ω_X^• the dualizing complex normalized relative to ω_S^•. If x ∈ X is a closed point lying over a closed point s of S, then ω_{X,x}^• is a normalized dualizing complex over 𝒪_{X,x} provided that ω_{S,s}^• is a normalized dualizing complex over 𝒪_{S,s}. Stalks are the derived stalks of representatives; the closedness of s is not used.

theorem isNormalizedDualizingComplex_derivedStalkOfComplex_normalizedDualizingComplex
    (x : X) (hx : IsClosed ({x} : Set X))
    (hωSs : haveI := hp.base_noetherian
      ∃ E : CochainComplex S.Modules ℤ, Nonempty (DerivedCategory.Q.obj E ≅ ωS.obj.obj) ∧
      Dualizing.IsNormalizedDualizingComplex.{u, u}
        (@derivedStalkOfComplex S (p x) (HasDerivedCategory.standard _) E)) :
    haveI := hp.source_noetherian
    ∀ E : CochainComplex X.Modules ℤ,
      Nonempty (DerivedCategory.Q.obj E ≅ (normalizedDualizingComplex hp ωS hωS).complex.obj.obj) →
        Dualizing.IsNormalizedDualizingComplex.{u, u}
          (@derivedStalkOfComplex X x (HasDerivedCategory.standard _) E)

Tag 0AWM, a lemma

Tag 0AWM in the Stacks Project.

Stacks.Duality.associatedShiftFunction_sub_eq_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/NormalizedDualizingDimensionFunction.lean, line 204. The attribute's comment: “RESTRICTED: three inputs are explicit hypotheses. That the shift functions of the two dualizing complexes are dimension functions is the unproved half of Tag 0AWF, carried as dimension functions delta_S and delta_X together with hdS and hdX. That f carries closed points to closed points -- the source's reduction to a proper f, through Nagata compactification and Tag 0AUC -- is hClosedImage. The identity at a closed point over a closed point, Tag 0AWL, is hClosedPoint; 0AWL itself is proved, but the bridge from normalized stalks to a value of associatedShiftFunction is not. What is proved is the body of the lemma: universal catenarity of S from Tag 0AWF, then that the difference of the two functions is determined by its values at closed points, by Tag 02JW and Tag 02IB and Tag 02IL, and that the transcendence degree vanishes at a closed point, by Tag 01TF”.

Stacks Project, Tag 0AWM. Let S be a Noetherian scheme and let ω_S^• be a dualizing complex. Let f : X ⟶ S be of finite type and let ω_X^• be the dualizing complex normalized relative to ω_S^•. For all x ∈ X

δ_X(x) - δ_S(f x) = trdeg_{κ(f x)} κ(x)

where δ_S, resp. δ_X, is the dimension function of ω_S^•, resp. ω_X^•, of [Stacks, Tag 0AWF] — here Stacks.Duality.associatedShiftFunction.

Universal catenarity of S, which [Stacks, Tag 02JW] needs, is derived from hωS by [Stacks, Tag 0AWF] (Stacks.Duality.isUniversallyCatenary_of_isDualizingComplex). What is carried are the three things this repository does not have:

δS, δX with hδS, hδX — that the shift functions are dimension functions. This is the companion half of [Stacks, Tag 0AWF], which StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/AssociatedShiftFunction.lean states explicitly that it does not prove; only the universally-catenary half is proved.

hClosedImage — that f carries closed points to closed points, the source's reduction to a proper f.

hClosedPoint — the identity at a closed point over a closed point, [Stacks, Tag 0AWL], proved as Stacks.Duality.isNormalizedDualizingComplex_derivedStalkOfComplex_normalizedDualizingComplex; what is missing is the bridge from that statement about normalized stalks to a value of Stacks.Duality.associatedShiftFunction.

The relation between ω_X^• and ω_S^• enters only through hClosedPoint, which is exactly where the source uses it; the complex ω_X^• is otherwise a parameter.

theorem associatedShiftFunction_sub_eq_trdeg {X S : Scheme.{u}}
    [IsLocallyNoetherian S] [IsLocallyNoetherian X]
    [HasDerivedCategory S.Modules] [HasDerivedCategory X.Modules]
    (f : X ⟶ S) [LocallyOfFiniteType f]
    {ωS : DerivedCategory S.Modules} (hωS : IsDualizingComplex ωS)
    (ωX : DerivedCategory X.Modules)
    (δS : DimensionFunction S) (hδS : ∀ s : S, δS s = associatedShiftFunction ωS s)
    (δX : DimensionFunction X) (hδX : ∀ y : X, δX y = associatedShiftFunction ωX y)
    (hClosedImage : ∀ y : X, IsClosed ({y} : Set X) → IsClosed ({f y} : Set S))
    (hClosedPoint : ∀ y : X, IsClosed ({y} : Set X) → IsClosed ({f y} : Set S) →
      associatedShiftFunction ωX y = associatedShiftFunction ωS (f y))
    (x : X) :
    letI := (f.residueFieldMap x).hom.toAlgebra
    associatedShiftFunction ωX x - associatedShiftFunction ωS (f x) =
      (Cardinal.toNat (Algebra.trdeg (S.residueField (f x)) (X.residueField x)) : ℤ)

Stacks.Duality.associatedShiftFunction_sub_eq_trdeg_of_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/DimensionFunctionTrdegCharts.lean, line 117.

Stacks Project, Tag 0AWM (Lemma 48.21.2). Let S be a Noetherian scheme with a dualizing complex ω_S^•, let p : X ⟶ S be of finite type, and let ω_X^• be normalized relative to ω_S^•: every point has an affine open neighbourhood U with ω_X^•|_U ≅ (U ⟶ S)^! ω_S^• for a compactification of U over S. Then for every x ∈ X, δ_X(x) - δ_S(p x) = trdeg_{κ(p x)} κ(x), where δ_X, δ_S are the dimension functions of ω_X^•, ω_S^• ([Stacks, Tag 0AWF]).

theorem associatedShiftFunction_sub_eq_trdeg_of_upperShriek
    {S X : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S] (p : X ⟶ S) [LocallyOfFiniteType p]
    (ωS : quasiCoherentDerivedCategory S) (hωS : IsDualizingComplex ωS.obj)
    (ωX : DerivedCategory X.Modules)
    (hωX : ∀ x : X, ∃ (U : X.Opens) (_ : IsAffine U.toScheme) (_ : x ∈ U)
      (j : CompactificationOf (Over.mk (ftsHomToBase (U.ι ≫ p)).left)),
      Nonempty ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj ωX ≅
        ((upperShriek (ftsHomToBase (U.ι ≫ p)) j).obj ωS).obj))
    (x : X) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian p
    letI := (p.residueFieldMap x).hom.toAlgebra
    associatedShiftFunction ωX x - associatedShiftFunction ωS.obj (p x) =
      (Cardinal.toNat (Algebra.trdeg (S.residueField (p x)) (X.residueField x)) : ℤ)

Stacks.Duality.associatedShiftFunction_sub_eq_trdeg_normalizedDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/RelativeDualizing/NormalizedDualizingComplexNagataCharts.lean, line 120.

[Stacks, Tag 0AWM]. Let S be a Noetherian scheme with a dualizing complex ω_S^•, let p : X ⟶ S be of finite type and ω_X^• the dualizing complex normalized relative to ω_S^•. For all x ∈ X, δ_X(x) - δ_S(p x) = trdeg_{κ(p x)} κ(x), where δ_S, δ_X are the dimension functions of ω_S^•, ω_X^• ([Stacks, Tag 0AWF]).

theorem associatedShiftFunction_sub_eq_trdeg_normalizedDualizingComplex (x : X) :
    haveI := hp.base_noetherian
    haveI := hp.source_noetherian
    letI := (p.residueFieldMap x).hom.toAlgebra
    associatedShiftFunction (normalizedDualizingComplex hp ωS hωS).complex.obj.obj x -
        associatedShiftFunction ωS.obj.obj (p x) =
      (Cardinal.toNat (Algebra.trdeg (S.residueField (p x)) (X.residueField x)) : ℤ)

Tag 0BV5, a lemma

Tag 0BV5 in the Stacks Project.

Stacks.Duality.neg_fibreDim_le_of_nontrivial_stalk_homology_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFibreDimension.lean, line 240. The attribute's comment: “the implication H^i(f^! 𝒪_Y)_x ≠ 0 ⟹ -dim_x(X_y) ≤ i, in full and with no affineness on X or Y. f^! is Tag 0A9Y, Stacks.Duality.upperShriek, of the compactification j (Tag 0F41); 𝒪_Y is DerivedPushforward.derivedStructureSheaf; 'H^i(-)_x ≠ 0' is Nontrivial on the stalk at x of the i-th cohomology sheaf; and dim_x(X_y) is topologicalKrullDimAt on the scheme-theoretic fibre, named by the hypothesis hd identifying it with a natural number d, as Tag 0E9P also does. ONE hypothesis is carried, h0BV2: on an affine open U ∋ x inside the preimage of an affine open V of Y, the restriction of f^!𝒪_Y to U is the associated sheaf of the algebraic upper shriek, along a polynomial presentation of f.appLE V U, of Γ(Y, V) in degree zero. That is clause (b) of Tag 0BV2, the affine formula, which the repository's Tag 0BV2 (Stacks.Duality.restrictedUpperShriekIsoOfOpenSquare) explicitly does not claim because Tag 0AA1 (f^! = Lf^*[1] for A^1_V -> V) is absent here; it is carried in the same shape as Tag 0B6U (a) carries it. h0BV2 asserts only an isomorphism, with no degree bound in it: the bound is Tag 0E9P (Dualizing.upperShriekFunctor_neg_relativeDimensionAt_le_of_nontrivial_localizedHomology), transported to the chart by the two dictionaries proved in this file and in Stacks.Flatness.topologicalKrullDimAt_fiber_eq_relativeDimensionAt. Tag 0E9Q is not used here, and the source does not use it for 0BV5; it is present in the library at the ring level, under StacksFrontier/RingTheory/Dualizing/UpperShriek/, and is consumed by the flat refinement in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFibreDimensionFlat.lean. The upper bound i ≤ 0 and the tor-amplitude statement of Tag 0BV6, for f flat, are NOT claimed”.

Stacks Project, Tag 0BV5 (Lemma 48.21.1). In Situation 48.16.1, let f : X ⟶ Y be a morphism of FTS S and let x ∈ X with image y ∈ Y. Then

H^i(f^!𝒪_Y)_x ≠ 0 ⟹ -dim_x(X_y) ≤ i,

the local dimension dim_x(X_y) of the scheme-theoretic fibre being named by the hypothesis hd that identifies it with a natural number d.

The affine identification of f^!𝒪_Y of Remark [Stacks, Tag 0BV2] is the carried hypothesis h0BV2; it names an isomorphism on an affine chart through x and asserts nothing about any degree. The bound itself is [Stacks, Tag 0E9P] for the algebraic upper shriek, moved to the chart by the stalk dictionary Stacks.Duality.nontrivial_stalk_homology_iff_nontrivial_localizedHomology and the fibre-dimension dictionary Stacks.Flatness.topologicalKrullDimAt_fiber_eq_relativeDimensionAt, both proved.

theorem neg_fibreDim_le_of_nontrivial_stalk_homology_upperShriek (x : X.left)
    (h0BV2 : ∃ (U : X.left.Opens) (hU : IsAffineOpen U) (V : Y.left.Opens)
      (_hV : IsAffineOpen V) (hUV : U ≤ f.left ⁻¹ᵁ V), x ∈ U ∧
      ∃ p : Dualizing.PolynomialPresentation (f.left.appLE V U hUV).hom,
        Nonempty ((Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj
            (((upperShriek f j).obj (derivedStructureSheaf Y.left)).obj) ≅
          (tilde.functor Γ(X.left, U) ⋙
            Scheme.Modules.restrictFunctor hU.isoSpec.hom).mapDerivedCategory.obj
              (p.upperShriekFunctor.{u, u}.obj (structureModel (Y := Y) V))))
    (d : ℕ)
    (hd : topologicalKrullDimAt (f.left.fiber (f.left x)) (f.left.asFiber x) =
      (d : WithBot ℕ∞))
    (i : ℤ)
    (hi : Nontrivial (((DerivedCategory.homologyFunctor X.left.Modules i).obj
      (((upperShriek f j).obj
        (derivedStructureSheaf Y.left)).obj)).presheaf.stalk x)) :
    -(d : ℤ) ≤ i

Stacks.Duality.neg_fibreDim_le_of_nontrivial_stalk_homology_upperShriek_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFibreDimensionCharts.lean, line 96.

Stacks Project, Tag 0BV5 (Lemma 48.21.3). In Situation 48.16.1 let f : X ⟶ Y be a morphism of FTS S and let x ∈ X with image y ∈ Y. Then

H^i(f^!𝒪_Y)_x ≠ 0 ⟹ -dim_x(X_y) ≤ i,

for every compactification j defining f^!; the local dimension dim_x(X_y) of the fibre is named by the hypothesis hd identifying it with a natural number d. The chart description of f^!𝒪_Y is Stacks.Duality.upperShriekStructureSheafCharts, and on a chart the bound is [Stacks, Tag 0E9P].

theorem neg_fibreDim_le_of_nontrivial_stalk_homology_upperShriek_unconditional
    (x : X.left) (d : ℕ)
    (hd : topologicalKrullDimAt (f.left.fiber (f.left x)) (f.left.asFiber x) =
      (d : WithBot ℕ∞))
    (i : ℤ)
    (hi : Nontrivial (((DerivedCategory.homologyFunctor X.left.Modules i).obj
      (((upperShriek f j).obj
        (derivedStructureSheaf Y.left)).obj)).presheaf.stalk x)) :
    -(d : ℤ) ≤ i

Tag 0BV6, a lemma

Tag 0BV6 in the Stacks Project.

Stacks.Duality.fibreDim_bounds_of_nontrivial_stalk_homology_upperShriek_of_flat_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFibreDimensionFlatCharts.lean, line 69. The attribute's comment: “first assertion: the bounds -dim_x(X_y) <= i <= 0 on nonzero stalks”.

Stacks Project, Tag 0BV6 (Lemma 48.21.4), the first assertion. In Situation 48.16.1 let f : X ⟶ Y be a flat morphism of FTS S and let x ∈ X with image y ∈ Y. Then

H^i(f^!𝒪_Y)_x ≠ 0 ⟹ -dim_x(X_y) ≤ i ≤ 0,

for every compactification j defining f^!, the local dimension dim_x(X_y) being named by hd. On a chart of Stacks.Duality.upperShriekStructureSheafCharts this is the ring-level [Stacks, Tag 0E9Q].

theorem fibreDim_bounds_of_nontrivial_stalk_homology_upperShriek_of_flat_unconditional
    [Flat f.left] (x : X.left) (d : ℕ)
    (hd : topologicalKrullDimAt (f.left.fiber (f.left x)) (f.left.asFiber x) =
      (d : WithBot ℕ∞))
    (i : ℤ)
    (hi : Nontrivial (((DerivedCategory.homologyFunctor X.left.Modules i).obj
      (((upperShriek f j).obj
        (derivedStructureSheaf Y.left)).obj)).presheaf.stalk x)) :
    -(d : ℤ) ≤ i ∧ i ≤ 0

Stacks.Duality.hasTorAmplitude_derivedScalarRestriction_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFibreDimensionFlatCharts.lean, line 110. The attribute's comment: “second assertion: Tor amplitude in [-d, 0] over f^{-1}O_Y when all fibres have dimension at most d”.

Stacks Project, Tag 0BV6 (Lemma 48.21.4), the second assertion. In Situation 48.16.1 let f : X ⟶ Y be a flat morphism of FTS S all of whose fibres have dimension at most d. Then f^!𝒪_Y has Tor amplitude in [-d, 0] as an object of D(X, f^{-1}𝒪_Y), for every compactification j defining f^!.

By [Stacks, Tag 09U9] this is a statement about the derived stalks read over the local rings of Y; on a chart of Stacks.Duality.upperShriekStructureSheafCharts it is the Tor amplitude clause of the ring-level [Stacks, Tag 0E9Q].

theorem hasTorAmplitude_derivedScalarRestriction_upperShriek [Flat f.left] (d : ℕ)
    (hd : ∀ y : Y.left, topologicalKrullDim (f.left.fiber y) ≤ (d : WithBot ℕ∞)) :
    Stacks.Cohomology.TorAmplitude.HasTorAmplitude
      (RingedSpace.inverseImage Y.left.toRingedSpace f.left.base)
      ((Scheme.Hom.derivedScalarRestriction f.left).obj (relativeDualizingComplexObj f j))
      (-(d : ℤ)) 0

Declarations registered for the tag:

Stacks.Duality.fibreDim_bounds_of_nontrivial_stalk_homology_upperShriek_of_flat, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekFibreDimensionFlat.lean, line 287 (StacksFrontier): “THE FIRST ASSERTION, both halves, BUT UNDER AN ASSUMED PREREQUISITE TAG, and NOT the tor-amplitude assertion. Proved: for f flat and x over y, if the stalk at x of H^i(f^! O_Y) is nontrivial then -dim_x(X_y) <= i <= 0, with no affineness on X or Y and flatness an instance. ASSUMED: h0BV2, the affine-chart description of f^! O_Y, which is clause (b) of Stacks 0BV2 and rests on Stacks 0AA1 (f^! = Lf^*[1] for A^1_V -> V). Tag 0AA1 is not proved in this library; this result becomes unconditional by composing with a proof of it. Note the same hypothesis is carried in the identical shape by the statements of Tags 0BV5 and 0B6U and by Duality/UpperShriekBounded.lean, so discharging 0AA1 unconditionalises those too. NOT PROVED: f^! O_Y has tor-amplitude in [-d,0] in D(X, f-inverse O_Y). Only its O_Y instance is proved, the vanishing of the cohomology SHEAVES outside [-d,0], as isZero_homology_upperShriek_derivedStructureSheaf_of_notMem_Icc below; the ring-level version at base is itself conditional on Tag 0BZV and the chart-to-sheaf assembly is absent.”.

Tag 0E9V, a lemma

Tag 0E9V in the Stacks Project.

Stacks.Duality.propertySkModule_modulesStalk_homology_upperShriek_of_residueTrdeg_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekTranscendenceDegreeCharts.lean, line 318. The attribute's comment: “the (S_2) property of the stalk H^{-r}(f^! O_Y)_x as an O_{X,x}-module”.

Stacks Project, Tag 0E9V (Lemma 48.21.5), the (S₂) clause. Under the hypotheses of the tag, the stalk H^{-r}(f^!𝒪_Y)_x satisfies (S₂) as an 𝒪_{X,x}-module, for every compactification j defining f^!. On a chart the stalk is the localization of H^{-r}(ω^•_{A/R}) at the prime of x, which is (S₂) by the ring-level [Stacks, Tag 0E9R].

theorem propertySkModule_modulesStalk_homology_upperShriek_of_residueTrdeg_le
    (x : X.left) (r : ℕ)
    (hCM : IsCohenMacaulayLocalRing (Y.left.presheaf.stalk (f.left.base x)))
    (htrdeg : ∀ ξ : X.left, closure {ξ} ∈ irreducibleComponents X.left → x ∈ closure {ξ} →
      Stacks.Chow.residueTrdeg f.left ξ ≤ (r : Cardinal)) :
    letI := module_finite_modulesStalk_homology_upperShriek f j x (-(r : ℤ))
    PropertySkModule (X.left.presheaf.stalk x) ((modulesStalkFunctor x).obj
      ((DerivedCategory.homologyFunctor X.left.Modules (-(r : ℤ))).obj
        (((upperShriek f j).obj (derivedStructureSheaf Y.left)).obj))) 2

Stacks.Duality.neg_le_of_nontrivial_stalk_homology_upperShriek_of_residueTrdeg_le_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekTranscendenceDegreeVanishing.lean, line 53. The attribute's comment: “the vanishing: H^i(f^! O_Y)_x nonzero implies -r <= i”.

Stacks Project, Tag 0E9V (Lemma 48.21.4), the vanishing. If 𝒪_{Y, f x} is Cohen–Macaulay and the residue transcendence degree of f is at most r at every generic point of a component of X through x, then H^i(f^!𝒪_Y)_x ≠ 0 implies -r ≤ i, for every j.

theorem neg_le_of_nontrivial_stalk_homology_upperShriek_of_residueTrdeg_le_unconditional
    (x : X.left) (r : ℕ)
    (hCM : IsCohenMacaulayLocalRing (Y.left.presheaf.stalk (f.left.base x)))
    (htrdeg : ∀ ξ : X.left, closure {ξ} ∈ irreducibleComponents X.left → x ∈ closure {ξ} →
      Stacks.Chow.residueTrdeg f.left ξ ≤ (r : Cardinal))
    (i : ℤ)
    (hi : Nontrivial (((DerivedCategory.homologyFunctor X.left.Modules i).obj
      (((upperShriek f j).obj
        (derivedStructureSheaf Y.left)).obj)).presheaf.stalk x)) :
    -(r : ℤ) ≤ i

Declarations registered for the tag:

Stacks.Duality.neg_le_of_nontrivial_stalk_homology_upperShriek_of_residueTrdeg_le, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekTranscendenceDegree.lean, line 429 (StacksFrontier): “THE VANISHING BOUND ONLY; the tag is NOT proved. Proved: in the stated situation, if the stalk at x of H^i(f^! O_Y) is nontrivial then -r <= i. NOT PROVED: the second conclusion, that the stalk H^{-r}(f^! O_Y)_x is (S_2) as an O_{X,x}-module -- nothing about (S_2) is stated in this file, and the module-level stalk dictionary it needs does not exist in the library (only the abelian-group version does). TWO HYPOTHESES ARE CARRIED, neither dischargeable here. h0BV2 is clause (b) of Stacks 0BV2, the affine formula for f^! O_Y, which needs Stacks 0AA1 (f^! = Lf^*[1] for A^1_V -> V), absent from this repository; the library's Stacks 0BV2 explicitly declines clause (b). NOTE IT IS CARRIED IN A STRENGTHENED FORM relative to the library's Stacks 0BV5 and 0B6U, which take one chart: here it must be COFINAL in neighbourhoods of x, which is what permits the chart shrinking. h0E9R is clause (1) of Stacks 0E9R at the SHARP bound r, whereas the library's subsingleton_localizedModule_homology_relativeDualizingComplex gives only the crude bound (the number of variables); the sharp bound needs the dimension formula of Stacks 0BAE via the duality formula of Stacks 0E9L localized at a maximal ideal. Stacks 0E9L itself is proved in general as Dualizing.PolynomialPresentation.nonempty_upperShriekFunctor_natIso_dualizingDerivedHom; the passage to the localization is the base change of Stacks 0BZV, conditional in this library.”.

Tag 0BV7, a lemma

Tag 0BV7 in the Stacks Project.

Stacks.Duality.exists_isCoherent_isFlatOver_iso_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekQuasiFinite.lean, line 141.

Stacks Project, Tag 0BV7 (Lemma 48.21.6). In Situation 48.16.1 let f : X ⟶ Y be a morphism of FTS S. If f is flat and quasi-finite, then f^!𝒪_Y = ω_{X/Y}[0] for some coherent 𝒪_X-module ω_{X/Y} flat over Y, for every compactification j defining f^!.

The fibres are discrete, so by [Stacks, Tag 0BV6] f^!𝒪_Y is concentrated in degree 0 and has Tor amplitude [0, 0] over Y; its cohomology sheaves are coherent by the chart models.

theorem exists_isCoherent_isFlatOver_iso_single [Flat f.left] [LocallyQuasiFinite f.left] :
    ∃ ω : X.left.Modules, _root_.SheafOfModules.IsCoherent ω ∧
      IsFlatOver f.left.toLRSHom.toShHom ω ∧
      Nonempty (relativeDualizingComplexObj f j ≅
        (DerivedCategory.singleFunctor X.left.Modules 0).obj ω)

Tag 0BV8, a lemma

Tag 0BV8 in the Stacks Project.

Stacks.Duality.exists_isCoherent_isFlatOver_iso_shift_upperShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/UpperShriekChartConsequences.lean, line 70.

Let S be Noetherian and f : X ⟶ Y a Cohen–Macaulay morphism of FTS S. Then f^!𝒪_Y = ω_{X/Y}[d] for a coherent 𝒪_X-module ω_{X/Y} flat over Y, where d is the locally constant relative dimension of X over Y: on the open where the relative dimension is d, f^!𝒪_Y is ω_{X/Y} placed in degree -d.

theorem exists_isCoherent_isFlatOver_iso_shift_upperShriek
    (hCM : f.left.IsCohenMacaulay (isLocallyNoetherian_fiber_left f)) :
    letI h := (isCohenMacaulay_iff_flat_and_fibers f.left (isLocallyNoetherian_fiber_left f)).mp hCM
    letI : Flat f.left := h.1
    letI := locallyOfFinitePresentation_left f
    ∃ ω : X.left.Modules, ω.IsCoherent ∧ IsFlatOver f.left.toLRSHom.toShHom ω ∧
      ∀ d : ℕ, Nonempty ((Scheme.Modules.restrictFunctor (relativeDimensionOpen f.left h.2 d).ι
          ).mapDerivedCategory.obj (relativeDualizingComplexObj f j) ≅
        ((DerivedCategory.singleFunctor _ 0).obj
          ((Scheme.Modules.restrictFunctor (relativeDimensionOpen f.left h.2 d).ι).obj ω))⟦
            (d : ℤ)⟧)

Tag 0BV9, a remark

Tag 0BV9 in the Stacks Project.

Stacks.Duality.NormalizedOnOpens.newShriekStructureSheaf_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/TwistedInverseImageFTS/NewShriekRelativeDualizingComplex.lean, line 98. The attribute's comment: “Lemmas 0BV5, 0BV6 (both assertions), 0BV7 and 0BV8 with f^! replaced by f_new^! = D_X o Lf^* o D_Y, for every morphism of schemes of finite type over a Noetherian base with a dualizing complex, separated or not”.

Stacks Project, Tag 0BV9 (Remark 48.21.7). Let S be a Noetherian scheme endowed with a dualizing complex ω_S^•, and let f : X ⟶ Y be a morphism of schemes of finite type over S, not necessarily separated. With ω_X^•, ω_Y^• normalized relative to ω_S^• and f_new^! 𝒪_Y = D_X(Lf^* D_Y(𝒪_Y)), Lemmas 0BV5, 0BV6, 0BV7 and 0BV8 hold with f^! replaced by f_new^!:

(0BV5) for x ∈ X with image y, H^i(f_new^! 𝒪_Y)_x ≠ 0 ⟹ -dim_x(X_y) ≤ i;

(0BV6) if f is flat, then H^i(f_new^! 𝒪_Y)_x ≠ 0 ⟹ -dim_x(X_y) ≤ i ≤ 0, and if all fibres of f have dimension ≤ d, then f_new^! 𝒪_Y has Tor amplitude in [-d, 0] as an object of D(X, f^{-1}𝒪_Y);

(0BV7) if f is flat and quasi-finite, then f_new^! 𝒪_Y = ω_{X/Y}[0] for some coherent 𝒪_X-module ω_{X/Y} flat over Y;

(0BV8) if f is Cohen–Macaulay, then f_new^! 𝒪_Y = ω_{X/Y}[d] for some coherent 𝒪_X-module ω_{X/Y} flat over Y, where d is the locally constant relative dimension of X over Y: on the open and closed locus where the relative dimension is d, f_new^! 𝒪_Y is ω_{X/Y} placed in degree -d.

The local dimension dim_x(X_y) is named by a natural number d.

theorem newShriekStructureSheaf_spec :
    -- Lemma 0BV5
    (∀ (x : X) (d : ℕ), topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞) →
      ∀ i : ℤ, Nontrivial (((@DerivedCategory.homologyFunctor X.Modules _ _
        (PerfectApproximation.standardModel X) i).obj
          (newShriekStructureSheaf c f 𝒦X 𝒦Y)).presheaf.stalk x) → -(d : ℤ) ≤ i) ∧
    -- Lemma 0BV6
    (Flat f →
      (∀ (x : X) (d : ℕ),
        topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = (d : WithBot ℕ∞) →
        ∀ i : ℤ, Nontrivial (((@DerivedCategory.homologyFunctor X.Modules _ _
          (PerfectApproximation.standardModel X) i).obj
            (newShriekStructureSheaf c f 𝒦X 𝒦Y)).presheaf.stalk x) → -(d : ℤ) ≤ i ∧ i ≤ 0) ∧
      ∀ d : ℕ, (∀ y : Y, topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞)) →
        letI := HasDerivedCategory.standard (StrictlyPerfect.OXMod.{u, u} X.toRingedSpace)
        letI := HasDerivedCategory.standard
          (StrictlyPerfect.OXMod.{u, u} (RingedSpace.inverseImage Y.toRingedSpace f.base))
        Stacks.Cohomology.TorAmplitude.HasTorAmplitude
          (RingedSpace.inverseImage Y.toRingedSpace f.base)
          ((Scheme.Hom.derivedScalarRestriction f).obj (newShriekStructureSheaf c f 𝒦X 𝒦Y))
          (-(d : ℤ)) 0) ∧
    -- Lemma 0BV7
    (Flat f → LocallyQuasiFinite f →
      letI := PerfectApproximation.standardModel X
      ∃ ω : X.Modules, ω.IsCoherent ∧ IsFlatOver f.toLRSHom.toShHom ω ∧
        Nonempty ((newShriekStructureSheaf c f 𝒦X 𝒦Y : DerivedCategory X.Modules) ≅
          (DerivedCategory.singleFunctor X.Modules 0).obj ω)) ∧
    -- Lemma 0BV8
    (∀ hCM : f.IsCohenMacaulay
        (isLocallyNoetherian_fiber_of_isFiniteTypeOverNoetherian (hp := hp) hpe),
      letI h := (isCohenMacaulay_iff_flat_and_fibers f
        (isLocallyNoetherian_fiber_of_isFiniteTypeOverNoetherian (hp := hp) hpe)).mp hCM
      letI : Flat f := h.1
      letI := locallyOfFinitePresentation_of_isFiniteTypeOverNoetherian (hp := hp) (hq := hq) hpe
      letI := PerfectApproximation.standardModel X
      ∃ ω : X.Modules, ω.IsCoherent ∧ IsFlatOver f.toLRSHom.toShHom ω ∧
        ∀ d : ℕ,
          letI := PerfectApproximation.standardModel (relativeDimensionOpen f h.2 d).toScheme
          Nonempty ((Scheme.Modules.restrictFunctor (relativeDimensionOpen f h.2 d).ι
              ).mapDerivedCategory.obj
                (newShriekStructureSheaf c f 𝒦X 𝒦Y : DerivedCategory X.Modules) ≅
            ((DerivedCategory.singleFunctor _ 0).obj
              ((Scheme.Modules.restrictFunctor (relativeDimensionOpen f h.2 d).ι).obj ω))⟦
                (d : ℤ)⟧))

Sources

LeanStacks.Duality.isNormalizedDualizingComplex_derivedStalkOfComplex · Stacks.Duality.isNormalizedDualizingComplex_derivedStalkOfComplex_normalizedDualizingComplex · Stacks.Duality.associatedShiftFunction_sub_eq_trdeg · Stacks.Duality.associatedShiftFunction_sub_eq_trdeg_of_upperShriek · Stacks.Duality.associatedShiftFunction_sub_eq_trdeg_normalizedDualizingComplex · Stacks.Duality.neg_fibreDim_le_of_nontrivial_stalk_homology_upperShriek · Stacks.Duality.neg_fibreDim_le_of_nontrivial_stalk_homology_upperShriek_unconditional · Stacks.Duality.fibreDim_bounds_of_nontrivial_stalk_homology_upperShriek_of_flat_unconditional

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

48.12 Right adjoint of… to 48.21 Dimension functions

Section48.12 Right adjoint of pushforward for proper flat morphisms#

Tag 0E4I, a lemma

Tag 0E4J, a lemma

Tag 0E4K, a lemma

Tag 0AAB, a lemma

Tag 0B6S, a remark

Tag 0G81, a remark

Tag 0E4L, a lemma

Tag 0E2P, a lemma

Tag 0E2Q, an equation

Tag 0E2R, an equation

Tag 0BRU, a remark

Sources

Section48.13 Right adjoint of pushforward for perfect proper morphisms#

Tag 0A9R, a lemma

Tag 0AAA, a lemma

Tag 0A9U, a lemma

Tag 0BZG, a lemma

Sources

Section48.14 Right adjoint of pushforward for effective Cartier divisors#

Tag 0B4B, a lemma

Tag 0B4C, an equation

Tag 0AA4, a lemma

Sources

Section48.15 Right adjoint of pushforward in examples#

Tag 0A9W, a lemma

Tag 0AAC, an example

Tag 0BQW, a lemma

Tag 0BQX, an equation

Tag 0BQY, a lemma

Tag 0BQZ, a lemma

Tag 0BR0, a lemma

Tag 0BRT, a lemma

Sources

Section48.16 Upper shriek functors#

Tag 0A9Y, the section

Tag 0F42, a situation

Tag 0AA0, a lemma

Tag 0ATX, a lemma

Tag 0ATY, a lemma

Tag 0B6T, a lemma

Sources

Section48.17 Properties of upper shriek functors#

Tag 0AU0, a lemma

Tag 0G4J, a lemma

Tag 0AA1, a lemma

Tag 0AA2, a lemma

Tag 0BV2, a remark

Tag 0AU1, a lemma

Tag 0AA3, a lemma

Tag 0AU2, a lemma

Tag 0B6U, a lemma

Tag 0E9T, a lemma

Tag 0B6V, a lemma

Sources

Section48.18 Base change for upper shriek#

Tag 0E9U, a lemma

Tag 0FWI, a lemma

Tag 0BZY, a lemma

Tag 0BZZ, a lemma

Sources

Section48.19 A duality theory#

Tag 0AU3, the section

Sources

Section48.20 Glueing dualizing complexes#

Tag 0AU4, a situation

Tag 0AU6, an item

Tag 0AU7, a lemma

Tag 0AU8, a lemma

Tag 0AU9, a lemma

Tag 0AUA, a definition

Tag 0AUB, a lemma

Tag 0AUC, a lemma

Tag 0AUD, a lemma

Tag 0AUE, a lemma

Tag 0BV3, a remark

Tag 0B6X, an example

Tag 0AX4, a remark

Tag 0B6W, a remark

Section48.12 Right adjoint of pushforward for proper flat morphisms #

Section48.13 Right adjoint of pushforward for perfect proper morphisms #

Section48.14 Right adjoint of pushforward for effective Cartier divisors #

Section48.15 Right adjoint of pushforward in examples #

Section48.16 Upper shriek functors #

Section48.17 Properties of upper shriek functors #

Section48.18 Base change for upper shriek #

Section48.19 A duality theory #

Section48.20 Glueing dualizing complexes #

Section48.21 Dimension functions #