20.55 An operator introduced by…

Section20.55 An operator introduced by Berthelot and Ogus#

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

Tag 0GT3, a lemma

Tag 0GT3 in the Stacks Project.

Stacks.IdealTorsion.isInvertible_of_isLocallyGeneratedByRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/IdealGeneratedByNonzerodivisor.lean, line 209. The attribute's comment: “(1) implies (2)”.

Condition (1) of Stacks 0GT3 implies condition (2). An ideal sheaf locally generated by a nonzerodivisor is invertible as an O_X-module. There is no hypothesis on the stalks of the structure sheaf: this half of the tag holds on every ringed space.

public theorem isInvertible_of_isLocallyGeneratedByRegular
    {I : SheafOfModules.{u} Oₓ} (i : I ⟶ 𝒪) (h : IsLocallyGeneratedByRegular X i) :
    Stacks.SheafOfModules.IsInvertible X.presheaf (structureSheafRing X).property I

Stacks.IdealTorsion.isLocallyGeneratedByRegular_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/IdealGeneratedByNonzerodivisor.lean, line 221. The attribute's comment: “(2) implies (1) when the stalks are local rings”.

Condition (2) of Stacks 0GT3 implies condition (1) when the stalks are local rings. An invertible ideal sheaf on a ringed space all of whose stalks O_{X,x} are local rings is locally generated by a nonzerodivisor. The hypothesis on the stalks is the one the tag requires and cannot be dropped: without it an invertible module need not be locally free of rank one.

public theorem isLocallyGeneratedByRegular_of_isInvertible
    [∀ x : X.carrier, IsLocalRing (ringStalk X x)]
    {I : SheafOfModules.{u} Oₓ} (i : I ⟶ 𝒪) [Mono i]
    (h : Stacks.SheafOfModules.IsInvertible X.presheaf (structureSheafRing X).property I) :
    IsLocallyGeneratedByRegular X i
Tag 0GT4, a situation

Tag 0GT4 in the Stacks Project.

Stacks.IdealTorsion.Eta.Situation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafCohomology.lean, line 135.

Situation 0GT4. A sheaf of ideals ι : I ⟶ O_X on a ringed space which is locally generated by a nonzerodivisor: every point has an open neighbourhood U carrying a section f of I which generates I|_U and acts injectively on O_U.

public structure Situation
Tag 0GT5, a lemma

Tag 0GT5 in the Stacks Project.

Stacks.IdealTorsion.idealTorsionFree_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/IdealTorsionFree.lean, line 1350.

Stacks Project, Tag 0GT5. For an ideal sheaf locally generated by a nonzerodivisor, the following are equivalent: F[I] = 0; F[I^n] = 0 for every n ≥ 1; multiplication I ⊗ F ⟶ F is injective; multiplication by every local generator is injective; and every stalk generator is a nonzerodivisor on the stalk of F.

public theorem idealTorsionFree_tfae
    {I : SheafOfModules.{u} Oₓ} (i : I ⟶ 𝒪) [Mono i]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank (C := Opens X)
      (J := Opens.grothendieckTopology X) I 1]
    (F : SheafOfModules.{u} Oₓ) :
    List.TFAE [
      IsIdealTorsionFree X i F,
      IsIdealPowerTorsionFree X i F,
      Mono (idealTensorMultiplication X i F),
      ∀ (U : Opens X) (f : I.val.obj (op U)),
        GeneratesIdealOn X U f → IsGeneratorRegularOn X i F U f,
      IsStalkwiseGeneratorRegular X i F]
Tag 0GT6, a lemma

Tag 0GT6 in the Stacks Project.

Stacks.IdealTorsion.Eta.etaStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheaf.lean, line 2281.

Stacks Project, Tag 0GT6. At a generator f of the ideal stalk I_x, the stalk of the sheaf-theoretic décalage η_I F is isomorphic, as a complex of modules over the local ring O_{X,x}, to the ordinary décalage η_f of the complex of stalks.

public noncomputable def etaStalkIso
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (CategoryTheory.ObjectProperty.FullSubcategory.mk X.presheaf X.IsSheaf))).property I]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n))
    (x : X) (f : ringStalk X x)
    (hf : GeneratesStalkIdeal X ι x f) :
    stalkComplex X x (etaObj X I ι F hF) ≅
      EtaComplex.etaObject f (stalkComplex X x F)

Stacks.IdealTorsion.Eta.etaStalkIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheaf.lean, line 2300. The attribute's comment: “generator-normalized degreewise map”.

In degree n, the comparison of Tag 0GT6 is the normalized ideal-power map applied to the first projection of the defining fibre product, read inside the localization.

public theorem etaStalkIso_hom
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (CategoryTheory.ObjectProperty.FullSubcategory.mk X.presheaf X.IsSheaf))).property I]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n))
    (x : X) (f : ringStalk X x)
    (hf : GeneratesStalkIdeal X ι x f) (n : ℤ) :
    (etaStalkIso X I ι F hF x f hf).hom.f n ≫
      ModuleCat.ofHom (Submodule.subtype (EtaComplex.term f (stalkComplex X x F) n)) =
    (stalkModuleFunctor X x).map
      (pullback.fst (idealPowerMap X I n (F.d n (n + 1)))
        (idealPowerIncl X I ι n (F.X (n + 1)))) ≫
      (idealPowerStalkComparison X I ι (F.X n) x f hf).map n
Tag 0F8N, a lemma

Tag 0F8N in the Stacks Project.

Stacks.IdealTorsion.Eta.etaCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafCohomology.lean, line 1351.

Stacks Project, Tag 0F8N. In Situation 0GT4, for a complex F of I-torsion-free O_X-modules there is a canonical isomorphism I^{⊗ n} ⊗ (H^n(F)/H^n(F)[I]) ≅ H^n(η_I F) of cohomology sheaves, where H^n(F)[I] is the subsheaf of H^n(F) annihilated by I, realized as the ideal-power annihilator subsheaf of Tag 0GT5, and the quotient as the cokernel of its inclusion.

public noncomputable def etaCohomologyIso (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property I]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n))
    (n : ℤ) :
    idealPowerTerm X I n
        (cokernel (idealPowerAnnihilatorSubsheaf X ι (F.homology n) 1).ι) ≅
      (etaObj X I ι F hF).homology n

Stacks.IdealTorsion.Eta.etaCohomologyIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafCohomology.lean, line 1367. The attribute's comment: “the canonical comparison”.

Stacks Project, Tag 0F8N. The isomorphism of Tag 0F8N is the one the source writes down: precomposed with the twisted quotient map it is etaHomologyMap, which by etaHomologyMap_cycles and etaCyclesIso_hom_fst sends a twisted cocycle g ⊗ s to the class of the cocycle of η_I F with underlying section g s. Since the twisted quotient map is an epimorphism, this determines the isomorphism uniquely.

public theorem etaCohomologyIso_hom (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property I]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n))
    (n : ℤ) :
    idealPowerMap X I n
        (cokernel.π (idealPowerAnnihilatorSubsheaf X ι (F.homology n) 1).ι) ≫
      (etaCohomologyIso X I ι F hF n).hom = etaHomologyMap X I ι F hF n
Tag 0F8P, a lemma

Tag 0F8P in the Stacks Project.

Stacks.IdealTorsion.Eta.quasiIso_etaMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafQuasiIso.lean, line 411.

Stacks Project, Tag 0F8P. In Situation 0GT4, if a map a : F ⟶ G of complexes of I-torsion-free O_X-modules is a quasi-isomorphism, then so is the induced map η_I a : η_I F ⟶ η_I G of décalages.

public theorem quasiIso_etaMap (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj (Oₓ).property I]
    {F G : CochainComplex (SheafOfModules.{u} Oₓ) ℤ} (a : F ⟶ G)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n))
    (hG : ∀ n : ℤ, IsIdealTorsionFree X ι (G.X n))
    (ha : QuasiIso a) :
    QuasiIso (etaMap X I ι a hF hG)
Tag 0F8Q, a lemma

Tag 0F8Q in the Stacks Project.

Stacks.IdealTorsion.Eta.derivedEtaOfRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafDerived.lean, line 422.

Stacks Project, Tag 0F8Q. In Situation 0GT4 — I ⊂ O_X an ideal sheaf locally generated by a section that is a nonzerodivisor on O_X — there is an additive functor Lη_I : D(O_X) ⥤ D(O_X) whose value on an object represented by a complex F of I-torsion-free O_X-modules is the class of the décalage η_I F, and likewise on morphisms; derivedEtaOfRegular_iso records that comparison and derivedEtaOfRegular_additive the additivity. The functor is not exact: it does not take distinguished triangles to distinguished triangles, and no such statement is made here.

The termwise I-torsion-free resolutions on which the construction rests are supplied by hregl, not assumed. The form that assumes them, derivedEta, is the one to use for an ideal whose resolutions are available without local generation by a nonzerodivisor — as happens for the pullback of I along a morphism of ringed spaces, and in the comparison of two ideals.

public noncomputable def derivedEtaOfRegular (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    (hregl : IsLocallyGeneratedByRegular X ι) :
    DerivedCategory (SheafOfModules.{u} Oₓ) ⥤ DerivedCategory (SheafOfModules.{u} Oₓ)

Stacks.IdealTorsion.Eta.derivedEtaOfRegular_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafDerived.lean, line 433. The attribute's comment: “the comparison with the chain-level décalage”.

Stacks Project, Tag 0F8Q. In Situation 0GT4, on an object of D(O_X) represented by a complex F of I-torsion-free O_X-modules, and on morphisms of such complexes, the derived décalage is the class of the chain-level décalage η_I F. The form of this comparison that assumes the torsion-free resolutions is derivedEta_iso.

public noncomputable def derivedEtaOfRegular_iso (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪)
    [Mono ι] (hregl : IsLocallyGeneratedByRegular X ι) :
    letI := Stacks.IdealTorsion.isInvertible_of_isLocallyGeneratedByRegular X ι hregl
    torsionFreeToDerived X ι ⋙ derivedEtaOfRegular X I ι hregl ≅
      etaFunctor X I ι ⋙ DerivedCategory.Q

Stacks.IdealTorsion.Eta.derivedEtaOfRegular_additive, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafDerived.lean, line 444. The attribute's comment: “additivity”.

Stacks Project, Tag 0F8Q. In Situation 0GT4 the derived décalage is additive. The form of this statement that assumes the torsion-free resolutions is derivedEta_additive.

public instance derivedEtaOfRegular_additive (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    (hregl : IsLocallyGeneratedByRegular X ι) :
    (derivedEtaOfRegular X I ι hregl).Additive

Stacks.IdealTorsion.Eta.hasTorsionFreeResolutions_of_isLocallyGeneratedByRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafTorsionFreeResolutions.lean, line 65. The attribute's comment: “the existence of termwise I-torsion-free resolutions of unbounded complexes, the first step of the proof”.

Termwise I-torsion-free resolutions exist. For an ideal sheaf locally generated by a nonzerodivisor, every cochain complex of O_X-modules receives a quasi-isomorphism from a complex of I-torsion-free O_X-modules. This is the first step of the proof of [Stacks, Tag 0F8Q]: a resolution with flat terms exists by Tag 06YS, and a flat module is I-torsion free by the third criterion of Tag 0GT5.

public theorem hasTorsionFreeResolutions_of_isLocallyGeneratedByRegular
    (I : SheafOfModules.{u} (structureSheaf X.sheaf))
    (ι : I ⟶ SheafOfModules.unit (structureSheaf X.sheaf)) (hι : Mono ι)
    (hregl : Stacks.IdealTorsion.IsLocallyGeneratedByRegular X ι) :
    HasTorsionFreeResolutions X ι

Stacks.IdealTorsion.Eta.hasTorsionFreeResolutions_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafTorsionFreeResolutions.lean, line 82. The attribute's comment: “the existence of termwise I-torsion-free resolutions of unbounded complexes for an invertible ideal sheaf on a ringed space whose stalks are local rings”.

Termwise I-torsion-free resolutions exist for an invertible ideal sheaf. On a ringed space whose stalks are local rings an invertible ideal sheaf is locally generated by a nonzerodivisor, so every cochain complex of O_X-modules receives a quasi-isomorphism from a complex of I-torsion-free modules.

public theorem hasTorsionFreeResolutions_of_isInvertible
    [∀ x : X.carrier, IsLocalRing
      (Stacks.SheafOfModules.TensorStalkRingedSpace.ringStalk X x)]
    (I : SheafOfModules.{u} (structureSheaf X.sheaf))
    (ι : I ⟶ SheafOfModules.unit (structureSheaf X.sheaf)) (hι : Mono ι)
    (hI : Stacks.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X).property I) :
    HasTorsionFreeResolutions X ι

Stacks.Divisors.Eta.hasTorsionFreeResolutions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EtaDerivedUnconditional.lean, line 64. The attribute's comment: “the existence of termwise I-torsion-free resolutions for the ideal sheaf of an effective Cartier divisor on a scheme”.

Termwise I-torsion-free resolutions exist for an effective Cartier divisor. Every cochain complex of 𝒪_X-modules receives a quasi-isomorphism from a complex whose terms are annihilated by no nonzero section of the ideal sheaf: the ideal sheaf is invertible and the stalks of 𝒪_X are local rings.

theorem hasTorsionFreeResolutions (D : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor D] :
    HasTorsionFreeResolutions X.toRingedSpace (idealSheafι D)

Stacks.Divisors.Eta.derivedEtaData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EtaDerivedUnconditional.lean, line 77. The attribute's comment: “the functor, its comparison with the chain-level décalage and the representability of every object, for the ideal sheaf of an effective Cartier divisor on a scheme”.

Stacks Project, Tag 0F8Q, for an effective Cartier divisor on a scheme. The derived décalage Lη_I : D(𝒪_X) ⟶ D(𝒪_X), its identification with the chain-level décalage η_I on complexes of I-torsion-free 𝒪_X-modules, and the fact that every object of D(𝒪_X) is represented by such a complex.

def derivedEtaData (D : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor D] : DerivedEta D
Tag 0GT8, an equation

Tag 0GT8 in the Stacks Project.

Stacks.IdealTorsion.Bockstein.bockstein_comp_bockstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafBockstein.lean, line 397. The attribute's comment: “square-zero Bockstein maps”.

Stacks Project, Tag 0GT8. Consecutive Bockstein operators compose to zero, β^{i+1} ∘ β^i = 0.

public theorem bockstein_comp_bockstein
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj
      ((Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf)).property I]
    (M : DerivedCategory (SheafOfModules.{u} Oₓ)) (i : ℤ) :
    bocksteinOperator X I ι M i ≫ bocksteinOperator X I ι M (i + 1) = 0

Stacks.IdealTorsion.Bockstein.bocksteinComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafBockstein.lean, line 418. The attribute's comment: “the Bockstein complex”.

Stacks Project, Tag 0GT8. The Bockstein complex H^•(M/I) of an object M of D(O_X): the integer-indexed complex whose i-th term is H^i(M ⊗^L I^i/I^{i+1}) and whose differentials are the Bockstein operators.

public noncomputable def bocksteinComplex
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj
      ((Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf)).property I]
    (M : DerivedCategory (SheafOfModules.{u} Oₓ)) : CochainComplex (SheafOfModules.{u} Oₓ) ℤ
Tag 0GT9, a lemma

Tag 0GT9 in the Stacks Project.

Stacks.IdealTorsion.Reduction.reductionComparisonQ, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafReductionDerivedIso.lean, line 78. The attribute's comment: “the canonical arrow in D(O_X)”.

The canonical arrow η_I F ⊗ O_X/I ⟶ H^•(F/I) in D(O_X), for a termwise I-torsion-free complex F: the image under DerivedCategory.Q of the canonical morphism of complexes Reduction.reductionComparisonChainMap from the reduction of the décalage to the chain-level Bockstein complex.

public noncomputable def reductionComparisonQ
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj (Oₓ).property I]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ k : ℤ, IsIdealTorsionFree X ι (F.X k)) :
    DerivedCategory.Q.obj (etaModIdealComplex X I ι F hF) ⟶
      DerivedCategory.Q.obj (bocksteinChainComplex X I ι F hF)

Stacks.IdealTorsion.Reduction.isIso_reductionComparisonQ_of_isLocallyGeneratedByRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafReductionDerivedIsoRegular.lean, line 221. The attribute's comment: “in Situation 0GT4: the canonical arrow of D(O_X) is invertible”.

Stacks Project, Tag 0GT9. In Situation 0GT4, on a complex F of I-torsion-free O_X-modules, the canonical arrow

η_I F ⊗ O_X/I ⟶ H^•(F/I)

of D(O_X) is invertible. The inputs are those of the situation: the ideal is locally generated by a nonzerodivisor and F is termwise I-torsion-free, which is what Lemma 20.55.6 provides for an arbitrary object of D(O_X).

public theorem isIso_reductionComparisonQ_of_isLocallyGeneratedByRegular
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj (Oₓ).property I]
    (hregl : Stacks.IdealTorsion.IsLocallyGeneratedByRegular X ι)
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ k : ℤ, IsIdealTorsionFree X ι (F.X k)) :
    IsIso (reductionComparisonQ X I ι F hF)

Stacks.IdealTorsion.Reduction.reductionComparisonQIsoOfRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafReductionDerivedIsoRegular.lean, line 241. The attribute's comment: “in Situation 0GT4: the canonical isomorphism in D(O_X)”.

Stacks Project, Tag 0GT9. The canonical isomorphism

η_I F ⊗ O_X/I ≅ H^•(F/I) in D(O_X),

in Situation 0GT4, as an explicit isomorphism. This is the tag's own conclusion: "there is a canonical isomorphism".

The forward map is DerivedCategory.Q.map of the named chain map reductionComparisonChainMap, and reductionComparisonQIsoOfRegular_hom says so by rfl.

public noncomputable def reductionComparisonQIsoOfRegular
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj (Oₓ).property I]
    (hregl : Stacks.IdealTorsion.IsLocallyGeneratedByRegular X ι)
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ k : ℤ, IsIdealTorsionFree X ι (F.X k)) :
    DerivedCategory.Q.obj (etaModIdealComplex X I ι F hF) ≅
      DerivedCategory.Q.obj (bocksteinChainComplex X I ι F hF)

Stacks.IdealTorsion.Reduction.exists_isIso_reductionComparisonQ_of_isLocallyGeneratedByRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafReductionDerivedIsoRegular.lean, line 300. The attribute's comment: “in Situation 0GT4, for an arbitrary object of D(O_X): a termwise I-torsion-free representative exists and the canonical arrow is invertible on it”.

Stacks Project, Tag 0GT9, at the tag's own quantifier. In Situation 0GT4, for an arbitrary object M of D(O_X) there is a complex F of I-torsion-free O_X-modules with Q F ≅ M on which the canonical arrow

η_I F ⊗ O_X/I ⟶ H^•(F/I)

is invertible. This is the tag read with its own "let M be an object of D(O_X)": the representative is produced by the proof. Its existence is Eta.torsionFreeResolutions_of_isLocallyGeneratedByRegular composed with the essential surjectivity of DerivedCategory.Q, and the invertibility is isIso_reductionComparisonQ_of_isLocallyGeneratedByRegular.

public theorem exists_isIso_reductionComparisonQ_of_isLocallyGeneratedByRegular
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.sheaf.obj (Oₓ).property I]
    (hregl : Stacks.IdealTorsion.IsLocallyGeneratedByRegular X ι)
    (M : DerivedCategory (SheafOfModules.{u} Oₓ)) :
    ∃ (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
      (hF : ∀ k : ℤ, IsIdealTorsionFree X ι (F.X k)),
      Nonempty (DerivedCategory.Q.obj F ≅ M) ∧ IsIso (reductionComparisonQ X I ι F hF)
Tag 0F9W, a lemma

Tag 0F9W in the Stacks Project.

Stacks.IdealTorsion.Eta.IdealPowerTensorComparison.map_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafTensor.lean, line 945. The attribute's comment: “uniqueness of the degreewise interchange”.

Any two such comparisons agree in every integer degree, negative ones included: the degree-0 normalization starts the recursion, and the recursion runs downwards as well as upwards because tensoring by I is an equivalence, hence faithful.

public theorem IdealPowerTensorComparison.map_eq (I L : SheafOfModules.{u} Oₓ)
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property I]
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property L]
    (c d : IdealPowerTensorComparison X I L) (n : ℤ) (M : SheafOfModules.{u} Oₓ) :
    c.map n M = d.map n M

Stacks.IdealTorsion.Eta.etaTensorInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafTensor.lean, line 1077.

Stacks Project, Tag 0F9W. Décalage by an invertible ideal commutes with tensoring by an invertible module: the décalage of F ⊗ L is canonically isomorphic to the décalage of F tensored by L.

public noncomputable def etaTensorInvertible (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property I]
    (L : SheafOfModules.{u} Oₓ)
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property L]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n)) :
    etaObj X I ι
          ((((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.sheaf).flip.obj L).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj F)
          (fun n => idealTorsionFree_tensorInvertible X I ι L (F.X n) (hF n)) ≅
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.sheaf).flip.obj L).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (etaObj X I ι F hF)

Stacks.IdealTorsion.Eta.etaTensorInvertible_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafTensor.lean, line 1122. The attribute's comment: “first degreewise projection”.

On the first projection of the defining fibre product, the comparison of Tag 0F9W is the interchange of the n-th ideal power with the invertible tensor factor.

public theorem etaTensorInvertible_fst (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property I]
    (L : SheafOfModules.{u} Oₓ)
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property L]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n)) (n : ℤ) :
    (etaTensorInvertible X I ι L F hF).hom.f n ≫
        ((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.sheaf).flip.obj L).map
          (X := etaTerm X I ι F n) (Y := idealPowerTerm X I n (F.X n))
          (pullback.fst (idealPowerMap X I n (F.d n (n + 1)))
            (idealPowerIncl X I ι n (F.X (n + 1)))) =
      pullback.fst _ _ ≫ (idealPowerTensorIso X I L (F.X n) n).hom

Stacks.IdealTorsion.Eta.etaTensorInvertible_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafTensor.lean, line 1139. The attribute's comment: “second degreewise projection”.

On the second projection of the defining fibre product, the comparison of Tag 0F9W is the interchange of the (n+1)-st ideal power with the invertible tensor factor.

public theorem etaTensorInvertible_snd (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [Mono ι]
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property I]
    (L : SheafOfModules.{u} Oₓ)
    [Stacks.SheafOfModules.IsInvertible X.presheaf (Oₓ).property L]
    (F : CochainComplex (SheafOfModules.{u} Oₓ) ℤ)
    (hF : ∀ n : ℤ, IsIdealTorsionFree X ι (F.X n)) (n : ℤ) :
    (etaTensorInvertible X I ι L F hF).hom.f n ≫
        ((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, u, u, u} X.sheaf).flip.obj L).map
          (X := etaTerm X I ι F n) (Y := idealPowerTerm X I (n + 1) (F.X (n + 1)))
          (pullback.snd (idealPowerMap X I n (F.d n (n + 1)))
            (idealPowerIncl X I ι n (F.X (n + 1)))) =
      pullback.snd _ _ ≫ (idealPowerTensorIso X I L (F.X (n + 1)) (n + 1)).hom
Tag 0GTA, a lemma

Tag 0GTA in the Stacks Project.

Stacks.IdealTorsion.Eta.isFiniteFreeStalkOfRank_homology_derivedEtaOfRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafStalk.lean, line 599. The attribute's comment: “in Situation 0GT4: if H^n(M)_x is finite free of rank r over O_{X,x}, then so is H^n(Lη_I M)_x, where Lη_I is derivedEtaOfRegular, the functor of Tag 0F8Q for that situation; the uniqueness of the rank over a nonzero stalk is rank_homology_derivedEtaOfRegular_eq”.

Stacks Project, Tag 0GTA, in Situation 0GT4. Let ι : I ⟶ O_X be an ideal sheaf locally generated by a section that is a nonzerodivisor on O_X, let M be an object of D(O_X) and let x be a point of X. If the stalk H^n(M)_x is finite free of rank r over O_{X,x}, then so is H^n(Lη_I M)_x.

The proof applies isFiniteFreeStalkOfRank_homology_leta: the derived décalage is derivedEtaOfRegular, the functor of Tag 0F8Q built from the situation, the torsion-free resolutions are torsionFreeResolutions_of_isLocallyGeneratedByRegular, and the freeness of rank one of I_x is isFiniteFreeStalkOfRank_one_of_isLocallyGeneratedByRegular. The invertibility of I comes from the implication (1) ⟹ (2) of Tag 0GT3. The statement holds at every point x, and the degree n may be negative.

public theorem isFiniteFreeStalkOfRank_homology_derivedEtaOfRegular
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [monoIncl : Mono ι]
    (hregl : IsLocallyGeneratedByRegular X ι)
    (M : DerivedCategory (SheafOfModules.{u} Oₓ))
    (x : X) (n : ℤ) (r : ℕ)
    (hr : IsFiniteFreeStalkOfRank X
      ((DerivedCategory.homologyFunctor (SheafOfModules.{u} Oₓ) n).obj M) x r) :
    IsFiniteFreeStalkOfRank X
      ((DerivedCategory.homologyFunctor (SheafOfModules.{u} Oₓ) n).obj
        ((@derivedEtaOfRegular X I ι monoIncl hregl).obj M)) x r

Stacks.IdealTorsion.Eta.rank_homology_derivedEtaOfRegular_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/EtaSheafStalk.lean, line 656. The attribute's comment: “the clause of the same rank, in Situation 0GT4: the ideal is locally generated by a nonzerodivisor and the derived décalage is derivedEtaOfRegular, the functor of Tag 0F8Q for that situation; the condition O_{X,x} ≠ 0 is Nontrivial on the stalk of the structure sheaf, and the finite freeness itself is isFiniteFreeStalkOfRank_homology_derivedEtaOfRegular”.

Stacks Project, Tag 0GTA, the clause "of the same rank", in Situation 0GT4 itself. Let ι : I ⟶ O_X be an ideal sheaf locally generated by a section that is a nonzerodivisor on O_X, let M be an object of D(O_X) and let x be a point of X at which the stalk O_{X,x} is nonzero. If H^n(M)_x is finite free of rank r and H^n(Lη_I M)_x is finite free of rank s, then s = r.

Together with isFiniteFreeStalkOfRank_homology_derivedEtaOfRegular this is the complete source statement: that statement supplies the finite freeness of H^n(Lη_I M)_x at the rank of H^n(M)_x, and this one that no other rank is possible, which is what makes "the same rank" a determinate assertion. The nonvanishing of O_{X,x} enters only here, through IsFiniteFreeStalkOfRank.rank_eq: over the zero ring every module is free of every rank.

public theorem rank_homology_derivedEtaOfRegular_eq
    (I : SheafOfModules.{u} Oₓ) (ι : I ⟶ 𝒪) [monoIncl : Mono ι]
    (hregl : IsLocallyGeneratedByRegular X ι)
    (M : DerivedCategory (SheafOfModules.{u} Oₓ))
    (x : X) [Nontrivial (ringStalk X x)] (n : ℤ) (r s : ℕ)
    (hr : IsFiniteFreeStalkOfRank X
      ((DerivedCategory.homologyFunctor (SheafOfModules.{u} Oₓ) n).obj M) x r)
    (hs : IsFiniteFreeStalkOfRank X
      ((DerivedCategory.homologyFunctor (SheafOfModules.{u} Oₓ) n).obj
        ((@derivedEtaOfRegular X I ι monoIncl hregl).obj M)) x s) :
    s = r
Sources
LeanStacks.IdealTorsion.isInvertible_of_isLocallyGeneratedByRegular · Stacks.IdealTorsion.isLocallyGeneratedByRegular_of_isInvertible · Stacks.IdealTorsion.Eta.Situation · Stacks.IdealTorsion.idealTorsionFree_tfae · Stacks.IdealTorsion.Eta.etaStalkIso · Stacks.IdealTorsion.Eta.etaStalkIso_hom · Stacks.IdealTorsion.Eta.etaCohomologyIso · Stacks.IdealTorsion.Eta.etaCohomologyIso_hom

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.