Theorems · Definition · category theory

CategoryTheory.NatTrans.retractArrowApp

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} →
          (τ : F ⟶ G) → {X Y : C} → CategoryTheory.Retract X Y → CategoryTheory.RetractArrow (τ.app X) (τ.app Y)

If X is a retract of Y, then for any natural transformation τ, the natural transformation τ.app X is a retract of τ.app Y.

Defined in

Mathlib.CategoryTheory.Retract

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category