isKernelCompMono_lift — Mathlib

English

The lift through a kernel is mono whenever the left factor is mono; the explicit lift is given by a universal construction.

Русский

Лифт через ядро моно, если левый фактор моно; явное выражение задаётся универсальным конструктором.

LaTeX

$$$\\forall W\\; k:W\\to X\\; h:\\; k\\to f \\; (h=f\\circ k)\\; [\\text{Mono}(k)]\\Rightarrow \\operatorname{Mono}(\\operatorname{kernel.lift} f k h).$$$

Lean4

theorem isKernelCompMono_lift {c : KernelFork f} (i : IsLimit c) {Z} (g : Y ⟶ Z) [hg : Mono g] {h : X ⟶ Z}
    (hh : h = f ≫ g) (s : KernelFork h) :
    (isKernelCompMono i g hh).lift s =
      i.lift
        (Fork.ofι s.ι
          (by
            rw [← cancel_mono g, Category.assoc, ← hh]
            simp)) :=
  rfl

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