Theorems · Definition · commutative algebra

localCohomology.isoOfFinal

{R : Type (max u v v')} →
  [inst : CommRing R] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        {E : Type v'} →
          [inst_2 : CategoryTheory.SmallCategory E] →
            (I' : CategoryTheory.Functor E D) →
              (I : CategoryTheory.Functor D (Ideal R)) →
                [I'.Initial] → (i : ℕ) → localCohomology.ofDiagram (I'.comp I) i ≅ localCohomology.ofDiagram I i

Local cohomology agrees along precomposition with a cofinal diagram.

Defined in

Mathlib.Algebra.Homology.LocalCohomology

Cited by

0 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCategoryTheory.SmallCategoryCategoryTheory.SmallCategoryCategoryTheory.Functor.Initial