covariant_sequence_exact₁' — Mathlib

English

Alternative formulation of covariant_sequence_exact₁', asserting the exactness of a short complex formed by the extClass and the selected postcomposition with X and h.

Русский

Альтернативная формулировка covariant_sequence_exact₁', утверждающая точность короткого комплекса, образованного extClass и выбранной посткомпозиции с X и h.

LaTeX

$$$(\\mathrm{ShortComplex.mk}(\\mathrm{AddCommGrpCat.ofHom}(hS.extClass.postcomp X h),\\; \\mathrm{AddCommGrpCat.ofHom}((mk_0 S.f).postcomp X (add_zero n_1)),\\; \\text{proof})).Exact$$$

Lean4

/-- Alternative formulation of `covariant_sequence_exact₁` -/
theorem covariant_sequence_exact₁' :
    (ShortComplex.mk (AddCommGrpCat.ofHom (hS.extClass.postcomp X h))
        (AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X (add_zero n₁)))
        (by
          ext x
          dsimp
          simp only [comp_assoc_of_third_deg_zero, ShortComplex.ShortExact.extClass_comp, comp_zero])).Exact :=
  by
  letI := HasDerivedCategory.standard C
  have :=
    (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₁ _
      (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 x
    exact preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hS x h
  · ext x; apply hom_comp_singleFunctor_map_shift (C := C)

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