English
There is an instance showing epi for a map in the nat-nat level of the HomologySequence construction.
Русский
Существует экземпляр эпиморфизма для отображения на уровне нат-нат в построении последовательности гомологий.
LaTeX
$$$\text{epi}((\mathrm{HomologySequence}.composableArrows_3 K i j).map' 2 3)$$$
Lean4
/-- The functor `HomologicalComplex C c ⥤ ComposableArrows C 3` that maps `K` to the
diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j`. -/
@[simps]
noncomputable def composableArrows₃Functor [CategoryWithHomology C] : HomologicalComplex C c ⥤ ComposableArrows C 3
where
obj K := composableArrows₃ K i j
map {K L}
φ :=
ComposableArrows.homMk₃ (homologyMap φ i) (opcyclesMap φ i)
(cyclesMap φ j)
-- Disable `Fin.reduceFinMk`, otherwise `Precomp.obj_succ` does not fire. (https://github.com/leanprover-community/mathlib4/issues/27382)
(homologyMap φ j) (by simp) (by simp [-Fin.reduceFinMk]) (by simp [-Fin.reduceFinMk])
