English
Let S be a short complex of modules and φ: S.moduleCatLeftHomologyData.K → M with f' composed with φ equal to zero. Then the hom component of the descH morphism is the lifting of φ.hom along the range inclusion, determined by the ker-condition encoded by h.
Русский
Пусть S — короткий комплекс модулей, и пусть φ: S.moduleCatLeftHomologyData.K → M удовлетворяет f' ∘ φ = 0. Тогда компоненту вида 'hom' отображения descH φ h можно описать как линейное восхождение φ.hom через включение образа, заданное условием на ядро, заданное h.
LaTeX
$$$ (\mathrm{descH}(\varphi,h))_{\mathrm{hom}} = \Big(\mathrm{range} \circ \mathrm{ModuleCat.Hom.hom} \Big).liftQ \; \varphi_{\mathrm{hom}} \\ \quad \quad \quad \Big( \mathrm{range\_le\_ker\_iff.2(\mathrm{ModuleCat.hom\_ext\_iff.1(h)})} \Big). $$$
Lean4
@[simp]
theorem moduleCatLeftHomologyData_descH_hom {M : ModuleCat R} (φ : S.moduleCatLeftHomologyData.K ⟶ M)
(h : S.moduleCatLeftHomologyData.f' ≫ φ = 0) :
(S.moduleCatLeftHomologyData.descH φ h).hom =
(LinearMap.range <| ModuleCat.Hom.hom _).liftQ φ.hom
(LinearMap.range_le_ker_iff.2 <| ModuleCat.hom_ext_iff.1 h) :=
rfl
