instIsIsoToRightDerivedZero'Self — Mathlib

English

For any functor F that preserves finite limits (left exact), and any X with an injective object, the object (InjectiveResolution X).toRightDerivedZero' F is an isomorphism.

Русский

Для любого функторa F, сохраняющего конечные пределы (слева точный), и любого X с инъективным объектом, отображение toRightDerivedZero' F от разрешения X является изоморфизмом.

LaTeX

$$IsIso ( (InjectiveResolution.self X).toRightDerivedZero' F )$$

Lean4

instance (F : C ⥤ D) [F.Additive] (X : C) [Injective X] : IsIso ((InjectiveResolution.self X).toRightDerivedZero' F) :=
  by
  dsimp [InjectiveResolution.toRightDerivedZero']
  rw [CochainComplex.isIso_liftCycles_iff]
  refine ⟨ShortComplex.Splitting.exact ?_, inferInstance⟩
  exact
    { r := 𝟙 _
      s := 0
      s_g := (F.map_isZero (isZero_zero _)).eq_of_src _ _ }

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