instIsNormalMonoCategory — Mathlib

English

Let R be a presheaf of rings on a category C, and consider the category of presheaves of R-modules. Then every monomorphism in this category is a kernel of some morphism (i.e., monos are normal).

Русский

Пусть R — функтор-распределение колец над C, и категория прешейфов модулей над R; тогда любой монообраз в этой категории является ядром некоторых гомоморфизмов (моно‑ядерно).

LaTeX

$$$\\forall f:\\, A \\xrightarrow{f} B\\ (f\\ \\text{ моно})\\;\\Rightarrow\\; \\exists g:\\, B \\to C\\; \\text{ such that }\\ f = \\ker(g).$$$

Lean4

noncomputable instance : IsNormalMonoCategory (PresheafOfModules.{v} R) where
  normalMonoOfMono i
    _ :=
    ⟨NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
        (evaluationJointlyReflectsLimits _ _ (fun _ => Abelian.isLimitMapConeOfKernelForkOfι _ _))⟩

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