contravariant_sequence_exact₂' — Mathlib

English

Alternative formulation of contravariant_sequence_exact₁': a certain five-term ShortComplex is Exact via Ext-hom equivalences and ladder arguments.

Русский

Альтернативная формулировка contravariant_sequence_exact₁': заданный пятиэлементный ShortComplex точен через эквиварианты гомологий Ext и лестничные аргументы.

LaTeX

$$$\\big(\\mathrm{ShortComplex.mk}(\\mathrm{AddCommGrpCat.ofHom}((\\mathrm{mk_0} S.f).precomp Y (zero_add n_0))),\\; \\mathrm{AddCommGrpCat.ofHom}((\\mathrm{hS.extClass.postcomp} X h)),\\; \\cdots\\big).Exact$$$

Lean4

/-- Alternative formulation of `contravariant_sequence_exact₂` -/
theorem contravariant_sequence_exact₂' (n : ℕ) :
    (ShortComplex.mk (AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y (zero_add n)))
        (AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y (zero_add n)))
        (by
          ext
          dsimp
          simp only [mk₀_comp_mk₀_assoc, ShortComplex.zero, mk₀_zero, zero_comp])).Exact :=
  by
  letI := HasDerivedCategory.standard C
  have :=
    (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₂ _
      (op_distinguished _ hS.singleTriangle_distinguished) n
  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)
  all_goals ext; apply singleFunctor_map_comp_hom (C := C)

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