contravariant_sequence_exact₃' — Mathlib

English

Alternative formulation of covariant_sequence_exact₁: a ladder of exactness aligns with the Ext-hom equivalence.

Русский

Альтернативная формулировка covariant_sequence_exact₁: лестница точности согласуется с эквивалентностью гомологических групп Ext.

LaTeX

$$$\\text{covariant\_sequence\_exact\_₁}(X,hS,n_0,n_1,h)\\;\\text{holds}$$$

Lean4

/-- Alternative formulation of `contravariant_sequence_exact₃` -/
theorem contravariant_sequence_exact₃' :
    (ShortComplex.mk (AddCommGrpCat.ofHom (hS.extClass.precomp Y h))
        (AddCommGrpCat.ofHom (((mk₀ S.g).precomp Y (zero_add n₁))))
        (by
          ext
          dsimp
          simp only [ShortComplex.ShortExact.comp_extClass_assoc])).Exact :=
  by
  letI := HasDerivedCategory.standard C
  have :=
    (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₁ _
      (op_distinguished _ hS.singleTriangle_distinguished) n₀ n₁ (by cutsat)
  rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
  apply
    Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv) (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv)
      (H := this)
  · ext; dsimp; apply preadditiveYoneda_homologySequenceδ_singleTriangle_apply
  · ext; apply singleFunctor_map_comp_hom (C := C)

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