isNormalMonoCategory — Mathlib

English

If a category has finite products and every coimage–image comparison is an isomorphism, then it is a normal epi category: every epi morphism is the cokernel of its kernel.

Русский

Если у категории имеются конечные произведения и для каждого f: X→Y сопоставление кообраза и образа — изоморфизм, то категория является нормальной эпик-категорией: каждый эпиморфизм является кокernel своего ядра.

LaTeX

$$$$ [HasFiniteProducts\\ C] \\land [\\forall f, IsIso(Abelian.coimageImageComparison f)] \\Rightarrow IsNormalEpiCategory C. $$$$

Lean4

/-- A category with finite products in which coimage-image comparisons are all isomorphisms
is a normal mono category.
-/
theorem isNormalMonoCategory : IsNormalMonoCategory C where
  normalMonoOfMono f
    m :=
    ⟨{  Z := _
        g := cokernel.π f
        w := by simp
        isLimit := by
          haveI : Limits.HasImages C := hasImages
          haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
          haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
          have aux :
            ∀ (s : KernelFork (cokernel.π f)),
              (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
                  Fork.ι (KernelFork.ofι f (by simp)) =
                Fork.ι s :=
            ?_
          · refine isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux ?_
            intro A g hg
            rw [KernelFork.ι_ofι] at hg
            rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
          · intro A
            simp only [KernelFork.ι_ofι, Category.assoc]
            convert limit.lift_π A WalkingParallelPair.zero using 2
            rw [IsIso.inv_comp_eq, eq_comm]
            exact (imageMonoFactorisation f).fac }⟩

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