imageIsoImage_inv — Mathlib

English

The inverse of imageIsoImage f is given by a kernel lift construction using image and cokernel.

Русский

Обратный образ-образ через imageIsoImage задаётся через подъем ядра с использованием образа и кокernel.

LaTeX

$$$$ (imageIsoImage f).inv = \\text{kernel.lift} \\_{\\cdot} \\Big( \\operatorname{Limits.image.ι} f \\Big) $$$$

Lean4

theorem imageIsoImage_inv :
    (imageIsoImage f).inv = kernel.lift _ (Limits.image.ι f) (by simp [← cancel_epi (factorThruImage f)]) :=
  by
  ext
  rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift, imageStrongEpiMonoFactorisation_e, Category.assoc,
    kernel.lift_ι, equalizer_as_kernel, kernel.lift_ι, Limits.image.fac]

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