hasKernels — Mathlib

English

If i: F⋙G ≅ 1_C and G ⊣ F, then HasKernels C.

Русский

Если i: F⋙G ≅ 1_C и G ⊣ F, то существуют ядра в C.

LaTeX

$$$\text{HasKernels}(C)$$$

Lean4

/-- No point making this an instance, as it requires `i`. -/
theorem hasKernels [PreservesFiniteLimits G] (i : F ⋙ G ≅ 𝟭 C) : HasKernels C :=
  {
    has_limit {X Y}
      f := by
      have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by simpa using NatIso.naturality_1 i f
      rw [← this]
      haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
      apply Limits.hasKernel_iso_comp }

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