48.32 Compactly supported… to 48.34 Lichtenbaum's theorem

Section48.32 Compactly supported cohomology for coherent modules#

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

Tag 0G50, a lemma

Tag 0G50 in the Stacks Project.

AlgebraicGeometry.lowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/CompactificationShriek.lean, line 388.

Stacks Project, Tag 0G50. In Situation [Stacks, Tag 0F42] let f : X ⟶ Y be a morphism of FTS_S. The functor Rf_! = Rf̄_* ∘ Rj_! of [Stacks, Section 0G4Z] (AlgebraicGeometry.lowerShriek) is, up to isomorphism, independent of the choice of the compactification j : X ⟶ X̄ of X over Y.

The proof is the source's. Two compactifications X̄₁, X̄₂ are dominated by a third, the scheme-theoretic closure X̄₃ of X in X̄₁ ×_Y X̄₂ (the closure of AlgebraicGeometry.compactificationPairMap; that X ⟶ X̄₃ is an open immersion is because X ⟶ X̄₁ ×_Y X̄₂ is a quasi-compact immersion), which is cofilteredness of the category of compactifications for these two objects; and a morphism g : X̄₃ ⟶ X̄ᵢ of compactifications gives Rf̄ᵢ_* ∘ Rjᵢ_! ≅ Rf̄ᵢ_* ∘ Rg_* ∘ Rj₃_! ≅ Rf̄₃_* ∘ Rj₃_! by [Stacks, Tag 0G4X] (AlgebraicGeometry.lowerShriekIsoOfFactor).

public def lowerShriekIso : lowerShriek f c₁ ≅ lowerShriek f c₂

CategoryTheory.Compactification.shriekImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/Independence.lean, line 120. The attribute's comment: “the per-compactification data, the cofilteredness of the category of compactifications, and the isomorphisms attached to its morphisms by Tag 0G4X, supplied as data”.

Stacks Project, Tag 0G50. The functor Rf_! is, up to isomorphism, independent of the choice of the compactification.

The compactifications of X over Y are the objects of a cofiltered category 𝒦, each carrying the data of a CategoryTheory.Compactification, and each morphism of 𝒦 induces an isomorphism of the attached functors Rf_! — the isomorphism of [Stacks, Tag 0G4X], produced by CategoryTheory.Compactification.shriekImageIsoOfMorphism. Any two compactifications are then dominated by a third, and the two isomorphisms to it compose to one between them.

public def shriekImageIso {𝒦 : Type w₁} [Category.{w₂} 𝒦] [IsCofiltered 𝒦] {ℳ : 𝒦 → Type u₃}
    [∀ c, Category.{v} (ℳ c)] (C : ∀ c, Compactification 𝒞 𝒟 (ℳ c))
    (e : ∀ {c c' : 𝒦}, (c ⟶ c') → ((C c').shriekImage ≅ (C c).shriekImage)) (c c' : 𝒦) :
    (C c).shriekImage ≅ (C c').shriekImage

CategoryTheory.CompactificationData.shriekImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/IndependenceLan.lean, line 51. The attribute's comment: “the per-compactification data, the cofilteredness of the category of compactifications, and the isomorphisms attached to its morphisms by Tag 0G4X, supplied as data”.

The functor Rf_! is, up to isomorphism, independent of the choice of the compactification.

The compactifications of X over Y are the objects of a cofiltered category 𝒦, each carrying the data of a CategoryTheory.CompactificationData, and each morphism of 𝒦 induces an isomorphism of the attached functors Rf_!, that of Stacks, Tag 0G4X. The isomorphism between the functors of c and c' is the composite of the isomorphisms to the functor of a compactification dominating both.

public def shriekImageIso {𝒦 : Type w₁} [Category.{w₂} 𝒦] [IsCofiltered 𝒦] {ℳ : 𝒦 → Type u₃}
    [∀ c, Category.{v} (ℳ c)] (C : ∀ c, CompactificationData 𝒞 𝒟 (ℳ c))
    [∀ c (A : ℳ c ⥤ Type v), (C c).direct.HasLeftKanExtension A]
    (e : ∀ {c c' : 𝒦}, (c ⟶ c') → ((C c').shriekImage ≅ (C c).shriekImage)) (c c' : 𝒦) :
    (C c).shriekImage ≅ (C c').shriekImage
Tag 0G51, a proposition

Tag 0G51 in the Stacks Project.

AlgebraicGeometry.lowerShriekHomIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekAdjunction.lean, line 443.

In Situation [Stacks, Tag 0F42] let f : X ⟶ Y be a morphism of FTS_S. Then Rf_! and f^! are adjoint in the following sense: for K in D^b_{Coh}(𝒪_X) and L in D^+_{Coh}(𝒪_Y)

Hom_X(K, f^! L) = Hom_{Pro-D^+_{Coh}(𝒪_Y)}(Rf_! K, L),

bifunctorially in K and L: an isomorphism of functors D^b_{Coh}(𝒪_X)ᵒᵖ ⥤ D^+_{Coh}(𝒪_Y) ⥤ Type, with components AlgebraicGeometry.lowerShriekHomEquiv. Here Rf_! and f^! are computed at an arbitrary compactification c of X over Y, Rf_! K is viewed in Pro-D^+_{Coh}(𝒪_Y) through D^b_{Coh} ⊆ D^+_{Coh}, and f^! L is read at the standard model of D(𝒪_X) (Stacks.Duality.UpperShriekDuality.upperShriekStd).

def lowerShriekHomIso :
    (lowerShriek f c ⋙ ProSeq.map (boundedCoherentToPlusCoh Y₁.left)).op ⋙ coyoneda ⋙
        (Functor.whiskeringLeft _ _ _).obj ProSeq.const ≅
      (boundedCoherentDerived X₁.left).ι.op ⋙ coyoneda ⋙
        (Functor.whiskeringLeft _ _ _).obj (upperShriekStd f c)
Tag 0G52, a lemma

Tag 0G52 in the Stacks Project.

AlgebraicGeometry.exists_shriekImage_distTriang_system, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/ShriekTrianglesData.lean, line 390.

In Situation [Stacks, Tag 0F42] let f : X ⟶ Y be a morphism of FTS_S and let

K ⟶ L ⟶ M ⟶ K[1]

be a distinguished triangle of D^b_{Coh}(𝒪_X). Then there is an inverse system of distinguished triangles

K_n ⟶ L_n ⟶ M_n ⟶ K_n[1]

of D^b_{Coh}(𝒪_Y) such that the pro-systems (K_n), (L_n) and (M_n) give Rf_! K, Rf_! L and Rf_! M.

Here Rf_! = Rf̄_* ∘ Rj_! is AlgebraicGeometry.lowerShriek f c, the functor of [Stacks, Section 0G4Z] attached to a compactification c, j : X ⟶ X̄, of X over Y with structure morphism f̄ : X̄ ⟶ Y: Rj_! is the extension by zero of [Stacks, Tag 0G4N] and Rf̄_* is the derived direct image D^b_{Coh}(𝒪_{X̄}) ⥤ D^b_{Coh}(𝒪_Y), applied termwise to pro-objects. The statement holds for every compactification; by [Stacks, Tag 0G50] the functor does not depend on it.

The proof is the source's. [Stacks, Tag 0G4M] for j (AlgebraicGeometry.DeligneTriangle.exists_extensionByZero_distTriang) gives an inverse system of distinguished triangles K̄_n ⟶ L̄_n ⟶ M̄_n ⟶ K̄_n[1] of D^b_{Coh}(𝒪_{X̄}) whose vertex systems give Rj_! K, Rj_! L and Rj_! M; the system K_n = Rf̄_* K̄_n, and likewise for L_n and M_n, works by the very definition of Rf_! (CategoryTheory.CompactificationData.exists_shriekImage_distTriang_system).

public theorem exists_shriekImage_distTriang_system (f : X₁ ⟶ Y₁)
    (c : CompactificationOf (Over.mk f.left)) (T : Triangle (BoundedCoherentDerived X₁.left))
    (hT : T ∈ distTriang (BoundedCoherentDerived X₁.left)) :
    ∃ TY : ℕᵒᵖ ⥤ Triangle (BoundedCoherentDerived Y₁.left),
      (∀ n, TY.obj n ∈ distTriang (BoundedCoherentDerived Y₁.left)) ∧
      Nonempty (ProSeq.of (TY ⋙ Triangle.π₁) ≅ (lowerShriek f c).obj T.obj₁) ∧
      Nonempty (ProSeq.of (TY ⋙ Triangle.π₂) ≅ (lowerShriek f c).obj T.obj₂) ∧
      Nonempty (ProSeq.of (TY ⋙ Triangle.π₃) ≅ (lowerShriek f c).obj T.obj₃)
Tag 0G53, a remark

Tag 0G53 in the Stacks Project.

CategoryTheory.Pro.exists_diagonalRepresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/DiagonalRepresentation.lean, line 494. The attribute's comment: “diagonal_representation”.

Stacks Project, Tag 0G53 (diagonal representation). A countable inverse system of pro-objects, each represented by an inverse sequence, has a diagonal inverse-sequence representation. Equivalently, naturally in N, colim_i colim_n Hom(M_{i,n}, N) is colim_k Hom(D_k, N).

public theorem exists_diagonalRepresentation {C : Type u} [Category.{v} C]
    (P : Functor ℕ (Functor C (Type v))) (M : ℕ → Functor ℕᵒᵖ C)
    (e : ∀ i, P.obj i ≅ Pro.coyonedaColim (liftedInverseSequence (M i))) :
    Nonempty (DiagonalRepresentation P M e)

CategoryTheory.Pro.diagonalRepresentation_uniqueUpToIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/DiagonalUniqueness.lean, line 39. The attribute's comment: “diagonal_uniqueness”.

The diagonal inverse sequence is uniquely pro-isomorphic to any other representation G of the same functor of points: there is a unique pro-morphism to G compatible with the comparison isomorphisms, and it has a two-sided inverse.

public theorem diagonalRepresentation_uniqueUpToIso {C : Type u} [Category.{v} C]
    (P : Functor ℕ (Functor C (Type v))) (M : ℕ → Functor ℕᵒᵖ C)
    (e : ∀ i, P.obj i ≅ Pro.coyonedaColim (liftedInverseSequence (M i)))
    (r : DiagonalRepresentation P M e) {I : Type v} [Category.{v} I]
    (G : Functor I C) (eG : colimit P ≅ Pro.coyonedaColim G) :
    ∃! φ : Pro.Hom (liftedInverseSequence r.system) G,
      (∃ ψ : Pro.Hom G (liftedInverseSequence r.system),
        (Pro.homEquiv G (liftedInverseSequence r.system)).symm ψ ≫
            (Pro.homEquiv (liftedInverseSequence r.system) G).symm φ =
          𝟙 (Pro.coyonedaColim (liftedInverseSequence r.system)) ∧
        (Pro.homEquiv (liftedInverseSequence r.system) G).symm φ ≫
            (Pro.homEquiv G (liftedInverseSequence r.system)).symm ψ =
          𝟙 (Pro.coyonedaColim G)) ∧
      eG.hom ≫ (Pro.homEquiv (liftedInverseSequence r.system) G).symm φ =
        r.comparison.hom
Tag 0G54, a remark

Tag 0G54 in the Stacks Project.

CategoryTheory.Pro.exists_compositionRepresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/Composition.lean, line 66. The attribute's comment: “the composition, for pro-object-valued functors with countable-index representations supplied as data”.

The composition of two compactly supported direct images: the termwise image under G of an inverse sequence M is represented by an inverse sequence in the target category.

public theorem exists_compositionRepresentation {C : Type u'} [Category.{v'} C] {D : Type u}
    [Category.{v} D] (G : Cᵒᵖ ⥤ D ⥤ Type v) (S : C → ℕᵒᵖ ⥤ D)
    (e : ∀ L : C, G.obj (op L) ≅ Pro.coyonedaColim (liftedInverseSequence (S L)))
    (M : ℕᵒᵖ ⥤ C) : Nonempty (CompositionRepresentation G M)

CategoryTheory.Pro.CompositionRepresentation.homColimitIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/Composition.lean, line 78. The attribute's comment: “the Hom-colimit formula, for pro-object-valued functors with countable-index representations supplied as data”.

Stacks Project, Tag 0G54, the displayed formula: for every object L, the colimit over n of Hom(G (M n), L) is the colimit over k of Hom(system_k, L).

public noncomputable def CompositionRepresentation.homColimitIso {C : Type u'} [Category.{v'} C]
    {D : Type u} [Category.{v} D] {G : Cᵒᵖ ⥤ D ⥤ Type v} {M : ℕᵒᵖ ⥤ C}
    (r : CompositionRepresentation G M) (L : D) :
    colimit ((M.rightOp ⋙ G) ⋙ (evaluation D (Type v)).obj L) ≅
      colimit ((liftedInverseSequence r.system).op ⋙ coyoneda ⋙
        (evaluation D (Type v)).obj L)

CategoryTheory.Pro.compositionRepresentation_uniqueUpToIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/Composition.lean, line 92. The attribute's comment: “uniqueness up to pro-isomorphism, for pro-object-valued functors with countable-index representations supplied as data”.

Stacks Project, Tag 0G54, uniqueness: two inverse sequences representing the termwise image of M under G are uniquely pro-isomorphic over their comparison isomorphisms. The pro-morphism and its inverse are expressed through Stacks 0G2X.

public theorem compositionRepresentation_uniqueUpToIso {C : Type u'} [Category.{v'} C]
    {D : Type u} [Category.{v} D] (G : Cᵒᵖ ⥤ D ⥤ Type v) (M : ℕᵒᵖ ⥤ C)
    (r r' : CompositionRepresentation G M) :
    ∃! φ : Pro.Hom (liftedInverseSequence r.system) (liftedInverseSequence r'.system),
      (∃ ψ : Pro.Hom (liftedInverseSequence r'.system) (liftedInverseSequence r.system),
        (Pro.homEquiv (liftedInverseSequence r'.system)
              (liftedInverseSequence r.system)).symm ψ ≫
            (Pro.homEquiv (liftedInverseSequence r.system)
              (liftedInverseSequence r'.system)).symm φ =
          𝟙 (Pro.coyonedaColim (liftedInverseSequence r.system)) ∧
        (Pro.homEquiv (liftedInverseSequence r.system)
              (liftedInverseSequence r'.system)).symm φ ≫
            (Pro.homEquiv (liftedInverseSequence r'.system)
              (liftedInverseSequence r.system)).symm ψ =
          𝟙 (Pro.coyonedaColim (liftedInverseSequence r'.system))) ∧
      r'.comparison.hom ≫ (Pro.homEquiv (liftedInverseSequence r.system)
          (liftedInverseSequence r'.system)).symm φ = r.comparison.hom

AlgebraicGeometry.lowerShriekComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/CompositionLowerShriek.lean, line 216. The attribute's comment: “the definition of Rg_! Rf_! K”.

Stacks Project, Tag 0G54, the definition. In Situation [Stacks, Tag 0F42] let f : X ⟶ Y and g : Y ⟶ Z be composable morphisms of FTS_S, with compactifications cf of X over Y and cg of Y over Z defining Rf_! and Rg_! ([Stacks, Section 0G4Z], AlgebraicGeometry.lowerShriek). For K in D^b_{Coh}(𝒪_X), Rf_! K is given by an inverse system (M_n) of D^b_{Coh}(𝒪_Y) (AlgebraicGeometry.lowerShriekObjIso), (Rg_! M_n) is an inverse system of Pro-D^b_{Coh}(𝒪_Z), and Rg_! Rf_! K is the pro-object of D^b_{Coh}(𝒪_Z) given by [Stacks, Tag 0G53] with

Hom(Rg_! Rf_! K, L) = colim_n Hom(Rg_! M_n, L)

for every L (AlgebraicGeometry.lowerShriekCompPointsIso); it is unique up to pro-isomorphism (AlgebraicGeometry.nonempty_iso_lowerShriekComp_iff) and does not depend on the inverse system (M_n) chosen. Functoriality in K is omitted, as in the source.

public noncomputable def lowerShriekComp (f : X ⟶ Y) (g : Y ⟶ Z)
    (cf : CompactificationOf (Over.mk f.left)) (cg : CompactificationOf (Over.mk g.left))
    (K : BoundedCoherentDerived X.left) : ProSeq (BoundedCoherentDerived Z.left)

AlgebraicGeometry.lowerShriekCompPointsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/CompositionLowerShriek.lean, line 229. The attribute's comment: “Hom(Rg_! Rf_! K, L) = colim_n Hom(Rg_! M_n, L) for every inverse system (M_n) giving Rf_! K”.

Stacks Project, Tag 0G54, the defining property: for every inverse system (M_n) of D^b_{Coh}(𝒪_Y) giving Rf_! K,

Hom(Rg_! Rf_! K, L) = colim_n Hom(Rg_! M_n, L)

naturally in L in D^b_{Coh}(𝒪_Z).

public noncomputable def lowerShriekCompPointsIso (f : X ⟶ Y) (g : Y ⟶ Z)
    (cf : CompactificationOf (Over.mk f.left)) (cg : CompactificationOf (Over.mk g.left))
    (K : BoundedCoherentDerived X.left) {M : ℕᵒᵖ ⥤ BoundedCoherentDerived Y.left}
    (e : ProSeq.of M ≅ (lowerShriek f cf).obj K) :
    (lowerShriekComp f g cf cg K).points ≅
      colimit (M.rightOp ⋙ ProSeq.pointsFunctor (lowerShriek g cg))

AlgebraicGeometry.lowerShriekCompHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/CompositionLowerShriek.lean, line 242. The attribute's comment: “Hom_Pro(Rg_! Rf_! K, L) = colim_n Hom_Pro(Rg_! M_n, L)”.

Stacks Project, Tag 0G54, the displayed formula with Hom-sets of pro-objects: for every inverse system (M_n) giving Rf_! K and every L in D^b_{Coh}(𝒪_Z),

Hom_{Pro}(Rg_! Rf_! K, L) = colim_n Hom_{Pro}(Rg_! M_n, L).

public noncomputable def lowerShriekCompHomEquiv (f : X ⟶ Y) (g : Y ⟶ Z)
    (cf : CompactificationOf (Over.mk f.left)) (cg : CompactificationOf (Over.mk g.left))
    (K : BoundedCoherentDerived X.left) {M : ℕᵒᵖ ⥤ BoundedCoherentDerived Y.left}
    (e : ProSeq.of M ≅ (lowerShriek f cf).obj K) (L : BoundedCoherentDerived Z.left) :
    (lowerShriekComp f g cf cg K ⟶ ProSeq.const.obj L) ≃
      colimit (M.rightOp ⋙ (lowerShriek g cg).op ⋙ yoneda.obj (ProSeq.const.obj L))

AlgebraicGeometry.nonempty_iso_lowerShriekComp_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/CompositionLowerShriek.lean, line 268. The attribute's comment: “uniqueness up to pro-isomorphism”.

Stacks Project, Tag 0G54, uniqueness: for an inverse system (M_n) giving Rf_! K, an inverse system (N_k) of D^b_{Coh}(𝒪_Z) satisfies Hom((N_k), L) = colim_n Hom(Rg_! M_n, L) naturally in L if and only if it gives Rg_! Rf_! K; so Rg_! Rf_! K is the unique pro-isomorphism class with that property.

public theorem nonempty_iso_lowerShriekComp_iff (f : X ⟶ Y) (g : Y ⟶ Z)
    (cf : CompactificationOf (Over.mk f.left)) (cg : CompactificationOf (Over.mk g.left))
    (K : BoundedCoherentDerived X.left) {M : ℕᵒᵖ ⥤ BoundedCoherentDerived Y.left}
    (e : ProSeq.of M ≅ (lowerShriek f cf).obj K) (N : ℕᵒᵖ ⥤ BoundedCoherentDerived Z.left) :
    Nonempty ((ProSeq.of N).points ≅
        colimit (M.rightOp ⋙ ProSeq.pointsFunctor (lowerShriek g cg))) ↔
      Nonempty (ProSeq.of N ≅ lowerShriekComp f g cf cg K)
Tag 0G55, a lemma

Tag 0G55 in the Stacks Project.

AlgebraicGeometry.lowerShriekCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekComposition.lean, line 260.

Stacks Project, Tag 0G55. In Situation [Stacks, Tag 0F42] let f : X ⟶ Y and g : Y ⟶ Z be composable morphisms of FTS_S. With notation as in [Stacks, Tag 0G54] we have Rg_! ∘ Rf_! = R(g ∘ f)_!: for K in D^b_{Coh}(𝒪_X) the composition Rg_! Rf_! K (AlgebraicGeometry.lowerShriekComp) is isomorphic to R(g ∘ f)_! K, for arbitrary compactifications cf, cg and cfg computing Rf_!, Rg_! and R(g ∘ f)_!.

The proof is the source's: both pro-objects have the functor of points L ↦ Hom_X(K, (g ∘ f)^! L) on D^b_{Coh}(𝒪_Z), by [Stacks, Tag 0G51] for g, f and g ∘ f and f^! ∘ g^! = (g ∘ f)^! ([Stacks, Tag 0ATX]); a pro-object is determined by its functor of points ([Stacks, Tag 0G2X]).

def lowerShriekCompIso (f : X ⟶ Y) (g : Y ⟶ Z)
    (cf : CompactificationOf (Over.mk f.left)) (cg : CompactificationOf (Over.mk g.left))
    (cfg : CompactificationOf (Over.mk (f ≫ g).left)) (K : BoundedCoherentDerived X.left) :
    lowerShriekComp f g cf cg K ≅ (lowerShriek (f ≫ g) cfg).obj K
Tag 0G56, a remark

Tag 0G56 in the Stacks Project.

AlgebraicGeometry.lowerShriekOpenImmersionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovariance.lean, line 236.

Stacks Project, Tag 0G56. In Situation [Stacks, Tag 0F42] let f : X ⟶ Y be a morphism of FTS_S, let j : U ⟶ X be an open immersion and g = f ∘ j = f|_U. Then there is a canonical morphism

Rg_!(K|_U) ⟶ Rf_! K,

functorial in K in D^b_{Coh}(𝒪_X). This is the third construction of the source: for L in D^b_{Coh}(𝒪_Y),

Hom(Rf\_! K, L) = Hom\_X(K, f^! L) ⟶ Hom\_U(K|\_U, (f^! L)|\_U) = Hom\_U(K|\_U, g^! L) = Hom(Rg\_!(K|\_U), L),

by [Stacks, Tag 0G51] twice and g^! = j^* ∘ f^! (the construction of the upper shriek functors, Stacks.Duality.UpperShriekDuality.upperShriekStdPrecompOpenIso), and the functoriality in L gives the morphism of pro-objects by [Stacks, Tag 0G2X] (AlgebraicGeometry.lowerShriekMapOfHom). Rf_! and Rg_! are computed at arbitrary compactifications c and cU.

def lowerShriekOpenImmersionMap (f : X ⟶ Y) (c : CompactificationOf (Over.mk f.left))
    (j : U ⟶ X) [IsOpenImmersion j.left] (cU : CompactificationOf (Over.mk (j ≫ f).left)) :
    restrictBoundedCoherentLift j.left ⋙ lowerShriek (j ≫ f) cU ⟶ lowerShriek f c

AlgebraicGeometry.lowerShriekOpenImmersionMapOfCompactification_eq_lowerShriekOpenImmersionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovarianceAgreement.lean, line 430. The attribute's comment: “constructions (2) and (3) give the same arrow”.

The agreement of constructions (2) and (3). In Situation [Stacks, Tag 0F42] let f : X ⟶ Y be a morphism of FTS_S, i : U ⟶ X an open immersion, g = f ∘ i, and j : X ⟶ X̄ a compactification of X over Y with f̄ : X̄ ⟶ Y. The canonical map Rg_!(K|_U) ⟶ Rf_! K given by Rf̄_* applied to the map Rj'_!(K|_U) ⟶ Rj_! K of [Stacks, Tag 0G4Y], j' = j ∘ i (construction (2), AlgebraicGeometry.lowerShriekOpenImmersionMapOfCompactification), is the map induced by Hom(Rf_! K, L) = Hom_X(K, f^! L) ⟶ Hom_U(K|_U, f^! L|_U) = Hom_U(K|_U, g^! L) = Hom(Rg_!(K|_U), L) (construction (3), AlgebraicGeometry.lowerShriekOpenImmersionMap), with Rg_! computed at the compactification j'.

theorem lowerShriekOpenImmersionMapOfCompactification_eq_lowerShriekOpenImmersionMap (f : X ⟶ Y)
    (c : CompactificationOf (Over.mk f.left)) (i : U ⟶ X) [IsOpenImmersion i.left] :
    lowerShriekOpenImmersionMapOfCompactification f c i =
      lowerShriekOpenImmersionMap f c i (c.precompOpen i.left)

AlgebraicGeometry.lowerShriekOpenImmersionMapOfCompactification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovarianceCompactification.lean, line 45. The attribute's comment: “construction (2): Rf̄_* applied to the map Rj'_!(K|_U) ⟶ Rj_! K of Tag 0G4Y”.

[Stacks, Tag 0G56], construction (2). Let f : X ⟶ Y be a morphism of FTS_S, i : U ⟶ X an open immersion, c a compactification j : X ⟶ X̄ of X over Y with structure morphism f̄ : X̄ ⟶ Y, and j' = j ∘ i the induced compactification of U over Y. With Rf_! = Rf̄_* ∘ Rj_! and Rg_! = Rf̄_* ∘ Rj'_! for g = f ∘ i, the canonical map Rg_!(K|_U) ⟶ Rf_! K, functorial in K in D^b_{Coh}(𝒪_X), is Rf̄_* applied to the map Rj'_!(K|_U) ⟶ Rj_! K of [Stacks, Tag 0G4Y].

def lowerShriekOpenImmersionMapOfCompactification (f : X ⟶ Y)
    (c : CompactificationOf (Over.mk f.left)) (i : U ⟶ X) [IsOpenImmersion i.left] :
    restrictBoundedCoherentLift i.left ⋙ lowerShriek (i ≫ f) (c.precompOpen i.left) ⟶
      lowerShriek f c

AlgebraicGeometry.lowerShriekOpenImmersionMapOfComposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovarianceComposition.lean, line 407. The attribute's comment: “construction (1): Rf_! applied to the map Ri_!(K|_U) ⟶ K of Tag 0G4Y, through Rg_! = Rf_! ∘ Ri_! of Tag 0G55, functorial in K”.

In Situation [Stacks, Tag 0F42] let f : X ⟶ Y be a morphism of FTS_S, i : U ⟶ X an open immersion and g = f ∘ i. The canonical map Rg_!(K|_U) ⟶ Rf_! K, functorial in K in D^b_{Coh}(𝒪_X), obtained from Rg_! = Rf_! ∘ Ri_! ([Stacks, Tag 0G55]) and Rf_! applied to the map Ri_!(K|_U) ⟶ K of [Stacks, Tag 0G4Y] (AlgebraicGeometry.lowerShriekOpenImmersionCompMap), with Ri_! computed at the compactification X of U over X and Rg_! at the compactification restricted from the compactification c of f.

def lowerShriekOpenImmersionMapOfComposition (f : X ⟶ Y) (c : CompactificationOf (Over.mk f.left))
    (i : U ⟶ X) [IsOpenImmersion i.left] :
    restrictBoundedCoherentLift i.left ⋙ lowerShriek (i ≫ f) (c.precompOpen i.left) ⟶
      lowerShriek f c

AlgebraicGeometry.lowerShriekOpenImmersionMapOfComposition_eq_lowerShriekOpenImmersionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovarianceComposition.lean, line 421. The attribute's comment: “constructions (1) and (3) give the same arrow”.

Rf_! applied to the map Ri_!(K|_U) ⟶ K of [Stacks, Tag 0G4Y] through Rg_! = Rf_! ∘ Ri_! is the map induced by Hom(Rf_! K, L) = Hom_X(K, f^! L) ⟶ Hom_U(K|_U, g^! L) = Hom(Rg_!(K|_U), L).

theorem lowerShriekOpenImmersionMapOfComposition_eq_lowerShriekOpenImmersionMap (f : X ⟶ Y)
    (c : CompactificationOf (Over.mk f.left)) (i : U ⟶ X) [IsOpenImmersion i.left] :
    lowerShriekOpenImmersionMapOfComposition f c i =
      lowerShriekOpenImmersionMap f c i (c.precompOpen i.left)

AlgebraicGeometry.lowerShriekOpenImmersionMapOfComposition_eq_lowerShriekOpenImmersionMapOfCompactification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovarianceComposition.lean, line 432. The attribute's comment: “constructions (1) and (2) give the same arrow”.

Rf_! applied to the map Ri_!(K|_U) ⟶ K of [Stacks, Tag 0G4Y] through Rg_! = Rf_! ∘ Ri_! is Rf̄_* applied to the map Rj'_!(K|_U) ⟶ Rj_! K of [Stacks, Tag 0G4Y], for the compactification j : X ⟶ X̄.

theorem lowerShriekOpenImmersionMapOfComposition_eq_lowerShriekOpenImmersionMapOfCompactification
    (f : X ⟶ Y) (c : CompactificationOf (Over.mk f.left)) (i : U ⟶ X) [IsOpenImmersion i.left] :
    lowerShriekOpenImmersionMapOfComposition f c i =
      lowerShriekOpenImmersionMapOfCompactification f c i
Tag 0G57, a remark

Tag 0G57 in the Stacks Project.

AlgebraicGeometry.lowerShriekEtaleMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekCovariance.lean, line 307.

Stacks Project, Tag 0G57. In Situation [Stacks, Tag 0F42] let

U --h--> X --f--> Y, g = f ∘ h

be a commutative diagram of FTS_S with h étale. Then there is a canonical morphism

Rg_!(h^* K) ⟶ Rf_! K,

functorial in K in D^b_{Coh}(𝒪_X), defined by the sequence of maps

Hom(Rf\_! K, L) = Hom\_X(K, f^! L) ⟶ Hom\_U(h^* K, h^*(f^! L)) = Hom\_U(h^* K, h^! f^! L) = Hom\_U(h^* K, g^! L) = Hom(Rg\_!(h^* K), L)

for L in D^b_{Coh}(𝒪_Y): [Stacks, Tag 0G51] twice, h^* = h^! ([Stacks, Tag 0FWI]) and h^! ∘ f^! = g^! ([Stacks, Tag 0ATX]); the functoriality in L gives the morphism of pro-objects by [Stacks, Tag 0G2X] (AlgebraicGeometry.lowerShriekMapOfHom). Rf_! and Rg_! are computed at arbitrary compactifications c and cU, and h^! at the compactification of h obtained from them (Stacks.Duality.CompCompactification.restrictCompactification).

def lowerShriekEtaleMap (f : X ⟶ Y) (c : CompactificationOf (Over.mk f.left)) (h : U ⟶ X)
    [Etale h.left] (g : U ⟶ Y) (w : h ≫ f = g) (cU : CompactificationOf (Over.mk g.left)) :
    boundedCoherentPullback h.left ⋙ lowerShriek g cU ⟶ lowerShriek f c
Tag 0G58, a remark

Tag 0G58 in the Stacks Project.

AlgebraicGeometry.lowerShriekFlatQuasiFiniteMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/LowerShriekFlatQuasiFinite.lean, line 243.

Stacks Project, Tag 0G58. In Situation [Stacks, Tag 0F42] let

U --h--> X --f--> Y, g = f ∘ h

be a commutative diagram of FTS_S with h flat and quasi-finite. Then there is a canonical transformation

Rg_! ∘ h^* ⟶ Rf_!

of functors on D^b_{Coh}(𝒪_X), constructed as in [Stacks, Tag 0G57] from the transformation h^* ⟶ h^! on D^+_{Coh}(𝒪_X) (Stacks.Duality.pullbackToUpperShriekOfFlatQuasiFinite) given by h^! K = h^* K ⊗ ω_{U/X}, ω_{U/X} = h^! 𝒪_X the relative dualizing module of h ([Stacks, Tag 0B6U], [Stacks, Tag 0BV7], [Stacks, Tag 0BVG], [Stacks, Tag 0BUL]), and the trace element τ_{U/X} : 𝒪_U ⟶ ω_{U/X} ([Stacks, Tag 0BVJ]): for L in D^b_{Coh}(𝒪_Y),

Hom(Rf\_! K, L) = Hom\_X(K, f^! L) ⟶ Hom\_U(h^* K, h^* f^! L) ⟶ Hom\_U(h^* K, h^! f^! L) = Hom\_U(h^* K, g^! L) = Hom(Rg\_!(h^* K), L),

by [Stacks, Tag 0G51] twice and h^! ∘ f^! = g^! ([Stacks, Tag 0ATX]); the functoriality in L gives the morphism of pro-objects by [Stacks, Tag 0G2X] (AlgebraicGeometry.lowerShriekMapOfHom). Quasi-finiteness is LocallyQuasiFinite, morphisms of FTS_S being quasi-compact. Rf_! and Rg_! are computed at arbitrary compactifications c and cU, and h^! at the compactification of h obtained from them (Stacks.Duality.CompCompactification.restrictCompactification).

def lowerShriekFlatQuasiFiniteMap (f : X ⟶ Y) (c : CompactificationOf (Over.mk f.left))
    (h : U ⟶ X) [Flat h.left] [LocallyQuasiFinite h.left] (g : U ⟶ Y) (w : h ≫ f = g)
    (cU : CompactificationOf (Over.mk g.left)) :
    boundedCoherentPullback h.left ⋙ lowerShriek g cU ⟶ lowerShriek f c
Sources
LeanAlgebraicGeometry.lowerShriekIso · CategoryTheory.Compactification.shriekImageIso · CategoryTheory.CompactificationData.shriekImageIso · AlgebraicGeometry.lowerShriekHomIso · AlgebraicGeometry.exists_shriekImage_distTriang_system · CategoryTheory.Pro.exists_diagonalRepresentation · CategoryTheory.Pro.diagonalRepresentation_uniqueUpToIso · CategoryTheory.Pro.exists_compositionRepresentation

Section48.33 Duality for compactly supported cohomology#

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

Tag 0G5A, a lemma

Tag 0G5A in the Stacks Project.

AlgebraicGeometry.compactSupportDualityEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactSupportDuality/Basic.lean, line 106. The attribute's comment: “the isomorphism of topological k-vector spaces”.

Stacks Project, Tag 0G5A. Let p : U ⟶ Spec k be separated of finite type over a field k and ω_{U/k}^• = p^!𝒪_{Spec k}. For K ∈ D^b_{Coh}(𝒪_U) and i ∈ ℤ there is a canonical isomorphism of topological k-vector spaces

Hom_k(H^i(U, K), k) ≃ H^{-i}_c(U, R𝓗om(K, ω_{U/k}^•)),

for the topology of pointwise convergence on the dual (the limit topology over the finite dimensional subspaces, Module.Dual.limitTopology_eq_iInf_finiteDimensional) and the limit topology of [Stacks, Section 0G59] on compactly supported cohomology. It is functorial in K (AlgebraicGeometry.compactSupportDualityEquiv_naturality). Here p^! and H^*_c are computed at an arbitrary compactification c of U (one exists by [Stacks, Tag 0F41]).

def compactSupportDualityEquiv (K : BoundedCoherentDerived U) (i : ℤ) :
    letI := HasDerivedCategory.standard U.Modules
    letI := HasDerivedCategory.standard (ModuleCat.{u} k)
    haveI := isNoetherian_of_locallyOfFiniteType p
    letI := Module.Dual.limitTopology k ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) i).obj
        ((derivedGlobalSectionsOver p).obj K.obj))
    Module.Dual k ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) i).obj
        ((derivedGlobalSectionsOver p).obj K.obj)) ≃L[k]
      compactSupportCohomology c
        (openDualObj (standardUpperShriekDualizingComplex p c)
          (isDualizingComplex_standardUpperShriekDualizingComplex p c) K) (-i)

AlgebraicGeometry.compactSupportDualityEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactSupportDuality/Basic.lean, line 130. The attribute's comment: “functoriality in K”.

Stacks Project, Tag 0G5A, functoriality. The isomorphisms of AlgebraicGeometry.compactSupportDualityEquiv are functorial in K: for α : K ⟶ K' and a linear form l on H^i(U, K'), the image of l ∘ H^i(α) is the image of l under the map H^{-i}_c(U, D_U K') ⟶ H^{-i}_c(U, D_U K) induced by D_U α.

theorem compactSupportDualityEquiv_naturality {K K' : BoundedCoherentDerived U} (α : K ⟶ K')
    (i : ℤ) (l :
      letI := HasDerivedCategory.standard U.Modules
      letI := HasDerivedCategory.standard (ModuleCat.{u} k)
      Module.Dual k ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) i).obj
        ((derivedGlobalSectionsOver p).obj K'.obj))) :
    letI := HasDerivedCategory.standard U.Modules
    letI := HasDerivedCategory.standard (ModuleCat.{u} k)
    haveI := isNoetherian_of_locallyOfFiniteType p
    compactSupportDualityEquiv p c K i
        (l ∘ₗ ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) i).map
          ((derivedGlobalSectionsOver p).map α.hom)).hom) =
      compactSupportCohomologyMap c
        (openDualMap (standardUpperShriekDualizingComplex p c)
          (isDualizingComplex_standardUpperShriekDualizingComplex p c) α) (-i)
        (compactSupportDualityEquiv p c K' i l)
Tag 0G5B, a lemma

Tag 0G5B in the Stacks Project.

AlgebraicGeometry.compactSupportDualityEquiv_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactSupportDuality/OpenRestriction.lean, line 593.

Let p : U ⟶ Spec k be separated of finite type over a field k, with a compactification c : U ⊆ X at which p^! and H^*_c are computed, as in [Stacks, Tag 0G5A] (AlgebraicGeometry.compactSupportDualityEquiv), and let V ⊆ U be an open, with the induced compactification V ⊆ U ⊆ X (AlgebraicGeometry.compactificationOpen). Then the square

Hom_k(H^i(U, K), k) ⟶ H^{-i}_c(U, R𝓗om(K, ω_{U/k}^•)) ↑ ↑ Hom_k(H^i(V, K|_V), k) ⟶ H^{-i}_c(V, R𝓗om(K|_V, ω_{V/k}^•))

commutes, for every K ∈ D^b_{Coh}(𝒪_U) and i ∈ ℤ: for every linear form l on H^i(V, K|_V), the image of l ∘ res under the duality isomorphism of U is the image under the right vertical arrow of the image of l under the duality isomorphism of V. Here the horizontal arrows are the isomorphisms of [Stacks, Tag 0G5A], the left vertical arrow is the contragredient of the restriction map res : H^i(U, K) ⟶ H^i(V, K|_V) (AlgebraicGeometry.cohomologyRestrict), and the right vertical arrow is the map of [Stacks, Remark 0G56] (AlgebraicGeometry.compactSupportOpenDualMap): Rq_* of the canonical map Rj'_!(L|_V) ⟶ Rj_! L of [Stacks, Tag 0G4Y], read through the canonical identification of R𝓗om(K|_V, ω_{V/k}^•) with R𝓗om(K, ω_{U/k}^•)|_V.

theorem compactSupportDualityEquiv_restrict (K : BoundedCoherentDerived U) (i : ℤ) :
    haveI := isNoetherian_of_locallyOfFiniteType p
    haveI := isNoetherian_of_locallyOfFiniteType (V.ι ≫ p)
    ∀ l : Module.Dual k ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) i).obj
      ((derivedGlobalSectionsOver (V.ι ≫ p)).obj ((restrictBoundedCoherentLift V.ι).obj K).obj)),
    compactSupportDualityEquiv p c K i (l ∘ₗ cohomologyRestrict p V K i) =
      compactSupportOpenDualMap p c V K i
        (compactSupportDualityEquiv (V.ι ≫ p) (compactificationOpen p c V)
          ((restrictBoundedCoherentLift V.ι).obj K) i l)
Tag 0G5C, a lemma

Tag 0G5C in the Stacks Project.

AlgebraicGeometry.degreeZeroCompactSupportMap_injective_and_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/CompactlySupportedCohomology/DegreeZeroCompactSupport.lean, line 604.

Let X be a proper scheme over a field k. Let K ∈ D^b_{Coh}(𝒪_X) with H^i(K) = 0 for i < 0, and set 𝓕 = H^0(K). Let Z ⊆ X be closed with complement U = X ∖ Z. Then

H^0_c(U, K|_U) ⊂ H^0(X, 𝓕)

is given by those global sections of 𝓕 which vanish in an open neighbourhood of Z.

Here H^0_c(U, K|_U) is AlgebraicGeometry.degreeZeroCompactSupport: the morphisms 𝒪_{Spec k} ⟶ Rg_!(K|_U) in Pro-D^b_{Coh}(𝒪_{Spec k}), for g : U ⟶ Spec k and the functor Rg_! = Rp_* ∘ Rj_! of [Stacks, Section 0G4Z] attached to the compactification j : U ⟶ X (which is lim_n H^0(X, K_n) for a Deligne system (K_n) with value K|_U, [Stacks, Section 0G59]); the map H^0_c(U, K|_U) ⟶ H^0(X, 𝓕) is AlgebraicGeometry.degreeZeroCompactSupportMap, induced by the map Rg_!(K|_U) ⟶ Rp_* K of [Stacks, Tag 0G56] for X its own compactification and H^0(X, K) = Γ(X, H^0(K)). The statement is that this map is injective with exactly that image.

public theorem degreeZeroCompactSupportMap_injective_and_range {k : Type u} [Field k]
    {X : Scheme.{u}}
    (p : X ⟶ Spec (.of k)) [IsProper p] (K : BoundedCoherentDerived X)
    (hK : ∀ i < 0, IsZero ((DerivedCategory.homologyFunctor X.Modules i).obj K.obj))
    (Z : TopologicalSpace.Closeds X) :
    letI : IsNoetherian X := @IsNoetherian.mk X (LocallyOfFiniteType.isLocallyNoetherian p)
      (QuasiCompact.compactSpace_of_compactSpace p)
    Function.Injective (degreeZeroCompactSupportMap p Z.compl K
        ((DerivedCategory.isGE_iff K.obj 0).2 hK)) ∧
      Set.range (degreeZeroCompactSupportMap p Z.compl K
        ((DerivedCategory.isGE_iff K.obj 0).2 hK)) =
        {σ | ∃ V : X.Opens, (Z : Set X) ⊆ V ∧
          ((DerivedCategory.homologyFunctor X.Modules 0).obj K.obj).presheaf.map
            (homOfLE (le_top : V ≤ ⊤)).op σ = 0}
Sources
LeanAlgebraicGeometry.compactSupportDualityEquiv · AlgebraicGeometry.compactSupportDualityEquiv_naturality · AlgebraicGeometry.compactSupportDualityEquiv_restrict · AlgebraicGeometry.degreeZeroCompactSupportMap_injective_and_range

Section48.34 Lichtenbaum's theorem#

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

Tag 0G5E, a lemma

Tag 0G5E in the Stacks Project.

Stacks.Duality.Lichtenbaum.le_topologicalKrullDim_and_isProper_of_not_isZero_rightDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Lichtenbaum/VarietyTopCohomology.lean, line 212.

[Stacks, Tag 0G5E]. Let U be a variety over a field k and let F be a coherent 𝒪_U-module. If H^d(U, F) is nonzero, then dim(U) ≥ d, and if equality holds, then U is proper over k.

Here H^d(U, F) is the d-th right derived functor of global sections on Mod(𝒪_U), and dim(U) is the topological Krull dimension. The proof is the source's. The bound is Grothendieck's vanishing theorem ([Stacks, Tag 02UZ]). If dim U = d, choose an integral scheme X proper over k containing U as an open subscheme ([Stacks, Tag 0F41], [Stacks, Tag 0A9Z]); then dim X = d, and if U is not proper then U ≠ X, so H^d(U, F) = 0 by duality ([Stacks, Tag 0G5A]) and the vanishing of H^{-d}_c(U, R𝓗om(F, ω_U^•)) (Stacks.Duality.Lichtenbaum.isZero_rightDerived_of_nonempty_compl).

theorem le_topologicalKrullDim_and_isProper_of_not_isZero_rightDerived (k : Type u) [Field k]
    {U : Scheme.{u}} (f : U ⟶ Spec (.of k)) [IsVariety k f] (F : U.Modules) [F.IsCoherent]
    (d : ℕ) (h : ¬ IsZero (((moduleGlobalSections U).rightDerived d).obj F)) :
    (d : WithBot ℕ∞) ≤ topologicalKrullDim U ∧ (topologicalKrullDim U = d → IsProper f)
Tag 0G5F, a theorem

Tag 0G5F in the Stacks Project.

Stacks.Duality.Lichtenbaum.tfae_isZero_cohomologyOverField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/Lichtenbaum/Theorem.lean, line 107.

[Stacks, Tag 0G5F]. Let X be a separated scheme of finite type over a field k, of dimension d (so X is nonempty). The following are equivalent:

  1. H^d(X, F) = 0 for all coherent 𝒪_X-modules F,
  2. H^d(X, F) = 0 for all quasi-coherent 𝒪_X-modules F, and
  3. no irreducible component X' ⊆ X of dimension d, viewed as an integral closed subscheme through its reduced induced structure, is proper over k.

Here H^d(X, F) is the k-vector space AlgebraicGeometry.cohomologyOverField k f F d.

theorem tfae_isZero_cohomologyOverField (k : Type u) [Field k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] (d : ℕ)
    (hd : topologicalKrullDim X = d) :
    List.TFAE
      [∀ (F : X.Modules) [F.IsCoherent], IsZero (cohomologyOverField k f F d),
       ∀ (F : X.Modules) [F.IsQuasicoherent], IsZero (cohomologyOverField k f F d),
       ∀ Z : irreducibleComponents X,
        let C := Scheme.IdealSheafData.vanishingIdeal (X := X)
          ⟨Z.1, isClosed_of_mem_irreducibleComponents Z.1 Z.2⟩
        topologicalKrullDim C.subscheme = d → ¬ IsProper (C.subschemeι ≫ f)]
Sources
LeanStacks.Duality.Lichtenbaum.le_topologicalKrullDim_and_isProper_of_not_isZero_rightDerived · Stacks.Duality.Lichtenbaum.tfae_isZero_cohomologyOverField

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.