iso_hom_π — Mathlib

English

For a morphism f with appropriate kernels and cokernels, and for a functor F that preserves zero morphisms, the map induced by F on the coimage projection commutes with the canonical coimage projection after applying F.

Русский

Для морфизма f с подходящими ядрами и образами и для сохраняющей нулевые морфизмы functor F, отображение, индуцированное F на проекции кообраза, коммутирует с канонической проекцией кообраза после применения F.

LaTeX

$$$F(\operatorname{coimage}.\pi f) \;\gg\; (\mathrm{PreservesCoimage.iso} F f).hom = \operatorname{coimage}.\pi (F.map f)$$$

Lean4

@[reassoc (attr := simp)]
theorem iso_hom_π : F.map (Abelian.coimage.π f) ≫ (PreservesCoimage.iso F f).hom = Abelian.coimage.π (F.map f) := by
  simp [iso]

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