Theorems · Theorem · category theory

CategoryTheory.PreservesImage.iso_inv

∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y),
  (CategoryTheory.PreservesImage.iso L f).inv =
    { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯,
            e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯, e_strong_epi := ⋯ }.toMonoIsImage.lift
      (CategoryTheory.Limits.Image.monoFactorisation (L.map f))

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Cited by

1 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasEqualizersCategoryTheory.Limits.HasImagesCategoryTheory.StrongEpiCategoryCategoryTheory.Limits.HasImagesCategoryTheory.Limits.PreservesLimitCategoryTheory.Limits.PreservesColimit