86 Duality for Spaces

Chapter 86 of the Stacks Project, Duality for Spaces, Tag 0E4V: the 9 sections of its 10 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 36 tags are carried by 61 declarations of the repository (all in StacksFrontier) and 3 registered declarations.

Section86.2 Dualizing complexes on algebraic spaces #

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

Tag 0E4Y, a lemma

Tag 0E4Y in the Stacks Project.

AlgebraicGeometry.Space.forall_isDualizingOnChart_iff_exists_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualizingComplexEtaleCharts.lean, line 295.

Stacks Project, Tag 0E4Y. Let X be a locally Noetherian algebraic space over S and let K be an object of D_QCoh(𝒪_X). Then the restriction K|_U is a dualizing complex on U, in the sense of Stacks 0E4X, for every étale morphism h_U ⟶ X with U a scheme if and only if it is one for some surjective such morphism.

The ascent from U to U ×_X V and the descent from there to V are Stacks 0E4N, applied to the dualizing complex ω_U with K|_U = ε^*ω_U and to the complex ω_V with K|_V = ε^*ω_V that Stacks 071Q provides; the two pullbacks to U ×_X V agree because ε^* commutes with étale pullback and is fully faithful on D_QCoh.

theorem forall_isDualizingOnChart_iff_exists_surjective
    (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (K : QuasicoherentDerivedCategory.{u, u} B S hS X hX) :
    (∀ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
        (hφ : (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) φ),
        IsDualizingRestriction B S hS X hX hN K.obj U φ hφ) ↔
      ∃ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X)
        (hφ : (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) φ),
        (MorphismProperty.presheaf (MorphismProperty.inverseImage
          (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS))) φ ∧
          IsDualizingRestriction B S hS X hX hN K.obj U φ hφ

Tag 0E4Z, a definition

Tag 0E4Z in the Stacks Project.

AlgebraicGeometry.Space.IsDualizingComplex, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualizingComplexEtaleCharts.lean, line 331. The attribute's comment: “the every-chart condition of 0E4Y; the restrictions of K to the etale scheme charts of X are the family L”.

Stacks Project, Tag 0E4Z. An object of D_QCoh(𝒪_X) on a locally Noetherian algebraic space X over S is a dualizing complex when its restriction to every étale scheme chart of X is a dualizing complex on that chart, in the sense of Stacks 0A87.

This is the chart-family formulation, written before the restriction of an object of D(𝒪_X) to a chart was available: the object is presented by a family L of complexes on the Zariski sites of the charts, quasicoherent and pullback_compat are what membership in D_QCoh(𝒪_X) says about the family of its restrictions, and isDualizingOnChart is the every-chart condition of Stacks 0E4Y. The notion phrased on an object of D_QCoh(𝒪_X) itself is AlgebraicGeometry.Space.IsDualizingComplexOnSpace.

structure IsDualizingComplex (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (L : ∀ (U : BigFppfOver B S hS) (φ : yoneda.obj U ⟶ X),
      (MorphismProperty.presheaf (MorphismProperty.inverseImage
        (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) φ →
      DerivedCategory ((BigFppfOver.toScheme B S hS).obj U).Modules) : Prop

AlgebraicGeometry.Space.IsDualizingComplexOnSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualizingComplexEtaleCharts.lean, line 461.

Stacks Project, Tag 0E4Z. An object K of D_QCoh(𝒪_X) on a locally Noetherian algebraic space X over S is a dualizing complex when it satisfies the equivalent conditions of Stacks 0E4Y: its restriction K|_U to every étale morphism h_U ⟶ X with U a scheme is a dualizing complex on U in the sense of Stacks 0E4X, that is K|_U = ε^*ω_U for a dualizing complex ω_U on U (AlgebraicGeometry.Space.IsDualizingRestriction). By AlgebraicGeometry.Space.forall_isDualizingOnChart_iff_exists_surjective it is enough to ask this for one surjective such morphism.

def IsDualizingComplexOnSpace (hX : IsAlgebraicSpace B S hS X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (K : QuasicoherentDerivedCategory.{u, u} B S hS X hX) : Prop

Tag 0E50, a lemma

Tag 0E50 in the Stacks Project.

AlgebraicGeometry.AffineEtaleDuality.isIso_comparison_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleDuality/Derived.lean, line 366.

Stacks 0E50. Let A be a Noetherian ring and X = Spec A, let 𝒪_étale be the structure sheaf of the small étale site of X, and let ε : (X_étale, 𝒪_étale) ⟶ (X, 𝒪_X) be the comparison morphism. For K, L ∈ D(A) with K ∈ D_Coh(A) and L of finite injective dimension, the canonical map ε^* (R Hom_A(K, L))~ ⟶ R SheafHom_{𝒪_étale}(ε^* K̃, ε^* L̃) is an isomorphism in D(𝒪_étale).

The source is lifted to the module universe of the derived internal Hom, which on the small étale site lands one universe up (AlgebraicGeometry.SmallEtale.derivedSheafHomBifunctor).

theorem isIso_comparison_app [IsNoetherianRing A] (K L : DerivedCategory (ModuleCat.{u} A))
    (hK : ∀ n : ℤ, Module.Finite A ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj K))
    (hL : StacksDraft.InjectiveDimension.HasFiniteInjectiveDimension L) :
    IsIso ((comparison A B hX).app (op K, L))

Tag 0E51, a lemma

Tag 0E51 in the Stacks Project.

AlgebraicGeometry.Space.dualizingComplex_duality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DerivedDuality/SpaceDuality.lean, line 240.

Stacks 0E51. Let X be a locally Noetherian algebraic space and K a dualizing complex on X (Stacks 0E4Z). Then

K is an object of D_Coh(𝒪_X);

D = R𝓗om_{𝒪_X}(-, K) carries D_Coh(𝒪_X) to itself and induces an anti-equivalence D : D_Coh(𝒪_X)ᵒᵖ ≌ D_Coh(𝒪_X), which comes equipped with the canonical isomorphism id → D ∘ D whose components are the biduality morphisms L ⟶ R𝓗om(R𝓗om(L, K), K);

if X is quasi-compact, D carries D^+_Coh(𝒪_X) to D^-_Coh(𝒪_X) and D^-_Coh(𝒪_X) to D^+_Coh(𝒪_X) (and induces an anti-equivalence between them), and induces an anti-equivalence D^b_Coh(𝒪_X)ᵒᵖ ≌ D^b_Coh(𝒪_X).

theorem dualizingComplex_duality (K : QuasicoherentDerivedCategory.{u, u} B S hS F hF)
    (hK : IsDualizingComplexOnSpace B S hS F hF hN K) :
    coherentDerived B S hS F hF K.obj ∧
    ∃ hD : ∀ L, coherentDerived B S hS F hF L →
        coherentDerived B S hS F hF ((dualFunctor B S hS F hF K.obj).obj (op L)),
      (∃ e : (coherentDerived B S hS F hF).FullSubcategoryᵒᵖ ≌
          (coherentDerived B S hS F hF).FullSubcategory,
        e.functor = (coherentDerived B S hS F hF).lift
          ((coherentDerived B S hS F hF).ι.op ⋙ dualFunctor B S hS F hF K.obj)
          (fun L => hD _ L.unop.2)) ∧
      (∃ η : 𝟭 (coherentDerived B S hS F hF).FullSubcategory ≅
          ((coherentDerived B S hS F hF).lift
            ((coherentDerived B S hS F hF).ι.op ⋙ dualFunctor B S hS F hF K.obj)
            (fun L => hD _ L.unop.2)).rightOp ⋙
          (coherentDerived B S hS F hF).lift
            ((coherentDerived B S hS F hF).ι.op ⋙ dualFunctor B S hS F hF K.obj)
            (fun L => hD _ L.unop.2),
        ∀ L, (coherentDerived B S hS F hF).ι.map (η.hom.app L) =
          (derivedBiduality B S hS F hF K.obj).app L.1) ∧
      (IsQuasiCompactSpace B S hS F →
        (∀ L, coherentDerivedPlus B S hS F hF L →
          coherentDerivedMinus B S hS F hF ((dualFunctor B S hS F hF K.obj).obj (op L))) ∧
        (∀ L, coherentDerivedMinus B S hS F hF L →
          coherentDerivedPlus B S hS F hF ((dualFunctor B S hS F hF K.obj).obj (op L))) ∧
        (∃ (hpm : ∀ L, coherentDerivedPlus B S hS F hF L →
            coherentDerivedMinus B S hS F hF ((dualFunctor B S hS F hF K.obj).obj (op L)))
          (e : (coherentDerivedPlus B S hS F hF).FullSubcategoryᵒᵖ ≌
            (coherentDerivedMinus B S hS F hF).FullSubcategory),
          e.functor = (coherentDerivedMinus B S hS F hF).lift
            ((coherentDerivedPlus B S hS F hF).ι.op ⋙ dualFunctor B S hS F hF K.obj)
            (fun L => hpm _ L.unop.2)) ∧
        (∃ (hb : ∀ L, coherentDerivedBounded B S hS F hF L →
            coherentDerivedBounded B S hS F hF ((dualFunctor B S hS F hF K.obj).obj (op L)))
          (e : (coherentDerivedBounded B S hS F hF).FullSubcategoryᵒᵖ ≌
            (coherentDerivedBounded B S hS F hF).FullSubcategory),
          e.functor = (coherentDerivedBounded B S hS F hF).lift
            ((coherentDerivedBounded B S hS F hF).ι.op ⋙ dualFunctor B S hS F hF K.obj)
            (fun L => hb _ L.unop.2)))

Tag 0E52, a lemma

Tag 0E52 in the Stacks Project.

AlgebraicGeometry.Space.exists_isInvertible_tensor_iso_of_isDualizingComplexOnSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualizingUniqueness/Uniqueness.lean, line 195.

Stacks 0E52. Let S be a scheme and X a locally Noetherian algebraic space over S. If K and K' are dualizing complexes on X (Stacks 0E4Z), then K' is isomorphic to K ⊗^L_{𝒪_X} L for some invertible object L of D(𝒪_X).

D(𝒪_X) is the derived category of the 𝒪_X-modules on the small étale site of X, and ⊗^L_{𝒪_X} with its unit 𝒪_X is AlgebraicGeometry.Space.derivedMonoidalOfModel, the derived tensor product of Stacks 0FPT read on the equi-universe model of the small étale ringed site. The proof is the source's: R𝓗om(K', K) is invertible because affine locally K' is a shift of K (Stacks 0A7F, 0ATP) and R𝓗om(K, K) = 𝒪_X, and K' ≅ R𝓗om(R𝓗om(K', K), K) by biduality (Stacks 0E51).

theorem exists_isInvertible_tensor_iso_of_isDualizingComplexOnSpace
    (hN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (K K' : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (hK : IsDualizingComplexOnSpace B S hS X.1 X.2 hN K)
    (hK' : IsDualizingComplexOnSpace B S hS X.1 X.2 hN K') :
    letI := derivedMonoidalOfModel B S hS X.1 X.2
    ∃ L, IsInvertible L ∧ Nonempty (K'.obj ≅ K.obj ⊗ L)

Tag 0E53, a lemma

Tag 0E53 in the Stacks Project.

AlgebraicGeometry.Space.exists_dimensionFunction_of_isDualizingComplex_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualizingDimensionFunction.lean, line 108.

Let X be a locally Noetherian quasi-separated algebraic space over a scheme S and let ω_X^• be a dualizing complex on X (Stacks 0E4Z). Then the function δ : |X| → ℤ for which ω^•_{X, x̄}[-δ x] is a normalized dualizing complex over 𝒪_{X, x̄} at every geometric point x̄ of X over x is a dimension function on |X|.

theorem exists_dimensionFunction_of_isDualizingComplex_chart
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (ω : QuasicoherentDerivedCategory.{u, u} B S hS X hX)
    (hω : IsDualizingComplexOnSpace B S hS X hX hN ω)
    (δ : points B S hS X → ℤ)
    (hδ : IsNormalizingShiftAtGeometricPoints B S hS ⟨X, hX⟩ hN ω.obj δ) :
    ∃ d : DimensionFunction (points B S hS X), ∀ x : points B S hS X, d x = δ x

AlgebraicGeometry.Space.exists_dimensionFunction_isNormalizedDualizingComplex_geometricDerivedStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualizingDimensionFunction.lean, line 371.

Let X be a locally Noetherian quasi-separated algebraic space over a scheme S and let ω_X^• be a dualizing complex on X (Stacks 0E4Z). Then there is a dimension function δ on |X| such that at every geometric point x̄ of X, lying over x ∈ |X|, the stalk ω_{X, x̄}^• is a dualizing complex over the étale local ring 𝒪_{X, x̄} and δ x is the unique integer n for which ω_{X, x̄}^•[-n] is a normalized dualizing complex. In particular the normalizing shift exists at every geometric point and depends only on the point of |X| under it.

theorem exists_dimensionFunction_isNormalizedDualizingComplex_geometricDerivedStalk
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (hXqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal X)
    (hN : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (ω : QuasicoherentDerivedCategory.{u, u} B S hS X hX)
    (hω : IsDualizingComplexOnSpace B S hS X hX hN ω) :
    ∃ δ : DimensionFunction (points B S hS X),
      ∀ x : GeometricPoint B S hS X,
        letI := isNoetherianRing_geometricStalkRing B S hS ⟨X, hX⟩ hN x
        letI := isLocalRing_geometricStalkRing B S hS ⟨X, hX⟩ x
        Dualizing.IsDualizingComplex ((geometricDerivedStalk B S hS (X := ⟨X, hX⟩) x).obj ω.obj) ∧
          ∀ n : ℤ, Dualizing.IsNormalizedDualizingComplex.{u, u}
              ((geometricDerivedStalk B S hS (X := ⟨X, hX⟩) x).obj ω.obj⟦-n⟧) ↔ n = δ x.image

Sources

LeanAlgebraicGeometry.Space.forall_isDualizingOnChart_iff_exists_surjective · AlgebraicGeometry.Space.IsDualizingComplex · AlgebraicGeometry.Space.IsDualizingComplexOnSpace · AlgebraicGeometry.AffineEtaleDuality.isIso_comparison_app · AlgebraicGeometry.Space.dualizingComplex_duality · AlgebraicGeometry.Space.exists_isInvertible_tensor_iso_of_isDualizingComplexOnSpace · AlgebraicGeometry.Space.exists_dimensionFunction_of_isDualizingComplex_chart · AlgebraicGeometry.Space.exists_dimensionFunction_isNormalizedDualizingComplex_geometricDerivedStalk

Section86.3 Right adjoint of pushforward #

Section 86.3 of the Stacks Project, Tag 0E54. 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 0E55, a lemma

Tag 0E55 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.isLeftAdjoint_quasicoherentDerivedPushforward, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/CompactGeneration/QcqsCompactGenerationRegistration.lean, line 18 (StacksFrontier).

Tag 0E56, a lemma

Tag 0E56 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjoint_boundedBelow, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/CountablePseudoCoherentDualityTags.lean, line 32 (StacksFrontier).

Tag 0E57, an equation

Tag 0E57 in the Stacks Project.

Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/PushforwardTrace.lean, line 122.

Equation 86.3.2.1 of [Stacks, Tag 0E57]. For a morphism of ringed topoi f : (Sh(C), O_C) ⟶ (Sh(D), O_D), a right adjoint a of Rf_*, and objects L of D(O_C) and K of D(O_D), the canonical map

Rf_*RHom_{O_C}(L, a(K)) ⟶ RHom_{O_D}(Rf_*L, K).

It is the projection formula for derived internal Hom of [Stacks, Tag 0B6D] at L and a(K), followed by RHom_{O_D}(Rf_*L, −) applied to the counit Rf_*a(K) ⟶ K of Rf_* ⊣ a.

def pushforwardTrace
    (L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))) :
    (derivedPushforward f).obj ((HX.obj (op L)).obj (a.obj K)) ⟶
      (HY.obj (op ((derivedPushforward f).obj L))).obj K

Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/PushforwardTrace.lean, line 136. The attribute's comment: “the defining composition”.

The trace map is that composition. Equation 86.3.2.1 is the projection formula for derived internal Hom of [Stacks, Tag 0B6D] followed by the derived internal Hom out of Rf_*L of the counit Rf_*a(K) ⟶ K, and this records it as an equation, so a consumer never unfolds the definition.

theorem pushforwardTrace_eq
    (L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))) :
    pushforwardTrace f hmos HX HY DX DY adj L K =
      projectionFormulaInternalHomMap f hmos HX HY DX.toTensorHomBijection
        DY.toTensorHomBijection L (a.obj K) ≫
        (HY.obj (op ((derivedPushforward f).obj L))).map (adj.counit.app K)

Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace_naturality_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/PushforwardTrace.lean, line 147. The attribute's comment: “naturality in the first variable”.

The trace map is contravariant in L.

theorem pushforwardTrace_naturality_source
    {L L' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (g : L' ⟶ L)
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))) :
    (derivedPushforward f).map ((HX.map g.op).app (a.obj K)) ≫
        pushforwardTrace f hmos HX HY DX DY adj L' K =
      pushforwardTrace f hmos HX HY DX DY adj L K ≫
        (HY.map ((derivedPushforward f).map g).op).app K

Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace_naturality_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/PushforwardTrace.lean, line 161. The attribute's comment: “naturality in the second variable”.

The trace map is covariant in K.

theorem pushforwardTrace_naturality_target
    (L : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    {K K' : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))}
    (φ : K ⟶ K') :
    (derivedPushforward f).map ((HX.obj (op L)).map (a.map φ)) ≫
        pushforwardTrace f hmos HX HY DX DY adj L K' =
      pushforwardTrace f hmos HX HY DX DY adj L K ≫
        (HY.obj (op ((derivedPushforward f).obj L))).map φ

Tag 0E58, a lemma

Tag 0E58 in the Stacks Project.

AlgebraicGeometry.Space.isIso_coherator_map_smallEtalePushforwardTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTrace.lean, line 118.

Let f : X ⟶ Y be a morphism of quasi-compact and quasi-separated algebraic spaces, a the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y), L in D_QCoh(𝒪_X) and K in D_QCoh(𝒪_Y). Then the trace map Rf_*R𝓗om(L, a(K)) ⟶ R𝓗om(Rf_*L, K) becomes an isomorphism after applying any right adjoint DQ_Y of the inclusion D_QCoh(𝒪_Y) ⟶ D(𝒪_Y).

theorem isIso_coherator_map_smallEtalePushforwardTrace
    {DQ : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2) ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2}
    (adjQ : (QcohDerived B S hS Y).ι ⊣ DQ)
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    IsIso (DQ.map (smallEtalePushforwardTrace hZ f hXqc hXqs hYqs L K))

Tag 0GG3, an example

Tag 0GG3 in the Stacks Project.

AlgebraicGeometry.Space.UncoheratedTrace.coherator_cannot_be_dropped, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityCoheratorNecessary.lean, line 286. The attribute's comment: “the counterexample of 0GEU on algebraic spaces: for f : A^1_S -> S with S affine carrying t with no t^j = t^(j+1) b (S = Spec Z, t = 2), L = O_X, K = O_Y, the left side of the 0E57 map lies in D_QCoh, the right side has H^0 the non-quasi-coherent product of copies of O_Y, and no map between them is an isomorphism, for every right adjoint a”.

The statement of [Stacks, Tag 0E58] is not true without the coherator DQ_Y. Let S be an affine scheme of the big fppf site with a regular function t admitting no equation t^j = t^{j+1} b (for instance S = Spec ℤ, t = 2), let Y = h_S, X = h_{𝔸¹_S}, f : X ⟶ Y the structure morphism, L = 𝒪_X and K = 𝒪_Y. Then:

X and Y are quasi-compact and quasi-separated algebraic spaces;

Rf_* sends D_QCoh(𝒪_X) into D_QCoh(𝒪_Y), and L, K lie in D_QCoh;

the left hand side Rf_*R𝓗om_{𝒪_X}(L, M) lies in D_QCoh(𝒪_Y) for every M in D_QCoh(𝒪_X), in particular for M = a(K);

the right hand side R𝓗om_{𝒪_Y}(Rf_*L, K) has zeroth cohomology sheaf ∏_{n ≥ 0} 𝒪_Y, which is not quasi-coherent, so the right hand side is not in D_QCoh(𝒪_Y);

hence, for every right adjoint a of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y), no morphism Rf_*R𝓗om_{𝒪_X}(L, a(K)) ⟶ R𝓗om_{𝒪_Y}(Rf_*L, K) — the map (0E57) in particular — is an isomorphism.

theorem coherator_cannot_be_dropped (hZ : B.Contains (⊤_ Scheme.{u})) (t : Γ(S, ⊤))
    (ht : ∀ (j : ℕ) (b : Γ(S, ⊤)), t ^ j ≠ t ^ (j + 1) * b) :
    (IsQuasiCompactSpace B S hS (affineLineAlgebraicSpace B S hS).1 ∧
      IsAbsolutelyQuasiSeparated B S hS hZ (affineLineAlgebraicSpace B S hS).1 ∧
      IsQuasiCompactSpace B S hS (affineBaseSpace B S hS).1 ∧
        IsAbsolutelyQuasiSeparated B S hS hZ (affineBaseSpace B S hS).1) ∧
    PreservesQuasicoherentDerived Rf ∧
    quasicoherentDerivedProperty (affineLineAlgebraicSpace B S hS)
      (structureSheafDerived B S hS (affineLineAlgebraicSpace B S hS)) ∧
    quasicoherentDerivedProperty (affineBaseSpace B S hS)
      (structureSheafDerived B S hS (affineBaseSpace B S hS)) ∧
    (∀ M : DerivedCategory (Modules.{u, u} B S hS (affineLineAlgebraicSpace B S hS).1
      (affineLineAlgebraicSpace B S hS).2),
      quasicoherentDerivedProperty (affineLineAlgebraicSpace B S hS) M →
        quasicoherentDerivedProperty (affineBaseSpace B S hS) (traceSource B S hS Rf M)) ∧
    Nonempty ((DerivedCategory.homologyFunctor _ 0).obj (traceTarget B S hS Rf) ≅
      piUnit (affineBaseSpace B S hS).2) ∧
    ¬ (piUnit (affineBaseSpace B S hS).2).IsQuasicoherentOnSite ∧
    ¬ quasicoherentDerivedProperty (affineBaseSpace B S hS) (traceTarget B S hS Rf) ∧
    ∀ (a : QuasicoherentDerivedCategoryOfModel (affineBaseSpace B S hS) ⥤
      QuasicoherentDerivedCategoryOfModel (affineLineAlgebraicSpace B S hS))
      (_ : liftQuasicoherentDerived Rf (preservesQuasicoherentDerived B S hS Rf α) ⊣ a)
      (φ : traceSource B S hS Rf
          (a.obj ⟨structureSheafDerived B S hS (affineBaseSpace B S hS),
            structureSheafDerived_mem B S hS (affineBaseSpace B S hS)⟩).obj ⟶
        traceTarget B S hS Rf),
      ¬ IsIso φ

Tag 0GG4, a remark

Tag 0GG4 in the Stacks Project.

AlgebraicGeometry.Space.coheratorPushforwardSheafHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTraceCriterion.lean, line 60. The attribute's comment: “the identification of the coherators by Stacks 0CR5”.

Stacks 0GG4, the identification of the coherators. For right adjoints DQ_X, DQ_Y of the inclusions D_QCoh ⟶ D, DQ_Y(Rf_*R𝓗om(L, a(K))) ≅ Rf_*DQ_X(R𝓗om(L, a(K))) (Stacks 0CR5).

def coheratorPushforwardSheafHomIso
    {DQX : DerivedCategory (Modules.{u, u} B S hS X.1 X.2) ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2}
    {DQY : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2) ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2}
    (adjX : (QcohDerived B S hS X).ι ⊣ DQX) (adjY : (QcohDerived B S hS Y).ι ⊣ DQY)
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    DQY.obj ((derivedModulePushforward B S hS f).obj
        (((smallEtaleDerivedSheafHom B S hS X).obj (op L.obj)).obj
          ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K).obj)) ≅
      (quasicoherentDerivedPushforward B S hS f
          (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Y.2 hYqs hXqc f.hom)
          (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X.2 hXqs f.hom)).obj
        (DQX.obj (((smallEtaleDerivedSheafHom B S hS X).obj (op L.obj)).obj
          ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K).obj))

AlgebraicGeometry.Space.isIso_coherator_counit_pushforward_sheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTraceCriterion.lean, line 85. The attribute's comment: “erasing the coherator on the source of the map of Stacks 0E58”.

Stacks 0GG4, erasing the coherator on the source. If R𝓗om(L, a(K)) has quasi-coherent cohomology, then DQ_Y(Rf_*R𝓗om(L, a(K))) ⟶ Rf_*R𝓗om(L, a(K)) is an isomorphism.

theorem isIso_coherator_counit_pushforward_sheafHom
    {DQ : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2) ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2}
    (adjQ : (QcohDerived B S hS Y).ι ⊣ DQ)
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (h : QcohDerived B S hS X (((smallEtaleDerivedSheafHom B S hS X).obj (op L.obj)).obj
      ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K).obj)) :
    IsIso (adjQ.counit.app ((derivedModulePushforward B S hS f).obj
      (((smallEtaleDerivedSheafHom B S hS X).obj (op L.obj)).obj
        ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K).obj)))

AlgebraicGeometry.Space.isIso_coherator_counit_sheafHom_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTraceCriterion.lean, line 104. The attribute's comment: “erasing the coherator on the target of the map of Stacks 0E58”.

Stacks 0GG4, erasing the coherator on the target. If R𝓗om(Rf_*L, K) has quasi-coherent cohomology, then DQ_Y(R𝓗om(Rf_*L, K)) ⟶ R𝓗om(Rf_*L, K) is an isomorphism.

theorem isIso_coherator_counit_sheafHom_pushforward
    {DQ : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2) ⥤
      QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2}
    (adjQ : (QcohDerived B S hS Y).ι ⊣ DQ)
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (h : QcohDerived B S hS Y (((smallEtaleDerivedSheafHom B S hS Y).obj
      (op ((derivedModulePushforward B S hS f).obj L.obj))).obj K.obj)) :
    IsIso (adjQ.counit.app (((smallEtaleDerivedSheafHom B S hS Y).obj
      (op ((derivedModulePushforward B S hS f).obj L.obj))).obj K.obj))

AlgebraicGeometry.Space.isIso_smallEtalePushforwardTrace_of_qcohDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTraceCriterion.lean, line 121. The attribute's comment: “the map of Stacks 0E57 is an isomorphism if both sides have quasi-coherent cohomology”.

Stacks 0GG4, the quasi-coherence criterion. If R𝓗om(L, a(K)) and R𝓗om(Rf_*L, K) both have quasi-coherent cohomology, then the map Rf_*R𝓗om(L, a(K)) ⟶ R𝓗om(Rf_*L, K) of Stacks 0E57 is an isomorphism.

theorem isIso_smallEtalePushforwardTrace_of_qcohDerived
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hA : QcohDerived B S hS X (((smallEtaleDerivedSheafHom B S hS X).obj (op L.obj)).obj
      ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K).obj))
    (hB : QcohDerived B S hS Y (((smallEtaleDerivedSheafHom B S hS Y).obj
      (op ((derivedModulePushforward B S hS f).obj L.obj))).obj K.obj)) :
    IsIso (smallEtalePushforwardTrace hZ f hXqc hXqs hYqs L K)

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

Stacks 0GG4 (1). If L and Rf_*L are perfect, then the map Rf_*R𝓗om(L, a(K)) ⟶ R𝓗om(Rf_*L, K) of Stacks 0E57 is an isomorphism.

theorem isIso_smallEtalePushforwardTrace_of_isPerfect
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hL : RingedSite.IsPerfect (smallEtaleRingedSite B S hS X.1 X.2) L.obj)
    (hfL : RingedSite.IsPerfect (smallEtaleRingedSite B S hS Y.1 Y.2)
      ((derivedModulePushforward B S hS f).obj L.obj)) :
    IsIso (smallEtalePushforwardTrace hZ f hXqc hXqs hYqs L K)

AlgebraicGeometry.Space.isIso_smallEtalePushforwardTrace_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTraceCriterion.lean, line 156. The attribute's comment: “(2)”.

Stacks 0GG4 (2). If K is bounded below and L and Rf_*L are pseudo-coherent, then the map Rf_*R𝓗om(L, a(K)) ⟶ R𝓗om(Rf_*L, K) of Stacks 0E57 is an isomorphism.

theorem isIso_smallEtalePushforwardTrace_of_isPseudoCoherent
    (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hK : DerivedCategoryB.IsBoundedBelow K.obj)
    (hL : RingedSite.IsPseudoCoherent (smallEtaleRingedSite B S hS X.1 X.2) L.obj)
    (hfL : RingedSite.IsPseudoCoherent (smallEtaleRingedSite B S hS Y.1 Y.2)
      ((derivedModulePushforward B S hS f).obj L.obj)) :
    IsIso (smallEtalePushforwardTrace hZ f hXqc hXqs hYqs L K)

Tag 0GG5, an example

Tag 0GG5 in the Stacks Project.

AlgebraicGeometry.Space.isIso_smallEtalePushforwardTrace_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPushforwardTraceProper.lean, line 107.

Stacks 0GG5. Let f : X ⟶ Y be a proper morphism of Noetherian algebraic spaces over S, L in D^-_Coh(𝒪_X) and K in D^+_QCoh(𝒪_Y). Then the map Rf_*R𝓗om(L, a(K)) ⟶ R𝓗om(Rf_*L, K) of Stacks 0E57 is an isomorphism.

theorem isIso_smallEtalePushforwardTrace_of_isProper (hf : IsProper B S hS f.hom)
    (hX : IsNoetherian B S hS hZ X.1) (hY : IsNoetherian B S hS hZ Y.1)
    (L : DerivedCategory (Modules.{u, u} B S hS X.1 X.2))
    (hL : DerivedCategoryB.derivedCategoryBMinus (isCoherent.{u, u} B S hS X.1 X.2) L)
    (K : DerivedCategory (Modules.{u, u} B S hS Y.1 Y.2))
    (hK : DerivedCategoryB.derivedCategoryBPlus
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS Y.1 Y.2).O))) K) :
    IsIso (smallEtalePushforwardTrace hZ f hX.1 hX.2.1 hY.2.1
      ⟨L, fun i => (hL.2 i).toIsQuasicoherentOnSite⟩ ⟨K, hK.2⟩)

Tag 0E59, a lemma

Tag 0E59 in the Stacks Project.

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

Stacks 0E59. Let f : X ⟶ Y be a morphism of quasi-separated and quasi-compact algebraic spaces. For all L in D_QCoh(𝒪_X) and K in D_QCoh(𝒪_Y) the map of Stacks 0E57 induces an isomorphism RHom_X(L, a(K)) ⟶ RHom_Y(Rf_*L, K) of global derived homs.

theorem isIso_globalDerivedHomTrace (L : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    IsIso (globalDerivedHomTrace hZ f hXqc hXqs hYqs L K)

Sources

LeanAlgebraicGeometry.Space.isLeftAdjoint_quasicoherentDerivedPushforward · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjoint_boundedBelow · Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace · Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace_eq · Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace_naturality_source · Stacks.Cohomology.PushforwardTraceOnRingedTopoi.pushforwardTrace_naturality_target · AlgebraicGeometry.Space.isIso_coherator_map_smallEtalePushforwardTrace · AlgebraicGeometry.Space.UncoheratedTrace.coherator_cannot_be_dropped

Section86.4 Right adjoint of pushforward and base change, I #

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

Tag 0E5B, an equation

Tag 0E5B in the Stacks Project.

AlgebraicGeometry.Space.TorIndependentBaseChangeSquare, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChange.lean, line 71. The attribute's comment: “the Tor-independent cartesian square”.

A cartesian square of algebraic spaces over S whose upper right and lower left corners are Tor independent over the lower right corner.

structure TorIndependentBaseChangeSquare (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityRightAdjointBaseChange.lean, line 178.

For a cartesian square of algebraic spaces with X and Y' quasi-compact and quasi-separated and Y quasi-separated, the transformation Rg'_* ∘ a' ⟶ a ∘ Rg_* between the right adjoints a, a' of Rf_*, Rf'_* on D_QCoh (Stacks 0E55): the mate of the base change map Lg^* ∘ Rf_* ⟶ Rf'_* ∘ L(g')^* of Stacks 07A7.

def quasicoherentDerivedRightAdjointBaseChange :
    quasicoherentDerivedRightAdjoint hZ f'
          (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc)
          (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) hY'qs ⋙
        quasicoherentDerivedPushforward B S hS g'
          (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ X.2 hXqs
            (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc) g'.hom)
          (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X'.2
            (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) g'.hom) ⟶
      quasicoherentDerivedPushforward B S hS g
          (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Y.2 hYqs hY'qc g.hom)
          (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ Y'.2 hY'qs g.hom) ⋙
        quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs

Tag 0E5C, a lemma

Tag 0E5C in the Stacks Project.

AlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChangeMap.lean, line 105.

Stacks 0E5C. For a cartesian square of quasi-compact quasi-separated algebraic spaces with X and Y' Tor independent over Y, the base change transformation Rg'_* ∘ a' ⟶ a ∘ Rg_* of Stacks 0E5B is an isomorphism.

theorem isIso_quasicoherentDerivedRightAdjointBaseChange :
    IsIso (quasicoherentDerivedRightAdjointBaseChange hZ sq hXqc hXqs hYqs hY'qc hY'qs)

Tag 0E5D, an equation

Tag 0E5D in the Stacks Project.

AlgebraicGeometry.Space.TorIndependentBaseChangeSquare.DualityData.twistedInverseImageBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChange.lean, line 165.

The base change map L(g')^* ∘ a ⟶ a' ∘ Lg^* between twisted inverse images, the composition of the unit of Lg^* ⊣ Rg_*, the inverse of the base change map Rg'_* ∘ a' ⟶ a ∘ Rg_* between right adjoints, and the counit of L(g')^* ⊣ Rg'_*.

noncomputable def twistedInverseImageBaseChange (hbc : IsIso D.baseChange) :
    D.twistedInverseImage ⋙ D.pullbackG' ⟶ D.pullbackG ⋙ D.twistedInverseImage'

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChangeMap.lean, line 117.

The base change map L(g')^* ∘ a ⟶ a' ∘ Lg^* (Stacks 0E5D) of a cartesian square of quasi-compact quasi-separated algebraic spaces with X and Y' Tor independent over Y: the unit of Lg^* ⊣ Rg_*, the inverse of the isomorphism of Stacks 0E5C, and the counit of L(g')^* ⊣ Rg'_*.

def quasicoherentDerivedRightAdjointBaseChangeMap :
    quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs ⋙ quasicoherentDerivedModulePullback g' ⟶
      quasicoherentDerivedModulePullback g ⋙
        quasicoherentDerivedRightAdjoint hZ f'
          (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc)
          (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) hY'qs

Tag 0E5E, a lemma

Tag 0E5E in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_vertical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChangeMap.lean, line 214.

Stacks 0E5E. For two vertically stacked cartesian squares of quasi-compact quasi-separated algebraic spaces, with f and l as well as g and m Tor independent, the base change map of Stacks 0E5D for the outer rectangle is the composite of those of the two squares, read through the identifications a ∘ b = c and a' ∘ b' = c' of the right adjoints of R(g ∘ f)_* = Rg_* ∘ Rf_* and R(g' ∘ f')_* = Rg'_* ∘ Rf'_*.

theorem quasicoherentDerivedRightAdjointBaseChangeMap_vertical (K) :
    (quasicoherentDerivedRightAdjointBaseChangeMap hZ (sqt.paste_vert sqb) hXqc hXqs hZqs
        hZ'qc hZ'qs (torIndependent_rectangle_vertical sqb hTt hTb)).app K =
      (quasicoherentDerivedModulePullback k).map
          ((RightAdjointBaseChange.rightAdjointCompIso (squareAdjF hZ hXqc hXqs hYqs)
            (squareAdjF hZ hYqc hYqs hZqs) (squareAdjF hZ hXqc hXqs hZqs)
            (quasicoherentDerivedPushforwardCompIso f g
              (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Y.2 hYqs hXqc f.hom)
              (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X.2 hXqs f.hom)
              (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Z.2 hZqs hYqc g.hom)
              (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ Y.2 hYqs g.hom)
              (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Z.2 hZqs hXqc (f ≫ g).hom)
              (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X.2 hXqs
                (f ≫ g).hom))).inv.app K) ≫
        (quasicoherentDerivedRightAdjointBaseChangeMap hZ sqt hXqc hXqs hYqs hY'qc hY'qs
          hTt).app ((quasicoherentDerivedRightAdjoint hZ g hYqc hYqs hZqs).obj K) ≫
        (quasicoherentDerivedRightAdjoint hZ f'
            (isQuasiCompactSpace_of_isPullback hZ sqt hXqc hYqs hY'qc)
            (isAbsolutelyQuasiSeparated_of_isPullback hZ sqt hXqs hY'qs) hY'qs).map
          ((quasicoherentDerivedRightAdjointBaseChangeMap hZ sqb hYqc hYqs hZqs hZ'qc hZ'qs
            hTb).app K) ≫
        (RightAdjointBaseChange.rightAdjointCompIso (squareAdjF' hZ sqt hXqc hXqs hYqs hY'qc hY'qs)
          (squareAdjF' hZ sqb hYqc hYqs hZqs hZ'qc hZ'qs)
          (squareAdjF' hZ (sqt.paste_vert sqb) hXqc hXqs hZqs hZ'qc hZ'qs)
          (quasicoherentDerivedPushforwardCompIso f' g'
            (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Y'.2 hY'qs
              (isQuasiCompactSpace_of_isPullback hZ sqt hXqc hYqs hY'qc) f'.hom)
            (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X'.2
              (isAbsolutelyQuasiSeparated_of_isPullback hZ sqt hXqs hY'qs) f'.hom)
            (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Z'.2 hZ'qs hY'qc g'.hom)
            (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ Y'.2 hY'qs g'.hom)
            (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Z'.2 hZ'qs
              (isQuasiCompactSpace_of_isPullback hZ sqt hXqc hYqs hY'qc) (f' ≫ g').hom)
            (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X'.2
              (isAbsolutelyQuasiSeparated_of_isPullback hZ sqt hXqs hY'qs)
              (f' ≫ g').hom))).hom.app ((quasicoherentDerivedModulePullback m).obj K)

Tag 0E5F, a lemma

Tag 0E5F in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_horizontal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChangeMap.lean, line 288.

Stacks 0E5F. For two horizontally composed cartesian squares of quasi-compact quasi-separated algebraic spaces, with f and h as well as f' and h' Tor independent, the base change map of Stacks 0E5D for the outer rectangle is the composite of those of the two squares, read through L(g ∘ g')^* = L(g')^* ∘ Lg^* and L(h ∘ h')^* = L(h')^* ∘ Lh^*.

theorem quasicoherentDerivedRightAdjointBaseChangeMap_horizontal (K) :
    (quasicoherentDerivedRightAdjointBaseChangeMap hZ (sql.paste_horiz sqr) hXqc hXqs hYqs
        hY''qc hY''qs (torIndependent_rectangle_horizontal sqr hTr hTl)).app K =
      (quasicoherentDerivedModulePullbackCompIso g' g).inv.app
          ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K) ≫
        (quasicoherentDerivedModulePullback g').map
          ((quasicoherentDerivedRightAdjointBaseChangeMap hZ sqr hXqc hXqs hYqs hY'qc hY'qs
            hTr).app K) ≫
        (quasicoherentDerivedRightAdjointBaseChangeMap hZ sql hX'qc hX'qs hY'qs hY''qc
          hY''qs hTl).app ((quasicoherentDerivedModulePullback h).obj K) ≫
        (quasicoherentDerivedRightAdjoint hZ f''
          (isQuasiCompactSpace_of_isPullback hZ (sql.paste_horiz sqr) hXqc hYqs hY''qc)
          (isAbsolutelyQuasiSeparated_of_isPullback hZ (sql.paste_horiz sqr) hXqs hY''qs)
          hY''qs).map ((quasicoherentDerivedModulePullbackCompIso h' h).hom.app K)

Tag 0E5G, a remark

Tag 0E5G in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_grid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChangeMapGrid.lean, line 276.

Stacks 0E5G. Let S be a scheme and consider a commutative diagram
X'' --k'--> X' --k--> X
 |f''        |f'       |f
 v           v         v
Y'' --l'--> Y' --l--> Y
 |g''        |g'       |g
 v           v         v
Z'' --m'--> Z' --m--> Z
of quasi-compact and quasi-separated algebraic spaces over S whose squares A B / C D are cartesian, with (f, l), (g, m), (f', l'), (g', m') Tor independent pairs. Let a, a', a'', b, b', b'' be the right adjoints of Stacks 0E55 for f, f', f'', g, g', g'' (AlgebraicGeometry.Space.quasicoherentDerivedRightAdjoint). Then the two transformations (k')^* ∘ k^* ∘ a ∘ b ⟶ a'' ∘ b'' ∘ (m')^* ∘ m^* built from the base change maps (Stacks 0E5D) of the rectangles, γ_{A+C} ∘ γ_{B+D} (columns) and γ_{C+D} ∘ γ_{A+B} (rows), are equal. Here the maps of the rectangles are read through the identifications of Stacks 0E5E and 0E5F (quasicoherentDerivedRightAdjointBaseChangeMapPasteVert, quasicoherentDerivedRightAdjointBaseChangeMapPasteHoriz), and the equality is stated at every object K of D_QCoh(𝒪_Z).

Of the source's standing hypothesis that all nine spaces are quasi-compact and quasi-separated, two parts are not assumed: X'' inherits both properties from the cartesian squares, and quasi-compactness of Z is not used.

theorem quasicoherentDerivedRightAdjointBaseChangeMap_grid (K) :
    (quasicoherentDerivedModulePullback k').map
        ((quasicoherentDerivedRightAdjointBaseChangeMapPasteVert hZ sqB sqD hXqc hXqs hYqc hYqs
          hZqs hY'qc hY'qs hZ'qc hZ'qs hTB hTD).app K) ≫
      (quasicoherentDerivedRightAdjointBaseChangeMapPasteVert hZ sqA sqC hX'qc hX'qs hY'qc hY'qs
        hZ'qs hY''qc hY''qs hZ''qc hZ''qs hTA hTC).app
          ((quasicoherentDerivedModulePullback m).obj K) =
    (quasicoherentDerivedRightAdjointBaseChangeMapPasteHoriz hZ sqB sqA hXqc hXqs hYqs hY''qc
        hY''qs hTB hTA).app
          ((quasicoherentDerivedRightAdjoint hZ g hYqc hYqs hZqs).obj K) ≫
      (quasicoherentDerivedRightAdjoint hZ f''
          (isQuasiCompactSpace_of_isPullback hZ (sqA.paste_horiz sqB) hXqc hYqs hY''qc)
          (isAbsolutelyQuasiSeparated_of_isPullback hZ (sqA.paste_horiz sqB) hXqs hY''qs)
          hY''qs).map
        ((quasicoherentDerivedRightAdjointBaseChangeMapPasteHoriz hZ sqD sqC hYqc hYqs hZqs
          hZ''qc hZ''qs hTD hTC).app K)

Sources

LeanAlgebraicGeometry.Space.TorIndependentBaseChangeSquare · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChange · AlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChange · AlgebraicGeometry.Space.TorIndependentBaseChangeSquare.DualityData.twistedInverseImageBaseChange · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_vertical · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_horizontal · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_grid

Section86.5 Right adjoint of pushforward and base change, II #

Section 86.5 of the Stacks Project, Tag 0E5H. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0E5I, a lemma

Tag 0E5I in the Stacks Project.

AlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityRightAdjointBaseChangeAffinePerfect.lean, line 53. The attribute's comment: “(2)”.

Stacks 0E5I (2). For a cartesian square
X' --g'--> X
|f'        |f
Y' --g---> Y
with Y, Y' affine, Y Noetherian, f proper and perfect, and X, Y' Tor independent over Y, the base change map L(g')^* a(K) ⟶ a'(Lg^*K) of Stacks 0E5D is an isomorphism for every K ∈ D_QCoh(𝒪_Y).

theorem isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_isPerfect
    {X Y X' Y' : AlgebraicSpaces B S hS} {f : X ⟶ Y} {g : Y' ⟶ Y} {f' : X' ⟶ Y'} {g' : X' ⟶ X}
    (sq : IsPullback g' f' f g) (hf : IsProper B S hS f.hom) (hfp : IsPerfect B S hS f.hom)
    (hY : IsAffineSpace B S hS Y.1) (hYN : IsNoetherian B S hS hZ Y.1)
    (hY' : IsAffineSpace B S hS Y'.1) (hTor : TorIndependent X.2 Y'.2 Y.2 f.hom g.hom)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    IsIso ((quasicoherentDerivedRightAdjointBaseChangeMap hZ sq
      (isQuasiCompactSpace_of_isQuasiCompact_hom_of_isAffineSpace B S hS f hf.2.1.2 hY)
      (isAbsolutelyQuasiSeparated_of_isQuasiSeparated_hom_of_isAffineSpace B S hS hZ f
        (isQuasiSeparated_of_isSeparated B S hS hf.1) hY)
      (isAbsolutelyQuasiSeparated_of_isAffineSpace B S hS hZ hY) hY'.isQuasiCompactSpace
      (isAbsolutelyQuasiSeparated_of_isAffineSpace B S hS hZ hY') hTor).app K)

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

Stacks 0E5I (3). Let g : U' ⟶ U be a morphism of affine schemes of finite Tor dimension, with U Noetherian, and consider a cartesian square
X' --g'--> X
|f'        |f
U' --g---> U
with f proper and X, U' Tor independent over U. Then the base change map L(g')^* a(K) ⟶ a'(Lg^*K) of Stacks 0E5D is an isomorphism for every K ∈ D^+_QCoh(𝒪_U).

theorem isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_hasFiniteTorDimension
    {U' U : BigFppfOver B S hS} [IsAffine ((BigFppfOver.toScheme B S hS).obj U)]
    [IsAffine ((BigFppfOver.toScheme B S hS).obj U')] (g₀ : U' ⟶ U)
    {X X' : AlgebraicSpaces B S hS} {f : X ⟶ ⟨yoneda.obj U, isAlgebraicSpace_yoneda B S hS U⟩}
    {f' : X' ⟶ ⟨yoneda.obj U', isAlgebraicSpace_yoneda B S hS U'⟩} {g' : X' ⟶ X}
    (sq : IsPullback g' f' f (representedSpaceMap B S hS g₀)) (hf : IsProper B S hS f.hom)
    (hY : IsNoetherian B S hS hZ (yoneda.obj U))
    (hTor : TorIndependent X.2 (isAlgebraicSpace_yoneda B S hS U')
      (isAlgebraicSpace_yoneda B S hS U) f.hom (representedSpaceMap B S hS g₀).hom)
    (hg : AlgebraicGeometry.Space.HasFiniteTorDimension (representedSpaceMap B S hS g₀))
    (K : QuasicoherentDerivedCategory.{u, u} B S hS (yoneda.obj U)
      (isAlgebraicSpace_yoneda B S hS U))
    (hK : DerivedCategoryB.IsBoundedBelow K.obj) :
    IsIso ((quasicoherentDerivedRightAdjointBaseChangeMap hZ sq
      (isQuasiCompactSpace_of_isQuasiCompact_hom_of_isAffineSpace B S hS f hf.2.1.2
        (isAffineSpace_yoneda B S hS U inferInstance))
      (isAbsolutelyQuasiSeparated_of_isQuasiSeparated_hom_of_isAffineSpace B S hS hZ f
        (isQuasiSeparated_of_isSeparated B S hS hf.1) (isAffineSpace_yoneda B S hS U inferInstance))
      (isAbsolutelyQuasiSeparated_of_isAffineSpace B S hS hZ
        (isAffineSpace_yoneda B S hS U inferInstance))
      (isAffineSpace_yoneda B S hS U' inferInstance).isQuasiCompactSpace
      (isAbsolutelyQuasiSeparated_of_isAffineSpace B S hS hZ
        (isAffineSpace_yoneda B S hS U' inferInstance)) hTor).app K)

Declarations registered for the tag:

AlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_isFlat, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/DualityRightAdjointBaseChangeAffineTags.lean, line 22 (StacksFrontier): “(1)”.

Sources

LeanAlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_isPerfect · AlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_hasFiniteTorDimension · AlgebraicGeometry.Space.isIso_quasicoherentDerivedRightAdjointBaseChangeMap_app_of_isFlat

Section86.6 Right adjoint of pushforward and trace maps #

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

Tag 0E5L, a lemma

Tag 0E5L in the Stacks Project.

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

Stacks 0E5L. The trace maps and the base change maps agree: Lg^* of the trace Rf_* a K ⟶ K is the base change map β at a K, followed by Rf'_* of the map α of Stacks 0E5D and the trace Rf'_* a' (Lg^* K) ⟶ Lg^* K.

theorem quasicoherentDerivedRightAdjointBaseChangeMap_trace (K) :
    (squareBaseChange hZ sq hXqc hXqs hYqs hY'qc hY'qs).app
          ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj K) ≫
        (quasicoherentDerivedPushforward B S hS f'
          (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Y'.2 hY'qs
            (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc) f'.hom)
          (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X'.2
            (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) f'.hom)).map
          ((quasicoherentDerivedRightAdjointBaseChangeMap hZ sq hXqc hXqs hYqs hY'qc hY'qs
            hTor).app K) ≫
        (squareAdjF' hZ sq hXqc hXqs hYqs hY'qc hY'qs).counit.app
          ((quasicoherentDerivedModulePullback g).obj K) =
      (quasicoherentDerivedModulePullback g).map
        ((squareAdjF hZ hXqc hXqs hYqs).counit.app K)

Tag 0E5M, a lemma

Tag 0E5M in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityBaseChangeMap.lean, line 170.

Stacks 0E5M. The units and the base change maps agree: L(g')^* of the unit K ⟶ a (Rf_* K), followed by the map α of Stacks 0E5D at Rf_* K and by a' of the base change map β, is the unit L(g')^* K ⟶ a' (Rf'_* L(g')^* K).

theorem quasicoherentDerivedRightAdjointBaseChangeMap_unit (K) :
    (quasicoherentDerivedModulePullback g').map ((squareAdjF hZ hXqc hXqs hYqs).unit.app K) ≫
        (quasicoherentDerivedRightAdjointBaseChangeMap hZ sq hXqc hXqs hYqs hY'qc hY'qs
          hTor).app ((quasicoherentDerivedPushforward B S hS f
            (isQuasiCompact_of_isQuasiCompactSpace B S hS hZ Y.2 hYqs hXqc f.hom)
            (isQuasiSeparated_of_isAbsolutelyQuasiSeparated_source B S hS hZ X.2 hXqs
              f.hom)).obj K) ≫
        (quasicoherentDerivedRightAdjoint hZ f'
          (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc)
          (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) hY'qs).map
          ((squareBaseChange hZ sq hXqc hXqs hYqs hY'qc hY'qs).app K) =
      (squareAdjF' hZ sq hXqc hXqs hYqs hY'qc hY'qs).unit.app
        ((quasicoherentDerivedModulePullback g').obj K)

Sources

LeanAlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_trace · AlgebraicGeometry.Space.quasicoherentDerivedRightAdjointBaseChangeMap_unit

Section86.7 Right adjoint of pushforward and pullback #

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

Tag 0E5P, an equation

Tag 0E5P in the Stacks Project.

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullbackTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 290. The attribute's comment: “two-variable construction”.

The two-variable comparison map of [Stacks, Tag 0E5P]: Lf^*K ⊗ᴸ_{𝒪_X} a(L) ⟶ a(K ⊗ᴸ_{𝒪_Y} L), for a right adjoint a of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y). It is the map adjoint to the inverse of the projection formula Rf_*(Lf^*K ⊗ᴸ_{𝒪_X} a(L)) ≅ K ⊗ᴸ_{𝒪_Y} Rf_*(a(L)) followed by the identity of K tensored with the trace map adja.counit.app L : Rf_*(a(L)) ⟶ L.

def compareWithPullbackTensor (K L : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    (D.tensorX.obj (D.pullback.obj K)).obj (a.obj L) ⟶ a.obj ((D.tensorY.obj K).obj L)

AlgebraicGeometry.Space.PullbackComparisonData.homEquiv_symm_compareWithPullbackTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 298. The attribute's comment: “two-variable adjunction characterization”.

The adjoint transpose of the two-variable comparison map is the inverse projection formula followed by the identity of K tensored with the trace map.

theorem homEquiv_symm_compareWithPullbackTensor
    (K L : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    (adja.homEquiv _ _).symm (D.compareWithPullbackTensor adja K L) =
      inv (D.projectionFormulaMap (a.obj L) K) ≫
        (D.tensorY.obj K).map (adja.counit.app L)

AlgebraicGeometry.Space.PullbackComparisonData.projectionFormulaMap_comp_map_compareWithPullbackTensor_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 319. The attribute's comment: “two-variable characterization without the inverse”.

The two-variable comparison map as the source constructs it: the projection formula, followed by Rf_* of the comparison map and the trace map, is the identity of K tensored with the trace map. This is the characterization with no inverse in it.

theorem projectionFormulaMap_comp_map_compareWithPullbackTensor_comp_counit
    (K L : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    D.projectionFormulaMap (a.obj L) K ≫
        D.pushforward.map (D.compareWithPullbackTensor adja K L) ≫
          adja.counit.app ((D.tensorY.obj K).obj L) =
      (D.tensorY.obj K).map (adja.counit.app L)

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullbackTensor_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 383. The attribute's comment: “two-variable naturality”.

The two-variable comparison map is natural in K and L jointly.

theorem compareWithPullbackTensor_naturality
    {K K' L L' : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2} (h : K ⟶ K') (g : L ⟶ L') :
    (D.tensorX.map (D.pullback.map h)).app (a.obj L) ≫
        (D.tensorX.obj (D.pullback.obj K')).map (a.map g) ≫
          D.compareWithPullbackTensor adja K' L' =
      D.compareWithPullbackTensor adja K L ≫
        a.map ((D.tensorY.map h).app L ≫ (D.tensorY.obj K').map g)

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 401.

Equation 86.7.0.1 of [Stacks, Tag 0E5P]: the comparison map Lf^*K ⊗ᴸ_{𝒪_X} a(𝒪_Y) ⟶ a(K), the two-variable comparison map at L = 𝒪_Y followed by a applied to the right unitor K ⊗ᴸ_{𝒪_Y} 𝒪_Y ≅ K.

def compareWithPullback (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    (D.tensorX.obj (D.pullback.obj K)).obj
        (a.obj (derivedStructureSheaf B S hS Y.1 Y.2)) ⟶ a.obj K

AlgebraicGeometry.Space.PullbackComparisonData.projectionFormulaMap_comp_map_compareWithPullback_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 429. The attribute's comment: “characterization without the inverse”.

Equation 86.7.0.1 as the source constructs it: the projection formula, followed by Rf_* of the displayed comparison map and the trace map, is the identity of K tensored with the trace map at 𝒪_Y, followed by the right unitor.

theorem projectionFormulaMap_comp_map_compareWithPullback_comp_counit
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    D.projectionFormulaMap (a.obj (derivedStructureSheaf B S hS Y.1 Y.2)) K ≫
        D.pushforward.map (D.compareWithPullback adja ρ K) ≫ adja.counit.app K =
      (D.tensorY.obj K).map (adja.counit.app (derivedStructureSheaf B S hS Y.1 Y.2)) ≫
        ρ.hom.app K

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullback_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 455. The attribute's comment: “functoriality in K”.

Equation 86.7.0.1 is functorial in K.

theorem compareWithPullback_naturality
    {K K' : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2} (h : K ⟶ K') :
    (D.tensorX.map (D.pullback.map h)).app
          (a.obj (derivedStructureSheaf B S hS Y.1 Y.2)) ≫
        D.compareWithPullback adja ρ K' =
      D.compareWithPullback adja ρ K ≫ a.map h

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullbackNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 496. The attribute's comment: “functoriality in K, as a natural transformation”.

Equation 86.7.0.1 as a natural transformation of functors of K, which is its functoriality in K.

def compareWithPullbackNatTrans :
    D.compareWithPullbackSource (a.obj (derivedStructureSheaf B S hS Y.1 Y.2)) ⟶ a

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullbackNatTrans_commShift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 623. The attribute's comment: “compatibility with distinguished triangles”.

Compatibility of Equation 86.7.0.1 with distinguished triangles: the displayed comparison map commutes with translation, so it carries the third morphism of a distinguished triangle of D_QCoh(𝒪_Y) to the third morphism of its image.

theorem compareWithPullbackNatTrans_commShift :
    NatTrans.CommShift (D.compareWithPullbackNatTrans adja ρ) ℤ

AlgebraicGeometry.Space.PullbackComparisonData.compareWithPullback_shift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparison.lean, line 630. The attribute's comment: “compatibility with distinguished triangles, componentwise”.

Equation 86.7.0.1 at a translate of K, which is that compatibility componentwise.

theorem compareWithPullback_shift (n : ℤ)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    D.compareWithPullback adja ρ ((shiftFunctor _ n).obj K) =
      ((D.compareWithPullbackSource
          (a.obj (derivedStructureSheaf B S hS Y.1 Y.2))).commShiftIso n).hom.app K ≫
        (shiftFunctor _ n).map (D.compareWithPullback adja ρ K) ≫
          (a.commShiftIso n).inv.app K

AlgebraicGeometry.Space.quasicoherentDerivedCompareWithPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparisonCanonical.lean, line 371.

Stacks 0E5P. Let f : X ⟶ Y be a morphism of quasi-compact quasi-separated algebraic spaces over S and let a be the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) (Stacks 0E55). The map Lf^*K ⊗^L_{𝒪_X} a(𝒪_Y) ⟶ a(K), the two-variable map at L = 𝒪_Y followed by a of the unitor, is functorial in K.

def quasicoherentDerivedCompareWithPullback :
    quasicoherentDerivedModulePullback f ⋙ (quasicoherentDerivedTensor B S hS X).flip.obj
        ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj
          (derivedStructureSheaf B S hS Y.1 Y.2)) ⟶
      quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs

AlgebraicGeometry.Space.quasicoherentDerivedCompareWithPullback_commShift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparisonCanonical.lean, line 395.

Stacks 0E5P, compatibility with distinguished triangles. The map Lf^*K ⊗^L_{𝒪_X} a(𝒪_Y) ⟶ a(K) commutes with the shift, so it carries the third morphism of a distinguished triangle in K to the third morphism of its image.

theorem quasicoherentDerivedCompareWithPullback_commShift :
    NatTrans.CommShift (quasicoherentDerivedCompareWithPullback hZ f hXqc hXqs hYqs) ℤ

Tag 0E5Q, a lemma

Tag 0E5Q in the Stacks Project.

AlgebraicGeometry.Space.isIso_quasicoherentDerivedCompareWithPullbackTensor_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparisonPerfectDual.lean, line 51. The attribute's comment: “the map Lf^*K ⊗ a(L) → a(K ⊗ L) is an isomorphism for K perfect”.

Stacks 0E5Q. Let f : X ⟶ Y be a morphism of quasi-compact and quasi-separated algebraic spaces and a the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y). For K, L ∈ D_QCoh(𝒪_Y) with K perfect, the map Lf^*K ⊗^L a(L) ⟶ a(K ⊗^L L) is an isomorphism.

theorem isIso_quasicoherentDerivedCompareWithPullbackTensor_of_isPerfect
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (hK : RingedSite.IsPerfect (smallEtaleRingedSite B S hS Y.1 Y.2) K.obj)
    (L : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    IsIso (quasicoherentDerivedCompareWithPullbackTensor hZ f hXqc hXqs hYqs K L)

AlgebraicGeometry.Space.isIso_quasicoherentDerivedCompareWithPullback_app_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparisonPerfectDual.lean, line 63. The attribute's comment: “in particular, the map (0E5P) Lf^*K ⊗ a(O_Y) → a(K) is an isomorphism for K perfect”.

Stacks 0E5Q, in particular. For K ∈ D_QCoh(𝒪_Y) perfect, the map Lf^*K ⊗^L a(𝒪_Y) ⟶ a(K) of Stacks 0E5P is an isomorphism.

theorem isIso_quasicoherentDerivedCompareWithPullback_app_of_isPerfect
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (hK : RingedSite.IsPerfect (smallEtaleRingedSite B S hS Y.1 Y.2) K.obj) :
    IsIso ((quasicoherentDerivedCompareWithPullback hZ f hXqc hXqs hYqs).app K)

Tag 0E5R, a lemma

Tag 0E5R in the Stacks Project.

AlgebraicGeometry.Space.quasicoherentDerivedCompareWithPullback_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparisonCanonicalBaseChange.lean, line 247.

For a cartesian square of quasi-compact quasi-separated algebraic spaces with X and Y' Tor independent over Y and K ∈ D_QCoh(𝒪_Y), the square

L(g')^*(Lf^*K ⊗^L a(𝒪_Y)) ⟶ L(g')^*a(K) ⟶ a'(Lg^*K) (L(g')^* of Stacks 0E5P, then the base change map of Stacks 0E5D)

equals L(g')^*(Lf^*K ⊗^L a(𝒪\_Y)) ⟶ L(g')^*Lf^*K ⊗^L L(g')^*a(𝒪\_Y) ⟶ L(f')^*Lg^*K ⊗^L a'(𝒪\_\{Y'}) ⟶ a'(Lg^*K): Stacks 07A4 for g', the identification of the two iterated pullbacks around the square and Stacks 0E5D at 𝒪_Y followed by a'(Lg^*𝒪_Y ≅ 𝒪_{Y'}), then Stacks 0E5P for f'.

theorem quasicoherentDerivedCompareWithPullback_baseChange
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    (quasicoherentDerivedModulePullback g').map
          ((quasicoherentDerivedCompareWithPullback hZ f hXqc hXqs hYqs).app K) ≫
        (quasicoherentDerivedRightAdjointBaseChangeMap hZ sq hXqc hXqs hYqs hY'qc hY'qs
          hTor).app K =
      (quasicoherentDerivedPullbackTensorComparison g').app
          ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj
            (derivedStructureSheaf B S hS Y.1 Y.2), (quasicoherentDerivedModulePullback f).obj K) ≫
        ((quasicoherentDerivedTensor B S hS X').map
            (ObjectProperty.homMk
              ((smallEtaleDerivedModulePullbackSquareIso B S hS f g f' g' sq.w).hom.app K.obj ≫
                (smallEtaleDerivedModulePullbackCompIso B S hS f' g).inv.app K.obj) :
              (quasicoherentDerivedModulePullback g').obj
                  ((quasicoherentDerivedModulePullback f).obj K) ⟶
                (quasicoherentDerivedModulePullback f').obj
                  ((quasicoherentDerivedModulePullback g).obj K))).app
            ((quasicoherentDerivedModulePullback g').obj
              ((quasicoherentDerivedRightAdjoint hZ f hXqc hXqs hYqs).obj
                (derivedStructureSheaf B S hS Y.1 Y.2))) ≫
          ((quasicoherentDerivedTensor B S hS X').obj ((quasicoherentDerivedModulePullback f').obj
              ((quasicoherentDerivedModulePullback g).obj K))).map
            ((quasicoherentDerivedRightAdjointBaseChangeMap hZ sq hXqc hXqs hYqs hY'qc hY'qs
                hTor).app (derivedStructureSheaf B S hS Y.1 Y.2) ≫
              (quasicoherentDerivedRightAdjoint hZ f'
                (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc)
                (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) hY'qs).map
                (ObjectProperty.homMk
                  (smallEtaleDerivedModulePullbackUnitIso (B := B) (S := S) (hS := hS) g).hom :
                  (quasicoherentDerivedModulePullback g).obj
                      (derivedStructureSheaf B S hS Y.1 Y.2) ⟶
                    derivedStructureSheaf B S hS Y'.1 Y'.2)) ≫
            (quasicoherentDerivedCompareWithPullback hZ f'
              (isQuasiCompactSpace_of_isPullback hZ sq hXqc hYqs hY'qc)
              (isAbsolutelyQuasiSeparated_of_isPullback hZ sq hXqs hY'qs) hY'qs).app
              ((quasicoherentDerivedModulePullback g).obj K)

Sources

Section86.8 Right adjoint of pushforward for proper flat morphisms #

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

Tag 0E5T, a lemma

Tag 0E5T in the Stacks Project.

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

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

theorem preservesCoproducts_rightAdjoint_quasicoherentDerivedPushforward_of_isProper
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y.1) (hf : IsProper B S hS f.hom)
    (hfl : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom) :
    haveI := isLeftAdjoint_quasicoherentDerivedPushforward hZ f
      (isQuasiCompactSpace_of_isQuasiCompact B S hS Y.2 hYqc f.hom hfp.2.1)
      (isAbsolutelyQuasiSeparated_of_isQuasiSeparated B S hS hZ X.2 hYqs hfp.2.2) hYqs
    ∀ I : Type u, PreservesColimitsOfShape (Discrete I)
      (quasicoherentDerivedPushforward B S hS f hfp.2.1 hfp.2.2).rightAdjoint

Tag 0E5U, a lemma

Tag 0E5U in the Stacks Project.

AlgebraicGeometry.Space.isIso_quasicoherentDerivedCompareWithPullback_app_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityPullbackComparisonProperFlat.lean, line 43.

Let Y be a quasi-compact and quasi-separated algebraic space and f : X ⟶ Y a proper, flat morphism of finite presentation, with right adjoint a of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) (Stacks 0E55). The map Lf^*K ⊗^L a(𝒪_Y) ⟶ a(K) of Stacks 0E5P is an isomorphism for every K ∈ D_QCoh(𝒪_Y).

theorem isIso_quasicoherentDerivedCompareWithPullback_app_of_isProper
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y.1) (hf : IsProper B S hS f.hom)
    (hfl : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (K : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2) :
    IsIso ((quasicoherentDerivedCompareWithPullback hZ f
      (isQuasiCompactSpace_of_isQuasiCompact B S hS Y.2 hYqc f.hom hfp.2.1)
      (isAbsolutelyQuasiSeparated_of_isQuasiSeparated B S hS hZ X.2 hYqs hfp.2.2) hYqs).app K)

Tag 0E5V, a lemma

Tag 0E5V in the Stacks Project.

AlgebraicGeometry.Space.isLE_derivedModulePushforward_affineRightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DualityRelativeDualizingAffineBounds.lean, line 50. The attribute's comment: “(2)”.

Stacks 0E5V (2). For Y affine and f : X ⟶ Y proper, flat and of finite presentation, Rf_* a(𝒪_Y) has vanishing cohomology sheaves in positive degrees.

theorem isLE_derivedModulePushforward_affineRightAdjoint (hf : IsProper B S hS f.hom)
    (hfl : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (hY : IsAffineSpace B S hS Y.1) :
    ((derivedModulePushforward B S hS f).obj
      ((affineRightAdjoint hZ f hfp hY).obj
        (derivedStructureSheaf B S hS Y.1 Y.2)).obj).IsLE 0

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

Stacks 0E5V (1). For Y affine and f : X ⟶ Y proper, flat and of finite presentation, with a the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y), the object a(𝒪_Y) of D(𝒪_X) is Y-perfect.

theorem isPerfectRelativeToCanonical_affineRightAdjoint {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsProper B S hS f.hom) (hfl : IsFlat B S hS f.hom)
    (hfp : IsFinitePresentation B S hS f.hom) (hY : IsAffineSpace B S hS Y.1) :
    IsPerfectRelativeToCanonical.{u, u + 1, u + 1} B S hS f hfl hfp.1
      ((affineRightAdjoint hZ f hfp hY).obj (derivedStructureSheaf B S hS Y.1 Y.2)).obj

AlgebraicGeometry.Space.isIso_smallEtaleDerivedHomothety_affineRightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplexAffinePerfect.lean, line 114. The attribute's comment: “(3)”.

Stacks 0E5V (3). For Y affine and f : X ⟶ Y proper, flat and of finite presentation, with a the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y), the map 𝒪_X ⟶ R𝓗om(a(𝒪_Y), a(𝒪_Y)) is an isomorphism.

theorem isIso_smallEtaleDerivedHomothety_affineRightAdjoint {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsProper B S hS f.hom) (hfl : IsFlat B S hS f.hom)
    (hfp : IsFinitePresentation B S hS f.hom) (hY : IsAffineSpace B S hS Y.1) :
    IsIso (smallEtaleDerivedHomothety B S hS X
      ((affineRightAdjoint hZ f hfp hY).obj (derivedStructureSheaf B S hS Y.1 Y.2)).obj)

Sources

LeanAlgebraicGeometry.Space.preservesCoproducts_rightAdjoint_quasicoherentDerivedPushforward_of_isProper · AlgebraicGeometry.Space.isIso_quasicoherentDerivedCompareWithPullback_app_of_isProper · AlgebraicGeometry.Space.isLE_derivedModulePushforward_affineRightAdjoint · AlgebraicGeometry.Space.isPerfectRelativeToCanonical_affineRightAdjoint · AlgebraicGeometry.Space.isIso_smallEtaleDerivedHomothety_affineRightAdjoint

Section86.9 Relative dualizing complexes for proper flat morphisms #

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

Tag 0E5X, a definition

Tag 0E5X in the Stacks Project.

AlgebraicGeometry.Space.RelativeDualizingComplex, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplex.lean, line 189.

Let f : X ⟶ Y be a proper, flat morphism of algebraic spaces over S of finite presentation. A relative dualizing complex for X/Y is a pair (ω, τ) of a Y-perfect object ω of D(𝒪_X) and a map τ : Rf_* ω ⟶ 𝒪_Y such that for every cartesian square g' ≫ f = f' ≫ g with Y' an affine scheme, the pair (L(g')^* ω, Lg^* τ) is isomorphic to the pair (a'(𝒪_{Y'}), Tr_{f', 𝒪_{Y'}}) of the right adjoint a' of Rf'_* (Stacks 0E55) and its trace map (Stacks 0E5K).

structure RelativeDualizingComplex {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (_hf : IsProper B S hS f.hom) (hfl : IsFlat B S hS f.hom)
    (hfp : IsFinitePresentation B S hS f.hom) extends RelativeDualizingPair f hfl hfp

Tag 0E5Y, a lemma

Tag 0E5Y in the Stacks Project.

AlgebraicGeometry.Space.RelativeDualizingComplex.isIso_smallEtaleDerivedHomothety_and_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplexAffinePerfect.lean, line 159.

Stacks 0E5Y. Let f : X ⟶ Y be a proper, flat morphism of algebraic spaces of finite presentation. For a relative dualizing complex (ω, τ), the map 𝒪_X ⟶ R𝓗om(ω, ω) is an isomorphism and Rf_* ω has vanishing cohomology sheaves in positive degrees.

theorem isIso_smallEtaleDerivedHomothety_and_isLE (ω : RelativeDualizingComplex hZ f hf hfl hfp) :
    IsIso (smallEtaleDerivedHomothety B S hS X ω.ω) ∧
      ((derivedModulePushforward B S hS f).obj ω.ω).IsLE 0

Tag 0E5Z, a lemma

Tag 0E5Z in the Stacks Project.

AlgebraicGeometry.Space.RelativeDualizingComplex.existsUnique_iso_of_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplexAffinePerfect.lean, line 169.

Stacks 0E5Z. Let f : X ⟶ Y be a proper, flat morphism of algebraic spaces of finite presentation. Two relative dualizing complexes (ω₁, τ₁), (ω₂, τ₂) on X/Y have a unique isomorphism of pairs: a unique e : ω₁ ≅ ω₂ with τ₂ ∘ Rf_* e = τ₁.

theorem existsUnique_iso_of_relativeDualizingComplex
    (D₁ D₂ : RelativeDualizingComplex hZ f hf hfl hfp) :
    ∃! e : D₁.ω ≅ D₂.ω, (derivedModulePushforward B S hS f).map e.hom ≫ D₂.τ = D₁.τ

Tag 0E60, a lemma

Tag 0E60 in the Stacks Project.

AlgebraicGeometry.Space.RelativeDualizingPair.isAffineBaseChangePair_of_isEtaleCovering_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplexAffinePerfect.lean, line 189.

Stacks 0E60. Let f : X ⟶ Y be a proper, flat morphism of algebraic spaces of finite presentation, (ω, τ) a pair of a Y-perfect object of D(𝒪_X) and a map τ : Rf_* ω ⟶ 𝒪_Y, and X_i ⟶ Y_i the base changes of f to the members of an étale covering {Y_i ⟶ Y} by affines, over which (ω, τ) is isomorphic to (a_i(𝒪_{Y_i}), Tr). Then (ω, τ) is a relative dualizing complex: its base change to every affine Y' is isomorphic to (a'(𝒪_{Y'}), Tr).

theorem isAffineBaseChangePair_of_isEtaleCovering_of_isProper
    (P : RelativeDualizingPair f hfl hfp) (hf : IsProper B S hS f.hom)
    {ι : Type v} {Yi Xi : ι → AlgebraicSpaces B S hS} {fi : ∀ i, Xi i ⟶ Yi i}
    {gi : ∀ i, Yi i ⟶ Y} {g'i : ∀ i, Xi i ⟶ X} (sqi : ∀ i, IsPullback (g'i i) (fi i) f (gi i))
    (hYi : ∀ i, IsAffineSpace B S hS (Yi i).1)
    (hcov : IsEtaleCovering B S hS (fun i => (Yi i).1) (fun i => (gi i).hom))
    (hi : ∀ i, IsAffineBaseChangePair hZ (sqi i) hfp (hYi i) P.ω P.τ)
    ⦃X' Y' : AlgebraicSpaces B S hS⦄ (f' : X' ⟶ Y') (g : Y' ⟶ Y) (g' : X' ⟶ X)
    (sq : IsPullback g' f' f g) (hY' : IsAffineSpace B S hS Y'.1) :
    IsAffineBaseChangePair hZ sq hfp hY' P.ω P.τ

Tag 0E61, a lemma

Tag 0E61 in the Stacks Project.

AlgebraicGeometry.Space.RelativeDualizingComplex.nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplexExistence.lean, line 412.

Stacks 0E61: existence of relative dualizing complexes. Let f : X ⟶ Y be a proper, flat morphism of algebraic spaces over S which is of finite presentation. Then there exists a relative dualizing complex (ω_{X/Y}, τ) for X/Y (Stacks 0E5X).

theorem RelativeDualizingComplex.nonempty (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (hfl : IsFlat B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom) :
    Nonempty (RelativeDualizingComplex hZ f hf hfl hfp)

Tag 0E6C, a lemma

Tag 0E6C in the Stacks Project.

AlgebraicGeometry.Space.RelativeDualizingComplex.baseChange_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeDualizingComplexBaseChange.lean, line 237.

Stacks 0E6C. Let g' ≫ f = f' ≫ g be a cartesian square of algebraic spaces over S with f : X ⟶ Y proper, flat and of finite presentation, and let (ω, τ) be a relative dualizing complex for f. Then (L(g')^* ω, Lg^* τ) is a relative dualizing complex for f': L(g')^* ω is Y'-perfect, and the map τ' : Rf'_* L(g')^* ω ⟶ 𝒪_{Y'} which is Lg^* τ through the base change map has the base change property of Stacks 0E5X.

theorem baseChange_spec :
    IsPerfectRelativeToCanonical.{u, u + 1, u + 1} B S hS f'
        ((isFlat_isStableUnderBaseChange B S hS).of_isPullback sq hfl)
        ((isLocallyOfFinitePresentation_isStableUnderBaseChange B S hS).of_isPullback sq
          hfp.1)
        ((smallEtaleDerivedModulePullback B S hS g').obj D.ω) ∧
      ∃ τ' : (derivedModulePushforward B S hS f').obj
          ((smallEtaleDerivedModulePullback B S hS g').obj D.ω) ⟶
            (derivedStructureSheaf B S hS Y'.1 Y'.2).obj,
        smallEtaleDerivedModuleBaseChangeMap B S hS f g f' g' sq.w D.ω ≫ τ' =
            (smallEtaleDerivedModulePullback B S hS g).map D.τ ≫
              (smallEtaleDerivedModulePullbackUnitIso (B := B) (S := S) (hS := hS) g).hom ∧
          ∀ ⦃X'' Y'' : AlgebraicSpaces B S hS⦄ (f'' : X'' ⟶ Y'') (h : Y'' ⟶ Y')
            (g'' : X'' ⟶ X') (sq₂ : IsPullback g'' f'' f' h) (hY'' : IsAffineSpace B S hS Y''.1),
            IsAffineBaseChangePair hZ sq₂
              ((isFinitePresentation_isStableUnderBaseChange B S hS).of_isPullback sq hfp)
              hY'' ((smallEtaleDerivedModulePullback B S hS g').obj D.ω) τ'

Sources

LeanAlgebraicGeometry.Space.RelativeDualizingComplex · AlgebraicGeometry.Space.RelativeDualizingComplex.isIso_smallEtaleDerivedHomothety_and_isLE · AlgebraicGeometry.Space.RelativeDualizingComplex.existsUnique_iso_of_relativeDualizingComplex · AlgebraicGeometry.Space.RelativeDualizingPair.isAffineBaseChangePair_of_isEtaleCovering_of_isProper · AlgebraicGeometry.Space.RelativeDualizingComplex.nonempty · AlgebraicGeometry.Space.RelativeDualizingComplex.baseChange_spec

Section86.10 Comparison with the case of schemes #

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

Tag 0E6E, a lemma

Tag 0E6E in the Stacks Project.

AlgebraicGeometry.Space.representedRightAdjointIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentedRightAdjointDuality.lean, line 87.

Stacks 0E6E. Let f : X ⟶ Y be the morphism of quasi-compact and quasi-separated representable algebraic spaces over S represented by a morphism g : T' ⟶ T of the big fppf site, with underlying morphism of schemes f_0 = g_0 : X_0 ⟶ Y_0. Let a be the right adjoint of Rf_* : D_QCoh(𝒪_X) ⥤ D_QCoh(𝒪_Y) of Stacks 0E55 and a_0 the right adjoint of Rf_{0,*} : D_QCoh(𝒪_{X_0}) ⥤ D_QCoh(𝒪_{Y_0}) of Stacks 0A9E. Then a_0 and a correspond under the equivalences D_QCoh(𝒪_{X_0}) ≌ D_QCoh(𝒪_X), D_QCoh(𝒪_{Y_0}) ≌ D_QCoh(𝒪_Y) of Stacks 071Q.

def representedRightAdjointIso :
    haveI : CompactSpace (B.inclusion.obj T'.left) :=
      compactSpace_of_isQuasiCompactSpace_yoneda_obj B S hS hXqc
    haveI : QuasiSeparatedSpace (B.inclusion.obj T'.left) :=
      (isAbsolutelyQuasiSeparated_yoneda_iff_quasiSeparatedSpace B S hS hZ T').1 hXqs
    haveI : CompactSpace (B.inclusion.obj T.left) :=
      compactSpace_of_isQuasiCompactSpace_yoneda_obj B S hS hYqc
    haveI : QuasiSeparatedSpace (B.inclusion.obj T.left) :=
      (isAbsolutelyQuasiSeparated_yoneda_iff_quasiSeparatedSpace B S hS hZ T).1 hYqs
    haveI :=
      Stacks.Duality.DerivedPushforward.isLeftAdjoint_qcqsRestrictedDerivedPushforward_of_qcqs
        (B.inclusion.map g.left)
    haveI := isLeftAdjoint_quasicoherentDerivedPushforward hZ (representedSpaceMap B S hS g)
      hXqc hXqs hYqs
    (Stacks.Duality.DerivedPushforward.qcqsRestrictedDerivedPushforward
        (B.inclusion.map g.left)).rightAdjoint ⋙
        (representedDualityQuasicoherentDerivedEquivalence B S hS T').functor ≅
      (representedDualityQuasicoherentDerivedEquivalence B S hS T).functor ⋙
        (quasicoherentDerivedPushforward B S hS (representedSpaceMap B S hS g)
          (representedSpaceMap_isQuasiCompact hZ g hXqc hYqs)
          (representedSpaceMap_isQuasiSeparated hZ g hXqs)).rightAdjoint

Sources

LeanAlgebraicGeometry.Space.representedRightAdjointIso

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

86 Duality for Spaces

Section86.2 Dualizing complexes on algebraic spaces#

Tag 0E4Y, a lemma

Tag 0E4Z, a definition

Tag 0E50, a lemma

Tag 0E51, a lemma

Tag 0E52, a lemma

Tag 0E53, a lemma

Sources

Section86.3 Right adjoint of pushforward#

Tag 0E55, a lemma

Tag 0E56, a lemma

Tag 0E57, an equation

Tag 0E58, a lemma

Tag 0GG3, an example

Tag 0GG4, a remark

Tag 0GG5, an example

Tag 0E59, a lemma

Sources

Section86.4 Right adjoint of pushforward and base change, I#

Tag 0E5B, an equation

Tag 0E5C, a lemma

Tag 0E5D, an equation

Tag 0E5E, a lemma

Tag 0E5F, a lemma

Tag 0E5G, a remark

Sources

Section86.5 Right adjoint of pushforward and base change, II#

Tag 0E5I, a lemma

Sources

Section86.6 Right adjoint of pushforward and trace maps#

Tag 0E5L, a lemma

Tag 0E5M, a lemma

Sources

Section86.7 Right adjoint of pushforward and pullback#

Tag 0E5P, an equation

Tag 0E5Q, a lemma

Tag 0E5R, a lemma

Sources

Section86.8 Right adjoint of pushforward for proper flat morphisms#

Tag 0E5T, a lemma

Tag 0E5U, a lemma

Tag 0E5V, a lemma

Sources

Section86.9 Relative dualizing complexes for proper flat morphisms#

Tag 0E5X, a definition

Tag 0E5Y, a lemma

Tag 0E5Z, a lemma

Tag 0E60, a lemma

Tag 0E61, a lemma

Tag 0E6C, a lemma

Sources

Section86.10 Comparison with the case of schemes#

Tag 0E6E, a lemma

Sources

Section86.2 Dualizing complexes on algebraic spaces #

Section86.3 Right adjoint of pushforward #

Section86.4 Right adjoint of pushforward and base change, I #

Section86.5 Right adjoint of pushforward and base change, II #

Section86.6 Right adjoint of pushforward and trace maps #

Section86.7 Right adjoint of pushforward and pullback #

Section86.8 Right adjoint of pushforward for proper flat morphisms #

Section86.9 Relative dualizing complexes for proper flat morphisms #

Section86.10 Comparison with the case of schemes #