Confused about NatIso of functors in mathlib

Stream: new members

[Shanghe Chen]

Hi I am learning how to use the category theory part in mathlib and I came to the part about natural isomorphism about functors between category. How is NatIso defined as an isomorphism in a category in mathlib? hoving the notation ≅ in the following code snippet, the doc says it's an isomorphisms between objects of a category:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.NatIso

open CategoryTheory
set_option autoImplicit true

variable [Category C] [Category D]
variable (F G: C ⥤ D)
variable (ε : F ≅ G)
#check ε.hom

[Yaël Dillies]

Good question! Can you guess what category it is an isomorphism in?

[Shanghe Chen]

But treating functors as object requires defining functors and natural transformations as a category. I don't see how to find the instance of category in the definition

[Shanghe Chen]

Yaël Dillies 发言道：

Good question! Can you guess what category it is an isomorphism in?

Yeah I think it should be the category of functors and natural transformations. Can I print the instance with some code in the above snippet?

[Yaël Dillies]

So you agree that C ⥤ D is the category we are taking isomorphisms in?

[Shanghe Chen]

Yeah I agree with this. But checking the type with #check C ⥤ D gives me a type rather than a category. I want to see the category instance used when writing variable (ε : F ≅ G)

[Yaël Dillies]

Okay so now there are many ways you can figure out what the instance is. Here are a few (in no particular order):

1. Go to #docs and search for strings like categoryfunctor, functorcategory, categorycategoryfunctor
2. Use Loogle with a string like Category (_ ⥤ _)
3. Inspect the term in the infoview by clicking on the natural isomorphism, seeing what the Category (C ⥤ D) instance is. Here you should only need to click once, but you can in theory click arbitrarily long inside the term
4. Write #synth Category (C ⥤ D) in your Lean file

[Shanghe Chen]

Oh I get it with #check (inferInstance : (Category (C ⥤ D))) too. Yeah I will try the ways you give too. Thank you very much Yaël :tada:

[Adam Topaz]

NatIso’s are indeed defined as isomorphisms in the category of functors. But we have some convenience definitions for construction such isomorphisms most notably docs#CategoryTheory.NatIso.ofComponents