hasKernel_iso_comp — Mathlib

English

If f is an isomorphism and g has a kernel, then the composition f ∘ g has a kernel.

Русский

Если f является изоморфизмом, а у g есть ядро, тогда произведение f ∘ g имеет ядро.

LaTeX

$$$\forall f,g:\; X \xrightarrow{f} Y \xrightarrow{g} Z,\; IsIso(f) \Rightarrow HasKernel(g) \Rightarrow HasKernel(f\circ g).$$$

Lean4

instance hasKernel_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : HasKernel (f ≫ g) where
  exists_limit :=
    ⟨{  cone := KernelFork.ofι (kernel.ι g ≫ inv f) (by simp)
        isLimit :=
          isLimitAux _ (fun s => kernel.lift _ (s.ι ≫ f) (by simp)) (by simp) fun s (m : _ ⟶ kernel _) w =>
            by
            simp_rw [← w]
            apply equalizer.hom_ext
            simp }⟩

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