imageToKernel_comp_hom_inv_comp — Mathlib

English

A similar statement to the previous one under assumptions of equalizers and images, giving a formula for imageToKernel with an Iso f h and g isomorphism.

Русский

Похожее утверждение в условиях существования эквивалентов: imageToKernel с изоморфизмами f и g.

LaTeX

$$imageToKernel (f ≫ i.hom) (i.inv ≫ g) w = (imageSubobjectCompIso _ _).hom ≫ imageToKernel f g (by simpa using w) ≫ (kernelSubobjectIsoComp i.inv g).inv$$

Lean4

@[simp]
theorem imageToKernel_comp_hom_inv_comp [HasEqualizers V] [HasImages V] {Z : V} {i : B ≅ Z} (w) :
    imageToKernel (f ≫ i.hom) (i.inv ≫ g) w =
      (imageSubobjectCompIso _ _).hom ≫ imageToKernel f g (by simpa using w) ≫ (kernelSubobjectIsoComp i.inv g).inv :=
  by
  ext
  simp

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