Theorems · Definition · category theory

CategoryTheory.Limits.image.isoStrongEpiMono

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {I' : C} →
            (e : X ⟶ I') →
              (m : I' ⟶ Y) →
                CategoryTheory.CategoryStruct.comp e m = f →
                  [CategoryTheory.StrongEpi e] → [CategoryTheory.Mono m] → I' ≅ CategoryTheory.Limits.image f

If C has strong epi mono factorisations, then the image is unique up to isomorphism, in that if f factors as a strong epi followed by a mono, this factorisation is essentially the image factorisation.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Images

Cited by

5 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasStrongEpiMonoFactorisationsCategoryTheory.StrongEpiCategoryTheory.Mono