instIsClosedUnderIsomorphismsHomologicalKernel

English

The homological kernel associated to a homological functor is closed under isomorphisms of functors: changing the functor by an isomorphism preserves the kernel property.

Русский

Гомологическое ядро гомологического функторa сохраняется под изоморфизмами функторов: изменение функторa на изоморфизм сохраняет свойство ядра.

LaTeX

$$$\text{F.homologicalKernel.IsClosedUnderIsomorphisms}$$$

Lean4

instance : F.homologicalKernel.IsClosedUnderIsomorphisms where
  of_iso e hX n := (hX n).of_iso ((shiftFunctor C n ⋙ F).mapIso e.symm)

Похожие утверждения