imageToKernel_epi_of_zero_of_mono

English

A further formulation of functorial behavior of imageToKernel under isomorphisms f and g, using imageSubobjectCompIso and kernelSubobjectIsoComp.

Русский

Дальнейшая формулировка поведения imageToKernel при изоморфизмах через imageSubobjectCompIso и kernelSubobjectIsoComp.

LaTeX

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

Lean4

/-- `imageToKernel` for `A --0--> B --g--> C`, where `g` is a mono is itself an epi
(i.e. the sequence is exact at `B`).
-/
instance imageToKernel_epi_of_zero_of_mono [HasKernels V] [HasZeroObject V] [Mono g] :
    Epi (imageToKernel (0 : A ⟶ B) g (by simp)) :=
  epi_of_target_iso_zero _ (kernelSubobjectIso g ≪≫ kernel.ofMono g)

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