Theorems · Definition · category theory

CategoryTheory.RetractArrow.map

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {X Y Z W : C} →
          {f : X ⟶ Y} →
            {g : Z ⟶ W} →
              CategoryTheory.RetractArrow f g →
                (F : CategoryTheory.Functor C D) → CategoryTheory.RetractArrow (F.map f) (F.map g)

If a morphism f is a retract of g, then F.map f is a retract of F.map g for any functor F.

Defined in

Mathlib.CategoryTheory.Retract

Cited by

5 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category