20.34 Cohomology with support… to 20.44 Global derived hom

Section20.34 Cohomology with support in a closed subset, II#

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

Tag 0A3B, a lemma

Tag 0A3B in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.derivedPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsCanonicalMaps.lean, line 277. The attribute's comment: “the adjunction i_*^D ⊣ RℋZ as a term, not an existence statement”.

Stacks 0A3B (1), as a term. Let Z be a closed subset of a ringed space X and let i : (Z, 𝒪_X|_Z) ⟶ (X, 𝒪_X) be the inclusion. The functor D(𝒪_X|_Z) ⥤ D(𝒪_X) induced by i_* is left adjoint to the right derived functor RH_Z : D(𝒪_X) ⥤ D(𝒪_X|_Z) of sections supported on Z.

This is the adjunction whose mere existence is derivedPushforward_adj_derivedSupportedSectionsOnClosed, and its unit is the canonical comparison by derivedPushforwardAdjunction_unit_app.

noncomputable def derivedPushforwardAdjunction (X : RingedSpace.{u, u}) (Z : Set X.carrier)
    (hZ : IsClosed Z) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory ⊣
      derivedSupportedSectionsOnClosed X Z hZ

Stacks.Cohomology.SupportedComplexes.derivedPushforwardCompDerivedSupportedSectionsIsoId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsCanonicalMaps.lean, line 378. The attribute's comment: “RℋZ ∘ i_*^D ≅ 𝟭, as a chosen natural isomorphism”.

Stacks 0A3B (2) as a natural isomorphism. Composing RH_Z with the derived pushforward from the closed subset is the identity on D(𝒪_X|_Z), the isomorphism being the inverse of the unit of derivedPushforwardAdjunction.

noncomputable def derivedPushforwardCompDerivedSupportedSectionsIsoId (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory ⋙
        derivedSupportedSectionsOnClosed X Z hZ ≅
      𝟭 (DerivedCategory (_root_.SheafOfModules.{u}
        (structureSheafRing (closedSubsetRingedSpace X Z))))

Stacks.Cohomology.SupportedComplexes.derivedPushforward_adj_derivedSupportedSectionsOnClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedAdjunction.lean, line 511. The attribute's comment: “adjunction”.

Stacks 0A3B (1). Let Z be a closed subset of a ringed space X and let i : (Z, 𝒪_X|_Z) ⟶ (X, 𝒪_X) be the inclusion. The right derived functor RH_Z : D(𝒪_X) ⥤ D(𝒪_X|_Z) of sections supported on Z is right adjoint to the functor D(𝒪_X|_Z) ⥤ D(𝒪_X) induced by i_*.

theorem derivedPushforward_adj_derivedSupportedSectionsOnClosed (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    Nonempty
      ((modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory ⊣
        derivedSupportedSectionsOnClosed X Z hZ)

Stacks.Cohomology.SupportedComplexes.exists_isIso_unit_derivedPushforward_adj_derivedSupportedSectionsOnClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedAdjunction.lean, line 526. The attribute's comment: “pushforward identity”.

Stacks 0A3B (2). Let Z be a closed subset of a ringed space X and let i : (Z, 𝒪_X|_Z) ⟶ (X, 𝒪_X) be the inclusion. For K in D(𝒪_X|_Z) one has RH_Z(i_* K) = K: the unit of the derived adjunction of Stacks 0A3B (1) is an isomorphism. The adjunction is pinned down by the compatibility of its unit with the unit M ⟶ H_Z(i_* M) of the underived adjunction, which identifies the invertible map as the canonical comparison.

theorem exists_isIso_unit_derivedPushforward_adj_derivedSupportedSectionsOnClosed
    (X : RingedSpace.{u, u}) (Z : Set X.carrier) (hZ : IsClosed Z) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    ∃ Ad : (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory ⊣
        derivedSupportedSectionsOnClosed X Z hZ,
      (∀ M : HomotopyCategory (_root_.SheafOfModules.{u}
          (structureSheafRing (closedSubsetRingedSpace X Z))) (ComplexShape.up ℤ),
        Ad.unit.app (DerivedCategory.Qh.obj M) ≫
            (derivedSupportedSectionsOnClosed X Z hZ).map
              ((modulePushforward
                (closedSubsetInclusion X Z)).mapDerivedCategoryFactorsh.hom.app M) =
          DerivedCategory.Qh.map
              ((Adjunction.mapHomotopyCategoryAdjunction
                (modulePushforward_supportedSectionsOnClosed_adjunction X Z hZ)
                (ComplexShape.up ℤ)).unit.app M) ≫
            (derivedSupportedSectionsOnClosedUnit X Z hZ).app
              (((modulePushforward (closedSubsetInclusion X Z)).mapHomotopyCategory
                (ComplexShape.up ℤ)).obj M)) ∧ IsIso Ad.unit

Stacks.Cohomology.SupportedComplexes.isZero_rightDerivedPlus_supportedSectionsOnClosed_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedAdjunction.lean, line 576. The attribute's comment: “higher vanishing”.

Stacks 0A3B (3). Let Z be a closed subset of a ringed space X, let i : (Z, 𝒪_X|_Z) ⟶ (X, 𝒪_X) be the inclusion and let 𝒢 be a sheaf of 𝒪_X|_Z-modules on Z. Then the higher derived sheaves of sections supported on Z of the pushforward of 𝒢 vanish: H^p_Z(i_* 𝒢) = 0 for p > 0.

theorem isZero_rightDerivedPlus_supportedSectionsOnClosed_modulePushforward
    (X : RingedSpace.{u, u}) (Z : Set X.carrier) (hZ : IsClosed Z)
    (G : _root_.SheafOfModules.{u} (structureSheafRing (closedSubsetRingedSpace X Z)))
    (p : ℤ) (hp : 0 < p) :
    letI : EnoughInjectives (_root_.SheafOfModules.{u} (structureSheafRing X)) :=
      IsGrothendieckAbelian.enoughInjectives
    IsZero (((supportedSectionsOnClosedFunctor X Z hZ).rightDerivedPlus p).obj
      ((modulePushforward (closedSubsetInclusion X Z)).obj G))
Tag 0AEF, a lemma

Tag 0AEF in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.isIso_derivedPushforwardAdjunction_counit_app_of_supported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedEquivalence.lean, line 228. The attribute's comment: “part (2): the counit i_*RℋZ(K) ⟶ K is invertible at every K supported on Z, which is the essential-image content of the equivalence”.

Stacks 0AEF, part (2). For K in D(𝒪_X) whose cohomology sheaves are supported on the closed subset Z, the canonical map i_* RH_Z(K) ⟶ K — the counit of the adjunction i_*^D ⊣ RH_Z of Stacks 0A3B (1) — is an isomorphism.

theorem isIso_derivedPushforwardAdjunction_counit_app_of_supported (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z)
    (K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)))
    (hK : AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X) Z K) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    IsIso ((derivedPushforwardAdjunction X Z hZ).counit.app K)

Stacks.Cohomology.SupportedComplexes.derivedPushforwardSupportedSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedEquivalence.lean, line 246. The attribute's comment: “part (2): the same invertible counit, as the isomorphism i_*RℋZ(K) ≅ K”.

Stacks 0AEF, part (2), as an isomorphism. For K in D(𝒪_X) with cohomology sheaves supported on Z, the canonical map i_* RH_Z(K) ⟶ K is an isomorphism i_* RH_Z(K) ≅ K.

def derivedPushforwardSupportedSectionsIso (X : RingedSpace.{u, u}) (Z : Set X.carrier)
    (hZ : IsClosed Z) (K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)))
    (hK : AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X) Z K) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.obj
        ((derivedSupportedSectionsOnClosed X Z hZ).obj K) ≅ K

Stacks.Cohomology.SupportedComplexes.closedSubsetDerivedPushforwardEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedEquivalence.lean, line 262. The attribute's comment: “part (2): i_* : D(𝒪_X|_Z) ⥤ D_Z(𝒪_X) is an equivalence”.

Stacks 0AEF, part (2). Derived pushforward along the inclusion of a closed subset Z is an equivalence of D(𝒪_X|_Z) with the full subcategory D_Z(𝒪_X) of D(𝒪_X) of complexes whose cohomology sheaves are supported on Z.

def closedSubsetDerivedPushforwardEquivalence (X : RingedSpace.{u, u}) (Z : Set X.carrier)
    (hZ : IsClosed Z) :
    DerivedCategory (_root_.SheafOfModules.{u}
        (structureSheafRing (closedSubsetRingedSpace X Z))) ≌
      SupportedDerivedCategory X Z

Stacks.Cohomology.SupportedComplexes.closedSubsetDerivedPushforwardEquivalence_functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedEquivalence.lean, line 277. The attribute's comment: “part (2): the functor of the equivalence is i_*”.

Stacks 0AEF, part (2). The equivalence onto the supported complexes is induced by i_*: composed with the inclusion of D_Z(𝒪_X) into D(𝒪_X) it is i_*^D.

def closedSubsetDerivedPushforwardEquivalence_functor (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z) :
    (letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    (closedSubsetDerivedPushforwardEquivalence X Z hZ).functor ⋙
        (supportedDerivedProperty X Z).ι ≅
      (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory)

Stacks.Cohomology.SupportedComplexes.closedSubsetDerivedPushforwardEquivalence_inverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedEquivalence.lean, line 295. The attribute's comment: “part (2): the quasi-inverse is RℋZ restricted to D_Z”.

Stacks 0AEF, part (2). The quasi-inverse of the equivalence is the derived functor RH_Z of sections supported on Z, restricted to D_Z(𝒪_X).

This is the RH_Z half of the source's i^{-1}|_{D_Z(𝒪_X)} = RH_Z|_{D_Z(𝒪_X)}; the i^{-1} half is closedSubsetDerivedPushforwardEquivalence_inverse_iso_derivedModulePullback in ClosedSubsetDerivedPullback.lean.

def closedSubsetDerivedPushforwardEquivalence_inverse (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z) :
    (closedSubsetDerivedPushforwardEquivalence X Z hZ).inverse ≅
      (supportedDerivedProperty X Z).ι ⋙ derivedSupportedSectionsOnClosed X Z hZ

Stacks.Cohomology.SupportedComplexes.derivedPushforwardSupportedSections_isRightAdjoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedEquivalence.lean, line 312. The attribute's comment: “part (3)”.

Stacks 0AEF, part (3). The functor D(𝒪_X) ⥤ D_Z(𝒪_X) given by K ↦ i_* RH_Z(K) — RH_Z followed by derived pushforward, which lands in D_Z(𝒪_X) by part (1) — is right adjoint to the inclusion D_Z(𝒪_X) ⥤ D(𝒪_X).

This is the formal consequence of part (2) and Stacks 0A3B (1) that [Stacks, Tag 0AEF] says it is: by part (2) the inclusion is the quasi-inverse of i_*^D : D(𝒪_X|_Z) ≌ D_Z(𝒪_X) followed by i_*^D, so composing that equivalence with the adjunction i_*^D ⊣ RH_Z of Stacks 0A3B (1) exhibits the inclusion as a left adjoint; see iotaAdjunctionOfCounitIso.

def derivedPushforwardSupportedSections_isRightAdjoint (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z) :
    (supportedDerivedProperty X Z).ι ⊣
      derivedSupportedSectionsOnClosed X Z hZ ⋙ derivedPushforwardToSupported X Z hZ

Stacks.Cohomology.SupportedComplexes.derivedSupportedSectionsIsoDerivedModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedPullback.lean, line 128. The attribute's comment: “part (2): on D_Z the quasi-inverse RℋZ agrees with i⁻¹”.

On the full subcategory D_Z(𝒪_X) of complexes with cohomology sheaves supported on the closed subset Z, the right derived functor RH_Z of sections supported on Z agrees with inverse image i^{-1} along the inclusion.

def derivedSupportedSectionsIsoDerivedModulePullback (X : RingedSpace.{u, u})
    (Z : Set X.carrier) (hZ : IsClosed Z) :
    (letI := preservesFiniteLimits_modulePullback_closedSubsetInclusion X Z
    letI := preservesFiniteColimits_modulePullback (closedSubsetInclusion X Z)
    (supportedDerivedProperty X Z).ι ⋙ derivedSupportedSectionsOnClosed X Z hZ ≅
      (supportedDerivedProperty X Z).ι ⋙
        (modulePullback (closedSubsetInclusion X Z)).mapDerivedCategory)

Stacks.Cohomology.SupportedComplexes.closedSubsetDerivedPushforwardEquivalence_inverse_iso_derivedModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetDerivedPullback.lean, line 152. The attribute's comment: “part (2): the quasi-inverse is i⁻¹ restricted to D_Z”.

The quasi-inverse of the equivalence i_*^D : D(𝒪_X|_Z) ≌ D_Z(𝒪_X) is inverse image i^{-1} restricted to D_Z(𝒪_X).

def closedSubsetDerivedPushforwardEquivalence_inverse_iso_derivedModulePullback
    (X : RingedSpace.{u, u}) (Z : Set X.carrier) (hZ : IsClosed Z) :
    (letI := preservesFiniteLimits_modulePullback_closedSubsetInclusion X Z
    letI := preservesFiniteColimits_modulePullback (closedSubsetInclusion X Z)
    (closedSubsetDerivedPushforwardEquivalence X Z hZ).inverse ≅
      (supportedDerivedProperty X Z).ι ⋙
        (modulePullback (closedSubsetInclusion X Z)).mapDerivedCategory)

Stacks.Cohomology.SupportedComplexes.pushforward_supported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ClosedSubsetPushforward.lean, line 116. The attribute's comment: “part (1)”.

Stacks 0AEF, part (1). For K in the derived category of 𝒪_X|_Z-modules, the cohomology sheaves of i_* K are supported on Z.

theorem pushforward_supported (X : RingedSpace.{u, u}) (Z : Set X.carrier) (hZ : IsClosed Z)
    (K : DerivedCategory (Stacks.Cohomology.DerivedPushforwardComposition.ModuleSheaves
      (closedSubsetRingedSpace X Z))) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X) Z
      ((modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.obj K)
Tag 0G6Z, a lemma

Tag 0G6Z in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.isKInjective_supportedSectionsOnClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsKInjective.lean, line 62.

Stacks 0G6Z. Let Z be a closed subset of a ringed space X and let i : (Z, 𝒪_X|_Z) ⟶ (X, 𝒪_X) be the inclusion. If I is a K-injective complex of 𝒪_X-modules, then the complex H_Z(I) of sections supported on Z is a K-injective complex of 𝒪_X|_Z-modules.

theorem isKInjective_supportedSectionsOnClosed (X : RingedSpace.{u, u}) (Z : Set X.carrier)
    (hZ : IsClosed Z) (I : CochainComplex (_root_.SheafOfModules.{u} (structureSheafRing X)) ℤ)
    [I.IsKInjective] :
    CochainComplex.IsKInjective
      (((Stacks.SheafOfModules.SupportedSections.supportedSectionsOnClosedFunctor
        X Z hZ).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)
Tag 0G70, a lemma

Tag 0G70 in the Stacks Project.

Stacks.Cohomology.LocalToGlobalSupport.derivedSectionsWithSupportIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/LocalToGlobalSectionsWithSupport.lean, line 396.

Stacks 0G70. Let Z be a closed subset of a ringed space X and let i : (Z, 𝒪_X|_Z) ⟶ (X, 𝒪_X) be the inclusion. Then RΓ(Z, -) ∘ RH_Z = RΓ_Z(X, -) as functors D(𝒪_X) ⥤ D(𝒪_X(X)): for every right derived functor RΓ(Z, -) of global sections on Z and every right derived functor RΓ_Z(X, -) of global sections supported on Z, there is a canonical natural isomorphism from the composite of RH_Z with RΓ(Z, -) to RΓ_Z(X, -). It is canonical by uniqueness of right derived functors: it is the unique transformation compatible with the comparisons to the underived functors, by derivedSectionsWithSupportIso_hom_fac together with derivedSectionsWithSupportIso_hom_unique.

def derivedSectionsWithSupportIso
    [RΓZ'.IsRightDerivedFunctor αΓ
      (HomotopyCategory.quasiIso (ClosedModuleSheaves X Z) (ComplexShape.up ℤ))]
    [RΓZ.IsRightDerivedFunctor αZ
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))] :
    derivedSupportedSectionsOnClosed X Z hZ ⋙ RΓZ' ≅ RΓZ

Stacks.Cohomology.LocalToGlobalSupport.derivedSectionsWithSupportIso_hom_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/LocalToGlobalSectionsWithSupport.lean, line 410. The attribute's comment: “the comparison is the canonical one”.

Stacks 0G70, the normalization that makes the isomorphism the canonical one. The isomorphism of Stacks 0G70 carries the comparison localToGlobalUnit of RΓ(Z, -) ∘ RH_Z to the comparison αZ of RΓ_Z(X, -).

theorem derivedSectionsWithSupportIso_hom_fac
    [RΓZ'.IsRightDerivedFunctor αΓ
      (HomotopyCategory.quasiIso (ClosedModuleSheaves X Z) (ComplexShape.up ℤ))]
    [RΓZ.IsRightDerivedFunctor αZ
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))] :
    localToGlobalUnit X Z hZ RΓZ' αΓ ≫ Functor.whiskerLeft DerivedCategory.Qh
        (derivedSectionsWithSupportIso X Z hZ RΓZ' αΓ RΓZ αZ).hom =
      αZ
Tag 0G71, a lemma

Tag 0G71 in the Stacks Project.

Stacks.Cohomology.SectionsWithSupport.canonicalDerivedGlobalSections_isRightDerivedFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/CanonicalSectionsWithSupportTriangle.lean, line 124. The attribute's comment: “RΓ(X, -) on the unbounded derived category D(O_X) exists: the middle term of the triangle is a genuine right derived functor of global sections”.

RΓ(X, -), with its unit, is a right derived functor of global sections along the quasi-isomorphisms of the unbounded homotopy category.

public instance canonicalDerivedGlobalSections_isRightDerivedFunctor :
    (canonicalDerivedGlobalSections X).IsRightDerivedFunctor
      (canonicalDerivedGlobalSectionsUnit X)
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))

Stacks.Cohomology.SectionsWithSupport.canonicalDerivedSectionsWithSupport_isRightDerivedFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/CanonicalSectionsWithSupportTriangle.lean, line 159. The attribute's comment: “RΓ_Z(X, -) on the unbounded derived category D(O_X) exists: the first term of the triangle is a genuine right derived functor of sections with support in Z”.

RΓ_Z(X, -), with its unit, is a right derived functor of sections with support along the quasi-isomorphisms of the unbounded homotopy category.

public instance canonicalDerivedSectionsWithSupport_isRightDerivedFunctor :
    (canonicalDerivedSectionsWithSupport X Z hZ).IsRightDerivedFunctor
      (canonicalDerivedSectionsWithSupportUnit X Z hZ)
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))

Stacks.Cohomology.SectionsWithSupport.canonicalDerivedSectionsOnComplement_isRightDerivedFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/CanonicalSectionsWithSupportTriangle.lean, line 191. The attribute's comment: “RΓ(U, -) for U = X ∖ Z on the unbounded derived category D(O_X) exists: the third term of the triangle is a genuine right derived functor of sections on the complement”.

RΓ(U, -), with its unit, is a right derived functor of sections on the complement along the quasi-isomorphisms of the unbounded homotopy category.

public instance canonicalDerivedSectionsOnComplement_isRightDerivedFunctor :
    (canonicalDerivedSectionsOnComplement X Z hZ).IsRightDerivedFunctor
      (canonicalDerivedSectionsOnComplementUnit X Z hZ)
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))

Stacks.Cohomology.SectionsWithSupport.canonicalSectionsWithSupportTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/CanonicalSectionsWithSupportTriangle.lean, line 262. The attribute's comment: “the distinguished triangle RΓ_Z(X,K) → RΓ(X,K) → RΓ(U,K) → RΓ_Z(X,K)[1] in D(O_X(X)), at the three constructed derived functors, functorial for K in D(O_X)”.

Stacks, Tag 0G71. Let Z be a closed subset of a ringed space X and let U = X ∖ Z. The triangle RΓ_Z(X, K) ⟶ RΓ(X, K) ⟶ RΓ(U, K) ⟶ RΓ_Z(X, K)[1] is distinguished in D(O_X(X)), functorially in K in D(O_X). The three functors are the total right derived functors constructed above, the two forward arrows are the canonical ones, and the connecting morphism is a natural transformation independent of K; nothing is quantified over.

public theorem canonicalSectionsWithSupportTriangle_distinguished
    (K : DerivedModuleSheaves X) :
    canonicalSectionsWithSupportTriangle X Z hZ K ∈ distTriang (DerivedGlobalModules X)

Stacks.Cohomology.SectionsWithSupport.derivedSectionsWithSupportTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SectionsWithSupportTriangle.lean, line 868.

Derived sections with support, global derived sections, and derived sections on the open complement form a distinguished triangle, naturally in the object of the unbounded derived category.

public noncomputable def derivedSectionsWithSupportTriangle
    (X : RingedSpace.{u, u}) (Z : Set X) (hZ : IsClosed Z)
    (RΓZ RΓ RΓU : DerivedModuleSheaves X ⥤ DerivedGlobalModules X)
    (aZ : homotopyToDerived X (sectionsWithSupport X Z hZ) ⟶ DerivedCategory.Qh ⋙ RΓZ)
    (aX : homotopyToDerived X
      (SheafOfModules.evaluation (structureSheafRing X) (op ⊤)) ⟶
        DerivedCategory.Qh ⋙ RΓ)
    (aU : homotopyToDerived X (sectionsOnComplement X Z hZ) ⟶ DerivedCategory.Qh ⋙ RΓU)
    [RΓZ.IsRightDerivedFunctor aZ
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RΓ.IsRightDerivedFunctor aX
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RΓU.IsRightDerivedFunctor aU
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))] :
    SectionsWithSupportTriangleData X RΓZ RΓ RΓU
      (derivedSupportInclusion X Z hZ RΓZ RΓ aZ aX)
      (derivedRestrictionToComplement X Z hZ RΓ RΓU aX aU)
Tag 0G72, a lemma

Tag 0G72 in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.derivedSupportedSectionsTriangleδ, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsCanonicalMaps.lean, line 457. The attribute's comment: “the connecting morphism δ of the triangle, as a term”.

The connecting map of Stacks 0G72, as a term. For chosen right derived functors RH of ℱ ↦ i_* ℋ_Z(ℱ) and RJ of ℱ ↦ j_*(ℱ|_U), this is the natural transformation δ : RJ ⟶ RH⟦1⟧ completing the two canonical maps RH ⟶ 𝟭 and 𝟭 ⟶ RJ to a distinguished triangle, by derivedSupportedSectionsTriangle_distinguished.

The existence statement exists_derivedSupportedSectionsTriangle is this map with the quantifier in front: the connecting map is constructed by Stacks.Cohomology.RestrictionCover.derivedTriangleOfShortExactOnInjectives as the connecting map of the short exact sequence of complexes obtained by applying the three functors to the functorial K-injective resolution, descended along the localization.

noncomputable def derivedSupportedSectionsTriangleδ :
    RJ ⟶ RH ⋙ shiftFunctor
      (DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X))) (1 : ℤ)

Stacks.Cohomology.SupportedComplexes.derivedSupportedSectionsTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsCanonicalMaps.lean, line 477. The attribute's comment: “the triangle i_RℋZ(K) ⟶ K ⟶ Rj_(K|_U) ⟶ [1] is distinguished”.

Stacks 0G72. The triangle of derivedSupportedSectionsTriangle is distinguished at every object K of D(𝒪_X).

theorem derivedSupportedSectionsTriangle_distinguished
    (K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X))) :
    derivedSupportedSectionsTriangle X Z hZ RH RJ aH aJ K ∈
      distTriang (DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)))

Stacks.Cohomology.SupportedComplexes.exists_derivedSupportedSectionsTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsSheafTriangle.lean, line 337.

Stacks 0G72. Let Z be a closed subset of a ringed space X and j : U = X ∖ Z ⟶ X the inclusion of the complement. For arbitrary right derived functors RH of ℱ ↦ i_* ℋ_Z(ℱ) and RJ of ℱ ↦ j_*(ℱ|_U) on the unbounded derived category of 𝒪_X-modules, the two canonical maps RH ⟶ 𝟭 and 𝟭 ⟶ RJ extend to a connecting map δ making RH(K) ⟶ K ⟶ RJ(K) ⟶ RH(K)⟦1⟧ a distinguished triangle for every K. All three maps are natural transformations of functors, so the triangle is functorial in K.

theorem exists_derivedSupportedSectionsTriangle (X : RingedSpace.{u, u}) (Z : Set X.carrier)
    (hZ : IsClosed Z)
    (RH RJ : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)))
    (aH : (supportedSectionsFunctor X Z).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RH)
    (aJ : (restrictPush (structureSheafRing X) (openComplement Z hZ)).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RJ)
    [RH.IsRightDerivedFunctor aH
      (HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (structureSheafRing X))
        (ComplexShape.up ℤ))]
    [RJ.IsRightDerivedFunctor aJ
      (HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (structureSheafRing X))
        (ComplexShape.up ℤ))] :
    ∃ δ : RJ ⟶ RH ⋙ shiftFunctor
        (DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X))) (1 : ℤ),
      ∀ K, Triangle.mk ((derivedSupportedSectionsToId X Z RH aH).app K)
          ((idToDerivedRestrictPush X Z hZ RJ aJ).app K) (δ.app K) ∈
        distTriang (DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)))
Tag 0G73, a lemma

Tag 0G73 in the Stacks Project.

Stacks.SheafOfModules.SupportedSections.isZero_derivedSupportedSections_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/PushforwardFromDisjointOpen.lean, line 177.

Stacks 0G73. Let Z be a closed subset of a ringed space X and let j : (U, 𝒪_X|_U) ⟶ (X, 𝒪_X) be the inclusion of an open subset with U ∩ Z = ∅. Then R H_Z(Rj_* K) = 0 for every K in D(𝒪_U).

theorem isZero_derivedSupportedSections_derivedPushforward
    (X : RingedSpace.{u, u}) (Z : Set X.carrier) (hZ : IsClosed Z) (U : Opens X.carrier)
    (hUZ : (U : Set X.carrier) ∩ Z = ∅)
    (Rj : DerivedCategory
        (_root_.SheafOfModules.{u} (structureSheafRing (X.restrict U.isOpenEmbedding))) ⥤
      DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)))
    (αj : (modulePushforward (X.ofRestrict U.isOpenEmbedding)).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rj)
    [Rj.IsRightDerivedFunctor αj (HomotopyCategory.quasiIso
      (_root_.SheafOfModules.{u} (structureSheafRing (X.restrict U.isOpenEmbedding)))
      (ComplexShape.up ℤ))]
    (RH : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing (RingedSpace.inverseImage X
        (ClosedImmersionSheaves.closedSubsetInclusion Z)))))
    (αH : (supportedSectionsOnClosedFunctor X Z hZ).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RH)
    [RH.IsRightDerivedFunctor αH (HomotopyCategory.quasiIso
      (_root_.SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ))]
    (K : DerivedCategory
      (_root_.SheafOfModules.{u} (structureSheafRing (X.restrict U.isOpenEmbedding)))) :
    IsZero (RH.obj (Rj.obj K))
Tag 0G74, a lemma

Tag 0G74 in the Stacks Project.

Stacks.Perfect.GysinAbelianSquare.pushforwardLocalCohomologyForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/Gysin/GysinDifferentialSquare.lean, line 135. The attribute's comment: “part (2) at the GYSIN MAP'S TARGET: the underlying abelian sheaf of i_H^n_T(F) is i_^ab H^n_T(F_ab), naturally in F, which is what lets H^n_T act on a morphism that is additive but not O_X-linear. No hypotheses beyond IsClosed T”.

The underlying sheaf of abelian groups of i_*ℋ ⁿ_T(ℱ[0]), with the local cohomology sheaf taken as the degree-n cohomology sheaf of R𝓗_T(ℱ[0]) in the unbounded derived category — the spelling of the target of AlgebraicGeometry.Scheme.Hom.gysinMap — is the abelian direct image of the abelian local cohomology sheaf ℋ ⁿ_T(ℱ_ab), naturally in ℱ.

public def pushforwardLocalCohomologyForgetIso {T : Set X} (hT : IsClosed T) (n : ℕ) :
    GysinLocalCohomology.localCohomologyPushforwardFunctor hT (n : ℤ) ⋙ abelianSheaf X ≅
      abelianSheaf X ⋙ abelianLocalCohomologyPushforward X.toRingedSpace T hT n

Stacks.Cohomology.SupportedComplexes.localCohomologySheafForgetComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/UnderlyingAbelianLocalCohomologyComparison.lean, line 250. The attribute's comment: “part (2), the canonical map; invertibility is proved in isIso_localCohomologySheafForgetComparison_of_isRightDerivedFunctor”.

Stacks 0G74, part (2): the canonical map. Let Z be a closed subset of a ringed space X, let RH be a right derived functor of the sections supported on Z of sheaves of 𝒪_X-modules and RHab one of the sections supported on Z of abelian sheaves. This is the canonical map RH_Z(K)_ab ⟶ RH_Z(K_ab) in D(Ab(Z)), natural in K, induced through the universal property of RH by the underived comparison of supported sections.

This map is an isomorphism: isIso_localCohomologySheafForgetComparison_of_isRightDerivedFunctor in UnderlyingAbelianLocalCohomologyInvertible.lean proves it, for aHab the derivation unit of a right derived functor of abelian supported sections.

def localCohomologySheafForgetComparison
    [RH.IsRightDerivedFunctor aH
      (HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (structureSheafRing X))
        (ComplexShape.up ℤ))] :
    RH ⋙ underlyingDerivedSheaf (structureSheafRing (closedSubsetRingedSpace X Z)) ⟶
      underlyingDerivedSheaf (structureSheafRing X) ⋙ RHab

Stacks.Cohomology.SupportedComplexes.localCohomologySheafFunctorForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/UnderlyingAbelianLocalCohomologyDegreewise.lean, line 122. The attribute's comment: “part (2) degreewise: ℋ ⁿ_Z(ℱ)_ab ≅ ℋ ⁿ_Z(ℱ_ab)”.

Stacks 0G74, part (2), on cohomology sheaves in every degree. Let Z be a closed subset of a ringed space X and let ℱ be a sheaf of 𝒪_X-modules with underlying abelian sheaf ℱ_ab. For every n : ℕ the degree-n local cohomology sheaf ℋ ⁿ_Z(ℱ), an 𝒪_X|_Z-module on Z, has underlying abelian sheaf the degree-n local cohomology sheaf ℋ ⁿ_Z(ℱ_ab) of the abelian sheaf ℱ_ab, naturally in ℱ.

Both sides are Mathlib's ℕ-indexed CategoryTheory.Functor.rightDerived, of supported sections of 𝒪_X-modules on the left and of abelian sheaves on the right. This is the statement a consumer needs in order to let ℋ ⁿ_Z act on a morphism of sheaves which is additive but not 𝒪_X-linear — a de Rham differential, say: the morphism has no image under the module-level functor at all, but its underlying morphism of abelian sheaves has one under the abelian functor, and this isomorphism transports the result back.

The proof passes from each ℕ-indexed derived functor to the degree-n cohomology of a total right derived functor on the unbounded derived category, where Stacks 0G74 part (2) applies, and back again; see the implementation notes.

def localCohomologySheafFunctorForgetIso (n : ℕ) :
    localCohomologySheafFunctor X Z hZ n ⋙
        _root_.SheafOfModules.toSheaf (structureSheafRing (closedSubsetRingedSpace X Z)) ≅
      _root_.SheafOfModules.toSheaf (structureSheafRing X) ⋙
        ClosedImmersionSheaves.localCohomologySheafFunctor Z hZ n

Stacks.Cohomology.SupportedComplexes.isIso_localCohomologySheafForgetComparison_of_isRightDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/UnderlyingAbelianLocalCohomologyInvertible.lean, line 624. The attribute's comment: “part (2), invertibility of the canonical map”.

Stacks 0G74, part (2). Let Z be a closed subset of a ringed space X, let RH be a right derived functor of the sections supported on Z of sheaves of 𝒪_X-modules and let RHab be one of the sections supported on Z of abelian sheaves. The canonical map

RH_Z(K)_ab ⟶ RH_Z(K_ab)

of localCohomologySheafForgetComparison is an isomorphism in D(Ab(Z)), in all degrees.

The proof is the source's. It is enough to check invertibility at the image of a K-injective complex K of 𝒪_X-modules, and a K-injective resolution of K with injective terms has the same image in the derived category, so one may take the terms of K injective. There the derivation unit of RH is invertible because K is K-injective, and the transported unit is invertible by abelianSupportedUnit_isIso_at_underlying_kInjective — which is where flasqueness enters: the underlying abelian sheaf of an injective 𝒪_X-module is flasque (Stacks 09SX), and supported sections of a flasque abelian sheaf are the kernel of a surjection between sections over two opens, so K_ab computes the derived functor even though it is neither K-injective nor a complex of injectives. The defining factorization localCohomologySheafForgetComparison_fac then forces the comparison itself to be invertible.

theorem isIso_localCohomologySheafForgetComparison_of_isRightDerivedFunctor
    (X : RingedSpace.{u, u}) (Z : Set X.carrier) (hZ : IsClosed Z)
    (RHab : DerivedCategory (Sheaf (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}) ⥤
      DerivedCategory (Sheaf (Opens.grothendieckTopology (TopCat.of Z)) AddCommGrpCat.{u}))
    (aHab : (abelianSupportedSectionsOnClosed X Z hZ).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RHab)
    [RHab.IsRightDerivedFunctor aHab
      (HomotopyCategory.quasiIso
        (Sheaf (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}) (ComplexShape.up ℤ))]
    (RH : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory
        (_root_.SheafOfModules.{u} (structureSheafRing (closedSubsetRingedSpace X Z))))
    (aH : (supportedSectionsOnClosedFunctor X Z hZ).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RH)
    [RH.IsRightDerivedFunctor aH
      (HomotopyCategory.quasiIso (_root_.SheafOfModules.{u} (structureSheafRing X))
        (ComplexShape.up ℤ))] :
    IsIso (localCohomologySheafForgetComparison X Z hZ RHab aHab RH aH)

Stacks.Cohomology.SupportedComplexes.localCohomologySheafFunctorZeroForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/UnderlyingAbelianLocalCohomologySheaves.lean, line 189. The attribute's comment: “part (2) in degree 0 only; the comparison in higher degrees is not proved here, see isIso_localCohomologySheafForgetComparison_of_isRightDerivedFunctor for the derived form”.

Stacks 0G74, part (2), in degree zero. Let Z be a closed subset of a ringed space X and let ℱ be a sheaf of 𝒪_X-modules with underlying abelian sheaf ℱ_ab. The degree-zero local cohomology sheaf ℋ ⁰_Z(ℱ), an 𝒪_X|_Z-module on Z, has underlying abelian sheaf the degree-zero local cohomology sheaf ℋ ⁰_Z(ℱ_ab) of ℱ_ab, naturally in ℱ.

In degree zero both sides are the supported-sections functor itself, H_Z being left exact, so this is supportedSectionsOnClosedForgetIso read through the two degree-zero identifications.

def localCohomologySheafFunctorZeroForgetIso (hZ : IsClosed Z) :
    localCohomologySheafFunctor X Z hZ 0 ⋙
        _root_.SheafOfModules.toSheaf (structureSheafRing (closedSubsetRingedSpace X Z)) ≅
      _root_.SheafOfModules.toSheaf (structureSheafRing X) ⋙
        ClosedImmersionSheaves.localCohomologySheafFunctor Z hZ 0

Stacks.Cohomology.UnderlyingAbelianSectionsWithSupport.sectionsWithSupportForgetComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/UnderlyingAbelianSectionsWithSupport.lean, line 531. The attribute's comment: “part (1), the canonical map, for given right derived functors of sections with support”.

Stacks 0G74, part (1): the canonical map. Let Z be a closed subset of a ringed space X, let RΓZ be a right derived functor of sections with support in Z of sheaves of O_X-modules and RΓZab one of sections with support in Z of abelian sheaves. This is the canonical map RΓ_Z(X, K) ⟶ RΓ_Z(X, K_ab) in D(Ab), natural in K, induced through the universal property of RΓZ by the underived comparison of sections with support.

def sectionsWithSupportForgetComparison
    [RΓZ.IsRightDerivedFunctor aZ
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RΓZab.IsRightDerivedFunctor aZab
      (HomotopyCategory.quasiIso (AbelianSheavesOnSpace X) (ComplexShape.up ℤ))] :
    RΓZ ⋙ underlyingDerivedGlobalModules X ⟶
      underlyingDerivedSheaf (structureSheafRing X) ⋙ RΓZab

Stacks.Cohomology.UnderlyingAbelianSectionsWithSupport.sectionsWithSupportForgetComparison_isIso, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/UnderlyingAbelianSectionsWithSupport.lean, line 560. The attribute's comment: “part (1), the map is an isomorphism, for given right derived functors of Gamma_Z”.

Stacks 0G74, part (1). Let (X, O_X) be a ringed space, Z ⊆ X a closed subset and K an object of D(O_X) with image K_ab in D(ℤ_X). The canonical map RΓ_Z(X, K) ⟶ RΓ_Z(X, K_ab) is an isomorphism in D(Ab), naturally in K.

instance sectionsWithSupportForgetComparison_isIso
    [RΓZ.IsRightDerivedFunctor aZ
      (HomotopyCategory.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RΓZab.IsRightDerivedFunctor aZab
      (HomotopyCategory.quasiIso (AbelianSheavesOnSpace X) (ComplexShape.up ℤ))] :
    IsIso (sectionsWithSupportForgetComparison X Z hZ RΓZab aZab RΓZ aZ)
Tag 0G75, a remark

Tag 0G75 in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.supportedTensorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedTensor.lean, line 215. The attribute's comment: “the canonical map K|_Z ⊗^L R𝓗_Z(M) ⟶ R𝓗_Z(K ⊗^L M); not functoriality in either complex”.

Stacks Project, Tag 0G75. For K and M in D(𝒪_X) and i : Z ⟶ X the inclusion of a closed subset, the canonical map K|_Z ⊗^L_{𝒪_X|_Z} R𝓗_Z(M) ⟶ R𝓗_Z(K ⊗^L_{𝒪_X} M) in D(𝒪_X|_Z): the map corresponding to supportedTensorMateMap under the adjunction i_* ⊣ R𝓗_Z of Tag 0A3B.

def supportedTensorMap
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    ((derivedTensorProductFunctor (closedSubsetRingedSpace X Z).sheaf).obj
        ((derivedPullback (closedSubsetInclusion X Z)).obj K)).obj
        ((derivedSupportedSectionsOnClosed X Z hZ).obj M) ⟶
      (derivedSupportedSectionsOnClosed X Z hZ).obj
        (((derivedTensorProductFunctor X.sheaf).obj K).obj M)

Stacks.Cohomology.SupportedComplexes.supportedTensorMap_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedTensor.lean, line 228. The attribute's comment: “the adjunction equation characterizing the canonical map”.

Stacks Project, Tag 0G75. The adjunction equation characterizing the canonical map: pushing it forward and composing with the counit of Tag 0A3B gives the displayed composite. This is what "by adjointness of i_* and R𝓗_Z" means in the source.

theorem supportedTensorMap_mate
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.map
          (supportedTensorMap X Z hZ K M) ≫
        (derivedPushforwardAdjunction X Z hZ).counit.app
          (((derivedTensorProductFunctor X.sheaf).obj K).obj M) =
      supportedTensorMateMap X Z hZ K M
Tag 0G76, a remark

Tag 0G76 in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.supportedCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedTensor.lean, line 298. The attribute's comment: “the cup product H^a(X, K) × H^b_Z(X, M) ⟶ H^(a+b)_Z(X, K ⊗^L M), as the source's four-step composite over an arbitrary presentation of the three groups by corepresenting objects; the source's own presentation by shifted structure sheaves is supportedCupProductOfClasses”. References: SGA 4½ Cycle (1.2.2), “(1.2.2.3), special case”.

Stacks Project, Tag 0G76. The cup product of a class ξ on X with a class η supported on Z: restrict ξ to Z, tensor the two on Z, and follow with the map of Tag 0G75. Reading W = 𝒪_Z[-a-b], U = 𝒪_X[-a] and V = 𝒪_Z[-b], and reading morphisms out of 𝒪_Z[-n] into R𝓗_Z(-) as classes in H^n_Z(X, -) by Tag 0G70, this is the source's H^a(X, K) × H^b_Z(X, M) ⟶ H^{a+b}_Z(X, K ⊗^L M). The source's identification 𝒪_Z[-a-b] = (𝒪_X[-a])|_Z ⊗^L 𝒪_Z[-b] is the morphism χ.

def supportedCupProduct
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    {U : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    {V W : DerivedCategory (SheafOfModules.{u}
      (structureSheafRing (closedSubsetRingedSpace X Z)))}
    (χ : W ⟶ ((derivedTensorProductFunctor (closedSubsetRingedSpace X Z).sheaf).obj
      ((derivedPullback (closedSubsetInclusion X Z)).obj U)).obj V)
    (ξ : U ⟶ K) (η : V ⟶ (derivedSupportedSectionsOnClosed X Z hZ).obj M) :
    W ⟶ (derivedSupportedSectionsOnClosed X Z hZ).obj
      (((derivedTensorProductFunctor X.sheaf).obj K).obj M)

Stacks.Cohomology.SupportedComplexes.supportedCupProductOfClasses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedTensor.lean, line 356. The attribute's comment: “the cup product H^a(X, K) × H^b_Z(X, M) ⟶ H^(a+b)_Z(X, K ⊗^L M) on classes represented by morphisms out of shifted structure sheaves, in the source's degrees”. References: SGA 4½ Cycle (1.2.2), “(1.2.2.2)”.

Stacks Project, Tag 0G76. The cup product of a class ξ ∈ H^a(X, K) and a class η ∈ H^b_Z(X, M) = H^b(Z, R𝓗_Z(M)), landing in H^{a+b}_Z(X, K ⊗^L M) = H^{a+b}(Z, R𝓗_Z(K ⊗^L M)): restrict ξ to Z, tensor the two classes on Z and follow with the map of Tag 0G75, after the identification 𝒪_Z[-a-b] = (𝒪_X[-a])|_Z ⊗^L 𝒪_Z[-b] of the corepresenting objects.

def supportedCupProductOfClasses
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (a b : ℤ)
    (ξ : shiftedStructureSheaf X a ⟶ K)
    (η : shiftedStructureSheaf (closedSubsetRingedSpace X Z) b ⟶
      (derivedSupportedSectionsOnClosed X Z hZ).obj M) :
    shiftedStructureSheaf (closedSubsetRingedSpace X Z) (a + b) ⟶
      (derivedSupportedSectionsOnClosed X Z hZ).obj
        (((derivedTensorProductFunctor X.sheaf).obj K).obj M)
Tag 0G77, a lemma

Tag 0G77 in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.forgetSupport_supportedCupProduct_square, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ForgetSupportCupProductComparison.lean, line 240.

Stacks Project, Tag 0G77. Let Z be a closed subset of a ringed space (X, 𝒪_X) and let K, M be objects of D(𝒪_X). The square

H^a(X, K) × H^b_Z(X, M) -----> H^{a+b}_Z(X, K ⊗^L M)
    |                                  |
    v                                  v
H^a(X, K) × H^b(X, M) -------> H^{a+b}(X, K ⊗^L M)

commutes, where the top arrow is the cup product of [Stacks, Tag 0G76], the bottom arrow is the cup product of [Stacks, Tag 0FP2] and the verticals forget support. A class of H^a(X, K) is a morphism ξ : 𝒪_X[-a] ⟶ K and a class of H^b_Z(X, M) = H^b(Z, R𝓗_Z(M)) is a morphism η : 𝒪_Z[-b] ⟶ R𝓗_Z(M) ([Stacks, Tag 0G70]); forgetting support is precomposition with the comparison 𝒪_X[-p] ⟶ i_*𝒪_Z[-p] followed by the counit i_*R𝓗_Z(-) ⟶ - of [Stacks, Tag 0A3B].

theorem forgetSupport_supportedCupProduct_square (X : RingedSpace.{u, u}) (Z : Set X.carrier)
    (hZ : IsClosed Z) (a b : ℤ) (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (ξ : shiftedUnitObject X a ⟶ K)
    (η : shiftedUnitObject (closedSubsetRingedSpace X Z) b ⟶
      (derivedSupportedSectionsOnClosed X Z hZ).obj M) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    shiftedUnitToPushforward Z (a + b) ≫
        (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.map
          (supportedCupProductOfClasses X Z hZ K M a b ξ η) ≫
        (derivedPushforwardAdjunction X Z hZ).counit.app
          (((derivedTensorProductFunctor X.sheaf).obj K).obj M) =
      (shiftedUnitTensorIso X a b).hom ≫
        ((derivedTensorProductFunctor X.sheaf).map ξ).app (shiftedUnitObject X b) ≫
        ((derivedTensorProductFunctor X.sheaf).obj K).map
          (shiftedUnitToPushforward Z b ≫
            (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.map η ≫
            (derivedPushforwardAdjunction X Z hZ).counit.app M)
Tag 0G78, a remark

Tag 0G78 in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.isIso_supportedPullbackMap_of_cohomologySupportedOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedPullbackInvertible.lean, line 234. The attribute's comment: “the canonical map is an isomorphism when K has cohomology sheaves supported on Z, for an arbitrary morphism of ringed spaces”.

The canonical map of [Stacks, Tag 0G78] is an isomorphism at a complex supported on Z. If every cohomology sheaf of K is supported on Z then the adjunction map ε_K : i_* R𝓗_Z(K) ⟶ K is itself an isomorphism, by [Stacks, Tag 0AEF] part (2), so the hypothesis of isIso_supportedPullbackMap_of_isIso_map_counit is immediate.

No hypothesis on f is used. This is the special case of the invertibility of Tag 0G78 that the library's Tag 0AEF already supplies, for an arbitrary morphism of ringed spaces; for an open immersion and an arbitrary K see isIso_supportedPullbackMap_of_isOpenImmersion.

theorem isIso_supportedPullbackMap_of_cohomologySupportedOn
    (hZ' : IsClosed (closedSubsetPreimage f Z))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hK : AlgebraicGeometry.CohomologySupportedOn (structureSheafRing X) Z K) :
    IsIso (supportedPullbackMap f Z hZ hZ' K)

Stacks.Cohomology.SupportedComplexes.isIso_supportedPullbackMap_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedPullbackOpenImmersion.lean, line 241. The attribute's comment: “the canonical map is an isomorphism along an open immersion of ringed spaces, unconditionally”.

[Stacks, Tag 0G78] along an open immersion, unconditionally. For an open immersion of ringed spaces f : X' ⟶ X, a closed Z ⊆ X and Z' = f^{-1}(Z), the canonical map

L(f|_{Z'})^* R𝓗_Z(K) ⟶ R𝓗_{Z'}(Lf^* K)

of [Stacks, Tag 0G78] is an isomorphism for every K in D(𝒪_X).

Nothing is assumed beyond f being an open immersion and Z being closed. The proof is isIso_supportedPullbackMap_of_natIso applied to derivedSupportedSectionsOnClosedPullbackNatIso.

theorem isIso_supportedPullbackMap_of_isOpenImmersion (hZ : IsClosed Z)
    (hZ' : IsClosed (closedSubsetPreimage f Z))
    (K : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing X))) :
    letI := pushforward_preservesFiniteLimits X Z
    letI := pushforward_preservesFiniteColimits X Z hZ
    letI := pushforward_preservesFiniteLimits X' (closedSubsetPreimage f Z)
    letI := pushforward_preservesFiniteColimits X' (closedSubsetPreimage f Z) hZ'
    IsIso (supportedPullbackMap f Z hZ hZ' K)

Stacks.Cohomology.SupportedComplexes.isIso_supportedPullbackBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedPullback.lean, line 449. The attribute's comment: “the Remark's own assertion that the map of functors Lf^ i_ -> i'_ L(f|Z')^ of Remark 20.28.3 (Tag 08HY) is an isomorphism in this case, proved for every M in D(O_X|Z), in particular at M = RHZ(K); the source's stalkwise justification is replaced by the essential-image half of Tag 0AEF part (2)”.

[Stacks, Tag 0G78]: the map of functors of [Stacks, Tag 08HY] is an isomorphism in this case, for every object of D(𝒪_X|_Z). The base-change transformation of [Stacks, Tag 08HY] for the square of the restriction,

Lf^*(Ri_*M) ⟶ Ri'_*(L(f|_{Z'})^*M),

is an isomorphism for every M, in particular at M = R𝓗_Z(K).

This is the essential-image half of [Stacks, Tag 0AEF] part (2) applied twice. The base-change map is, by [Stacks, Tag 08HY]'s adjoint characterization, the unit of Li'^* ⊣ Ri'_* at Lf^*(Ri_*M) followed by Ri'_* of a composite of three isomorphisms: the two composition isomorphisms of [Stacks, Tag 0D5S], and the derived counit Li^*(Ri_*M) ⟶ M, which is invertible because Ri_* is fully faithful for a closed-subset inclusion. So only the unit is in question, and the unit of an adjunction with fully faithful right adjoint is invertible exactly on the essential image of that right adjoint. The source Lf^*(Ri_*M) lies there: Ri_*M has its cohomology supported on Z, derived pullback carries that to support on Z' = f^{-1}(Z) by cohomologySupportedOn_derivedPullback, and [Stacks, Tag 0AEF] part (2) puts every Z'-supported complex in the essential image of Ri'_*.

theorem isIso_supportedPullbackBaseChangeMap
    (M : DerivedCategory (SheafOfModules.{u}
      (structureSheafRing (closedSubsetRingedSpace X Z)))) :
    IsIso (supportedPullbackBaseChangeMap f Z M)

Stacks.Cohomology.SupportedComplexes.supportedPullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedPullback.lean, line 523. The attribute's comment: “the canonical map and the adjunction equation characterizing it; the invertibility of the base-change transformation of Tag 08HY, which is the stalkwise step of the source, is isIso_supportedPullbackBaseChangeMap above”.

[Stacks, Tag 0G78]. Let f : (X', 𝒪_{X'}) ⟶ (X, 𝒪_X) be a morphism of ringed spaces, let Z ⊆ X be closed and let Z' = f^{-1}(Z). For K in D(𝒪_X) the canonical map

L(f|_{Z'})^* R𝓗_Z(K) ⟶ R𝓗_{Z'}(Lf^* K)

in D(𝒪_{X'}|_{Z'}): the map corresponding to supportedPullbackMateMap under the adjunction i'_* ⊣ R𝓗_{Z'} of [Stacks, Tag 0A3B] part (1).

def supportedPullbackMap (hZ' : IsClosed (closedSubsetPreimage f Z))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    (derivedPullback (closedSubsetRestriction f Z)).obj
        ((derivedSupportedSectionsOnClosed X Z hZ).obj K) ⟶
      (derivedSupportedSectionsOnClosed X' (closedSubsetPreimage f Z) hZ').obj
        ((derivedPullback f).obj K)

Stacks.Cohomology.SupportedComplexes.supportedPullbackMap_mate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedPullback.lean, line 538. The attribute's comment: “the factorization of the pulled-back adjunction map through the adjunction map on the preimage”.

[Stacks, Tag 0G78], the adjunction equation characterizing the canonical map. Pushing the canonical map forward from Z' and composing with the adjunction map i'_* R𝓗_{Z'}(Lf^* K) ⟶ Lf^* K of [Stacks, Tag 0A3B] gives the displayed composite. This is the unique factorization that the source obtains from part (3) of [Stacks, Tag 0AEF].

theorem supportedPullbackMap_mate (hZ' : IsClosed (closedSubsetPreimage f Z))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    (modulePushforward
            (closedSubsetInclusion X' (closedSubsetPreimage f Z))).mapDerivedCategory.map
          (supportedPullbackMap f Z hZ hZ' K) ≫
        (derivedPushforwardAdjunction X' (closedSubsetPreimage f Z) hZ').counit.app
          ((derivedPullback f).obj K) =
      supportedPullbackMateMap f Z hZ K

Stacks.Cohomology.SupportedComplexes.supportedPullbackMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedPullback.lean, line 556. The attribute's comment: “the uniqueness the Remark asserts: 'we find that the south-east arrow factors UNIQUELY over the south-west arrow'. This is the half of the universality of Tag 0AEF part (3) that supportedPullbackMap_mate does not state, and it is what makes the canonical map canonical -- neither the zero map nor the negative of it satisfies the characterization”.

The adjunction equation determines the canonical map of [Stacks, Tag 0G78]: no other morphism of that type satisfies it. Together with supportedPullbackMap_mate this says the map is the unique solution of the characterization, so the construction is not under-determined.

theorem supportedPullbackMap_unique (hZ' : IsClosed (closedSubsetPreimage f Z))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (g : (derivedPullback (closedSubsetRestriction f Z)).obj
        ((derivedSupportedSectionsOnClosed X Z hZ).obj K) ⟶
      (derivedSupportedSectionsOnClosed X' (closedSubsetPreimage f Z) hZ').obj
        ((derivedPullback f).obj K))
    (hg : (modulePushforward
              (closedSubsetInclusion X' (closedSubsetPreimage f Z))).mapDerivedCategory.map g ≫
          (derivedPushforwardAdjunction X' (closedSubsetPreimage f Z) hZ').counit.app
            ((derivedPullback f).obj K) =
        supportedPullbackMateMap f Z hZ K) :
    g = supportedPullbackMap f Z hZ hZ' K

Stacks.Cohomology.SupportedComplexes.supportedPullbackMap_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/SupportedSectionsDerivedPullback.lean, line 587. The attribute's comment: “the commutative triangle, with the base-change transformation of Tag 08HY on the left”.

[Stacks, Tag 0G78], the commutative triangle of the source. Composing the base-change transformation of [Stacks, Tag 08HY] with the pushforward from Z' of the canonical map and the adjunction map i'_* R𝓗_{Z'}(Lf^* K) ⟶ Lf^* K gives the derived pullback along f of the adjunction map i_* R𝓗_Z(K) ⟶ K.

This is supportedPullbackMap_mate with the inverse of the base-change transformation cleared from the statement, so it is the triangle of the source read literally: the diagonal arrow out of Lf^*(i_* R𝓗_Z(K)) factors through the adjunction map on the preimage.

theorem supportedPullbackMap_triangle (hZ' : IsClosed (closedSubsetPreimage f Z))
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    supportedPullbackBaseChangeMap f Z ((derivedSupportedSectionsOnClosed X Z hZ).obj K) ≫
          (closedPushforwardComparison X' (closedSubsetPreimage f Z)).inv.app _ ≫
          (modulePushforward
              (closedSubsetInclusion X' (closedSubsetPreimage f Z))).mapDerivedCategory.map
            (supportedPullbackMap f Z hZ hZ' K) ≫
          (derivedPushforwardAdjunction X' (closedSubsetPreimage f Z) hZ').counit.app
            ((derivedPullback f).obj K) =
      (derivedPullback f).map ((closedPushforwardComparison X Z).inv.app _) ≫
        (derivedPullback f).map ((derivedPushforwardAdjunction X Z hZ).counit.app K)
Tag 0G79, a lemma

Tag 0G79 in the Stacks Project.

Stacks.Cohomology.SupportedComplexes.forgetSupport_pullbackSupportedClass_preimage_shiftedUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/ForgetSupportAndPullback.lean, line 502. The attribute's comment: “the commuting square for the canonical map of Tag 0G78 itself, at the canonical corepresenting objects: the four groups are corepresented by the shifted structure sheaves of Tag 0G70, the four comparisons between them are the canonical ones, and their agreement across the square -- the pseudofunctoriality of the structure-sheaf comparison of Tag 01CD with respect to the composition isomorphism of derived pullbacks of Tag 0D5S -- is StacksDraft.UnitPullbackComposition.shiftedUnitIso_square_left. The binders are the degree p, the complex K and the class eta, which are the data of a class in H^p_Z(X, K)”.

Stacks Project, Tag 0G79, at the canonical corepresenting objects. The four groups are corepresented by the shifted structure sheaves of [Stacks, Tag 0G70] — 𝒪_X[-p], 𝒪_{X'}[-p], 𝒪_Z[-p], 𝒪_{Z'}[-p] with Z' = f^{-1}(Z) — and the four comparisons between them are the canonical ones: ρ, ρ' are shiftedUnitToPushforward, and c, d are the identifications Lf^*(𝒪_X[-p]) ≅ 𝒪_{X'}[-p] of Stacks.RingedSpace.derivedPullbackShiftedUnitIso.

Those four identifications agree across the square — that is the pseudofunctoriality of the structure-sheaf comparison of [Stacks, Tag 01CD] with respect to the composition isomorphism of [Stacks, Tag 0D5S], in which no derived pushforward, no base-change transformation of [Stacks, Tag 08HY], no R𝓗_Z and no adjunction map occur. It is proved in degree 0 (StacksDraft.UnitPullbackComposition.derivedPullbackCompIsoCanonical_hom_app_singleUnit), in an arbitrary degree p (StacksDraft.UnitPullbackComposition.derivedPullbackCompIsoCanonical_hom_app_shiftedUnit, which also needed the first CategoryTheory.NatTrans.CommShift for the composition comparison of [Stacks, Tag 0D5S], StacksDraft.UnitPullbackComposition.commShift_derivedPullbackCompComparisonCanonical), and around the square in the spelling this statement needs (StacksDraft.UnitPullbackComposition.shiftedUnitIso_square_left), which is what is supplied below.

theorem forgetSupport_pullbackSupportedClass_preimage_shiftedUnit (p : ℤ)
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (η : shiftedUnitObject (closedSubsetRingedSpace X Z) p ⟶
      (derivedSupportedSectionsOnClosed X Z hZ).obj K) :
    shiftedUnitToPushforward (X := X') (closedSubsetPreimage f Z) p ≫
        (modulePushforward
            (closedSubsetInclusion X' (closedSubsetPreimage f Z))).mapDerivedCategory.map
          ((derivedPullbackShiftedUnitIso (closedSubsetRestriction f Z) p).inv ≫
            (derivedPullback (closedSubsetRestriction f Z)).map η ≫
            supportedPullbackMap f Z hZ (isClosed_closedSubsetPreimage f Z hZ) K) ≫
        (derivedPushforwardAdjunction X' (closedSubsetPreimage f Z)
            (isClosed_closedSubsetPreimage f Z hZ)).counit.app ((derivedPullback f).obj K) =
      (derivedPullbackShiftedUnitIso f p).inv ≫ (derivedPullback f).map
        (shiftedUnitToPushforward Z p ≫
          (modulePushforward (closedSubsetInclusion X Z)).mapDerivedCategory.map η ≫
          (derivedPushforwardAdjunction X Z hZ).counit.app K)
Sources
LeanStacks.Cohomology.SupportedComplexes.derivedPushforwardAdjunction · Stacks.Cohomology.SupportedComplexes.derivedPushforwardCompDerivedSupportedSectionsIsoId · Stacks.Cohomology.SupportedComplexes.derivedPushforward_adj_derivedSupportedSectionsOnClosed · Stacks.Cohomology.SupportedComplexes.exists_isIso_unit_derivedPushforward_adj_derivedSupportedSectionsOnClosed · Stacks.Cohomology.SupportedComplexes.isZero_rightDerivedPlus_supportedSectionsOnClosed_modulePushforward · Stacks.Cohomology.SupportedComplexes.isIso_derivedPushforwardAdjunction_counit_app_of_supported · Stacks.Cohomology.SupportedComplexes.derivedPushforwardSupportedSectionsIso · Stacks.Cohomology.SupportedComplexes.closedSubsetDerivedPushforwardEquivalence

Section20.35 Inverse systems and cohomology, I#

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

Tag 0GYK, a lemma

Tag 0GYK in the Stacks Project.

Stacks.Cohomology.MittagLefflerCohomology.cohomology_transitionImage_stable_uniformly_of_powerCohomologyGradedACC, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/MittagLefflerCohomology/PowerCohomologyACC.lean, line 299. The attribute's comment: “uniform stabilization (footnote)”.

If the whole graded module ⨁ₙ Hᵖ⁺¹(X, Iⁿ𝓕ₙ₊₁) satisfies graded ACC, there is a single lag c such that, for every i, the image of Hᵖ(F_(i+c+1)) → Hᵖ(F_(i+1)) is already the stable image.

public theorem cohomology_transitionImage_stable_uniformly_of_powerCohomologyGradedACC
    (I : Ideal A) (F : ℕᵒᵖ ⥤ ModuleSheaf.{u, v, w} A X) (p : ℕ)
    (hquotient : IsQuotientTower.{u, v, w} I F)
    (hACC : PowerCohomologyHaveGradedACC.{u, v, w} I F (p + 1)) :
    ∃ c : ℕ, ∀ (i m : ℕ) (h : i + c ≤ m),
      transitionImage (F ⋙ cohomology.{u, v, w} (A := A) (X := X) p)
        i m ((Nat.le_add_right i c).trans h) =
      transitionImage (F ⋙ cohomology.{u, v, w} (A := A) (X := X) p)
        i (i + c) (Nat.le_add_right i c)

Stacks.Cohomology.MittagLefflerCohomology.isMittagLeffler_cohomology_of_powerCohomologyGradedACC, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/MittagLefflerCohomology/PowerCohomologyACC.lean, line 314. The attribute's comment: “Mittag-Leffler condition”.

If the whole graded module ⨁ₙ Hᵖ⁺¹(X, Iⁿ𝓕ₙ₊₁) satisfies graded ACC, the degree-p cohomology tower of an ideal-power quotient system satisfies the Mittag-Leffler condition.

public theorem isMittagLeffler_cohomology_of_powerCohomologyGradedACC
    (I : Ideal A) (F : ℕᵒᵖ ⥤ ModuleSheaf.{u, v, w} A X) (p : ℕ)
    (hquotient : IsQuotientTower.{u, v, w} I F)
    (hACC : PowerCohomologyHaveGradedACC.{u, v, w} I F (p + 1)) :
    IsMittagLefflerCategorical
      (F ⋙ cohomology.{u, v, w} (A := A) (X := X) p)
Tag 0GYL, a lemma

Tag 0GYL in the Stacks Project.

Stacks.Cohomology.MittagLefflerCohomology.cohomology_transitionImage_stable_uniformly, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/MittagLefflerCohomology/StableImagesACC.lean, line 1142. The attribute's comment: “uniform stabilization (footnote)”.

Under the same hypotheses, there is a single lag c such that, for every i, the image of Hᵖ(F_(i+c+1)) → Hᵖ(F_(i+1)) is already the stable image.

public theorem cohomology_transitionImage_stable_uniformly
    {A : Type u} [CommRing A] [Small.{v} A] (I : Ideal A)
    {X : Type w} [TopologicalSpace X]
    [UnivLE.{max w v, v}]
    (F : ℕᵒᵖ ⥤ ModuleSheaf.{u, v, w} A X) (p : ℕ)
    (hquotient : IsQuotientTower.{u, v, w} I F)
    (hACC : StableImagesHaveGradedACC.{u, v, w} I F (p + 1)) :
    ∃ c : ℕ, ∀ (i m : ℕ) (h : i + c ≤ m),
      transitionImage (F ⋙ cohomology.{u, v, w} (A := A) (X := X) p)
        i m ((Nat.le_add_right i c).trans h) =
      transitionImage (F ⋙ cohomology.{u, v, w} (A := A) (X := X) p)
        i (i + c) (Nat.le_add_right i c)

Stacks.Cohomology.MittagLefflerCohomology.isMittagLeffler_cohomology_of_stableImagesGradedACC, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/MittagLefflerCohomology/StableImagesACC.lean, line 1180. The attribute's comment: “Mittag-Leffler condition”.

If the stable images in degree p + 1 satisfy graded ACC, the degree-p cohomology tower of an ideal-power quotient system satisfies the Mittag-Leffler condition.

public theorem isMittagLeffler_cohomology_of_stableImagesGradedACC
    {A : Type u} [CommRing A] [Small.{v} A] (I : Ideal A)
    {X : Type w} [TopologicalSpace X]
    [UnivLE.{max w v, v}]
    (F : ℕᵒᵖ ⥤ ModuleSheaf.{u, v, w} A X) (p : ℕ)
    (hquotient : IsQuotientTower.{u, v, w} I F)
    (hACC : StableImagesHaveGradedACC.{u, v, w} I F (p + 1)) :
    IsMittagLefflerCategorical
      (F ⋙ cohomology.{u, v, w} (A := A) (X := X) p)
Tag 0GYM, a lemma

Tag 0GYM in the Stacks Project.

Stacks.Cohomology.QuotientTowers.cohomologyTowerLimit_topology_eq_adic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/QuotientTowers.lean, line 1435. The attribute's comment: “the same conclusion under the stronger ACC hypothesis on the ambient graded”.

For a quotient tower of sheaves F whose stable images satisfy ACC over gr_I(A), the inverse-limit topology on lim Hᵖ(X, F_n) equals the I-adic topology.

public theorem cohomologyTowerLimit_topology_eq_adic
    [Small.{v} A] [UnivLE.{max w v, v}]
    (I : Ideal A) (X : Type w) [TopologicalSpace X]
    (F : ℕᵒᵖ ⥤ ModuleSheaf.{u, v, w} A X) (p : ℕ)
    (hquotient : IsQuotientTower.{u, v, w} I F)
    (hACC : StableImagesHaveGradedACC.{u, v, w} I F p) :
    CohomologyTowerLimit.limitTopology (fun n => cohomologyModule.{u, v, w} F p n)
        (cohomologyTransition.{u, v, w} F p) =
      I.adicModuleTopology
        (CohomologyTowerLimit (fun n => cohomologyModule.{u, v, w} F p n)
          (cohomologyTransition.{u, v, w} F p))
Tag 0GYN, a lemma

Tag 0GYN in the Stacks Project.

Stacks.Cohomology.QuotientTowers.cohomologyTowerLimit_topology_eq_adic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/QuotientTowers.lean, line 1435.

For a quotient tower of sheaves F whose stable images satisfy ACC over gr_I(A), the inverse-limit topology on lim Hᵖ(X, F_n) equals the I-adic topology.

public theorem cohomologyTowerLimit_topology_eq_adic
    [Small.{v} A] [UnivLE.{max w v, v}]
    (I : Ideal A) (X : Type w) [TopologicalSpace X]
    (F : ℕᵒᵖ ⥤ ModuleSheaf.{u, v, w} A X) (p : ℕ)
    (hquotient : IsQuotientTower.{u, v, w} I F)
    (hACC : StableImagesHaveGradedACC.{u, v, w} I F p) :
    CohomologyTowerLimit.limitTopology (fun n => cohomologyModule.{u, v, w} F p n)
        (cohomologyTransition.{u, v, w} F p) =
      I.adicModuleTopology
        (CohomologyTowerLimit (fun n => cohomologyModule.{u, v, w} F p n)
          (cohomologyTransition.{u, v, w} F p))
Sources
LeanStacks.Cohomology.MittagLefflerCohomology.cohomology_transitionImage_stable_uniformly_of_powerCohomologyGradedACC · Stacks.Cohomology.MittagLefflerCohomology.isMittagLeffler_cohomology_of_powerCohomologyGradedACC · Stacks.Cohomology.MittagLefflerCohomology.cohomology_transitionImage_stable_uniformly · Stacks.Cohomology.MittagLefflerCohomology.isMittagLeffler_cohomology_of_stableImagesGradedACC · Stacks.Cohomology.QuotientTowers.cohomologyTowerLimit_topology_eq_adic

Section20.36 Inverse systems and cohomology, II#

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

Tag 0H39, a lemma

Tag 0H39 in the Stacks Project.

Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.stacks0H39_one_iff_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/TorsionFreeAndDivisibleSystems.lean, line 1419. The attribute's comment: “(1)⇔(2)”.

Conditions (1) and (2) on an inverse system are equivalent.

theorem stacks0H39_one_iff_two
    (f : End (𝟭 (SheafOfModules.{max u v} R)))
    (obj : ℕ → SheafOfModules.{max u v} R) (map : ∀ n, obj (n + 1) ⟶ obj n) :
    Condition1 f obj map ↔ Condition2 f obj map

Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.stacks0H39_two_iff_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/TorsionFreeAndDivisibleSystems.lean, line 1427. The attribute's comment: “(2)⇔(3)”.

Conditions (2) and (3) on an inverse system are equivalent.

theorem stacks0H39_two_iff_three
    (f : End (𝟭 (SheafOfModules.{max u v} R)))
    (obj : ℕ → SheafOfModules.{max u v} R) (map : ∀ n, obj (n + 1) ⟶ obj n) :
    Condition2 f obj map ↔ Condition3 f obj map

Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.stacks0H39_four_imp_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/TorsionFreeAndDivisibleSystems.lean, line 1435. The attribute's comment: “(4)⇒(3)”.

Condition (4) on an inverse system implies condition (3).

theorem stacks0H39_four_imp_three
    (f : End (𝟭 (SheafOfModules.{max u v} R)))
    (obj : ℕ → SheafOfModules.{max u v} R) (map : ∀ n, obj (n + 1) ⟶ obj n) :
    Condition4 f obj map → Condition3 f obj map
Tag 0EHA, a lemma

Tag 0EHA in the Stacks Project.

Stacks.Cohomology.InverseSystems.range_pow_eq_ker_limitProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/AdicTopologyOnLimitCohomology.lean, line 355.

Let f be a global section of O and let … → 𝓕₂ → 𝓕₁ be an inverse system of O-modules satisfying condition (1) of Stacks 0H39 for multiplication by f. For every c = n + 1 ≥ 1 the submodule f^c · lim Hᵖ(C, 𝓕ₙ) of lim Hᵖ(C, 𝓕ₙ) is the kernel of the projection to Hᵖ(C, 𝓕_c).

theorem range_pow_eq_ker_limitProjection (f : ↥(GlobalSectionRing O))
    (obj : ℕ → SheafOfModules.{max u v} O) (map : ∀ n, obj (n + 1) ⟶ obj n)
    (h : Condition1 (Stacks.SheafOfModules.globalSectionToEnd O ⟨f.1, f.2⟩) obj map) (p n : ℕ) :
    LinearMap.range (LinearMap.lsmul ↥(GlobalSectionRing O)
        (limit (Functor.ofOpSequence map ⋙ globalModuleCohomology.{u, v, max u v, max u v} O p) :
          ModuleCat.{max u v} ↥(GlobalSectionRing O)) (f ^ (n + 1))) =
      LinearMap.ker (limit.π (Functor.ofOpSequence map ⋙
        globalModuleCohomology.{u, v, max u v, max u v} O p) (op n)).hom

Stacks.Cohomology.InverseSystems.range_pow_eq_ker_limitProjection_and_limitTopology_eq_adic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/AdicTopologyOnLimitCohomology.lean, line 396. The attribute's comment: “both conclusions: f^c Hᵖ is the kernel of Hᵖ → Hᵖ(X, 𝓕_c) for all c ≥ 1, and the limit topology on Hᵖ is the f-adic topology”.

Let f be a global section of O and let … → 𝓕₂ → 𝓕₁ be an inverse system of O-modules satisfying condition (1) of Stacks 0H39 for multiplication by f, and let p ≥ 0. Put Hᵖ = lim Hᵖ(C, 𝓕ₙ). Then for every c = n + 1 ≥ 1 the submodule f^c Hᵖ is the kernel of Hᵖ → Hᵖ(C, 𝓕_c), and the limit topology on Hᵖ (the infimum of the topologies induced by the projections to the discrete Hᵖ(C, 𝓕_c)) is the f-adic topology.

theorem range_pow_eq_ker_limitProjection_and_limitTopology_eq_adic
    (f : ↥(GlobalSectionRing O))
    (obj : ℕ → SheafOfModules.{max u v} O) (map : ∀ n, obj (n + 1) ⟶ obj n)
    (h : Condition1 (Stacks.SheafOfModules.globalSectionToEnd O ⟨f.1, f.2⟩) obj map) (p : ℕ) :
    (∀ n : ℕ, LinearMap.range (LinearMap.lsmul ↥(GlobalSectionRing O)
        (limit (Functor.ofOpSequence map ⋙ globalModuleCohomology.{u, v, max u v, max u v} O p) :
          ModuleCat.{max u v} ↥(GlobalSectionRing O)) (f ^ (n + 1))) =
      LinearMap.ker (limit.π (Functor.ofOpSequence map ⋙
        globalModuleCohomology.{u, v, max u v, max u v} O p) (op n)).hom) ∧
    (⨅ n : ℕ, TopologicalSpace.induced
        (fun y : (limit (Functor.ofOpSequence map ⋙
            globalModuleCohomology.{u, v, max u v, max u v} O p) :
          ModuleCat.{max u v} ↥(GlobalSectionRing O)) =>
          (limit.π (Functor.ofOpSequence map ⋙
            globalModuleCohomology.{u, v, max u v, max u v} O p) (op n)).hom y) ⊥) =
      (Ideal.span {f}).adicModuleTopology
        (limit (Functor.ofOpSequence map ⋙ globalModuleCohomology.{u, v, max u v, max u v} O p) :
          ModuleCat.{max u v} ↥(GlobalSectionRing O))
Tag 0BLB, a lemma

Tag 0BLB in the Stacks Project.

Stacks.Modules.PrincipalAdicInverseSystem.isSMulRegular_limit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/PrincipalAdicNonzerodivisor.lean, line 39. The attribute's comment: “nonzerodivisor”.

The distinguished element of a principal-adic inverse system is a nonzerodivisor on the limit of its global sections.

lemma isSMulRegular_limit (S : PrincipalAdicInverseSystem.{u, w}) :
    IsSMulRegular S.M S.f

Stacks.Modules.PrincipalAdicInverseSystem.finite_limitGlobalSections, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/PrincipalAdicLimitFinite.lean, line 38. The attribute's comment: “finite”.

The limit of global sections of a principal-adic inverse system is finite over its base ring.

lemma finite_limitGlobalSections (S : PrincipalAdicInverseSystem.{u, w}) :
    Module.Finite S.A S.M

Stacks.Modules.PrincipalAdicInverseSystem.quotientEquivRange_firstProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/PrincipalAdicLimitImage.lean, line 64. The attribute's comment: “image”.

The quotient of the inverse limit by f maps isomorphically onto its image in the first term, by the map induced by the first projection.

def quotientEquivRange_firstProjection (S : PrincipalAdicInverseSystem.{u, w}) :
    (S.M ⧸ (LinearMap.lsmul S.A S.M S.f).range) ≃ₗ[S.A]
      LinearMap.range ((limit.π S.globalSectionsSystem (op 0)).hom)

Stacks.Modules.PrincipalAdicInverseSystem.quotientEquivRange_firstProjection_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/PrincipalAdicLimitImage.lean, line 73. The attribute's comment: “image”.

The canonical equivalence sends a class to the first projection of a representative.

theorem quotientEquivRange_firstProjection_mk (S : PrincipalAdicInverseSystem.{u, w})
    (x : S.M) :
    quotientEquivRange_firstProjection S (Submodule.Quotient.mk x) =
      ⟨(limit.π S.globalSectionsSystem (op 0)).hom x,
        LinearMap.mem_range_self _ x⟩
Tag 0BLC, a lemma

Tag 0BLC in the Stacks Project.

Stacks.Cohomology.InverseSystems.isMittagLefflerCategorical_of_finite_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/MittagLefflerCriteria.lean, line 460.

Stacks 0BLC. Let A be a ring, f ∈ A, X a topological space and … → ℱ₂ → ℱ₁ an inverse system of sheaves of A-modules satisfying condition (1) of Stacks 0H39. If H^{p+1}(X, ℱ₁) has finite length over A, or A is Noetherian and H^{p+1}(X, ℱ₁) is a finite A-module, then the inverse system n ↦ H^p(X, ℱ_n) satisfies the Mittag-Leffler condition.

theorem isMittagLefflerCategorical_of_finite_cohomology
    {X : Type u} [TopologicalSpace X]
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [∀ U, IsMulCommutative (R.obj.obj U)]
    (A : Type u) [CommRing A]
    [Algebra A (R.obj.obj (op (⊤ : Opens X)))] (f : A)
    (obj : ℕ → SheafOfModules.{u} R)
    (map : ∀ n, obj (n + 1) ⟶ obj n) (p : ℕ) :
    let E := SheafOfModules.evaluation R (op (⊤ : Opens X))
    let G := E.rightDerived (p + 1)
    letI : Module A (G.obj (obj 0)) :=
      Module.compHom (G.obj (obj 0)) (algebraMap A (R.obj.obj (op (⊤ : Opens X))))
    ((IsFiniteLength A (G.obj (obj 0))) ∨
      (IsNoetherianRing A ∧ Module.Finite A (G.obj (obj 0)))) →
    Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.Condition1
      (Stacks.SheafOfModules.terminalSectionToEnd R (⊤ : Opens X) isTerminalTop
        (algebraMap A (R.obj.obj (op (⊤ : Opens X))) f)) obj map →
    IsMittagLefflerCategorical
      (Functor.ofOpSequence map ⋙ E.rightDerived p)
Tag 0DXG, a lemma

Tag 0DXG in the Stacks Project.

Stacks.Cohomology.InverseSystems.isMittagLefflerCategorical_of_finite_cohomology_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/MittagLefflerCriteria.lean, line 784.

Stacks 0DXG. Let A be a ring, f ∈ A, X a topological space and … → ℱ₂ → ℱ₁ an inverse system of sheaves of A-modules satisfying condition (1) of Stacks 0H39. If for some m the image of H^{p+1}(X, ℱ_m) → H^{p+1}(X, ℱ₁) has finite length over A, or A is Noetherian and the intersection of all those images is a finite A-module, then the inverse system n ↦ H^p(X, ℱ_n) satisfies the Mittag-Leffler condition.

theorem isMittagLefflerCategorical_of_finite_cohomology_image
    {X : Type u} [TopologicalSpace X]
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [∀ U, IsMulCommutative (R.obj.obj U)]
    (A : Type u) [CommRing A]
    [Algebra A (R.obj.obj (op (⊤ : Opens X)))] (f : A)
    (obj : ℕ → SheafOfModules.{u} R)
    (map : ∀ n, obj (n + 1) ⟶ obj n) (p : ℕ) :
    let E := SheafOfModules.evaluation R (op (⊤ : Opens X))
    let G := E.rightDerived (p + 1)
    letI : Module A (G.obj (obj 0)) :=
      Module.compHom (G.obj (obj 0)) (algebraMap A (R.obj.obj (op (⊤ : Opens X))))
    letI : IsScalarTower A (R.obj.obj (op (⊤ : Opens X))) (G.obj (obj 0)) :=
      ⟨fun a b x => by
        rw [Algebra.smul_def]
        change (algebraMap A (R.obj.obj (op (⊤ : Opens X))) a * b) • x =
          (algebraMap A (R.obj.obj (op (⊤ : Opens X))) a) • (b • x)
        exact mul_smul _ _ _⟩
    ((∃ n : ℕ, IsFiniteLength A
        (↥((LinearMap.range (G.map (Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.proj obj
          map n)).hom).restrictScalars A))) ∨
      (IsNoetherianRing A ∧ Module.Finite A
        (↥(⨅ n : ℕ,
          (LinearMap.range (G.map (Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.proj obj
            map n)).hom).restrictScalars A)))) →
      Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.Condition1
        (Stacks.SheafOfModules.terminalSectionToEnd R (⊤ : Opens X) isTerminalTop
          (algebraMap A (R.obj.obj (op (⊤ : Opens X))) f)) obj map →
      IsMittagLefflerCategorical
        (Functor.ofOpSequence map ⋙ E.rightDerived p)
Sources
LeanStacks.Cohomology.InverseSystems.TorsionFreeDivisible.stacks0H39_one_iff_two · Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.stacks0H39_two_iff_three · Stacks.Cohomology.InverseSystems.TorsionFreeDivisible.stacks0H39_four_imp_three · Stacks.Cohomology.InverseSystems.range_pow_eq_ker_limitProjection · Stacks.Cohomology.InverseSystems.range_pow_eq_ker_limitProjection_and_limitTopology_eq_adic · Stacks.Modules.PrincipalAdicInverseSystem.isSMulRegular_limit · Stacks.Modules.PrincipalAdicInverseSystem.finite_limitGlobalSections · Stacks.Modules.PrincipalAdicInverseSystem.quotientEquivRange_firstProjection

Section20.37 Derived limits#

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

Tag 0D60, a lemma

Tag 0D60 in the Stacks Project.

Stacks.Cohomology.DerivedLimitSections.isDerivedLimit_map_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/SpaltensteinCriterion/DerivedSectionsLimit.lean, line 209. The attribute's comment: “commutation with derived limits”.

Derived sections over an open of a ringed space carry a countable derived inverse limit to a derived inverse limit: RΓ(U, R\lim Kₙ) = R\lim RΓ(U, Kₙ).

theorem isDerivedLimit_map_derivedSections
    (RGamma : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory AddCommGrpCat.{u})
    (comparison : (sections X U).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
      DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ RGamma)
    (hRGamma : RGamma.IsRightDerivedFunctor comparison
      (HomologicalComplex.quasiIso (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)))
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) (hL : IsDerivedLimit K L) :
    ∃ h : HasProduct (fun n : ℕ ↦ RGamma.obj (K.obj ⟨n⟩)),
      @IsDerivedLimit (DerivedCategory AddCommGrpCat.{u}) _ _ _ _ _ _
        (K ⋙ RGamma) h (RGamma.obj L)

Stacks.Cohomology.DerivedLimitSections.exists_shortExact_limOne_cohomology_derivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/SpaltensteinCriterion/DerivedSectionsLimit.lean, line 267. The attribute's comment: “short exact sequence”.

For every open U of a ringed space and every degree m, the cohomology of a countable derived inverse limit lies in the Milnor short exact sequence

0 ⟶ R¹\lim H^{m-1}(U, Kₙ) ⟶ H^m(U, R\lim Kₙ) ⟶ \lim H^m(U, Kₙ) ⟶ 0.

Here R¹\lim is the cokernel of the difference map 1 - shift on the product of the groups H^{m-1}(U, Kₙ). The map to the inverse limit is characterised by its composites with the limit projections, which are the maps on cohomology induced by the given structural maps L ⟶ Kₙ.

theorem exists_shortExact_limOne_cohomology_derivedLimit
    (RGamma : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory AddCommGrpCat.{u})
    (comparison : (sections X U).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
      DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ RGamma)
    (hRGamma : RGamma.IsRightDerivedFunctor comparison
      (HomologicalComplex.quasiIso (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)))
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
            K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))))
    (m : ℤ) :
    let Hprev := DerivedCategory.homologyFunctor AddCommGrpCat.{u} (m - 1)
    let Hcur := DerivedCategory.homologyFunctor AddCommGrpCat.{u} m
    let Fprev := K ⋙ RGamma ⋙ Hprev
    let Fcur := K ⋙ RGamma ⋙ Hcur
    let dprev : (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) ⟶ (∏ᶜ fun n : ℕ ↦ Fprev.obj ⟨n⟩) :=
      Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) (n + 1) ≫
            Fprev.map (homOfLE (Nat.le_succ n)).op
    ∃ (i : cokernel dprev ⟶ Hcur.obj (RGamma.obj L))
      (q : Hcur.obj (RGamma.obj L) ⟶ limit Fcur) (zero : i ≫ q = 0),
      ((ShortComplex.mk i q zero).ShortExact ∧
        ∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
          Hcur.map (RGamma.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)))

AlgebraicGeometry.GrothendieckExistence.isDerivedLimit_map_derivedSectionsLocallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/GrothendieckExistence/DerivedLimitBounded.lean, line 204. The attribute's comment: “commutation with derived limits, for the Γ(X, U)-module valued derived sections over an open at the locally small model”.

[Stacks, Tag 0D60], first assertion, for RΓ(U, -) at the locally small model. If K is a derived limit of an inverse system (Kₙ) in D(𝒪_X), then RΓ(U, K) is a derived limit of the system (RΓ(U, Kₙ)) in D(Γ(X, U)); the existence of the product of the images is part of the conclusion.

This is [Stacks, Tag 08U1]: 𝒪_X-modules are Grothendieck abelian, Γ(X, U)-modules have exact countable products, and sections over U preserve countable products, so the right derived functor of sections carries a derived-limit triangle to a derived-limit triangle. The instances of Tag 0D60 already in the library are stated either for Ab-valued derived sections over an open, or for module-valued derived sections over the base ring at HasDerivedCategory.standard; this one is Γ(X, U)-module valued at the locally small model, which is the model Stacks.Duality.Coherator.AffineAmplitudeIn is set at.

theorem isDerivedLimit_map_derivedSectionsLocallySmall (U : X.Opens)
    (L : ℕᵒᵖ ⥤ DerivedCategory X.Modules) [HasProduct fun n : ℕ => L.obj ⟨n⟩]
    (K : DerivedCategory X.Modules) (hK : IsDerivedLimit L K) :
    ∃ h : HasProduct fun n : ℕ => (derivedSectionsLocallySmall X U).obj (L.obj ⟨n⟩),
      @IsDerivedLimit (DerivedCategory (ModuleCat.{u} Γ(X, U))) _ _ _ _ _ _
        (L ⋙ derivedSectionsLocallySmall X U) h ((derivedSectionsLocallySmall X U).obj K)

Stacks.Cohomology.DerivedSectionsOverBase.isDerivedLimit_map_derivedSectionsOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/DerivedSectionsOverBase.lean, line 190. The attribute's comment: “commutation with derived limits, for derived sections over a base ring”.

Derived sections over a base ring commute with derived limits. If a distinguished triangle exhibits L as the derived limit of a countable inverse system (K_n) of objects of D(𝒪_X), then RΓ(X, L) is the derived limit of the system (RΓ(X, K_n)) in D(A); the existence of the product of the images is part of the conclusion.

theorem isDerivedLimit_map_derivedSectionsOver
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hL : IsDerivedLimit K L) :
    ∃ h : HasProduct (fun n : ℕ ↦ (derivedSectionsOver X ρ).obj (K.obj ⟨n⟩)),
      @IsDerivedLimit (DerivedCategory (ModuleCat.{u} A)) _ _ _ _ _ _
        (K ⋙ derivedSectionsOver X ρ) h ((derivedSectionsOver X ρ).obj L)

Stacks.Cohomology.DerivedSectionsOverBase.exists_shortExact_homology_derivedSectionsOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/DerivedSectionsOverBase.lean, line 216. The attribute's comment: “short exact sequence, for derived sections over a base ring; both maps normalized”.

The Milnor short exact sequence for the cohomology of derived sections of a derived limit. With L the derived limit of (K_n) in D(𝒪_X), the cohomology modules Hʳ(X, L) of its derived sections over A fit into short exact sequences

0 ⟶ R¹lim Hʳ⁻¹(X, K_n) ⟶ Hʳ(X, L) ⟶ lim Hʳ(X, K_n) ⟶ 0,

where R¹lim is the cokernel of 1 - shift on the product of the cohomologies. The inclusion descends the connecting morphism of the Milnor triangle and the projection is characterized by the limit projections.

The product of the images is taken as a hypothesis here, as it is in the general Milnor sequence; isDerivedLimit_map_derivedSectionsOver provides it.

theorem exists_shortExact_homology_derivedSectionsOver
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hL : IsDerivedLimit K L) :
    let F : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) := K ⋙ derivedSectionsOver X ρ
    let Y : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ F.obj (op n)
    let d : (∏ᶜ Y) ⟶ ∏ᶜ Y := Pi.lift fun n : ℕ ↦
      Pi.π Y n - Pi.π Y (n + 1) ≫ F.map (homOfLE (Nat.le_succ n)).op
    ∃ (a : (derivedSectionsOver X ρ).obj L ⟶ ∏ᶜ Y)
      (b : (∏ᶜ Y) ⟶ ((derivedSectionsOver X ρ).obj L)⟦(1 : ℤ)⟧),
      let T := Triangle.mk a d b
      T ∈ distTriang (DerivedCategory (ModuleCat.{u} A)) ∧
        ∀ r : ℤ,
          let H := DerivedCategory.homologyFunctor (ModuleCat.{u} A) r
          let H₁ := DerivedCategory.homologyFunctor (ModuleCat.{u} A) (r - 1)
          let homologySystem : ℕᵒᵖ ⥤ ModuleCat.{u} A := F ⋙ H
          let shiftedHomologySystem : ℕᵒᵖ ⥤ ModuleCat.{u} A := F ⋙ H₁
          let P : ModuleCat.{u} A :=
            ∏ᶜ fun n : ℕ ↦ shiftedHomologySystem.obj (op n)
          let δ : P ⟶ P := Pi.lift fun n : ℕ ↦
            Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (op n)) n -
              Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (op n)) (n + 1) ≫
                shiftedHomologySystem.map (homOfLE (Nat.le_succ n)).op
          ∃ (e : H₁.obj (∏ᶜ Y) ≅ P)
            (i : cokernel δ ⟶ H.obj ((derivedSectionsOver X ρ).obj L))
            (q : H.obj ((derivedSectionsOver X ρ).obj L) ⟶ limit homologySystem)
            (w : i ≫ q = 0),
            e.hom = piComparison H₁ Y ∧
              cokernel.π δ ≫ i = e.inv ≫
                DerivedCategory.HomologySequence.δ T (r - 1) r ∧
              (∀ n : ℕ, q ≫ limit.π homologySystem (op n) =
                H.map a ≫ H.map (Pi.π Y n)) ∧
              (ShortComplex.mk i q w).ShortExact

Stacks.Cohomology.DerivedLimits.isDerivedLimit_map_derivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimits.lean, line 248. The attribute's comment: “commutation with derived limits”.

Stacks 0D60, first assertion. Derived sections over an open carry a countable derived inverse limit to a derived inverse limit.

theorem isDerivedLimit_map_derivedSections
    (X : RingedSpace.{u, u})
    (U : Opens X.carrier)
    (RGamma : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory AddCommGrpCat.{u})
    (comparison :
      (SheafOfModules.toSheaf (structureSheafRing X) ⋙
          (sheafSections (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}).obj
            (op U)).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q ⟶
        DerivedCategory.Q ⋙ RGamma)
    (hRGamma : RGamma.IsRightDerivedFunctor comparison
      (HomologicalComplex.quasiIso (SheafOfModules.{u} (structureSheafRing X))
        (ComplexShape.up ℤ)))
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hL : IsDerivedLimit K L) :
    ∃ h : HasProduct (fun n : ℕ ↦ RGamma.obj (K.obj ⟨n⟩)),
      @IsDerivedLimit
        (DerivedCategory AddCommGrpCat.{u}) _ _ _ _ _ _
        (K ⋙ RGamma) h (RGamma.obj L)

Stacks.Cohomology.DerivedLimits.exists_shortExact_limOne_cohomology_derivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimits.lean, line 332. The attribute's comment: “short exact sequence”.

Stacks 0D60, second assertion. For every open U and degree m, the cohomology of a derived inverse limit lies in the Milnor short exact sequence 0 ⟶ R¹ lim Hᵐ⁻¹(U,Kₙ) ⟶ Hᵐ(U,R lim Kₙ) ⟶ lim Hᵐ(U,Kₙ) ⟶ 0.

Here R¹ lim is represented by the cokernel of the standard difference map on the product of the underlying cohomology groups. The last map is characterized by its composites with the limit projections, which are induced by the structural maps L ⟶ Kₙ.

theorem exists_shortExact_limOne_cohomology_derivedLimit
    (X : RingedSpace.{u, u})
    (U : Opens X.carrier)
    (RGamma : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory AddCommGrpCat.{u})
    (comparison :
      (SheafOfModules.toSheaf (structureSheafRing X) ⋙
          (sheafSections (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}).obj
            (op U)).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q ⟶
        DerivedCategory.Q ⋙ RGamma)
    (hRGamma : RGamma.IsRightDerivedFunctor comparison
      (HomologicalComplex.quasiIso (SheafOfModules.{u} (structureSheafRing X))
        (ComplexShape.up ℤ)))
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
            K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))))
    (m : ℤ) :
    let A := AddCommGrpCat.{u}
    let Hprev := DerivedCategory.homologyFunctor A (m - 1)
    let Hcur := DerivedCategory.homologyFunctor A m
    let Fprev := K ⋙ RGamma ⋙ Hprev
    let Fcur := K ⋙ RGamma ⋙ Hcur
    let dprev := Pi.lift fun n : ℕ ↦
      Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ ↦ Fprev.obj ⟨n⟩) (n + 1) ≫
          Fprev.map (homOfLE (Nat.le_succ n)).op
    ∃ (i : cokernel dprev ⟶
        Hcur.obj (RGamma.obj L))
      (q : Hcur.obj (RGamma.obj L) ⟶ limit Fcur)
      (zero : i ≫ q = 0),
      ((ShortComplex.mk i q zero).ShortExact ∧
        ∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
          Hcur.map (RGamma.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)))
Tag 0BKP, a lemma

Tag 0BKP in the Stacks Project.

Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.isDerivedLimit_map_derivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/DerivedLimits.lean, line 67.

Derived pushforward along a morphism of ringed spaces commutes with derived limits: it carries an object exhibited as the derived limit of a countable inverse system to the derived limit of the pushed-forward system.

theorem isDerivedLimit_map_derivedPushforward
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hL : IsDerivedLimit K L) :
    ∃ h : HasProduct (fun n : ℕ ↦ Rf.obj (K.obj ⟨n⟩)),
      @IsDerivedLimit (DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) _ _ _ _ _ _
        (K ⋙ Rf) h (Rf.obj L)
Tag 0BKQ, a remark

Tag 0BKQ in the Stacks Project.

Stacks.Cohomology.DerivedLimits.sheafificationCohomologyPresheafSystemIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitComparisonDiagram.lean, line 168. The attribute's comment: “the cohomology sheaf H^m(K_n) of each member of the inverse system is the sheafification of the cohomology presheaf U ↦ H^m(U, K_n), naturally in n”.

Stacks 0BKQ, first assertion. For an inverse system (Kₙ) in D(O) and a degree m, the cohomology sheaf 𝓗ᵐ_n = Hᵐ(Kₙ) is the sheafification of the cohomology presheaf underline 𝓗ᵐ_n : U ↦ Hᵐ(U, Kₙ), naturally in n: sheafifying the system of cohomology presheaves of the Kₙ gives the system of their cohomology sheaves, compatibly with the transition maps of the system.

This is Tag 0BKJ applied to each Kₙ, read as an isomorphism of systems; the same statement for a derived limit L of the system -- that 𝓗ᵐ = Hᵐ(R lim Kₙ) is the sheafification of underline 𝓗ᵐ : U ↦ Hᵐ(U, R lim Kₙ) -- is Tag 0BKJ at the single object L, i.e. the component (sheafificationCohomologyPresheafIso O m).app L. Both appear in Stacks.Cohomology.DerivedLimits.cohomologyDerivedLimitDiagram, which puts them into the remark's square.

def sheafificationCohomologyPresheafSystemIso {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} O)) (m : ℤ) :
    (K ⋙ derivedSectionsPresheaf O ⋙
          DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) m) ⋙
        PresheafOfModules.sheafification (𝟙 O.obj) ≅
      K ⋙ DerivedCategory.homologyFunctor (SheafOfModules.{u} O) m

Stacks.Cohomology.DerivedLimits.cohomologyDerivedLimitDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitComparisonDiagram.lean, line 198. The attribute's comment: “the cohomology sheaves of the system and of the derived limit are the sheafifications of the cohomology presheaves U ↦ H^m(U, K_n) and U ↦ H^m(U, R lim K_n), and the comparison square of the remark's diagram commutes”.

Stacks 0BKQ, first assertion and diagram. Let O be a sheaf of rings on a space, let (Kₙ) be an inverse system in D(O) and let L be a derived limit of it, given by its structural map p and the defining distinguished triangle. Fix a degree m, and let e be the Tag 0BKJ identification of the sheafification S of the cohomology presheaf underline 𝓗ᵐ with the cohomology sheaf 𝓗ᵐ; in particular e.hom.app (K.obj ⟨n⟩) says that 𝓗ᵐ_n is the sheafification of underline 𝓗ᵐ_n, and e.hom.app L says the same for L.

Then there are comparison maps a into the limit of the cohomology presheaves, b into the limit of the cohomology sheaves and c out of the sheafification of the former, each determined by its composites with the limit projections -- a and b by the maps induced by p ≫ πₙ, and c by the sheafified projections followed by e -- and the square

S a ≫ c = e L ≫ b

commutes. The map c is not asserted to be invertible: the source warns that lim 𝓗ᵐ_n need not be the sheafification of lim underline 𝓗ᵐ_n.

theorem cohomologyDerivedLimitDiagram {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} O))
    (L : DerivedCategory (SheafOfModules.{u} O))
    [HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
    (hp : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
            K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} O)))
    (m : ℤ) :
    let P := derivedSectionsPresheaf O ⋙
      DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) m
    let H := DerivedCategory.homologyFunctor (SheafOfModules.{u} O) m
    let S := PresheafOfModules.sheafification (𝟙 O.obj)
    let e := sheafificationCohomologyPresheafIso O m
    ∃ (a : P.obj L ⟶ limit (K ⋙ P))
      (b : H.obj L ⟶ limit (K ⋙ H))
      (c : S.obj (limit (K ⋙ P)) ⟶ limit (K ⋙ H)),
      (∀ n : ℕ,
        a ≫ limit.π (K ⋙ P) ⟨n⟩ =
          P.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
      (∀ n : ℕ,
        b ≫ limit.π (K ⋙ H) ⟨n⟩ =
          H.map (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
      (∀ n : ℕ,
        c ≫ limit.π (K ⋙ H) ⟨n⟩ =
          S.map (limit.π (K ⋙ P) ⟨n⟩) ≫ e.hom.app (K.obj ⟨n⟩)) ∧
      (S.map a ≫ c = e.hom.app L ≫ b)

Stacks.Cohomology.DerivedLimits.exists_shortExact_limOne_cohomology_derivedLimit_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimits.lean, line 389. The attribute's comment: “the short exact sequences of Equation 0BKR over each open U: 0 → R¹ lim H^(m-1)(U, K_n) → H^m(U, R lim K_n) → lim H^m(U, K_n) → 0”.

Stacks 0BKQ. For a family of derived-sections functors indexed by the opens of a ringed space, the cohomology of a derived inverse limit lies in the Milnor short exact sequence over each open.

The last map is pinned down by its composites with the limit projections; they are the maps on cohomology induced by the structural maps L ⟶ Kₙ.

This is the last assertion of the remark. Its first assertion, that the cohomology sheaves of the system and of the derived limit are the sheafifications of the cohomology presheaves, and the square of its diagram, are Stacks.Cohomology.DerivedLimits.sheafificationCohomologyPresheafSystemIso and Stacks.Cohomology.DerivedLimits.cohomologyDerivedLimitDiagram.

theorem exists_shortExact_limOne_cohomology_derivedLimit_family
    (X : RingedSpace.{u, u})
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [HasProduct fun n : ℕ => K.obj ⟨n⟩]
    (p : L ⟶ ∏ᶜ fun n : ℕ => K.obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ => K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ =>
        Pi.π (fun n : ℕ => K.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ => K.obj ⟨n⟩) (n + 1) ≫
            K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))))
    (RGamma : ∀ _U : Opens X.carrier,
      DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
        DerivedCategory AddCommGrpCat.{u})
    (comparison : ∀ U : Opens X.carrier,
      ((SheafOfModules.toSheaf (structureSheafRing X) ⋙
          (sheafSections (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}).obj
            (op U)).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q) ⟶ DerivedCategory.Q ⋙ RGamma U)
    (hRGamma : ∀ U : Opens X.carrier,
      (RGamma U).IsRightDerivedFunctor (comparison U)
        (HomologicalComplex.quasiIso
          (SheafOfModules.{u} (structureSheafRing X))
          (ComplexShape.up ℤ)))
    (U : Opens X.carrier) (m : ℤ) :
    let Fprev := K ⋙ RGamma U ⋙
      DerivedCategory.homologyFunctor AddCommGrpCat.{u} (m - 1)
    let Fcur := K ⋙ RGamma U ⋙
      DerivedCategory.homologyFunctor AddCommGrpCat.{u} m
    let dprev := Pi.lift fun n : ℕ =>
      Pi.π (fun n : ℕ => Fprev.obj ⟨n⟩) n -
        Pi.π (fun n : ℕ => Fprev.obj ⟨n⟩) (n + 1) ≫
          Fprev.map (homOfLE (Nat.le_succ n)).op
    ∃ (i : cokernel dprev ⟶
        (DerivedCategory.homologyFunctor AddCommGrpCat.{u} m).obj ((RGamma U).obj L))
      (q : (DerivedCategory.homologyFunctor AddCommGrpCat.{u} m).obj ((RGamma U).obj L) ⟶
        limit Fcur)
      (zero : i ≫ q = 0),
      ((ShortComplex.mk i q zero).ShortExact ∧
        ∀ n : ℕ, q ≫ limit.π Fcur ⟨n⟩ =
          (DerivedCategory.homologyFunctor AddCommGrpCat.{u} m).map
            ((RGamma U).map (p ≫ Pi.π (fun n : ℕ => K.obj ⟨n⟩) n)))
Tag 0BKS, a lemma

Tag 0BKS in the Stacks Project.

Stacks.Cohomology.SpaceInverseLimits.isDerivedLimit_single_limit_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryB/InverseLimitAsDerivedLimit.lean, line 354. The attribute's comment: “derived limit”.

If the terms of a countable inverse system of modules are acyclic on a basis and R¹ lim of their sections vanishes there, then the ordinary limit, placed in degree zero, is a derived inverse limit of the system.

public theorem isDerivedLimit_single_limit_of_isBasis (X : RingedSpace.{u, u})
    (F : Functor ℕᵒᵖ (SheafOfModules.{u} (structureSheafRing X)))
    (B : Set (Opens X.carrier)) (hB : Opens.IsBasis B)
    (hcoh : ∀ U ∈ B, ∀ n p : ℕ, 0 < p →
      IsZero (Hgroup (structureSheafRing X) U p (F.obj ⟨n⟩)))
    (hlimOne : ∀ U ∈ B, Epi (inverseLimitDifference (sectionsSystem X F U))) :
    ∃ h : HasProduct (fun n : ℕ =>
        (F ⋙ DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).obj ⟨n⟩),
      @IsDerivedLimit (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) _ _ _ _ _ _
        (F ⋙ DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0) h
        ((DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).obj
          (limit F))

Stacks.Cohomology.SpaceInverseLimits.isZero_cohomology_limit_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryB/InverseLimitAsDerivedLimit.lean, line 419. The attribute's comment: “higher cohomology”.

Under the same hypotheses, the ordinary inverse limit has vanishing positive-degree cohomology on every member of the basis.

public theorem isZero_cohomology_limit_of_isBasis (X : RingedSpace.{u, u})
    (F : Functor ℕᵒᵖ (SheafOfModules.{u} (structureSheafRing X)))
    (B : Set (Opens X.carrier)) (hB : Opens.IsBasis B)
    (hcoh : ∀ U ∈ B, ∀ n p : ℕ, 0 < p →
      IsZero (Hgroup (structureSheafRing X) U p (F.obj ⟨n⟩)))
    (hlimOne : ∀ U ∈ B, Epi (inverseLimitDifference (sectionsSystem X F U)))
    (U : Opens X.carrier) (hU : U ∈ B) (p : ℕ) (hp : 0 < p) :
    IsZero (Hgroup (structureSheafRing X) U p (limit F))
Tag 0D61, a lemma

Tag 0D61 in the Stacks Project.

Stacks.Cohomology.DerivedLimitStalk.cohomology_derivedLimit_projection_mono_on_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitStalkInjectivity.lean, line 233.

Stacks Project, Tag 0D61. A locally vanishing R¹ lim in degree m - 1 and eventual injectivity on cohomology in degree m, over a fundamental system of open neighbourhoods of x, force the projection from a derived limit to the stage n₀ to be injective on the stalk at x of the degree-m cohomology sheaf.

Both numbered conditions of the source appear as binders, in the source's own position — universally quantified over the members U of the fundamental system 𝔘: hlimOne is R¹ lim Hᵐ⁻¹(U, Kₙ) = 0, as the vanishing of the cokernel of the 1 - shift endomorphism of the product, and hinj is the injectivity of Hᵐ(U, Kₙ) ⟶ Hᵐ(U, K_{n₀}) for n ≥ n₀. The source's n(x) is n₀ and its 𝔘ₓ is 𝔘, given here as arguments rather than existentially; the derived limit R lim Kₙ is L together with p and hL, which say that p is the structural map of the defining distinguished triangle, so p ≫ Pi.π n₀ is the source's R lim Kₙ ⟶ K_{n₀} and not an arbitrary map.

public theorem cohomology_derivedLimit_projection_mono_on_stalk {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} O))
    (L : DerivedCategory (SheafOfModules.{u} O))
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
            K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} O)))
    (x : X) (m : ℤ) (n₀ : ℕ) (𝔘 : Set (Opens X))
    (hbasis : (nhds x).HasBasis (fun U : Opens X ↦ U ∈ 𝔘) (fun U ↦ (U : Set X)))
    (hlimOne : ∀ U ∈ 𝔘,
      let F := K ⋙ derivedSectionsPresheaf O ⋙
        DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) (m - 1) ⋙
        PresheafOfModules.evaluation O.obj (Opposite.op U)
      IsZero (cokernel (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ F.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ F.obj ⟨n⟩) (n + 1) ≫
            F.map (homOfLE (Nat.le_succ n)).op)))
    (hinj : ∀ U ∈ 𝔘,
      let F := K ⋙ derivedSectionsPresheaf O ⋙
        DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) m ⋙
        PresheafOfModules.evaluation O.obj (Opposite.op U)
      ∀ (n : ℕ) (hn : n₀ ≤ n), Mono (F.map (homOfLE hn).op)) :
    Mono ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
      ((SheafOfModules.forget O ⋙ PresheafOfModules.toPresheaf O.obj).map
        ((DerivedCategory.homologyFunctor (SheafOfModules.{u} O) m).map
          (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n₀))))
Tag 0D62, a lemma

Tag 0D62 in the Stacks Project.

Stacks.Cohomology.DerivedLimitStalk.exists_and_forall_isIso_to_derivedLimit_truncGETower_of_local_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitStalkInjectivity.lean, line 685. The attribute's comment: “the derived limit and the canonical map of Remark 0H72 exist, and every such canonical map is an isomorphism”.

Stacks Project, Tag 0D62. Let E be an object of the derived category of sheaves of 𝒪_X-modules on a ringed space, and suppose every point x carries a function p(x, -) and a fundamental system 𝔘ₓ of open neighbourhoods on whose members Hᵖ(U, H^{m-p}(E)) vanishes whenever p > p(x, m). Then the tower of truncations τ_{≥ -n} E from below has a derived limit R lim τ_{≥ -n} E with a canonical map of Remark 0H72 from E, and every such canonical map to every derived limit of the tower is an isomorphism.

public theorem exists_and_forall_isIso_to_derivedLimit_truncGETower_of_local_vanishing
    {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (E : DerivedCategory (SheafOfModules.{u} O))
    (hvanishing : ∀ x : X, ∃ (pb : ℤ → ℤ) (𝔘 : Set (Opens X)),
      (nhds x).HasBasis (fun U : Opens X ↦ U ∈ 𝔘) (fun U ↦ (U : Set X)) ∧
        ∀ U ∈ 𝔘, ∀ (p : ℕ) (m : ℤ), pb m < (p : ℤ) →
          IsZero ((PresheafOfModules.evaluation O.obj (Opposite.op U)).obj
            (cohomologyPresheaf O
              ((DerivedCategory.singleFunctor (SheafOfModules.{u} O) 0).obj
                ((DerivedCategory.homologyFunctor (SheafOfModules.{u} O)
                  (m - (p : ℤ))).obj E)) (p : ℤ)))) :
    (∃ (_ : HasProduct fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩)
      (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) ∧
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E)) ∧
    ∀ (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) →
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) →
      IsIso c
Tag 0D63, a lemma

Tag 0D63 in the Stacks Project.

Stacks.Cohomology.DerivedLimitStalk.isIso_to_isDerivedLimit_truncGETower_of_local_bound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitLocalBound.lean, line 76.

Let E be an object of the derived category of sheaves of 𝒪_X-modules on a ringed space, and suppose every point x carries an integer dₓ ≥ 0 and a fundamental system 𝔘ₓ of open neighbourhoods on whose members Hᵖ(U, Hᵠ(E)) vanishes whenever p > dₓ and q < 0. Then the canonical map from E to a derived limit of its tower of truncations τ_{≥ -n} E from below is an isomorphism.

public theorem isIso_to_isDerivedLimit_truncGETower_of_local_bound {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (E : DerivedCategory (SheafOfModules.{u} O))
    (hvanishing : ∀ x : X, ∃ (d : ℕ) (𝔘 : Set (Opens X)),
      (nhds x).HasBasis (fun U : Opens X ↦ U ∈ 𝔘) (fun U ↦ (U : Set X)) ∧
        ∀ U ∈ 𝔘, ∀ (p : ℕ) (q : ℤ), (d : ℤ) < (p : ℤ) → q < 0 →
          IsZero ((PresheafOfModules.evaluation O.obj (Opposite.op U)).obj
            (cohomologyPresheaf O
              ((DerivedCategory.singleFunctor (SheafOfModules.{u} O) 0).obj
                ((DerivedCategory.homologyFunctor (SheafOfModules.{u} O) q).obj E))
              (p : ℤ))))
    (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
    (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
      (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk pr (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
              (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} O)))
    (hc : ∀ n : ℕ, c ≫ pr ≫ Pi.π
      (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
      (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) :
    IsIso c
Tag 08U2, a lemma

Tag 08U2 in the Stacks Project.

Stacks.Cohomology.DerivedLimitStalk.exists_isIso_to_derivedLimit_truncGETower_of_vanishing_on_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitStalkInjectivity.lean, line 642. The attribute's comment: “the conclusion with the derived limit and the canonical map of Remark 0H72 constructed rather than quantified over”.

Stacks Project, Tag 08U2, in the form the source states it: the canonical map E ⟶ R lim τ_{≥ -n} E is an isomorphism. The derived limit and the canonical map are constructed by exists_presented_derivedLimit_truncGETower.

theorem exists_isIso_to_derivedLimit_truncGETower_of_vanishing_on_cover {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (E : DerivedCategory (SheafOfModules.{u} O))
    (pb : ℤ → ℤ) (𝔅 : Set (Opens X))
    (hcov : ∀ V : Opens X, ∃ 𝒰 : Set (Opens X), 𝒰 ⊆ 𝔅 ∧ (V : Set X) = ⋃ U ∈ 𝒰, (U : Set X))
    (hvanishing : ∀ U ∈ 𝔅, ∀ (p : ℕ) (m : ℤ), pb m < (p : ℤ) →
      IsZero ((PresheafOfModules.evaluation O.obj (Opposite.op U)).obj
        (cohomologyPresheaf O
          ((DerivedCategory.singleFunctor (SheafOfModules.{u} O) 0).obj
            ((DerivedCategory.homologyFunctor (SheafOfModules.{u} O)
              (m - (p : ℤ))).obj E)) (p : ℤ)))) :
    ∃ (_ : HasProduct fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩)
      (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) ∧
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) ∧ IsIso c

Stacks.Cohomology.DerivedLimitStalk.exists_and_forall_isIso_to_derivedLimit_truncGETower_of_vanishing_on_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitStalkInjectivity.lean, line 745. The attribute's comment: “the derived limit and the canonical map of Remark 0H72 exist, and every such canonical map is an isomorphism”.

Stacks Project, Tag 08U2. Let E be an object of the derived category of sheaves of 𝒪_X-modules on a ringed space, let p(-) be a function and let 𝔅 be a set of opens of X such that every open of X is a union of members of 𝔅 and Hᵖ(U, H^{m-p}(E)) vanishes for U ∈ 𝔅 and p > p(m). Then the tower of truncations τ_{≥ -n} E from below has a derived limit R lim τ_{≥ -n} E with a canonical map of Remark 0H72 from E, and every such canonical map to every derived limit of the tower is an isomorphism.

public theorem exists_and_forall_isIso_to_derivedLimit_truncGETower_of_vanishing_on_cover
    {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (E : DerivedCategory (SheafOfModules.{u} O))
    (pb : ℤ → ℤ) (𝔅 : Set (Opens X))
    (hcov : ∀ V : Opens X, ∃ 𝒰 : Set (Opens X), 𝒰 ⊆ 𝔅 ∧ (V : Set X) = ⋃ U ∈ 𝒰, (U : Set X))
    (hvanishing : ∀ U ∈ 𝔅, ∀ (p : ℕ) (m : ℤ), pb m < (p : ℤ) →
      IsZero ((PresheafOfModules.evaluation O.obj (Opposite.op U)).obj
        (cohomologyPresheaf O
          ((DerivedCategory.singleFunctor (SheafOfModules.{u} O) 0).obj
            ((DerivedCategory.homologyFunctor (SheafOfModules.{u} O)
              (m - (p : ℤ))).obj E)) (p : ℤ)))) :
    (∃ (_ : HasProduct fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩)
      (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) ∧
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E)) ∧
    ∀ (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) →
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) →
      IsIso c
Tag 0D64, a lemma

Tag 0D64 in the Stacks Project.

Stacks.Cohomology.DerivedLimitStalk.exists_and_forall_isIso_to_derivedLimit_truncGETower_of_dimension_bound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/DerivedLimitDimensionBound.lean, line 99. The attribute's comment: “the derived limit and the canonical map of Remark 0H72 exist, and every such canonical map is an isomorphism”.

Stacks Project, Tag 0D64. Let E be an object of the derived category of sheaves of 𝒪_X-modules on a ringed space, and suppose there are an integer d ≥ 0 and a basis 𝔅 for the topology of X on whose members Hᵖ(U, Hᵠ(E)) vanishes whenever p > d and q < 0. Then the tower of truncations τ_{≥ -n} E from below has a derived limit R lim τ_{≥ -n} E with a canonical map of Remark 0H72 from E, and every such canonical map to every derived limit of the tower is an isomorphism.

public theorem exists_and_forall_isIso_to_derivedLimit_truncGETower_of_dimension_bound
    {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (E : DerivedCategory (SheafOfModules.{u} O))
    (d : ℕ) (𝔅 : Set (Opens X)) (h𝔅 : Opens.IsBasis 𝔅)
    (hvanishing : ∀ U ∈ 𝔅, ∀ (p : ℕ) (q : ℤ), (d : ℤ) < (p : ℤ) → q < 0 →
      IsZero ((PresheafOfModules.evaluation O.obj (Opposite.op U)).obj
        (cohomologyPresheaf O
          ((DerivedCategory.singleFunctor (SheafOfModules.{u} O) 0).obj
            ((DerivedCategory.homologyFunctor (SheafOfModules.{u} O) q).obj E))
          (p : ℤ)))) :
    (∃ (_ : HasProduct fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩)
      (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) ∧
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E)) ∧
    ∀ (L : DerivedCategory (SheafOfModules.{u} O)) (c : E ⟶ L)
      (pr : L ⟶ ∏ᶜ fun n : ℕ ↦
        (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩),
      (∃ δ : (∏ᶜ fun n : ℕ ↦
          (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
        Triangle.mk pr (Pi.lift fun n : ℕ ↦
          Pi.π (fun n : ℕ ↦
            (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n -
            Pi.π (fun n : ℕ ↦
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) (n + 1) ≫
              (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).map
                (homOfLE (Nat.le_succ n)).op) δ ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))) →
      (∀ n : ℕ, c ≫ pr ≫ Pi.π
        (fun n : ℕ ↦ (Stacks.DerivedLimit.truncGETower (SheafOfModules.{u} O) E).obj ⟨n⟩) n =
        (DerivedCategory.TStructure.t.truncGEπ (-(n : ℤ))).app E) →
      IsIso c
Tag 0BKT, a lemma

Tag 0BKT in the Stacks Project.

Stacks.Algebraization.homologyIso_derivedSections_of_isAffineOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/AffineEdgeQuasicoherent.lean, line 77. The attribute's comment: “over an affine open of a scheme, for an object of D(𝒪_X) whose cohomology sheaves are all quasi-coherent: the acyclicity hypothesis of the tag is Serre vanishing on the affine opens, which quasi-coherence supplies, and the affine opens are a basis of the topology”. References: EGA III (1.3.1), “more general”; EGA III (4.1.7.21), “H^i(U”.

[Stacks, Tag 0BKT] over an affine open of a scheme. For an object L of D(𝒪_X) with quasi-coherent cohomology sheaves and an affine open U, the hypercohomology H^p(U, L) is the module of sections over U of the cohomology sheaf H^p(L).

The cohomology sheaves are acyclic over the affine opens by Serre vanishing (Stacks.Algebraization.isZero_rightDerived_evaluation_homology_of_isQuasicoherent), and the affine opens are a basis, so Stacks.Cohomology.AcyclicOpen.hypercohomologyIso applies.

public def homologyIso_derivedSections_of_isAffineOpen (X : Scheme.{u})
    (L : DerivedCategory X.Modules)
    (hqc : ∀ q : ℤ, ((DerivedCategory.homologyFunctor X.Modules q).obj L).IsQuasicoherent)
    (U : X.affineOpens) (p : ℤ) :
    (DerivedCategory.homologyFunctor (ModuleCat.{u} Γ(X, U.1)) p).obj
        ((derivedSections (structureSheafRing X.toRingedSpace) U.1).obj L) ≅
      ModuleCat.of Γ(X, U.1) Γ((DerivedCategory.homologyFunctor X.Modules p).obj L, U.1)

Stacks.Cohomology.AcyclicOpen.isIso_hypercohomologyEdge_app_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/HypercohomologyOverAcyclicOpens.lean, line 83.

Stacks Project Tag 0BKT. If every cohomology sheaf of K has vanishing higher cohomology over the members of a basis of opens, then over each member of that basis the hypercohomology edge morphism H^q(U, K) ⟶ Γ(U, H^q(K)) is invertible, in every degree.

theorem isIso_hypercohomologyEdge_app_of_isBasis
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (B : Set (Opens X.carrier)) (hB : Opens.IsBasis B)
    (hK : ∀ V ∈ B, ∀ p : ℕ, 0 < p → ∀ q : ℤ,
      IsZero (((SheafOfModules.evaluation (structureSheafRing X) (op V)).rightDerived p).obj
        ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) q).obj K)))
    (U : Opens X.carrier) (hU : U ∈ B) (q : ℤ) :
    IsIso ((hypercohomologyEdge (structureSheafRing X) U q).app K)
Tag 0BKU, a lemma

Tag 0BKU in the Stacks Project.

Stacks.Cohomology.DerivedLimits.cohomology_isLimit_of_isDerivedLimit_of_isBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/CohomologyOfADerivedLimit.lean, line 75.

Stacks Project, Tag 0BKU. Let (K_n) be an inverse system of objects of D(𝒪_X) and let L be a derived limit of it, exhibited by the structural map p and its distinguished triangle. If on a basis B of the topology the cohomology sheaves of the K_n are acyclic and the inverse systems of their sections have vanishing R¹ lim, then for every q the degree-q cohomology sheaf of L is the inverse limit of the degree-q cohomology sheaves of the K_n, through the maps induced by p.

theorem cohomology_isLimit_of_isDerivedLimit_of_isBasis
    (K : ℕᵒᵖ ⥤ DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    [hprod : HasProduct fun n : ℕ ↦ K.obj ⟨n⟩]
    (p : L ⟶ ∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩)
    (hL : ∃ δ : (∏ᶜ fun n : ℕ ↦ K.obj ⟨n⟩) ⟶ L⟦(1 : ℤ)⟧,
      Triangle.mk p (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) (n + 1) ≫
            K.map (homOfLE (Nat.le_succ n)).op) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))))
    (B : Set (Opens X.carrier)) (hB : Opens.IsBasis B)
    (hacyclic : ∀ U ∈ B, ∀ q : ℤ, ∀ n : ℕ, ∀ r : ℕ, 0 < r →
      IsZero (((SheafOfModules.evaluation (structureSheafRing X) (op U)).rightDerived r).obj
        ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) q).obj
          (K.obj ⟨n⟩))))
    (hlimOne : ∀ U ∈ B, ∀ q : ℤ,
      IsZero (Rlim.firstDerivedLimit
        (K ⋙ DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) q ⋙
          SheafOfModules.evaluation (structureSheafRing X) (op U) ⋙
            forget₂ (ModuleCat.{u} ((structureSheafRing X).obj.obj (op U))) AddCommGrpCat.{u})))
    (q : ℤ) :
    ∃ τ : (Functor.const ℕᵒᵖ).obj
        ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) q).obj L) ⟶
        K ⋙ DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) q,
      (∀ n : ℕ, τ.app ⟨n⟩ =
        (DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) q).map
          (p ≫ Pi.π (fun n : ℕ ↦ K.obj ⟨n⟩) n)) ∧
      Nonempty (IsLimit (Cone.mk _ τ))
Sources
LeanStacks.Cohomology.DerivedLimitSections.isDerivedLimit_map_derivedSections · Stacks.Cohomology.DerivedLimitSections.exists_shortExact_limOne_cohomology_derivedLimit · AlgebraicGeometry.GrothendieckExistence.isDerivedLimit_map_derivedSectionsLocallySmall · Stacks.Cohomology.DerivedSectionsOverBase.isDerivedLimit_map_derivedSectionsOver · Stacks.Cohomology.DerivedSectionsOverBase.exists_shortExact_homology_derivedSectionsOver · Stacks.Cohomology.DerivedLimits.isDerivedLimit_map_derivedSections · Stacks.Cohomology.DerivedLimits.exists_shortExact_limOne_cohomology_derivedLimit · Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.isDerivedLimit_map_derivedPushforward

Section20.38 Producing K-injective resolutions#

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

Tag 071A, an equation

Tag 071A in the Stacks Project.

Stacks.KInjective.nonempty_candidateKInjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/CandidateKInjectiveResolution.lean, line 97.

Every complex of sheaves of modules on a topological space admits a candidate K-injective resolution.

theorem nonempty_candidateKInjectiveResolution
    {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    (F : CochainComplex (SheafOfModules.{u} O) ℤ) :
    Nonempty (CandidateKInjectiveResolution O F)
Tag 071B, a lemma

Tag 071B in the Stacks Project.

Stacks.KInjective.quasiIso_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/CandidateKInjectiveQuasiIso.lean, line 97.

Stacks 071B. Let F be a complex of 𝒪_X-modules on a ringed space, with candidate K-injective resolution F ⟶ lim_n I_n as in Tag 071A, and write ℋ^q = H^q(F) for its cohomology sheaves. If a set B of opens of X covers every open of X and H^p(U, ℋ^q) = 0 for every U ∈ B, every p > d and every q < 0, then that canonical map is a quasi-isomorphism.

theorem quasiIso_canonicalMap (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    (F : CochainComplex (SheafOfModules.{u} O) ℤ)
    (R : CandidateKInjectiveResolution O F) (B : Set (Opens X)) (d : ℕ)
    (hB : ∀ V : Opens X, ∃ 𝒰 : Set (Opens X), 𝒰 ⊆ B ∧ (V : Set X) = ⋃ U ∈ 𝒰, (U : Set X))
    (hvan : ∀ U ∈ B, ∀ p : ℕ, d < p → ∀ q : ℤ, q < 0 →
      IsZero (((SheafOfModules.evaluation.{u} O (Opposite.op U)).rightDerived p).obj
        (F.homology q))) :
    QuasiIso R.canonicalMap
Tag 08BY, a lemma

Tag 08BY in the Stacks Project.

Stacks.Cohomology.SpaceInverseSystems.homology_isLimit_of_local_rlim_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/InverseSystemsOnASpace.lean, line 95. The attribute's comment: “canonical cohomology-limit comparison”.

Stacks 08BY. Cohomology of the termwise inverse limit is the inverse limit of the cohomology sheaves under local first-derived-limit vanishing and eventual stability.

theorem homology_isLimit_of_local_rlim_vanishing
    (X : RingedSpace.{u, u})
    (F : ℕᵒᵖ ⥤ CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ)
    (m : ℤ) (B : Set (Opens X.carrier)) (hB : Opens.IsBasis B) (n₀ : ℕ)
    (hneg2 : ∀ U ∈ B, IsZero (Rlim.firstDerivedLimit
      (F ⋙ InverseLimits.sectionsComplexFunctor (structureSheafRing X) U ⋙
        HomologicalComplex.eval Ab.{u} (ComplexShape.up ℤ) (m - 2))))
    (hneg1 : ∀ U ∈ B, IsZero (Rlim.firstDerivedLimit
      (F ⋙ InverseLimits.sectionsComplexFunctor (structureSheafRing X) U ⋙
        HomologicalComplex.eval Ab.{u} (ComplexShape.up ℤ) (m - 1))))
    (hHneg1 : ∀ U ∈ B, IsZero (Rlim.firstDerivedLimit
      (F ⋙ InverseLimits.sectionsComplexFunctor (structureSheafRing X) U ⋙
        HomologicalComplex.homologyFunctor Ab.{u} (ComplexShape.up ℤ) (m - 1))))
    (hstable : ∀ U ∈ B, ∀ (n : ℕ) (hn : n₀ ≤ n), IsIso
      ((HomologicalComplex.homologyFunctor Ab.{u} (ComplexShape.up ℤ) m).map
        ((InverseLimits.sectionsComplexFunctor (structureSheafRing X) U).map
          (F.map (homOfLE hn).op)))) :
    Nonempty (IsLimit
      ((HomologicalComplex.homologyFunctor
        (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ) m).mapCone
          (limit.cone F)))

Stacks.Cohomology.SpaceInverseSystems.homology_limit_projection_isIso_of_local_rlim_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/InverseSystemsOnASpace.lean, line 123. The attribute's comment: “projection to the stable stage”.

Stacks 08BY. The projection from the limit of degree-m cohomology sheaves to the stable stage is an isomorphism when the transition maps are locally isomorphisms on a basis.

theorem homology_limit_projection_isIso_of_local_rlim_vanishing
    (X : RingedSpace.{u, u})
    (F : ℕᵒᵖ ⥤ CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ)
    (m : ℤ) (B : Set (Opens X.carrier)) (hB : Opens.IsBasis B) (n₀ : ℕ)
    (hstable : ∀ U ∈ B, ∀ (n : ℕ) (hn : n₀ ≤ n), IsIso
      ((HomologicalComplex.homologyFunctor Ab.{u} (ComplexShape.up ℤ) m).map
        ((InverseLimits.sectionsComplexFunctor (structureSheafRing X) U).map
          (F.map (homOfLE hn).op)))) :
    IsIso (limit.π (F ⋙ HomologicalComplex.homologyFunctor
      (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ) m) (op n₀))
Sources
LeanStacks.KInjective.nonempty_candidateKInjectiveResolution · Stacks.KInjective.quasiIso_canonicalMap · Stacks.Cohomology.SpaceInverseSystems.homology_isLimit_of_local_rlim_vanishing · Stacks.Cohomology.SpaceInverseSystems.homology_limit_projection_isIso_of_local_rlim_vanishing

Section20.39 Inverse systems and cohomology, III#

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

Tag 0H3C, a lemma

Tag 0H3C in the Stacks Project.

Stacks.Cohomology.PrincipalFormalFunctions.formalFunctionsDiagram_principalKoszulTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalFunctionsDiagram.lean, line 749. The attribute's comment: “the whole diagram, with its maps the ones induced by E ⟶ E_n, the boundaries of E ⟶ E ⟶ E_n ⟶ E[1], the projections E^ ⟶ E_n and the triangle of E^, the sequences of Stacks 0BKG and 0H32 read through RΓ(X, E^) ≅ RΓ(X, E)^∧ (compatible with the maps to RΓ(X, E_n)); exactness of rows and columns and the three commutativities”.

Formal functions for a principal ideal on a ringed space: [Stacks, Tag 0H3C]. Let (X, 𝒪_X) be a ringed space, let ρ : A ⟶ Γ(X, 𝒪_X) be a homomorphism from a commutative ring A, let f ∈ A and let E ∈ D(𝒪_X). Let E_n = E ⊗_{𝒪_X} (𝒪_X --f^(n+1)--> 𝒪_X) be the f-power Koszul tower, the cone of multiplication by f^(n+1) on E, so that there are distinguished triangles E ⟶ E ⟶ E_n ⟶ E[1], and let E^ = R lim E_n, given with its distinguished triangle E^ ⟶ ∏ E_n ⟶ ∏ E_n ⟶ E^[1] whose middle map is 1 - shift. Write Hᵖ(X, -) for the cohomology of RΓ(X, -) : D(𝒪_X) ⥤ D(A), let (-)^∧ be derived f-adic completion (a left adjoint completion to the inclusion of the derived-complete objects), and let p ∈ ℤ. Then RΓ(X, E^) ≅ RΓ(X, E)^∧ by an isomorphism Φ which, composed with the unit RΓ(X, E) ⟶ RΓ(X, E)^∧ and the projections RΓ(X, E^) ⟶ RΓ(X, E_n), gives the maps RΓ(X, E) ⟶ RΓ(X, E_n) induced by E ⟶ E_n, and there is the commutative diagram with exact rows and columns

  • the top row 0 ⟶ Hᵖ(X, E)^ ⟶ lim Hᵖ(X, E_n) ⟶ T_f(Hᵖ⁺¹(X, E)) ⟶ 0, where Hᵖ(X, E)^ is the f-adic completion lim Hᵖ(X, E)/fⁿ⁺¹ and T_f the f-adic Tate module lim (-)[fⁿ⁺¹]; its first map is the limit of the maps Hᵖ(X, E)/fⁿ⁺¹ ⟶ Hᵖ(X, E_n) induced by E ⟶ E_n, its second the limit of the boundaries Hᵖ(X, E_n) ⟶ Hᵖ⁺¹(X, E)[fⁿ⁺¹] of E ⟶ E ⟶ E_n ⟶ E[1];
  • the middle row 0 ⟶ H⁰(Hᵖ(X, E)^∧) ⟶ Hᵖ(X, E^) ⟶ T_f(Hᵖ⁺¹(X, E)) ⟶ 0, the sequence of [Stacks, Tag 0H32] for K = RΓ(X, E) read through Hᵖ(Φ);
  • the left column 0 ⟶ R¹lim Hᵖ(X, E)[fⁿ] ⟶ H⁰(Hᵖ(X, E)^∧) ⟶ Hᵖ(X, E)^ ⟶ 0 of [Stacks, Tag 0BKG];
  • the middle column 0 ⟶ R¹lim Hᵖ⁻¹(X, E_n) ⟶ Hᵖ(X, E^) ⟶ lim Hᵖ(X, E_n) ⟶ 0, whose second map is induced by the projections E^ ⟶ E_n and whose first descends the boundary of the image under RΓ(X, -) of the triangle of E^, read through the isomorphism Hᵖ⁻¹(X, ∏ E_n) ≅ ∏ Hᵖ⁻¹(X, E_n);
  • the bottom isomorphism R¹lim Hᵖ(X, E)[fⁿ] ≅ R¹lim Hᵖ⁻¹(X, E_n), inverse to R¹lim of the boundaries Hᵖ⁻¹(X, E_n) ⟶ Hᵖ(X, E)[fⁿ⁺¹];

the right-hand column being the identity of T_f(Hᵖ⁺¹(X, E)).

theorem formalFunctionsDiagram_principalKoszulTower
    (E Ehat : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (a : Ehat ⟶ ∏ᶜ fun n : ℕ ↦ (principalKoszulTower X ρ f E).obj ⟨n⟩)
    (b : (∏ᶜ fun n : ℕ ↦ (principalKoszulTower X ρ f E).obj ⟨n⟩) ⟶ Ehat⟦(1 : ℤ)⟧)
    (hT : Triangle.mk a (Pi.lift fun n : ℕ ↦
        Pi.π (fun n : ℕ ↦ (principalKoszulTower X ρ f E).obj ⟨n⟩) n -
          Pi.π (fun n : ℕ ↦ (principalKoszulTower X ρ f E).obj ⟨n⟩) (n + 1) ≫
            (principalKoszulTower X ρ f E).map (homOfLE (Nat.le_succ n)).op) b ∈
      distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))))
    (p : ℤ) :
    let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
      fun L ↦ IsDerivedComplete (Ideal.span {f}) L
    ∀ (completion : DerivedCategory (ModuleCat.{u} A) ⥤ P.FullSubcategory)
      (adj : completion ⊣ P.ι),
      let completed := completion ⋙ P.ι
      let HH (q : ℤ) := DerivedCategory.homologyFunctor (ModuleCat.{u} A) q
      let RΓ := derivedSectionsOver X ρ
      let K := RΓ.obj E
      let H (q : ℤ) := (HH q).obj K
      let CE := DerivedCategory.Q.objPreimage E
      let eE := DerivedCategory.Q.objObjPreimageIso E
      let koszulTriangle (n : ℕ) := RΓ.mapTriangle.obj (DerivedCategory.Q.mapTriangle.obj
        (CochainComplex.mappingCone.triangle (smulComplex X (baseSmul X ρ f) CE ^ (n + 1)).asHom))
      let Y := fun n : ℕ ↦ (principalKoszulTower X ρ f E).obj ⟨n⟩
      let limitTriangle := RΓ.mapTriangle.obj (Triangle.mk a (Pi.lift fun n : ℕ ↦
        Pi.π Y n - Pi.π Y (n + 1) ≫
          (principalKoszulTower X ρ f E).map (homOfLE (Nat.le_succ n)).op) b)
      let cohTower (q : ℤ) := (principalKoszulTower X ρ f E ⋙ RΓ) ⋙ HH q
      let ordinaryCompletion := limit (CompletionSequences.powerQuotientSystem A (H p) f)
      let limitCoh := limit (cohTower p)
      let tate := CompletionSequences.adicTateModule A (H (p + 1)) f
      let H0CompletedHp := (HH 0).obj
        (completed.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (H p)))
      let HpEhat := (HH p).obj (RΓ.obj Ehat)
      let R1Torsion := CompletionSequences.firstDerivedLimit A
        (PrincipalTorsionTower.powerTorsionSystem A (H p) f)
      let R1PreviousCoh := CompletionSequences.firstDerivedLimit A (cohTower (p - 1))
      let productComparison : (HH (p - 1)).obj (RΓ.obj (∏ᶜ Y)) ⟶
          CompletionSequences.moduleProduct A (cohTower (p - 1)) :=
        Pi.lift fun n : ℕ ↦ (HH (p - 1)).map (RΓ.map (Pi.π Y n))
      ∃ (S : CompletionSequences.PrincipalCompletionSequences A f completed adj.unit)
        (Φ : RΓ.obj Ehat ≅ completed.obj K),
        let middleIn : H0CompletedHp ⟶ HpEhat :=
          (S.truncation K p).inclusion S.shift ≫ (HH p).map Φ.inv
        let middleOut : HpEhat ⟶ tate := (HH p).map Φ.hom ≫
          (S.truncation K p).projection f S.shift (S.moduleSequence (H (p + 1))).tateIso
        let leftIn : R1Torsion ⟶ H0CompletedHp := (S.moduleSequence (H p)).inclusion
        let leftOut : H0CompletedHp ⟶ ordinaryCompletion := (S.moduleSequence (H p)).projection
        ∃ (termIn : CompletionSequences.powerQuotientSystem A (H p) f ⟶ cohTower p)
          (termOut : cohTower p ⟶ PrincipalTorsionTower.powerTorsionSystem A (H (p + 1)) f)
          (previousOut : cohTower (p - 1) ⟶
            PrincipalTorsionTower.powerTorsionSystem A (H p) f)
          (topIn : ordinaryCompletion ⟶ limitCoh)
          (topOut : limitCoh ⟶ tate)
          (htop : topIn ≫ topOut = 0)
          (hmiddle : middleIn ≫ middleOut = 0)
          (hleft : leftIn ≫ leftOut = 0)
          (columnIn : R1PreviousCoh ⟶ HpEhat)
          (columnOut : HpEhat ⟶ limitCoh)
          (hcolumn : columnIn ≫ columnOut = 0)
          (bottom : R1Torsion ≅ R1PreviousCoh),
          (∀ n : ℕ, adj.unit.app K ≫ Φ.inv ≫ RΓ.map a ≫ RΓ.map (Pi.π Y n) =
            RΓ.map (eE.inv ≫ DerivedCategory.Q.map
              (CochainComplex.mappingCone.inr
                (smulComplex X (baseSmul X ρ f) CE ^ (n + 1)).asHom))) ∧
          (∀ n : ℕ,
            cokernel.π (PrincipalTorsionTower.powerMultiplication A (H p) (f ^ (n + 1))) ≫
                termIn.app ⟨n⟩ =
              (HH p).map (RΓ.map (eE.inv ≫ DerivedCategory.Q.map
                (CochainComplex.mappingCone.inr
                  (smulComplex X (baseSmul X ρ f) CE ^ (n + 1)).asHom)))) ∧
          (∀ n : ℕ,
            termOut.app ⟨n⟩ ≫
                kernel.ι (PrincipalTorsionTower.powerMultiplication A (H (p + 1)) (f ^ (n + 1))) =
              (HH 0).homologySequenceδ (koszulTriangle n) p (p + 1) (by omega) ≫
                (HH (p + 1)).map (RΓ.map eE.hom)) ∧
          (∀ n : ℕ,
            previousOut.app ⟨n⟩ ≫
                kernel.ι (PrincipalTorsionTower.powerMultiplication A (H p) (f ^ (n + 1))) =
              (HH 0).homologySequenceδ (koszulTriangle n) (p - 1) p (by omega) ≫
                (HH p).map (RΓ.map eE.hom)) ∧
          (∀ n : ℕ, topIn ≫ limit.π (cohTower p) ⟨n⟩ =
            limit.π (CompletionSequences.powerQuotientSystem A (H p) f) ⟨n⟩ ≫ termIn.app ⟨n⟩) ∧
          (∀ n : ℕ, topOut ≫
              limit.π (PrincipalTorsionTower.powerTorsionSystem A (H (p + 1)) f) ⟨n⟩ =
            limit.π (cohTower p) ⟨n⟩ ≫ termOut.app ⟨n⟩) ∧
          IsIso productComparison ∧
          (productComparison ≫
              cokernel.π (CompletionSequences.moduleDifference A (cohTower (p - 1))) ≫ columnIn =
            (HH 0).homologySequenceδ limitTriangle (p - 1) p (by omega)) ∧
          (∀ n : ℕ, columnOut ≫ limit.π (cohTower p) ⟨n⟩ =
            (HH p).map (RΓ.map a ≫ RΓ.map (Pi.π Y n))) ∧
          (cokernel.π (CompletionSequences.moduleDifference A (cohTower (p - 1))) ≫ bottom.inv =
            (Pi.lift fun n : ℕ ↦
              Pi.π (fun n : ℕ ↦ (cohTower (p - 1)).obj ⟨n⟩) n ≫ previousOut.app ⟨n⟩) ≫
              cokernel.π (CompletionSequences.moduleDifference A
                (PrincipalTorsionTower.powerTorsionSystem A (H p) f))) ∧
          (ShortComplex.mk topIn topOut htop).ShortExact ∧
          (ShortComplex.mk middleIn middleOut hmiddle).ShortExact ∧
          (ShortComplex.mk leftIn leftOut hleft).ShortExact ∧
          (ShortComplex.mk columnIn columnOut hcolumn).ShortExact ∧
          middleIn ≫ columnOut = leftOut ≫ topIn ∧
          middleOut = columnOut ≫ topOut ∧
          bottom.hom ≫ columnIn = leftIn ≫ middleIn
Tag 0H3D, a lemma

Tag 0H3D in the Stacks Project.

proIso_Ksys_Csys, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/ProIsomorphismOfKernelSystems.lean, line 640.

If M[f^n] stabilizes, then the inverse systems (K_n) and (C_n) are pro-isomorphic in D(A).

theorem proIso_Ksys_Csys {M : C} (f : M ⟶ M) [HasDerivedCategory C] (hf : Stabilizes f) :
    Nonempty (InverseSequence.ProIso (Ksys f) (Csys f))
Tag 0H3E, an example

Tag 0H3E in the Stacks Project.

Stacks.Cohomology.PrincipalFormalFunctions.nonempty_iso_derivedSections_quotientTower_derivedCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalFunctionsDiagram.lean, line 1180. The attribute's comment: “the identification RΓ(X, ℱ^) = RΓ(X, ℱ)^∧ and the resulting Hᵖ(X, ℱ^) = Hᵖ(RΓ(X, ℱ)^∧), on a ringed space, with derived f-adic completion presented as in Stacks 0BKG by an arbitrary left adjoint to the inclusion of the derived-complete objects; also derived completeness of RΓ(X, ℱ^)”.

Clause (7) of [Stacks, Tag 0H3E]: RΓ(X, ℱ^) = RΓ(X, ℱ)^∧ on a ringed space. Let (X, 𝒪_X) be a ringed space, let ρ : A ⟶ Γ(X, 𝒪_X) be a homomorphism from a commutative ring A, let f ∈ A and let ℱ be a sheaf of 𝒪_X-modules whose f-power torsion stabilizes. Let ℱ^ be a derived limit of the tower of honest quotients ℱ/f^(n+1)ℱ. Then

RΓ(X, ℱ^) ≅ RΓ(X, ℱ)^∧,

the object RΓ(X, ℱ^) is derived complete for (f), and for every p its p-th cohomology module is that of RΓ(X, ℱ)^∧ — the identification Hᵖ(X, ℱ^) = Hᵖ(RΓ(X, ℱ)^∧) the diagram of the source rests on.

This is the displayed equality of [Stacks, Tag 0BLD] on an arbitrary ringed space: the Koszul form of it is nonempty_iso_derivedSections_koszulTower_derivedCompletion, and the pro-isomorphism of [Stacks, Tag 0H3D] replaces the Koszul tower by the quotient tower. No quasi-coherence is needed, only stabilization of the f-power torsion.

theorem nonempty_iso_derivedSections_quotientTower_derivedCompletion
    (ℱ : SheafOfModules.{u} (structureSheafRing X))
    (hstab : Stabilizes ((baseSmul X ρ f).asHom.app ℱ))
    (Fhat : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hFhat : IsDerivedLimit (Csys ((baseSmul X ρ f).asHom.app ℱ)) Fhat) :
    let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
      fun L ↦ IsDerivedComplete (Ideal.span {f}) L
    ∀ (completion : DerivedCategory (ModuleCat.{u} A) ⥤ P.FullSubcategory)
      (_ : completion ⊣ P.ι),
      let completed := completion ⋙ P.ι
      let sglF :=
        (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).obj ℱ
      Nonempty ((derivedSectionsOver X ρ).obj Fhat ≅
          completed.obj ((derivedSectionsOver X ρ).obj sglF)) ∧
        IsDerivedComplete (Ideal.span {f}) ((derivedSectionsOver X ρ).obj Fhat) ∧
        ∀ p : ℤ, Nonempty
          ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj
              ((derivedSectionsOver X ρ).obj Fhat) ≅
            (DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj
              (completed.obj ((derivedSectionsOver X ρ).obj sglF)))

Stacks.Cohomology.PrincipalFormalFunctions.exists_formalFunctionsDiagram_quotientTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PrincipalFormalFunctionsDiagram.lean, line 1248. The attribute's comment: “the whole diagram for the quotient tower ℱ/fⁿℱ: the top row, the middle row, the left column, the middle column, the bottom isomorphism, the three commutativities, and the identification RΓ(X, ℱ^) = RΓ(X, ℱ)^∧; derived f-adic completion presented as in Stacks 0BKG by an arbitrary left adjoint to the inclusion of the derived-complete objects”.

Formal functions for a principal ideal along the quotient tower: the whole diagram of [Stacks, Tag 0H3E]. Let (X, 𝒪_X) be a ringed space, let ρ : A ⟶ Γ(X, 𝒪_X) be a homomorphism from a commutative ring A, let f ∈ A, let ℱ be a sheaf of 𝒪_X-modules whose f-power torsion stabilizes, and let ℱ^ be a derived limit of the tower of quotients ℱ/f^(n+1)ℱ. Then for every p the commutative diagram of the source exists, with exact rows and columns:

  • the top row 0 ⟶ Hᵖ(X, ℱ)^ ⟶ lim Hᵖ(X, ℱ/fⁿℱ) ⟶ T_f(Hᵖ⁺¹(X, ℱ)) ⟶ 0;
  • the middle row 0 ⟶ H⁰(Hᵖ(X, ℱ)^∧) ⟶ Hᵖ(X, ℱ^) ⟶ T_f(Hᵖ⁺¹(X, ℱ)) ⟶ 0;
  • the left column 0 ⟶ R¹lim Hᵖ(X, ℱ)[fⁿ] ⟶ H⁰(Hᵖ(X, ℱ)^∧) ⟶ Hᵖ(X, ℱ)^ ⟶ 0;
  • the middle column 0 ⟶ R¹lim Hᵖ⁻¹(X, ℱ/fⁿℱ) ⟶ Hᵖ(X, ℱ^) ⟶ lim Hᵖ(X, ℱ/fⁿℱ) ⟶ 0;
  • the bottom comparison R¹lim Hᵖ(X, ℱ)[fⁿ] ≅ R¹lim Hᵖ⁻¹(X, ℱ/fⁿℱ);

the three commutativities that make the nine terms a diagram, and the identification RΓ(X, ℱ^) ≅ RΓ(X, ℱ)^∧. As in [Stacks, Tag 0H32], S is the data of the two completion sequences of [Stacks, Tag 0BKG] for RΓ(X, ℱ), so the middle row and the left column are that source's own maps, and γ is the identification of Hᵖ(X, ℱ^) with Hᵖ(RΓ(X, ℱ)^∧).

This is exists_formalFunctionsDiagram_principalKoszulTower with the f-power Koszul tower replaced by the tower of honest quotients, the replacement being licensed by the pro-isomorphism of [Stacks, Tag 0H3D]. Only the two tower-dependent terms and Hᵖ(X, ℱ^) change, and they change by isomorphism: a pro-isomorphism shifts the index, so the limit and the first derived limit of the two cohomology towers agree as modules while the individual projections do not correspond, which is why the per-level normalizations of the Koszul form are not asserted here. The middle column is available with its maps normalized directly by the Milnor triangle of the quotient tower, as Stacks.Cohomology.QuotientTowerFormalFunctions .exists_shortExact_homology_derivedSections_quotientTower.

theorem exists_formalFunctionsDiagram_quotientTower
    (ℱ : SheafOfModules.{u} (structureSheafRing X))
    (hstab : Stabilizes ((baseSmul X ρ f).asHom.app ℱ))
    (Fhat : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hFhat : IsDerivedLimit (Csys ((baseSmul X ρ f).asHom.app ℱ)) Fhat)
    (p : ℤ) :
    let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
      fun L ↦ IsDerivedComplete (Ideal.span {f}) L
    ∀ (completion : DerivedCategory (ModuleCat.{u} A) ⥤ P.FullSubcategory)
      (adj : completion ⊣ P.ι),
      let completed := completion ⋙ P.ι
      let HH (q : ℤ) := DerivedCategory.homologyFunctor (ModuleCat.{u} A) q
      let sglF :=
        (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).obj ℱ
      let K := (derivedSectionsOver X ρ).obj sglF
      let H (q : ℤ) := (HH q).obj K
      let quotTower (q : ℤ) :=
        (Csys ((baseSmul X ρ f).asHom.app ℱ) ⋙ derivedSectionsOver X ρ) ⋙ HH q
      let ordinaryCompletion := limit (CompletionSequences.powerQuotientSystem A (H p) f)
      let limitQuot := limit (quotTower p)
      let tate := CompletionSequences.adicTateModule A (H (p + 1)) f
      let H0CompletedHp := (HH 0).obj
        (completed.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (H p)))
      let HpFhat := (HH p).obj ((derivedSectionsOver X ρ).obj Fhat)
      let R1Torsion := CompletionSequences.firstDerivedLimit A
        (PrincipalTorsionTower.powerTorsionSystem A (H p) f)
      let R1PreviousQuot := CompletionSequences.firstDerivedLimit A (quotTower (p - 1))
      ∃ (S : CompletionSequences.PrincipalCompletionSequences A f completed adj.unit)
        (γ : HpFhat ≅ (HH p).obj (completed.obj K)),
        let middleIn : H0CompletedHp ⟶ HpFhat := (S.truncation K p).inclusion S.shift ≫ γ.inv
        let middleOut : HpFhat ⟶ tate := γ.hom ≫ (S.truncation K p).projection f S.shift
          (S.moduleSequence (H (p + 1))).tateIso
        let leftIn : R1Torsion ⟶ H0CompletedHp := (S.moduleSequence (H p)).inclusion
        let leftOut : H0CompletedHp ⟶ ordinaryCompletion := (S.moduleSequence (H p)).projection
        ∃ (topIn : ordinaryCompletion ⟶ limitQuot)
          (topOut : limitQuot ⟶ tate)
          (htop : topIn ≫ topOut = 0)
          (hmiddle : middleIn ≫ middleOut = 0)
          (hleft : leftIn ≫ leftOut = 0)
          (columnIn : R1PreviousQuot ⟶ HpFhat)
          (columnOut : HpFhat ⟶ limitQuot)
          (hcolumn : columnIn ≫ columnOut = 0)
          (bottom : R1Torsion ≅ R1PreviousQuot),
          (ShortComplex.mk topIn topOut htop).ShortExact ∧
          (ShortComplex.mk middleIn middleOut hmiddle).ShortExact ∧
          (ShortComplex.mk leftIn leftOut hleft).ShortExact ∧
          (ShortComplex.mk columnIn columnOut hcolumn).ShortExact ∧
          middleIn ≫ columnOut = leftOut ≫ topIn ∧
          middleOut = columnOut ≫ topOut ∧
          bottom.hom ≫ columnIn = leftIn ≫ middleIn ∧
          Nonempty ((derivedSectionsOver X ρ).obj Fhat ≅ completed.obj K)

Stacks.Cohomology.QuotientTowerFormalFunctions.exists_shortExact_homology_derivedSections_quotientTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InverseSystems/QuotientTowerFormalFunctions.lean, line 351. The attribute's comment: “the middle column of the diagram, transported to the quotient tower ℱ/fⁿℱ by the pro-isomorphism of Tag 0H3D; its two maps normalized by the Milnor triangle of the quotient tower itself”.

Formal functions for a principal ideal along the quotient tower: the middle column. Let (X, 𝒪_X) be a ringed space, let ρ : A ⟶ Γ(X, 𝒪_X) be a homomorphism from a commutative ring A, let f ∈ A and let ℱ be a sheaf of 𝒪_X-modules whose f-power torsion stabilizes. Let ℱ^ be a derived limit of the tower of quotients ℱ/f^(n+1)ℱ and let E^ be a derived limit of the f-power Koszul tower. Then E^ ≅ ℱ^, and for every p the cohomology of RΓ(X, ℱ^) over A sits in a short exact sequence

0 ⟶ R¹lim Hᵖ⁻¹(X, ℱ/f^(n+1)ℱ) ⟶ Hᵖ(X, ℱ^) ⟶ lim Hᵖ(X, ℱ/f^(n+1)ℱ) ⟶ 0,

whose inclusion descends the connecting morphism of the Milnor triangle and whose projection is characterized by the limit projections, and whose outer terms are isomorphic to the outer terms of the corresponding sequence for the Koszul tower.

theorem exists_shortExact_homology_derivedSections_quotientTower (f : A)
    (ℱ : SheafOfModules.{u} (structureSheafRing X)) (hstab : Stabilizes ((baseSmul X ρ f).asHom.app ℱ))
    (Fhat Ehat : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (hFhat : IsDerivedLimit (Csys ((baseSmul X ρ f).asHom.app ℱ)) Fhat)
    (hEhat : IsDerivedLimit (Ksys ((baseSmul X ρ f).asHom.app ℱ)) Ehat) :
    let F : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      Csys ((baseSmul X ρ f).asHom.app ℱ) ⋙ derivedSectionsOver X ρ
    let G : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{u} A) :=
      Ksys ((baseSmul X ρ f).asHom.app ℱ) ⋙ derivedSectionsOver X ρ
    let Y : ℕ → DerivedCategory (ModuleCat.{u} A) := fun n ↦ F.obj (op n)
    let d : (∏ᶜ Y) ⟶ ∏ᶜ Y := Pi.lift fun n : ℕ ↦
      Pi.π Y n - Pi.π Y (n + 1) ≫ F.map (homOfLE (Nat.le_succ n)).op
    Nonempty (Ehat ≅ Fhat) ∧
      ∃ (a : (derivedSectionsOver X ρ).obj Fhat ⟶ ∏ᶜ Y)
        (b : (∏ᶜ Y) ⟶ ((derivedSectionsOver X ρ).obj Fhat)⟦(1 : ℤ)⟧),
        let T := Triangle.mk a d b
        T ∈ distTriang (DerivedCategory (ModuleCat.{u} A)) ∧
          ∀ p : ℤ,
            let H := DerivedCategory.homologyFunctor (ModuleCat.{u} A) p
            let H₁ := DerivedCategory.homologyFunctor (ModuleCat.{u} A) (p - 1)
            let homologySystem : ℕᵒᵖ ⥤ ModuleCat.{u} A := F ⋙ H
            let shiftedHomologySystem : ℕᵒᵖ ⥤ ModuleCat.{u} A := F ⋙ H₁
            let P : ModuleCat.{u} A :=
              ∏ᶜ fun n : ℕ ↦ shiftedHomologySystem.obj (op n)
            let δ : P ⟶ P := Pi.lift fun n : ℕ ↦
              Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (op n)) n -
                Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (op n)) (n + 1) ≫
                  shiftedHomologySystem.map (homOfLE (Nat.le_succ n)).op
            ∃ (e : H₁.obj (∏ᶜ Y) ≅ P)
              (i : cokernel δ ⟶ H.obj ((derivedSectionsOver X ρ).obj Fhat))
              (q : H.obj ((derivedSectionsOver X ρ).obj Fhat) ⟶ limit homologySystem)
              (w : i ≫ q = 0),
              e.hom = piComparison H₁ Y ∧
                cokernel.π δ ≫ i = e.inv ≫
                  DerivedCategory.HomologySequence.δ T (p - 1) p ∧
                (∀ n : ℕ, q ≫ limit.π homologySystem (op n) =
                  H.map a ≫ H.map (Pi.π Y n)) ∧
                (ShortComplex.mk i q w).ShortExact ∧
                Nonempty (limit homologySystem ≅ limit (G ⋙ H)) ∧
                Nonempty (cokernel δ ≅
                  CompletionSequences.firstDerivedLimit A (G ⋙ H₁))
Sources
LeanStacks.Cohomology.PrincipalFormalFunctions.formalFunctionsDiagram_principalKoszulTower · proIso_Ksys_Csys · Stacks.Cohomology.PrincipalFormalFunctions.nonempty_iso_derivedSections_quotientTower_derivedCompletion · Stacks.Cohomology.PrincipalFormalFunctions.exists_formalFunctionsDiagram_quotientTower · Stacks.Cohomology.QuotientTowerFormalFunctions.exists_shortExact_homology_derivedSections_quotientTower

Section20.40 Čech cohomology of unbounded complexes#

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

Tag 08C0, an equation

Tag 08C0 in the Stacks Project.

Stacks.Cech.globalSectionsToAlternatingCech, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingGlobalSections.lean, line 180.

Stacks Project, Tag 08C0. The functorial map from the complex of global sections to the total alternating Čech complex: in each cohomological degree a section is sent, in Čech degree zero, to its restrictions to the members of the family.

noncomputable def globalSectionsToAlternatingCech :
    globalSectionsUliftComplexFunctor.{u, v, w} X ⟶ alternatingCechTotalComplexFunctor U

Stacks.Cech.globalSectionsToAlternatingCech_app_f, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingGlobalSections.lean, line 208. The attribute's comment: “degree-zero restrictions and vanishing higher components”.

Stacks Project, Tag 08C0. In every cohomological degree the canonical map restricts a global section into alternating Čech degree zero and includes that summand into the total complex; in particular all of its positive Čech components vanish.

lemma globalSectionsToAlternatingCech_app_f
    (K : CochainComplex ((Opens X)ᵒᵖ ⥤ AddCommGrpCat.{w}) ℤ) (n : ℤ) :
    ((globalSectionsToAlternatingCech X U).app K).f n =
      globalSectionsAlternatingCechRestrictionInt X U (K.X n) ≫
        ((alternatingCechBicomplexFunctor U).obj K).ιTotal (up ℤ) 0 n n (by simp)
Tag 08C1, a lemma

Tag 08C1 in the Stacks Project.

Stacks.Cech.alternatingCechToDerivedGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/AlternatingDerivedGlobalSections.lean, line 275.

Stacks Project, Tag 08C1. For a ringed space (X, O_X) and a finite open covering U of X, the total alternating Čech complex of an unbounded complex of O_X-modules has a canonical map to its derived global sections, functorial in the complex and compatible with the augmentation of Tag 08C0.

noncomputable def alternatingCechToDerivedGlobalSections :
    AlternatingCechToDerivedGlobalSections X R
Tag 08C2, a lemma

Tag 08C2 in the Stacks Project.

Stacks.Cech.isIso_alternatingCechToDerivedComparison_of_acyclicBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/AlternatingCechComputesDerivedSections.lean, line 93.

[Stacks, Tag 08C2] Let (X, O_X) be a ringed space, let U : I → Opens X be a finite open covering of X and let F^• be a complex of O_X-modules. Let B be a set of open subsets of X such that every open of X is a union of members of B, such that every finite intersection of members of the covering lies in B, and such that for every W ∈ B and every p > 0 the cohomology groups H^p(W, F^q), H^p(W, Coker(F^{q-1} → F^q)) and H^p(W, H^q(F)) all vanish. Then the comparison map Tot(Č_alt^•(U, F^•)) ⟶ RΓ(X, F^•) of Tag 08C1 is an isomorphism in D(Ab).

theorem isIso_alternatingCechToDerivedComparison_of_acyclicBasis
    {I : Type u} [Finite I] (U : I → Opens X) (hU : (⊤ : Opens X) = iSup U)
    (F : CochainComplex (SheafOfModules.{u} R) ℤ)
    (B : Set (Opens X)) (hB : Opens.IsBasis B)
    (h_inter : ∀ (p : ℕ) (s : Fin (p + 1) → I), (⨅ k, U (s k)) ∈ B)
    (h_terms : ∀ W ∈ B, ∀ (q : ℤ) (p : ℕ), 0 < p →
      IsZero (((SheafOfModules.evaluation R (op W)).rightDerived p).obj (F.X q)))
    (h_cokernels : ∀ W ∈ B, ∀ (q : ℤ) (p : ℕ), 0 < p →
      IsZero (((SheafOfModules.evaluation R (op W)).rightDerived p).obj
        (cokernel (F.d (q - 1) q))))
    (h_homology : ∀ W ∈ B, ∀ (q : ℤ) (p : ℕ), 0 < p →
      IsZero (((SheafOfModules.evaluation R (op W)).rightDerived p).obj (F.homology q))) :
    IsIso ((alternatingCechToDerivedComparison X R U hU).app F)
Sources
LeanStacks.Cech.globalSectionsToAlternatingCech · Stacks.Cech.globalSectionsToAlternatingCech_app_f · Stacks.Cech.alternatingCechToDerivedGlobalSections · Stacks.Cech.isIso_alternatingCechToDerivedComparison_of_acyclicBasis

Section20.41 Hom complexes#

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

Tag 0A8K, the section

Tag 0A8K in the Stacks Project.

Stacks.SheafOfModules.sheafHomComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/InternalHomComplexQuasiIso.lean, line 121.

Stacks 0A8K. The internal Hom complex SheafHom•(K, I) of two complexes of O_X-modules on a ringed space: in degree n its sections over an open U are the degree-n cochains from K|_U to I|_U, that is the product over the pairs p + n = q of the sections of SheafHom(K^p, I^q), with the differential d(f) = d_I ∘ f - (-1)^n f ∘ d_K.

abbrev sheafHomComplex (K I : CochainComplex (StructureSheafModules Rc) ℤ) :
    SheafHomComplex Rc K I
Tag 0A8L, an equation

Tag 0A8L in the Stacks Project.

Stacks.SheafOfModules.sheafHomComplexHomologyEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/InternalHomComplexCohomology.lean, line 99. The attribute's comment: “H^n(Γ(U, SheafHom^•(L, M))) = Hom_{K(O_U)}(L|_U, M|_U[n]) for every open U of X and every n ∈ ℤ, with SheafHom^•(L, M) the internal Hom complex constructed in Tag 0A8K.”.

Stacks 0A8L. The n-th cohomology of the sections over U of the internal Hom complex SheafHom^•(L, M) of [Stacks, Tag 0A8K] is canonically the group of morphisms from L|_U to M|_U[n] in the homotopy category of complexes of O_U-modules.

noncomputable def sheafHomComplexHomologyEquiv (U : Opens X)
    (L M : CochainComplex (StructureSheafModules Rc) ℤ) (n : ℤ) :
    (sectionComplex Rc (sheafHomComplex Rc L M).obj U).homology n ≃+
      ((HomotopyCategory.quotient
          (SheafOfModules.{u} ((structureSheaf Rc).over U))
          (ComplexShape.up ℤ)).obj (restrictComplex Rc L U) ⟶
        (HomotopyCategory.quotient
          (SheafOfModules.{u} ((structureSheaf Rc).over U))
          (ComplexShape.up ℤ)).obj ((restrictComplex Rc M U)⟦n⟧))

Stacks.SheafOfModules.sheafHomComplexHomologyEquivHomotopyCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/HomotopyCategoryHoms.lean, line 55.

The n-th cohomology of the sections over U of the internal Hom complex from L to M is canonically the group of morphisms from L|_U to M|_U[n] in the homotopy category of complexes of O_U-modules.

noncomputable def sheafHomComplexHomologyEquivHomotopyCategory
    {X : TopCat.{u}} (Rc : TopCat.Sheaf CommRingCat.{u} X)
    (U : Opens X)
    (L M : CochainComplex (StructureSheafModules Rc) ℤ)
    (H : SheafHomComplex Rc L M) (n : ℤ) :
    (sectionComplex Rc H.obj U).homology n ≃+
      ((HomotopyCategory.quotient
          (SheafOfModules.{u} ((structureSheaf Rc).over U))
          (ComplexShape.up ℤ)).obj (restrictComplex Rc L U) ⟶
        (HomotopyCategory.quotient
          (SheafOfModules.{u} ((structureSheaf Rc).over U))
          (ComplexShape.up ℤ)).obj ((restrictComplex Rc M U)⟦n⟧))
Tag 0A8M, a lemma

Tag 0A8M in the Stacks Project.

Stacks.Cohomology.SheafHomComplexCurrying.sheafHomTensorIsoConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/TensorHomAdjunction.lean, line 385.

Stacks 0A8M. For complexes K, L, M of O_X-modules on a ringed space there is an isomorphism SheafHom•(K, SheafHom•(L, M)) ≅ SheafHom•(Tot(K ⊗_{O_X} L), M) of complexes of O_X-modules, functorial in K, L and M.

def sheafHomTensorIsoConstruction : SheafHomTensorIsoConstruction Rc
Tag 0A8N, a lemma

Tag 0A8N in the Stacks Project.

AlgebraicGeometry.RingedSite.compositionConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/InternalHom/CompositionMorphism.lean, line 406. The attribute's comment: “the ringed space case”.

Stacks 0A91. For complexes K, L, M of modules on a ringed site there is a canonical morphism of complexes of O-modules

Tot(SheafHom(L, M) ⊗_O SheafHom(K, L)) ⟶ SheafHom(K, M),

namely the one sending each homogeneous local pure tensor to the composite of its two factors, with no extra sign.

A ringed space is a ringed site, namely the site of its opens with the open-cover topology, so this also gives the composition morphism for complexes of modules on a ringed space.

noncomputable def compositionConstruction : CompositionConstruction X
Tag 0BYR, a lemma

Tag 0BYR in the Stacks Project.

Stacks.SheafOfModules.diagonalBetterConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorSheafHom.lean, line 283. The attribute's comment: “the canonical morphism”.

Stacks 0BYR. The canonical diagonal morphisms Tot(K ⊗ SheafHom(M, L)) ⟶ SheafHom(M, Tot(K ⊗ L)) for complexes of modules on a ringed space, sending a homogeneous local pure tensor k ⊗ φ to the internal Hom section m ↦ k ⊗ φ(m).

noncomputable def diagonalBetterConstruction : DiagonalBetterConstruction Rc

Stacks.SheafOfModules.diagonalBetter_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorSheafHom.lean, line 382. The attribute's comment: “functoriality in the first complex”.

Stacks 0BYR. The canonical diagonal morphism is covariant in the tensor factor.

theorem diagonalBetter_natural_left
    {K K' : CochainComplex (StructureSheafModules Rc) ℤ}
    (L M : CochainComplex (StructureSheafModules Rc) ℤ) (f : K ⟶ K') :
    diagonalBetter Rc K L M ≫ sheafHomComplexMap Rc (𝟙 M) (tensorTotalMap Rc f (𝟙 L)) =
      tensorTotalMap Rc f (𝟙 (sheafHomComplex Rc M L).obj) ≫ diagonalBetter Rc K' L M

Stacks.SheafOfModules.diagonalBetter_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorSheafHom.lean, line 392. The attribute's comment: “functoriality in the second complex”.

Stacks 0BYR. The canonical diagonal morphism is covariant in the target of the internal Hom complex.

theorem diagonalBetter_natural_right
    (K : CochainComplex (StructureSheafModules Rc) ℤ)
    {L L' : CochainComplex (StructureSheafModules Rc) ℤ}
    (M : CochainComplex (StructureSheafModules Rc) ℤ) (g : L ⟶ L') :
    diagonalBetter Rc K L M ≫ sheafHomComplexMap Rc (𝟙 M) (tensorTotalMap Rc (𝟙 K) g) =
      tensorTotalMap Rc (𝟙 K) (sheafHomComplexMap Rc (𝟙 M) g) ≫ diagonalBetter Rc K L' M

Stacks.SheafOfModules.diagonalBetter_natural_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorSheafHom.lean, line 403. The attribute's comment: “functoriality in the third complex”.

Stacks 0BYR. The canonical diagonal morphism is contravariant in the source of the internal Hom complex.

theorem diagonalBetter_natural_hom
    (K L : CochainComplex (StructureSheafModules Rc) ℤ)
    {M M' : CochainComplex (StructureSheafModules Rc) ℤ} (h : M' ⟶ M) :
    diagonalBetter Rc K L M ≫ sheafHomComplexMap Rc h (𝟙 (tensorTotal Rc K L)) =
      tensorTotalMap Rc (𝟙 K) (sheafHomComplexMap Rc h (𝟙 L)) ≫ diagonalBetter Rc K L M'
Tag 0A8Q, a lemma

Tag 0A8Q in the Stacks Project.

Stacks.SheafOfModules.diagonalTensorHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorHom.lean, line 573. The attribute's comment: “canonical diagonal morphism”.

The diagonal morphism sends a homogeneous section k of K to the homogeneous map l ↦ k ⊗ l from L to the total tensor product.

noncomputable def diagonalTensorHom
    (K L : CochainComplex (StructureSheafModules Rc) ℤ) :
    K ⟶ (sheafHomComplex Rc L (tensorTotal Rc K L)).obj

Stacks.SheafOfModules.diagonalTensorHom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorHom.lean, line 581. The attribute's comment: “canonical characterization”.

On local sections, the diagonal morphism is inclusion of the pure tensor in the appropriate summand of the total complex.

theorem diagonalTensorHom_apply
    (K L : CochainComplex (StructureSheafModules Rc) ℤ) (U : Opens X)
    (n p : ℤ) (k : (K.X n).val.obj (op U))
    (l : (L.X p).val.obj (op U)) :
    applyHomSection Rc (sheafHomComplex Rc L (tensorTotal Rc K L))
        U n p (n + p) (by omega)
        (((diagonalTensorHom Rc K L).f n).val.app (op U) k) l =
      tensorTotalSection Rc K L U n p k l

Stacks.SheafOfModules.diagonalTensorHom_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/DiagonalTensorHom.lean, line 627. The attribute's comment: “functoriality in both complexes”.

The diagonal morphism is natural in K and dinatural in L.

theorem diagonalTensorHom_natural
    {K K' L L' : CochainComplex (StructureSheafModules Rc) ℤ}
    (f : K ⟶ K') (g : L ⟶ L') :
    diagonalTensorHom Rc K L ≫
        sheafHomComplexMap Rc (𝟙 L) (tensorTotalMap Rc f g) =
      f ≫ diagonalTensorHom Rc K' L' ≫
        sheafHomComplexMap Rc g (𝟙 (tensorTotal Rc K' L'))
Tag 0A8P, a lemma

Tag 0A8P in the Stacks Project.

Stacks.SheafOfModules.evaluationConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHomEvaluation/TensorTotalEvaluation.lean, line 65. The attribute's comment: “canonical evaluation morphism”.

Stacks 0A8P. The canonical evaluation morphisms for internal Hom complexes of modules on a ringed space, specified on homogeneous local pure tensors by the signed formula φ ⊗ k ↦ (-1)^(r + (-a) * r) (ψ ↦ φ (ψ k)). It is the evaluation morphism of the ringed site of opens of the space.

noncomputable def evaluationConstruction : EvaluationConstruction Rc

Stacks.SheafOfModules.evaluateAndMore_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHomEvaluation/TensorTotalEvaluation.lean, line 80. The attribute's comment: “functoriality in all three complexes”.

Stacks 0A8P. Evaluation is covariant in K and M and contravariant in L.

theorem evaluateAndMore_natural
    {K K' L L' M M' : CochainComplex (StructureSheafModules Rc) ℤ}
    (k : K ⟶ K') (l : L' ⟶ L) (m : M ⟶ M') :
    tensorTotalMap Rc (sheafHomComplexMap Rc l m) k ≫
        evaluateAndMore Rc K' L' M' =
      evaluateAndMore Rc K L M ≫
        sheafHomComplexMap Rc (sheafHomComplexMap Rc k l) m
Tag 0A8R, a lemma

Tag 0A8R in the Stacks Project.

Stacks.SheafOfModules.sheafHomComplexHomologyEquivDerivedCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedCategoryHoms.lean, line 118.

Stacks 0A8R. If I is K-injective, degree-zero cohomology over U of the internal Hom complex from L to I is canonically the group of derived morphisms between the objects represented by their restrictions to the open subspace U.

noncomputable def sheafHomComplexHomologyEquivDerivedCategory
    {X : TopCat.{u}} (Rc : TopCat.Sheaf CommRingCat.{u} X) (U : Opens X)
    (L I : CochainComplex (StructureSheafModules Rc) ℤ) [I.IsKInjective]
    (H : SheafHomComplex Rc L I)
    (LU MU : DerivedCategory
      (SheafOfModules.{u} (resRing U (structureSheaf Rc))))
    (eL : DerivedCategory.Qh.obj
      ((HomotopyCategory.quotient _ _).obj
        (restrictComplexToSubspace (structureSheaf Rc) U L)) ≅ LU)
    (eM : DerivedCategory.Qh.obj
      ((HomotopyCategory.quotient _ _).obj
        ((restrictComplexToSubspace (structureSheaf Rc) U I)⟦(0 : ℤ)⟧)) ≅ MU) :
    (sectionComplex Rc H.obj U).homology 0 ≃+
      (LU ⟶ MU)

Stacks.SheafOfModules.sheafHomComplexHomologyEquivDerivedCategory_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedCategoryHoms.lean, line 161. The attribute's comment: “canonical comparison on section classes”.

Stacks 0A8R. The canonical identification sends a section cohomology class first to its homotopy-class morphism, transports that morphism from the slice-site model to the open-subspace model, and then localizes it. In particular this fixes its value on the identity class and its behaviour under changing the two representatives.

theorem sheafHomComplexHomologyEquivDerivedCategory_apply
    {X : TopCat.{u}} (Rc : TopCat.Sheaf CommRingCat.{u} X) (U : Opens X)
    (L I : CochainComplex (StructureSheafModules Rc) ℤ) [I.IsKInjective]
    (H : SheafHomComplex Rc L I)
    (LU MU : DerivedCategory
      (SheafOfModules.{u} (resRing U (structureSheaf Rc))))
    (eL : DerivedCategory.Qh.obj
      ((HomotopyCategory.quotient _ _).obj
        (restrictComplexToSubspace (structureSheaf Rc) U L)) ≅ LU)
    (eM : DerivedCategory.Qh.obj
      ((HomotopyCategory.quotient _ _).obj
        ((restrictComplexToSubspace (structureSheaf Rc) U I)⟦(0 : ℤ)⟧)) ≅ MU)
    (z : (sectionComplex Rc H.obj U).homology 0) :
    sheafHomComplexHomologyEquivDerivedCategory Rc U L I H LU MU eL eM z =
      (let E := U.sheafOfModulesEquivOver (structureSheaf Rc)
            let Fh := E.functor.mapHomotopyCategory (ComplexShape.up ℤ)
       let K := restrictComplex Rc L U
       let J := (restrictComplex Rc I U)⟦(0 : ℤ)⟧
       let eK := (E.functor.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).app K ≪≫
         (HomotopyCategory.quotient _ _).mapIso
           (eqToIso (mapHomologicalComplex_restrictComplex Rc U L))
       let eJ := (E.functor.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).app J ≪≫
         (HomotopyCategory.quotient _ _).mapIso
           (eqToIso (mapHomologicalComplex_restrictComplex_shiftZero Rc U I))
       eL.inv ≫ DerivedCategory.Qh.map
         (eK.inv ≫ Fh.map
           (sheafHomComplexHomologyEquivHomotopyCategory
             Rc U L I H 0 z) ≫ eJ.hom) ≫ eM.hom)
Tag 0A8S, a lemma

Tag 0A8S in the Stacks Project.

Stacks.SheafOfModules.sheafHomComplexMap_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/HomComplexAndStrictPerfection/InternalHomComplexQuasiIso.lean, line 158.

Stacks 0A8S. A quasi-isomorphism between K-injective complexes, together with a quasi-isomorphism in the contravariant variable, induces a quasi-isomorphism between the corresponding canonical internal Hom complexes. This is what makes the derived internal Hom of complexes of O_X-modules well defined.

theorem sheafHomComplexMap_quasiIso
    {I' I L' L : CochainComplex (StructureSheafModules Rc) ℤ}
    (i : I' ⟶ I) [QuasiIso i] [I'.IsKInjective] [I.IsKInjective]
    (l : L' ⟶ L) [QuasiIso l] :
    QuasiIso (sheafHomComplexMap Rc l i)
Tag 0A8T, a lemma

Tag 0A8T in the Stacks Project.

Stacks.SheafOfModules.isKInjective_sheafHomComplex_of_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/KFlatIntoKInjective.lean, line 45.

The internal Hom complex SheafHom^•(L, I) from a K-flat complex L of O_X-modules into a K-injective complex I of O_X-modules is K-injective.

theorem isKInjective_sheafHomComplex_of_isKFlat
    (L I : CochainComplex (StructureSheafModules Rc) ℤ)
    (hL : IsKFlat Rc L) [I.IsKInjective] :
    (sheafHomComplex Rc L I).obj.IsKInjective
Sources
LeanStacks.SheafOfModules.sheafHomComplex · Stacks.SheafOfModules.sheafHomComplexHomologyEquiv · Stacks.SheafOfModules.sheafHomComplexHomologyEquivHomotopyCategory · Stacks.Cohomology.SheafHomComplexCurrying.sheafHomTensorIsoConstruction · AlgebraicGeometry.RingedSite.compositionConstruction · Stacks.SheafOfModules.diagonalBetterConstruction · Stacks.SheafOfModules.diagonalBetter_natural_left · Stacks.SheafOfModules.diagonalBetter_natural_right

Section20.42 Internal hom in the derived category#

Section 20.42 of the Stacks Project, Tag 08DH. 15 tags here are carried by 43 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08DI, an equation

Tag 08DI in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomTensorEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedInternalHom.lean, line 144.

Stacks 08DI. For objects K, L, M of D(O_X) on a ringed space, morphisms into the derived internal hom are canonically identified with morphisms out of the derived tensor product,

Hom_{D(O_X)}(K, RSheafHom(L, M)) = Hom_{D(O_X)}(K ⊗^L_{O_X} L, M),

as an isomorphism of abelian groups.

def derivedSheafHomTensorEquiv (K L M : DerivedCategory (StructureSheafModules Rc)) :
    (K ⟶ ((derivedSheafHom Rc).obj (op L)).obj M) ≃+
      (((derivedTensor Rc).obj K).obj L ⟶ M)
Tag 08DK, a lemma

Tag 08DK in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomGlobalSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedCategorySections.lean, line 79. The attribute's comment: “global sections”.

Stacks 08DK globally. For objects L, M of D(O_X) the degree-zero global hypercohomology of the derived internal Hom RSheafHom(L, M) is the group of morphisms L ⟶ M in the derived category of O_X-modules.

def derivedSheafHomGlobalSectionsEquiv (L M : DerivedCategory (StructureSheafModules Rc)) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections (ringedSite Rc)).obj
          (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op L)).obj M)) :
        Type u) ≃+ (L ⟶ M)

Stacks.SheafOfModules.derivedSheafHomSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedCategorySections.lean, line 94. The attribute's comment: “sections over an open”.

Stacks 08DK over an open. For objects L, M of D(O_X) and an open U ⊆ X the degree-zero hypercohomology over U of the derived internal Hom RSheafHom(L, M) is the group of morphisms L|_U ⟶ M|_U in the derived category of O_U-modules.

def derivedSheafHomSectionsEquiv (L M : DerivedCategory (StructureSheafModules Rc)) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((Stacks.Cohomology.Localization.derivedSectionsOverObject (ringedSite Rc) U).obj
          (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op L)).obj M)) :
        Type u) ≃+
      ((SheafOfModules.overFunctor.{u} (structureSheaf Rc) U).mapDerivedCategory.obj L ⟶
        (SheafOfModules.overFunctor.{u} (structureSheaf Rc) U).mapDerivedCategory.obj M)
Tag 08DJ, a lemma

Tag 08DJ in the Stacks Project.

Stacks.SheafOfModules.derivedCurryingData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedCurryingOnARingedSpace.lean, line 352. References: SGA 6 I (7.4), “first isomorphism”.

Stacks 08DJ. Let (X, O_X) be a ringed space and let K, L, M be objects of D(O_X). There is a canonical isomorphism

RSheafHom(K, RSheafHom(L, M)) ≅ RSheafHom(K ⊗^L_{O_X} L, M)

in D(O_X), functorial in K, L and M, which recovers the tensor--internal-Hom bijection of Stacks 08DI on taking H⁰(X, -).

def derivedCurryingData : DerivedCurryingData Rc
Tag 08DL, a lemma

Tag 08DL in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedRestrictionToOpens.lean, line 129.

Stacks 08DL. For objects K, L of D(O_X) the derived internal Hom commutes with restriction to an open U: restricting RSheafHom(K, L) to the opens contained in U gives the derived internal Hom RSheafHom(K|_U, L|_U) of the restrictions.

def derivedSheafHomRestrictionIso (K L : DerivedCategory (StructureSheafModules Rc)) :
    (derivedRestrict Rc U).obj
        (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op K)).obj L) ≅
      ((RingedSite.derivedSheafHomBifunctor ((ringedSite Rc).over U)).obj
          (op ((derivedRestrict Rc U).obj K))).obj ((derivedRestrict Rc U).obj L)

Stacks.SheafOfModules.derivedSheafHomRestrictionIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedRestrictionToOpens.lean, line 158. The attribute's comment: “functoriality in the first variable”.

The comparison of Stacks 08DL is natural in the contravariant variable: restricting the map RSheafHom(K, L) ⟶ RSheafHom(K', L) induced by f : K' ⟶ K gives the map induced by f|_U.

theorem derivedSheafHomRestrictionIso_natural_left
    {K K' L : DerivedCategory (StructureSheafModules Rc)} (f : K' ⟶ K) :
    (derivedRestrict Rc U).map
        (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).map f.op).app L) ≫
        (derivedSheafHomRestrictionIso Rc U K' L).hom =
      (derivedSheafHomRestrictionIso Rc U K L).hom ≫
        ((RingedSite.derivedSheafHomBifunctor ((ringedSite Rc).over U)).map
          ((derivedRestrict Rc U).map f).op).app ((derivedRestrict Rc U).obj L)

Stacks.SheafOfModules.derivedSheafHomRestrictionIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedRestrictionToOpens.lean, line 171. The attribute's comment: “functoriality in the second variable”.

The comparison of Stacks 08DL is natural in the covariant variable: restricting the map RSheafHom(K, L) ⟶ RSheafHom(K, L') induced by g : L ⟶ L' gives the map induced by g|_U.

theorem derivedSheafHomRestrictionIso_natural_right
    {K L L' : DerivedCategory (StructureSheafModules Rc)} (g : L ⟶ L') :
    (derivedRestrict Rc U).map
        (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op K)).map g) ≫
        (derivedSheafHomRestrictionIso Rc U K L').hom =
      (derivedSheafHomRestrictionIso Rc U K L).hom ≫
        ((RingedSite.derivedSheafHomBifunctor ((ringedSite Rc).over U)).obj
          (op ((derivedRestrict Rc U).obj K))).map ((derivedRestrict Rc U).map g)

Stacks.SheafOfModules.sheafHomRestrictionComplexMap_isRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedRestrictionToOpens.lean, line 202. The attribute's comment: “restriction of internal-Hom complexes”.

On every local homogeneous cochain, the chain-level comparison of Stacks 08DL is the canonical restriction isomorphism of internal Homs of modules. This is what pins the comparison down: a cochain over V ⊆ U is sent to the cochain it already is, read along the identification of Opens X / V with the opens contained in V inside Opens X / U.

theorem sheafHomRestrictionComplexMap_isRestriction
    (A B : CochainComplex (StructureSheafModules Rc) ℤ) :
    RingedSite.IsInternalHomRestrictionMap (ringedSite Rc) U A B
      (sheafHomRestrictionComplexMap Rc U A B)

Stacks.SheafOfModules.derivedSheafHomRestrictionIso_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedRestrictionToOpens.lean, line 212. The attribute's comment: “canonical model characterization”.

On the classes of complexes A and B with B K-injective, both sides of Stacks 08DL are the class of an internal Hom complex, and the comparison is the class of the chain-level restriction map. Together with naturality this determines the comparison.

theorem derivedSheafHomRestrictionIso_model
    (A B : CochainComplex (SheafOfModules.{u} (Tensor.ringSheaf (ringedSite Rc).O)) ℤ)
    [B.IsKInjective] :
    letI : PreservesFiniteLimits
        (SheafOfModules.overFunctor.{u} (Tensor.ringSheaf (ringedSite Rc).O) U) :=
      ‹PreservesFiniteLimits (SheafOfModules.overFunctor.{u} (structureSheaf Rc) U)›
    letI : PreservesFiniteColimits
        (SheafOfModules.overFunctor.{u} (Tensor.ringSheaf (ringedSite Rc).O) U) :=
      ‹PreservesFiniteColimits (SheafOfModules.overFunctor.{u} (structureSheaf Rc) U)›
    (derivedSheafHomRestrictionIso Rc U
          (DerivedCategory.Q.obj A) (DerivedCategory.Q.obj B)).hom ≫
        (RingedSite.restrictionTargetComparison (ringedSite Rc) U A B).hom =
      (RingedSite.restrictionSourceComparison (ringedSite Rc) U A B).hom ≫
        DerivedCategory.Q.map (sheafHomRestrictionComplexMap Rc U A B)
Tag 08I0, a lemma

Tag 08I0 in the Stacks Project.

Stacks.SheafOfModules.exists_distinguished_derivedSheafHom_first, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedSheafHomExactness.lean, line 107. The attribute's comment: “exactness in the source”.

Stacks 08I0, exactness in the source. On a ringed space, the derived internal hom into a fixed object carries a distinguished triangle of D(O_X) to a distinguished triangle: the two morphisms RSheafHom(T.obj₃, E) ⟶ RSheafHom(T.obj₂, E) ⟶ RSheafHom(T.obj₁, E) induced by T.mor₂ and T.mor₁ extend by a connecting morphism to a distinguished triangle.

The order of the two morphisms is reversed, which is the contravariance of the first variable.

theorem exists_distinguished_derivedSheafHom_first
    (E : DerivedCategory (StructureSheafModules Rc))
    (T : Triangle (DerivedCategory (StructureSheafModules Rc)))
    (hT : T ∈ distTriang (DerivedCategory (StructureSheafModules Rc))) :
    ∃ δ : ((derivedSheafHom Rc).flip.obj E).obj (op T.obj₁) ⟶
        (((derivedSheafHom Rc).flip.obj E).obj (op T.obj₃))⟦(1 : ℤ)⟧,
      Triangle.mk
        (((derivedSheafHom Rc).flip.obj E).map T.mor₂.op)
        (((derivedSheafHom Rc).flip.obj E).map T.mor₁.op)
        δ ∈ distTriang (DerivedCategory (StructureSheafModules Rc))

Stacks.SheafOfModules.exists_distinguished_derivedSheafHom_second, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedSheafHomExactness.lean, line 124. The attribute's comment: “exactness in the target”.

Stacks 08I0, exactness in the target. On a ringed space, the derived internal hom out of a fixed object carries a distinguished triangle of D(O_X) to a distinguished triangle: the two morphisms RSheafHom(E, T.obj₁) ⟶ RSheafHom(E, T.obj₂) ⟶ RSheafHom(E, T.obj₃) induced by T.mor₁ and T.mor₂ extend by a connecting morphism to a distinguished triangle.

theorem exists_distinguished_derivedSheafHom_second
    (E : DerivedCategory (StructureSheafModules Rc))
    (T : Triangle (DerivedCategory (StructureSheafModules Rc)))
    (hT : T ∈ distTriang (DerivedCategory (StructureSheafModules Rc))) :
    ∃ δ : ((derivedSheafHom Rc).obj (op E)).obj T.obj₃ ⟶
        (((derivedSheafHom Rc).obj (op E)).obj T.obj₁)⟦(1 : ℤ)⟧,
      Triangle.mk
        (((derivedSheafHom Rc).obj (op E)).map T.mor₁)
        (((derivedSheafHom Rc).obj (op E)).map T.mor₂)
        δ ∈ distTriang (DerivedCategory (StructureSheafModules Rc))
Tag 0A8V, a lemma

Tag 0A8V in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomComposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedComposition.lean, line 100. The attribute's comment: “the canonical composition morphism”.

For objects K, L, M of D(O_X) on a ringed space, the canonical composition morphism

RSheafHom(L, M) ⊗^L_{O_X} RSheafHom(K, L) ⟶ RSheafHom(K, M)

in D(O_X), obtained from the composition morphism of internal Hom complexes after passing to K-injective representatives of L and M and a K-flat model of the internal Hom complex into the representative of L.

def derivedSheafHomComposition
    (K L M : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))) :
    ((derivedTensor Rc).obj (((derivedSheafHom Rc).obj (op L)).obj M)).obj
        (((derivedSheafHom Rc).obj (op K)).obj L) ⟶
      ((derivedSheafHom Rc).obj (op K)).obj M

Stacks.SheafOfModules.derivedSheafHomComposition_natural_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedComposition.lean, line 110. The attribute's comment: “functoriality in the source”.

Derived composition is contravariant in the source object.

theorem derivedSheafHomComposition_natural_source
    {K K' : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))}
    (k : K' ⟶ K)
    (L M : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))) :
    derivedSheafHomComposition Rc K L M ≫ derivedSheafHomMap Rc k (𝟙 M) =
      derivedTensorMap Rc (𝟙 (((derivedSheafHom Rc).obj (op L)).obj M))
          (derivedSheafHomMap Rc k (𝟙 L)) ≫
        derivedSheafHomComposition Rc K' L M

Stacks.SheafOfModules.derivedSheafHomComposition_natural_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedComposition.lean, line 123. The attribute's comment: “functoriality in the target”.

Derived composition is covariant in the target object.

theorem derivedSheafHomComposition_natural_target
    (K L : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc)))
    {M M' : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))}
    (m : M ⟶ M') :
    derivedSheafHomComposition Rc K L M ≫ derivedSheafHomMap Rc (𝟙 K) m =
      derivedTensorMap Rc (derivedSheafHomMap Rc (𝟙 L) m)
          (𝟙 (((derivedSheafHom Rc).obj (op K)).obj L)) ≫
        derivedSheafHomComposition Rc K L M'

Stacks.SheafOfModules.derivedSheafHomComposition_dinatural_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedComposition.lean, line 138. The attribute's comment: “functoriality in the intermediate object”.

Derived composition is dinatural in the intermediate object: a morphism L ⟶ L' may be absorbed covariantly into the left tensor factor or contravariantly into the right one, with the same result.

theorem derivedSheafHomComposition_dinatural_middle
    (K : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc)))
    {L L' : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))}
    (l : L ⟶ L')
    (M : DerivedCategory (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))) :
    derivedTensorMap Rc (𝟙 (((derivedSheafHom Rc).obj (op L')).obj M))
          (derivedSheafHomMap Rc (𝟙 K) l) ≫
        derivedSheafHomComposition Rc K L' M =
      derivedTensorMap Rc (derivedSheafHomMap Rc l (𝟙 M))
          (𝟙 (((derivedSheafHom Rc).obj (op K)).obj L)) ≫
        derivedSheafHomComposition Rc K L M

Stacks.SheafOfModules.derivedSheafHomComposition_kFlatModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedComposition.lean, line 157. The attribute's comment: “comparison with composition of complexes”.

On K-injective representatives J of L and I of M and any map f from a K-flat complex H to the internal Hom complex SheafHom^•(K, J), derived composition is the class of the composition morphism of internal Hom complexes Tot(SheafHom^•(J, I) ⊗_{O_X} SheafHom^•(K, J)) ⟶ SheafHom^•(K, I).

theorem derivedSheafHomComposition_kFlatModel
    (K J I H : CochainComplex (_root_.SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc)) ℤ)
    [hJ : J.IsKInjective] [hI : I.IsKInjective] (hH : IsKFlat Rc H)
    (f : H ⟶ (sheafHomComplex Rc K J).obj) :
    ((derivedTensor Rc).obj
            (((derivedSheafHom Rc).obj (op (DerivedCategory.Q.obj J))).obj
              (DerivedCategory.Q.obj I))).map
          (DerivedCategory.Q.map f ≫
            (@RingedSite.derivedSheafHomComparison (ringedSite Rc) _ K J hJ).inv) ≫
        derivedSheafHomComposition Rc (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj J)
          (DerivedCategory.Q.obj I) ≫
        (@RingedSite.derivedSheafHomComparison (ringedSite Rc) _ K I hI).hom =
      (RingedSite.derivedEvaluationSourceComparison (ringedSite Rc)
            (canonicalDerivedTensorProduct (ringedSite Rc)) (derivedInternalHom Rc)
            H J I hH).hom ≫
        DerivedCategory.Q.map (tensorTotalMap Rc (𝟙 (sheafHomComplex Rc J I).obj) f) ≫
        DerivedCategory.Q.map (RingedSite.compositionMap (ringedSite Rc) K J I)
Tag 0BYS, a lemma

Tag 0BYS in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedTensorHomDiagonal_natural_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 519. The attribute's comment: “functoriality in the source of the internal Hom”.

Stacks 0BYS. The diagonal morphism is contravariant in the source of the internal Hom, for an arbitrary morphism of D(O).

theorem derivedTensorHomDiagonal_natural_hom (g : M' ⟶ M) :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).map
          (((derivedSheafHomBifunctor X).map g.op).app L) ≫
        derivedTensorHomDiagonal X K L M' =
      derivedTensorHomDiagonal X K L M ≫
        ((derivedSheafHomBifunctor X).map g.op).app
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).obj L)

AlgebraicGeometry.RingedSite.derivedTensorHomDiagonal_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 684. The attribute's comment: “functoriality in the target of the internal Hom”.

Stacks 0BYS. The diagonal morphism is covariant in the target of the internal Hom, for an arbitrary morphism of D(O).

theorem derivedTensorHomDiagonal_natural_right (g : L ⟶ L') :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).map
          (((derivedSheafHomBifunctor X).obj (op M)).map g) ≫
        derivedTensorHomDiagonal X K L' M =
      derivedTensorHomDiagonal X K L M ≫
        ((derivedSheafHomBifunctor X).obj (op M)).map
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).obj K).map g)

AlgebraicGeometry.RingedSite.derivedTensorHomDiagonal_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 930. The attribute's comment: “functoriality in the tensor factor”.

Stacks 0BYS. The diagonal morphism is covariant in the tensor factor, for an arbitrary morphism of D(O).

A morphism of D(O) does not lift to the chosen K-flat representatives, which are not K-injective. It is instead written as a right fraction inv (Q s₀) ≫ Q g₀ (DerivedCategory.right_fac) and the apex of that roof is replaced by a K-flat resolution of it (Stacks 06YS), giving a roof A ⟵ P ⟶ A' with all three complexes K-flat and the left leg invertible in D(O). The one-sided K-flat comparison of Stacks 06YU is then available at all three vertices, which makes the tensored left leg invertible with no K-flatness of the other factor, and the square closes from the complex-level functoriality of Stacks 0BYR.

theorem derivedTensorHomDiagonal_natural_left (f : K ⟶ K') :
    ((Stacks.SheafOfModules.derivedTensorProductFunctor X).map f).app
          (((derivedSheafHomBifunctor X).obj (op M)).obj L) ≫
        derivedTensorHomDiagonal X K' L M =
      derivedTensorHomDiagonal X K L M ≫
        ((derivedSheafHomBifunctor X).obj (op M)).map
          (((Stacks.SheafOfModules.derivedTensorProductFunctor X).map f).app L)

Stacks.SheafOfModules.canonicalDerivedTensorHomDiagonal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 1085. The attribute's comment: “the canonical morphism”.

Stacks 0BYS. The canonical morphism

K ⊗^L_{O_X} RSheafHom(M, L) ⟶ RSheafHom(M, K ⊗^L_{O_X} L)

in D(O_X) for objects K, L, M of the derived category of a ringed space.

def canonicalDerivedTensorHomDiagonal : DerivedTensorHomDiagonal Rc

Stacks.SheafOfModules.derivedTensorHomDiagonal_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 1100. The attribute's comment: “the characterisation on representatives”.

Stacks 0BYS. The canonical morphism is the class of the complex-level morphism of Stacks 0BYR between the chosen representatives, read through the K-flat and K-injective comparisons.

theorem derivedTensorHomDiagonal_eq (K L M : DerivedCategory (StructureSheafModules Rc)) :
    (RingedSite.derivedTensorHomSourceIso (ringedSite Rc) K L M).inv ≫
        derivedTensorHomDiagonal Rc K L M ≫
        (RingedSite.derivedTensorHomTargetIso (ringedSite Rc) K L M).hom =
      DerivedCategory.Q.map
        (RingedSite.derivedTensorHomModelMap (ringedSite Rc) K L M)

Stacks.SheafOfModules.derivedTensorHomDiagonal_natural_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 1111. The attribute's comment: “functoriality in the source of the internal Hom”.

Stacks 0BYS. The canonical morphism is contravariant in the source M of the internal Hom, for an arbitrary morphism of D(O_X).

theorem derivedTensorHomDiagonal_natural_hom
    (K L : DerivedCategory (StructureSheafModules Rc))
    {M M' : DerivedCategory (StructureSheafModules Rc)} (g : M' ⟶ M) :
    ((derivedTensorProductFunctor (ringedSite Rc)).obj K).map
          (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).map g.op).app L) ≫
        derivedTensorHomDiagonal Rc K L M' =
      derivedTensorHomDiagonal Rc K L M ≫
        ((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).map g.op).app
          (((derivedTensorProductFunctor (ringedSite Rc)).obj K).obj L)

Stacks.SheafOfModules.derivedTensorHomDiagonal_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 1125. The attribute's comment: “functoriality in the tensor factor”.

Stacks 0BYS. The canonical morphism is covariant in the tensor factor K, for an arbitrary morphism of D(O_X).

theorem derivedTensorHomDiagonal_natural_left
    {K K' : DerivedCategory (StructureSheafModules Rc)}
    (L M : DerivedCategory (StructureSheafModules Rc)) (f : K ⟶ K') :
    ((derivedTensorProductFunctor (ringedSite Rc)).map f).app
          (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op M)).obj L) ≫
        derivedTensorHomDiagonal Rc K' L M =
      derivedTensorHomDiagonal Rc K L M ≫
        ((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op M)).map
          (((derivedTensorProductFunctor (ringedSite Rc)).map f).app L)

Stacks.SheafOfModules.derivedTensorHomDiagonal_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomDiagonal.lean, line 1139. The attribute's comment: “functoriality in the target of the internal Hom”.

Stacks 0BYS. The canonical morphism is covariant in the target L of the internal Hom, for an arbitrary morphism of D(O_X).

theorem derivedTensorHomDiagonal_natural_right
    (K : DerivedCategory (StructureSheafModules Rc))
    {L L' : DerivedCategory (StructureSheafModules Rc)}
    (M : DerivedCategory (StructureSheafModules Rc)) (g : L ⟶ L') :
    ((derivedTensorProductFunctor (ringedSite Rc)).obj K).map
          (((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op M)).map g) ≫
        derivedTensorHomDiagonal Rc K L' M =
      derivedTensorHomDiagonal Rc K L M ≫
        ((RingedSite.derivedSheafHomBifunctor (ringedSite Rc)).obj (op M)).map
          (((derivedTensorProductFunctor (ringedSite Rc)).obj K).map g)
Tag 0A8W, a lemma

Tag 0A8W in the Stacks Project.

Stacks.SheafOfModules.derivedTensorHomUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomUnit.lean, line 226. The attribute's comment: “the canonical morphism, as the unit of Stacks 08DI”.

Stacks 0A8W. For objects K, L of D(O_X) on a ringed space, the canonical morphism

K ⟶ RSheafHom(L, K ⊗^L_{O_X} L)

in D(O_X): the morphism corresponding to the identity of K ⊗^L_{O_X} L under the tensor–internal-Hom bijection of Stacks 08DI.

def derivedTensorHomUnit (K L : DerivedCategory (StructureSheafModules Rc)) :
    K ⟶ ((derivedSheafHom Rc).obj (op L)).obj (((derivedTensor Rc).obj K).obj L)

Stacks.SheafOfModules.canonicalDerivedTensorHomUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomUnit.lean, line 265. The attribute's comment: “the canonical morphism, built as the source builds it”.

Stacks 0A8W. For objects K, L of D(O_X) on a ringed space, the canonical morphism

K ⟶ RSheafHom(L, K ⊗^L_{O_X} L)

in D(O_X), built the way the source builds it: on the chosen K-flat representative A of K and the chosen K-injective representative B of L it is the diagonal morphism of complexes of Stacks 0A93, A ⟶ SheafHom(B, Tot(A ⊗_{O_X} B)), followed by the augmentation of Tot(A ⊗_{O_X} B) into its chosen K-injective resolution, read through the comparisons identifying source and target with classes of complexes.

A ringed space is a ringed site, so this is the morphism of Stacks 0A99 read off along Stacks.SheafOfModules.ringedSite. It is the construction that carries the functoriality of the tag, in canonicalDerivedTensorHomUnit_natural_left and canonicalDerivedTensorHomUnit_natural_right below.

def canonicalDerivedTensorHomUnit (K L : DerivedCategory (StructureSheafModules Rc)) :
    K ⟶ ((derivedSheafHom Rc).obj (op L)).obj (((derivedTensor Rc).obj K).obj L)

Stacks.SheafOfModules.canonicalDerivedTensorHomUnit_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomUnit.lean, line 275. The attribute's comment: “the characterisation on representatives”.

Stacks 0A8W. The canonical morphism built the source's way is the class of the diagonal morphism of complexes of Stacks 0A93 followed by the K-injective resolution augmentation, read through the comparisons of its source and target with classes of complexes. This is the equation that pins the morphism down; in particular it is not an arbitrary morphism between the two objects.

theorem canonicalDerivedTensorHomUnit_eq (K L : DerivedCategory (StructureSheafModules Rc)) :
    (RingedSite.kFlatModelIso (ringedSite Rc) K).hom ≫
        canonicalDerivedTensorHomUnit Rc K L ≫
        (RingedSite.diagonalTargetIso (ringedSite Rc) K L L).hom =
      DerivedCategory.Q.map (RingedSite.diagonalComplexMap (ringedSite Rc)
        (RingedSite.kFlatModel (ringedSite Rc) K)
        (RingedSite.kInjectiveModel (ringedSite Rc) L))

Stacks.SheafOfModules.canonicalDerivedTensorHomUnit_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomUnit.lean, line 292. The attribute's comment: “functoriality in K”.

Stacks 0A8W: the canonical morphism is functorial in K. For a morphism k : K ⟶ K' of D(O_X) the square

k ≫ u_{K',L} = u_{K,L} ≫ RSheafHom(𝟙_L, k ⊗ 𝟙_L)

commutes in D(O_X): the first variable of the morphism acts covariantly, both on the source and inside the derived tensor product.

theorem canonicalDerivedTensorHomUnit_natural_left
    (L : DerivedCategory (StructureSheafModules Rc))
    {K K' : DerivedCategory (StructureSheafModules Rc)} (k : K ⟶ K') :
    k ≫ canonicalDerivedTensorHomUnit Rc K' L =
      canonicalDerivedTensorHomUnit Rc K L ≫
        ((derivedSheafHom Rc).obj (op L)).map (((derivedTensor Rc).map k).app L)

Stacks.SheafOfModules.canonicalDerivedTensorHomUnit_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorHomUnit.lean, line 309. The attribute's comment: “functoriality in L”.

Stacks 0A8W: the canonical morphism is functorial in L. For a morphism l : L' ⟶ L of D(O_X) the square

u_{K,L} ≫ RSheafHom(l, 𝟙) = u_{K,L'} ≫ RSheafHom(𝟙_{L'}, 𝟙_K ⊗ l)

commutes in D(O_X): the second variable acts contravariantly in the source of the internal Hom and covariantly inside the derived tensor product, which is the dinaturality that the statement of the tag asserts.

theorem canonicalDerivedTensorHomUnit_natural_right
    (K : DerivedCategory (StructureSheafModules Rc))
    {L L' : DerivedCategory (StructureSheafModules Rc)} (l : L' ⟶ L) :
    canonicalDerivedTensorHomUnit Rc K L ≫
        ((derivedSheafHom Rc).map l.op).app (((derivedTensor Rc).obj K).obj L) =
      canonicalDerivedTensorHomUnit Rc K L' ≫
        ((derivedSheafHom Rc).obj (op L')).map (((derivedTensor Rc).obj K).map l)
Tag 08I1, a lemma

Tag 08I1 in the Stacks Project.

Stacks.SheafOfModules.derivedTensorDualToSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorDual.lean, line 155. The attribute's comment: “the canonical map”.

Stacks 08I1: the canonical map M ⊗^L_{O_X} L^∨ ⟶ RSheafHom(L, M). It is the derived composition morphism of Stacks 0A8V, taken at intermediate object the structure sheaf, after the left tensor factor M has been identified with RSheafHom(O_X, M).

def derivedTensorDualToSheafHom
    (L M : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))) :
    ((derivedTensor Rc).obj M).obj (derivedDual Rc L) ⟶
      ((derivedSheafHom Rc).obj (op L)).obj M

Stacks.SheafOfModules.derivedTensorDualToSheafHom_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorDual.lean, line 181. The attribute's comment: “functoriality in M of the canonical map”.

The canonical map of Stacks 08I1 is functorial in M. This is the covariant naturality of the derived composition morphism of Stacks 0A8V in its target, together with the naturality of the identification of M with RSheafHom(O_X, M).

theorem derivedTensorDualToSheafHom_naturality
    (L : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc)))
    {M M' : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))} (m : M ⟶ M') :
    ((derivedTensor Rc).map m).app (derivedDual Rc L) ≫
        derivedTensorDualToSheafHom Rc L M' =
      derivedTensorDualToSheafHom Rc L M ≫ ((derivedSheafHom Rc).obj (op L)).map m

Stacks.SheafOfModules.derivedTensorDualToSheafHom_naturality_tensorMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorDual.lean, line 194. The attribute's comment: “functoriality in M of the canonical map”.

Functoriality in M of the canonical map of Stacks 08I1, in the derivedTensorMap and derivedSheafHomMap spelling of the induced maps on the derived tensor product and the derived internal Hom.

theorem derivedTensorDualToSheafHom_naturality_tensorMap
    (L : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc)))
    {M M' : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))} (m : M ⟶ M') :
    derivedTensorMap Rc m (𝟙 (derivedDual Rc L)) ≫ derivedTensorDualToSheafHom Rc L M' =
      derivedTensorDualToSheafHom Rc L M ≫ derivedSheafHomMap Rc (𝟙 L) m

Stacks.SheafOfModules.derivedTensorDualGlobalSectionsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorDual.lean, line 255. The attribute's comment: “the induced map on degree-zero global cohomology”.

Stacks 08I1: the induced map on degree-zero global cohomology. The canonical map M ⊗^L_{O_X} L^∨ ⟶ RSheafHom(L, M) induces a map of abelian groups

H⁰(X, M ⊗^L_{O_X} L^∨) ⟶ Hom_{D(O_X)}(L, M),

namely its degree-zero global hypercohomology followed by the identification H⁰(X, RSheafHom(L, M)) ≅ Hom_{D(O_X)}(L, M) of Stacks 08DK.

def derivedTensorDualGlobalSectionsMap
    (L M : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf.{u, u, u} Rc))) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((derivedModuleGlobalSections (ringedSite Rc)).obj
          (((derivedTensor Rc).obj M).obj (derivedDual Rc L))) : Type u) →+ (L ⟶ M)

Stacks.SheafOfModules.derivedTensorDualGlobalSectionsMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorDualGlobalFunctoriality.lean, line 143. The attribute's comment: “functoriality in M of the induced map on degree-zero global cohomology”.

Stacks 08I1: the induced map H⁰(X, M ⊗^L_{O_X} L^∨) ⟶ Hom_{D(O_X)}(L, M) is functorial in M. For m : M ⟶ M' the degree-zero global hypercohomology of m ⊗ 1 carries the induced map at M to the induced map at M' followed by postcomposition with m.

This is the ringed-site statement AlgebraicGeometry.RingedSite.derivedTensorDualGlobalSectionsMap_naturality, read along Stacks.SheafOfModules.ringedSite for the canonical derived tensor product.

theorem derivedTensorDualGlobalSectionsMap_naturality
    (L : DerivedCategory (StructureSheafModules Rc))
    {M M' : DerivedCategory (StructureSheafModules Rc)} (m : M ⟶ M')
    (z : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections (ringedSite Rc)).obj
        (((derivedTensor Rc).obj M).obj (derivedDual Rc L))) : Type u)) :
    derivedTensorDualGlobalSectionsMap Rc L M'
        ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
          ((derivedModuleGlobalSections (ringedSite Rc)).map
            (((derivedTensor Rc).map m).app (derivedDual Rc L))) z) =
      derivedTensorDualGlobalSectionsMap Rc L M z ≫ m

Stacks.SheafOfModules.derivedTensorDualGlobalSectionsMap_naturality_tensorMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorDualGlobalFunctoriality.lean, line 160. The attribute's comment: “functoriality in M of the induced map on degree-zero global cohomology”.

Functoriality in M of the induced map of Stacks 08I1, in the derivedTensorMap spelling of the map induced on the derived tensor product.

theorem derivedTensorDualGlobalSectionsMap_naturality_tensorMap
    (L : DerivedCategory (StructureSheafModules Rc))
    {M M' : DerivedCategory (StructureSheafModules Rc)} (m : M ⟶ M')
    (z : ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
      ((derivedModuleGlobalSections (ringedSite Rc)).obj
        (((derivedTensor Rc).obj M).obj (derivedDual Rc L))) : Type u)) :
    derivedTensorDualGlobalSectionsMap Rc L M'
        ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).map
          ((derivedModuleGlobalSections (ringedSite Rc)).map
            (derivedTensorMap Rc m (𝟙 (derivedDual Rc L)))) z) =
      derivedTensorDualGlobalSectionsMap Rc L M z ≫ m
Tag 0A8U, a lemma

Tag 0A8U in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomEvaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHomEvaluation/DerivedEvaluation.lean, line 91. The attribute's comment: “the canonical evaluation morphism”.

Stacks 0A8U. For objects K, L, M of D(O_X) on a ringed space there is a canonical evaluation morphism

RSheafHom(L, M) ⊗^L_{O_X} K ⟶ RSheafHom(RSheafHom(K, L), M)

in D(O_X), obtained from the evaluation morphism of internal Hom complexes after passing to a K-flat representative of K and K-injective representatives of L and M.

def derivedSheafHomEvaluation (K L M : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf Rc))) :
    ((derivedTensor Rc).obj (((derivedSheafHom Rc).obj (op L)).obj M)).obj K ⟶
      ((derivedSheafHom Rc).obj (op (((derivedSheafHom Rc).obj (op K)).obj L))).obj M

Stacks.SheafOfModules.derivedSheafHomEvaluation_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHomEvaluation/DerivedEvaluation.lean, line 101. The attribute's comment: “functoriality in all three objects”.

Stacks 0A8U. Derived evaluation is functorial in all three objects at once: covariant in the object being tensored, contravariant in the source of the inner internal hom, and covariant in its target.

theorem derivedSheafHomEvaluation_natural
    {K K' L L' M M' : DerivedCategory (SheafOfModules.{u} (Tensor.ringSheaf Rc))}
    (f : K ⟶ K') (g : L' ⟶ L) (h : M ⟶ M') :
    derivedTensorMap Rc (derivedSheafHomMap Rc g h) f ≫
        derivedSheafHomEvaluation Rc K' L' M' =
      derivedSheafHomEvaluation Rc K L M ≫
        derivedSheafHomMap Rc (derivedSheafHomMap Rc f g) h

Stacks.SheafOfModules.derivedSheafHomEvaluation_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHomEvaluation/DerivedEvaluation.lean, line 115. The attribute's comment: “comparison with evaluation of complexes”.

Stacks 0A8U. On a K-flat representative P of K and K-injective representatives J of L and I of M, derived evaluation is the class of the evaluation morphism of internal Hom complexes Tot(SheafHom^•(J, I) ⊗_{O_X} P) ⟶ SheafHom^•(SheafHom^•(P, J), I).

theorem derivedSheafHomEvaluation_model
    (P J I : CochainComplex (SheafOfModules.{u} (Tensor.ringSheaf Rc)) ℤ)
    (hP : IsKFlat Rc P) [J.IsKInjective] [I.IsKInjective] :
    derivedSheafHomEvaluation Rc (DerivedCategory.Q.obj P) (DerivedCategory.Q.obj J)
          (DerivedCategory.Q.obj I) ≫
        (RingedSite.derivedEvaluationTargetComparison (ringedSite Rc)
          (derivedInternalHom Rc) P J I).hom =
      (RingedSite.derivedEvaluationSourceComparison (ringedSite Rc)
          (canonicalDerivedTensorProduct (ringedSite Rc)) (derivedInternalHom Rc)
          P J I hP).hom ≫
        DerivedCategory.Q.map (RingedSite.evaluationMap (ringedSite Rc) P J I)
Tag 0FXP, a remark

Tag 0FXP in the Stacks Project.

Stacks.SheafOfModules.derivedSheafHomTensorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/DerivedTensorInternalHom.lean, line 177.

Stacks 0FXP. For objects K, K', M, M' of D(O_X) on a ringed space there is a canonical morphism

RSheafHom(K, K') ⊗^L_{O_X} RSheafHom(M, M') ⟶ RSheafHom(K ⊗^L_{O_X} M, K' ⊗^L_{O_X} M'),

the morphism adjoint under Stacks 08DI to the interchange of the two middle factors of RSheafHom(K, K') ⊗^L RSheafHom(M, M') ⊗^L K ⊗^L M followed by evaluation of each internal hom.

def derivedSheafHomTensorMap (K K' M M' : DerivedCategory (StructureSheafModules Rc)) :
    ((derivedTensor Rc).obj (((derivedSheafHom Rc).obj (op K)).obj K')).obj
        (((derivedSheafHom Rc).obj (op M)).obj M') ⟶
      ((derivedSheafHom Rc).obj (op (((derivedTensor Rc).obj K).obj M))).obj
        (((derivedTensor Rc).obj K').obj M')
Tag 0B69, a remark

Tag 0B69 in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomPushforward.pushforwardSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomPushforwardMap.lean, line 113.

Stacks 0B69: the canonical map Rf_*R𝓗om_{𝒪_X}(L, K) ⟶ R𝓗om_{𝒪_Y}(Rf_*L, Rf_*K) for a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and objects K, L of D(𝒪_X).

By the tensor–internal-hom bijection of Stacks 08DI it is the same datum as a map Rf_*R𝓗om(L, K) ⊗^L_{𝒪_Y} Rf_*L ⟶ Rf_*K, and that datum is the relative cup product of Stacks 0B68 followed by the derived pushforward of the evaluation map.

def pushforwardSheafHomMap (K L : DerivedCategory (Mod X.sheaf)) :
    (derivedPushforward f).obj (sheafHomObj X L K) ⟶
      sheafHomObj Y ((derivedPushforward f).obj L) ((derivedPushforward f).obj K)
Tag 0G7A, a remark

Tag 0G7A in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomEvaluation.tensorMap_pushforwardSheafHomMap_sheafHomEval, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomEvaluationSquare.lean, line 262. The attribute's comment: “the square commutes, for every morphism of ringed spaces f and all K, M; this is the whole of the remark. The source states it for K, M ∈ D(𝒪_Y), which is a slip — the diagram applies both R𝓗om_{𝒪_X} and Rf_* to K and M, so the arrows type-check only for K, M ∈ D(𝒪_X), and that is the form here”.

Stacks 0G7A. For a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and objects K, M of D(𝒪_X) the square

Rf_*R𝓗om_{𝒪_X}(K, M) ⊗^L_{𝒪_Y} Rf_*K ⟶ Rf_*(R𝓗om_{𝒪_X}(K, M) ⊗^L_{𝒪_X} K) ⟶ Rf_*M, Rf_*R𝓗om_{𝒪_X}(K, M) ⊗^L_{𝒪_Y} Rf_*K ⟶ R𝓗om_{𝒪_Y}(Rf_*K, Rf_*M) ⊗^L_{𝒪_Y} Rf_*K ⟶ Rf_*M

commutes: the map of Stacks 0B69 tensored with the identity of Rf_*K followed by the evaluation on Y agrees with the relative cup product of Stacks 0B68 followed by the derived pushforward of the evaluation on X.

That the bijection of Stacks 08DI on Y evaluates, which is the content of the square, is tensorEquivIsEvaluation.

theorem tensorMap_pushforwardSheafHomMap_sheafHomEval
    (K M : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf))) :
    tensorMap Y (pushforwardSheafHomMap f M K) (𝟙 ((derivedPushforward f).obj K)) ≫
        sheafHomEval Y ((derivedPushforward f).obj K) ((derivedPushforward f).obj M) =
      Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct f (sheafHomObj X K M) K ≫
        (derivedPushforward f).map (sheafHomEval X K M)
Tag 08I3, a remark

Tag 08I3 in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomPullback.derivedPullbackSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomPullbackMap.lean, line 376.

Tag 08I3: the canonical map Lh^*R𝓗om(K, L) ⟶ R𝓗om(Lh^*K, Lh^*L) for a morphism of ringed spaces h : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and objects K, L of D(𝒪_Y).

By the tensor–internal-hom bijection of Tag 08DI it is the same datum as a map Lh^*R𝓗om(K,L) ⊗^L_{𝒪_X} Lh^*K ⟶ Lh^*L, and that is the derived pullback of the evaluation R𝓗om(K,L) ⊗^L_{𝒪_Y} K ⟶ L preceded by the monoidality comparison of Tag 079U.

def derivedPullbackSheafHomMap :
    (derivedPullbackFunctor h).obj
        (((Stacks.SheafOfModules.derivedSheafHom Y.sheaf).obj (op K)).obj L) ⟶
      ((Stacks.SheafOfModules.derivedSheafHom X.sheaf).obj
          (op ((derivedPullbackFunctor h).obj K))).obj
        ((derivedPullbackFunctor h).obj L)
Tag 08I4, a remark

Tag 08I4 in the Stacks Project.

Stacks.Cohomology.DerivedInternalHomBaseChange.derivedBaseChangeSheafHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/InternalHomBaseChange.lean, line 116.

Tag 08I4: the base change map for a derived internal hom. For a commutative square of ringed spaces with h : X' ⟶ X over g : S' ⟶ S and objects K, L of D(𝒪_X), the canonical map

Lg^* Rf_* R𝓗om_{𝒪_X}(K, L) ⟶ R(f')_* R𝓗om_{𝒪_{X'}}(Lh^*K, Lh^*L)

in D(𝒪_{S'}). It is the derived base change map of Tag 08HY at R𝓗om_{𝒪_X}(K, L) followed by R(f')_* of the canonical map of Tag 08I3, which is the adjoint of the three-step composition the source describes.

def derivedBaseChangeSheafHomMap :
    (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj
          (((Stacks.SheafOfModules.derivedSheafHom X.sheaf).obj (op K)).obj L)) ⟶
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f').obj
        (((Stacks.SheafOfModules.derivedSheafHom X'.sheaf).obj
            (op ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback h).obj
              K))).obj
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback h).obj L))
Sources
LeanStacks.SheafOfModules.derivedSheafHomTensorEquiv · Stacks.SheafOfModules.derivedSheafHomGlobalSectionsEquiv · Stacks.SheafOfModules.derivedSheafHomSectionsEquiv · Stacks.SheafOfModules.derivedCurryingData · Stacks.SheafOfModules.derivedSheafHomRestrictionIso · Stacks.SheafOfModules.derivedSheafHomRestrictionIso_natural_left · Stacks.SheafOfModules.derivedSheafHomRestrictionIso_natural_right · Stacks.SheafOfModules.sheafHomRestrictionComplexMap_isRestriction

Section20.43 Ext sheaves#

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

Tag 0BQP, the section

Tag 0BQP in the Stacks Project.

Stacks.SheafOfModules.derivedSheafExt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/ExtSheaves.lean, line 127. The attribute's comment: “the definition of the Ext sheaves: SheafExt^n(K, L) is the n-th cohomology sheaf of RSheafHom(K, L), for K and L objects of D(O_X) and n an integer”. References: EGA 0 (12.3.1), “more general”; SGA 4 V (6.0), “special case”.

The Ext sheaves. For objects K, L of D(O_X) and an integer n, the Ext sheaf SheafExt^n(K, L) is the degree-n cohomology sheaf of the derived internal Hom RSheafHom(K, L), an O_X-module.

abbrev derivedSheafExt (K L : DerivedCategory (StructureSheafModules Rc)) (n : ℤ) :
    StructureSheafModules Rc

Stacks.SheafOfModules.derivedSheafExtFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/ExtSheaves.lean, line 137. The attribute's comment: “the Ext sheaves are functorial in both variables, contravariantly in the first”. References: EGA 0 (12.3.1), “more general”; SGA 4 V (6.0), “6.0.1, special case”.

The Ext sheaves as a bifunctor. SheafExt^n(-, -) is a functor of both variables, contravariant in the first: it is the derived internal Hom followed by the degree-n cohomology sheaf.

def derivedSheafExtFunctor (n : ℤ) :
    (DerivedCategory (StructureSheafModules Rc))ᵒᵖ ⥤
      DerivedCategory (StructureSheafModules Rc) ⥤ StructureSheafModules Rc

Stacks.SheafOfModules.derivedSheafExtIsoSheafifyPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/ExtSheaves.lean, line 181. The attribute's comment: “the Ext sheaf is the sheafification of the presheaf of degree-n hypercohomology of RSheafHom(K, L) on the opens of X; the identification of that presheaf's values with the Ext groups Ext^n(K|_U, L|_U) is Tag 08DK and is cited, not composed in here”.

The Ext sheaf is a sheafification. SheafExt^n(K, L) is the sheaf of O_X-modules associated to the presheaf of degree-n hypercohomology of RSheafHom(K, L), whose value over an open U is Ext^n_{D(O_U)}(K|_U, L|_U) by [Stacks, Tag 08DK].

This is [Stacks, Tag 0BKJ] — a cohomology sheaf is the sheafification of the cohomology presheaf — read at RSheafHom(K, L).

def derivedSheafExtIsoSheafifyPresheaf (K L : DerivedCategory (StructureSheafModules Rc))
    (n : ℤ) :
    (PresheafOfModules.sheafification (𝟙 (structureSheaf Rc).obj)).obj
        (derivedSheafExtPresheaf Rc K L n) ≅ derivedSheafExt Rc K L n

Stacks.SheafOfModules.hypercohomologySpectralSequence_e₂_derivedSheafExt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/ExtSheaves.lean, line 222. The attribute's comment: “the second page of the local-to-global spectral sequence of Ext: the Tag 0BKM hypercohomology spectral sequence of RSheafHom(K, L) has E_2^{p, q} = H^p(X, SheafExt^q(K, L)); convergence to Ext^{p+q}(K, L) is not claimed here -- the Tag 0BKM convergence clause needs a bounded below complex representing RSheafHom(K, L) and is stated of an existentially produced spectral sequence rather than of the canonical one carrying this second page, and the Ext reading of the abutment is Tag 08DK”. References: SGA 7 VIII (1.1), “partial”.

The second page of the local-to-global spectral sequence of Ext. The hypercohomology spectral sequence of [Stacks, Tag 0BKM] applied to RSheafHom(K, L) has second page

E_2^{p, q} = H^p(X, SheafExt^q(K, L)),

the hypercohomology of the Ext sheaves. Its abutment is H^{p + q}(X, RSheafHom(K, L)), which is Ext^{p + q}_{D(O_X)}(K, L) by [Stacks, Tag 08DK].

theorem hypercohomologySpectralSequence_e₂_derivedSheafExt
    (K L : DerivedCategory (_root_.SheafOfModules.{u} (structureSheafRing Y))) (p q : ℤ) :
    Nonempty ((((hypercohomologySpectralSequence Y
          (((derivedSheafHom Y.sheaf).obj (op K)).obj L)).spectralSequence.page 2).X (p, q)) ≅
      (DerivedCategory.homologyFunctor
          (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op ⊤))) p).obj
        ((hypercohomologySpectralSequence Y
            (((derivedSheafHom Y.sheaf).obj (op K)).obj L)).truncation.RΓ.obj
          ((DerivedCategory.singleFunctor (_root_.SheafOfModules.{u} (structureSheafRing Y)) 0).obj
            (derivedSheafExt Y.sheaf K L q))))
Sources
LeanStacks.SheafOfModules.derivedSheafExt · Stacks.SheafOfModules.derivedSheafExtFunctor · Stacks.SheafOfModules.derivedSheafExtIsoSheafifyPresheaf · Stacks.SheafOfModules.hypercohomologySpectralSequence_e₂_derivedSheafExt

Section20.44 Global derived hom#

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

Tag 0B6A, the section

Tag 0B6A in the Stacks Project.

Stacks.SheafOfModules.globalDerivedHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/GlobalDerivedHomOnASpace.lean, line 52. The attribute's comment: “the global derived hom RHom_X(K, L) = RΓ(X, RSheafHom(K, L)) in D(Γ(X, O_X)) of a ringed space”.

The global derived hom RHom_X(K, L) = RΓ(X, RSheafHom(K, L)) of a ringed space: the derived internal Hom of two objects of D(O_X), followed by derived global sections valued in modules over the ring Γ(X, O_X) of global sections of the structure sheaf.

def globalDerivedHom :
    (DerivedCategory (StructureSheafModules Rc))ᵒᵖ ⥤
      DerivedCategory (StructureSheafModules Rc) ⥤
        DerivedCategory (ModuleCat.{u} (GlobalSectionRing (structureSheaf Rc)))

Stacks.SheafOfModules.globalDerivedHomDegreeZeroEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/InternalHom/GlobalDerivedHomOnASpace.lean, line 69. The attribute's comment: “the degree-zero cohomology of RHom_X(K, L) is Hom_{D(O_X)}(K, L)”.

The degree-zero cohomology of RHom_X(K, L), read on its underlying complex of abelian groups, is the group of morphisms K ⟶ L in the derived category of O_X-modules.

def globalDerivedHomDegreeZeroEquiv (K L : DerivedCategory (StructureSheafModules Rc)) :
    ((DerivedCategory.homologyFunctor AddCommGrpCat.{u} 0).obj
        ((RingedSite.underlyingDerivedGroup (ringedSite Rc)).obj
          (((globalDerivedHom Rc).obj (op K)).obj L)) : Type u) ≃+ (K ⟶ L)
Sources
LeanStacks.SheafOfModules.globalDerivedHom · Stacks.SheafOfModules.globalDerivedHomDegreeZeroEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.