English
In a Short Complex with forgetful Ab-structure, for x2 with g x2 = 0, applying iCycles to cycles Mk x2 hx2 and then forgetting yields x2.
Русский
В кратком комплексе с забыванием в Ab для элемента x2 с g x2 = 0, применение iCycles к cyclesMk x2 hx2 и последующее забывание возвращают x2.
LaTeX
$$$(\\forget_2 C Ab).map S.iCycles (S.cyclesMk x_2 hx_2) = x_2$$$
Lean4
@[simp]
theorem i_cyclesMk [S.HasHomology] (x₂ : (forget₂ C Ab).obj S.X₂) (hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0) :
(forget₂ C Ab).map S.iCycles (S.cyclesMk x₂ hx₂) = x₂ :=
by
dsimp [cyclesMk]
-- `abCyclesIso_inv_apply_iCycles` is not in `simp`-normal form, so we first
-- have to simplify it.
have := abCyclesIso_inv_apply_iCycles (S.map (forget₂ C Ab)) ⟨x₂, hx₂⟩
simp only [map_X₂, map_X₃, map_g] at this
rw [← ConcreteCategory.comp_apply, S.mapCyclesIso_hom_iCycles (forget₂ C Ab), this]
