instEpiMap'ComposableArrows₃OfNatNat

English

The diagram K.homology i → K.opcycles i → K.cycles j → K.homology j is exact when c.Rel i j.

Русский

Диаграмма K.homology i → K.opcycles i → K.cycles j → K.homology j точна, когда c.Rel i j.

LaTeX

$$$\text{composableArrows}_3\;\text{is exact for } c.Rel i j$$$

Lean4

instance [K.HasHomology i] [K.HasHomology j] : Epi ((composableArrows₃ K i j).map' 2 3) := by
  -- Disable `Fin.reduceFinMk`, otherwise `Precomp.obj_succ` does not fire. (https://github.com/leanprover-community/mathlib4/issues/27382)

  dsimp [-Fin.reduceFinMk]
  infer_instance

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