Theorems · Definition · category theory

CategoryTheory.NatIso.ofComponents

{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} →
          (app : (X : C) → F.obj X ≅ G.obj X) →
            autoParam
                (∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom =
                    CategoryTheory.CategoryStruct.comp (app X).hom (G.map f))
                CategoryTheory.NatIso.ofComponents._auto_1 →
              (F ≅ G)

Construct a natural isomorphism between functors by giving object level isomorphisms, and checking naturality only in the forward direction.

Defined in

Mathlib.CategoryTheory.NatIso

Cited by

178 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 108 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category