Theorems · Definition · category theory

CategoryTheory.MonoOver.exists

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasImages C] →
        (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)

In the case where f is not a monomorphism but C has images, we can still take the "forward map" under it, which agrees with MonoOver.map f.

Defined in

Mathlib.CategoryTheory.Subobject.MonoOver

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasImages