English
There is a natural isomorphism between local cohomology defined via final diagram and via precomposition with I.
Русский
Существует естественный изоморфизм локальной когомогности, определяемой через итоговую диаграмму и через пред-композицию с I.
LaTeX
$$$\\text{isoOfFinal } I' I i : ofDiagram (I'.comp I) i \\cong ofDiagram I i$$$
Lean4
/-- Local cohomology agrees along precomposition with a cofinal diagram. -/
@[nolint unusedHavesSuffices]
def isoOfFinal [Functor.Initial I'] (i : ℕ) : ofDiagram.{max u v, v'} (I' ⋙ I) i ≅ ofDiagram.{max u v', v} I i :=
have := hasColimitDiagram.{max u v', v} I i
have := hasColimitDiagram.{max u v, v'} (I' ⋙ I) i
HasColimit.isoOfNatIso (diagramComp.{u} I' I i) ≪≫ Functor.Final.colimitIso _ _
