isNormalEpiCategory — Mathlib

English

As above: a category with finite products and iso coimage–image maps becomes a normal epi category.

Русский

Аналогично: категория с конечными продуктами и изоморфизмами кообраза-образа становится нормальной эпик-категорией.

LaTeX

$$$$ [HasFiniteProducts\\ C] \\Rightarrow IsNormalEpiCategory C \\text{ if } [\\forall f, IsIso(Abelian.coimageImageComparison f)]. $$$$

Lean4

/-- A category with finite products in which coimage-image comparisons are all isomorphisms
is a normal epi category.
-/
theorem isNormalEpiCategory : IsNormalEpiCategory C where
  normalEpiOfEpi f
    m :=
    ⟨{  W := kernel f
        g := kernel.ι _
        w := kernel.condition _
        isColimit := by
          haveI : Limits.HasImages C := hasImages
          haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
          haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
          have aux :
            ∀ (s : CokernelCofork (kernel.ι f)),
              Cofork.π (CokernelCofork.ofπ f (by simp)) ≫
                  inv (imageMonoFactorisation f).m ≫
                    inv (Abelian.coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
                Cofork.π s :=
            ?_
          · refine
              isColimitAux _
                (fun A => inv (imageMonoFactorisation f).m ≫ inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _)
                aux ?_
            intro A g hg
            rw [CokernelCofork.π_ofπ] at hg
            rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
          · intro A
            simp only [CokernelCofork.π_ofπ, ← Category.assoc]
            convert colimit.ι_desc A WalkingParallelPair.one using 2
            rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']
            exact (imageMonoFactorisation f).fac }⟩

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