Theorems · Definition · category theory

CategoryTheory.Discrete.natIso

{C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} →
        ((i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) → (F ≅ G)

For functors out of a discrete category, a natural isomorphism is just a collection of isomorphisms, as the naturality squares are trivial.

Defined in

Mathlib.CategoryTheory.Discrete.Basic

Cited by

28 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category