doc-next-gen

Mathlib.CategoryTheory.Functor.Category

Module docstring

{"# The category of functors and natural transformations between two fixed categories.

We provide the category instance on C ⥤ D, with morphisms the natural transformations.

At the end of the file, we provide the left and right unitors, and the associator, for functor composition. (In fact functor composition is definitionally associative, but very often relying on this causes extremely slow elaboration, so it is better to insert it explicitly.)

Universes

If C and D are both small categories at the same universe level, this is another small category at that level. However if C and D are both large categories at the same universe level, this is a small category at the next higher level. "}

CategoryTheory.Functor.category instance
: Category.{max u₁ v₂} (C ⥤ D)
Full source 
/-- `Functor.category C D` gives the category structure on functors and natural transformations
between categories `C` and `D`.

Notice that if `C` and `D` are both small categories at the same universe level,
this is another small category at that level.
However if `C` and `D` are both large categories at the same universe level,
this is a small category at the next higher level.
-/
instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where
  Hom F G := NatTrans F G
  id F := NatTrans.id F
  comp α β := vcomp α β
The Category of Functors Between Two Categories
Informal description
For any two categories $\mathcal{C}$ and $\mathcal{D}$, the collection of functors from $\mathcal{C}$ to $\mathcal{D}$ forms a category, where the morphisms are natural transformations between functors. The identity morphism for a functor $F$ is the identity natural transformation $\text{id}_F$, and composition of morphisms is given by vertical composition of natural transformations.
CategoryTheory.NatTrans.ext' theorem
{α β : F ⟶ G} (w : α.app = β.app) : α = β
Full source 
@[ext]
theorem ext' {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w
Natural Transformation Extensionality
Informal description
For any two natural transformations $\alpha, \beta \colon F \Rightarrow G$ between functors $F$ and $G$, if the components $\alpha_X$ and $\beta_X$ are equal for all objects $X$ in the domain category (i.e., $\alpha_X = \beta_X$ for all $X$), then $\alpha = \beta$.
CategoryTheory.NatTrans.vcomp_eq_comp theorem
(α : F ⟶ G) (β : G ⟶ H) : vcomp α β = α ≫ β
Full source 
@[simp]
theorem vcomp_eq_comp (α : F ⟶ G) (β : G ⟶ H) : vcomp α β = α ≫ β := rfl
Vertical Composition Equals Categorical Composition in Functor Category
Informal description
For any natural transformations $\alpha \colon F \Rightarrow G$ and $\beta \colon G \Rightarrow H$ between functors $F, G, H \colon \mathcal{C} \to \mathcal{D}$, the vertical composition $\alpha \circ \beta$ is equal to the categorical composition $\alpha \ggg \beta$ in the functor category $\mathcal{C} \to \mathcal{D}$.
CategoryTheory.NatTrans.vcomp_app' theorem
(α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X
Full source 
theorem vcomp_app' (α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X := rfl
Componentwise Vertical Composition of Natural Transformations
Informal description
For any natural transformations $\alpha \colon F \Rightarrow G$ and $\beta \colon G \Rightarrow H$ between functors $F, G, H \colon \mathcal{C} \to \mathcal{D}$, and for any object $X$ in $\mathcal{C}$, the component of the vertical composition $\alpha \ggg \beta$ at $X$ is equal to the composition of the components $\alpha_X \circ \beta_X$ in $\mathcal{D}$.
CategoryTheory.NatTrans.congr_app theorem
{α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X
Full source 
theorem congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw [h]
Componentwise Equality of Natural Transformations
Informal description
For any two natural transformations $\alpha, \beta \colon F \to G$ between functors $F, G \colon \mathcal{C} \to \mathcal{D}$, if $\alpha = \beta$, then their components at any object $X$ in $\mathcal{C}$ are equal, i.e., $\alpha_X = \beta_X$.
CategoryTheory.NatTrans.id_app theorem
(F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X)
Full source 
@[simp]
theorem id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
Identity Natural Transformation Component at Object $X$
Informal description
For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and any object $X$ in $\mathcal{C}$, the component of the identity natural transformation $\mathrm{id}_F$ at $X$ is equal to the identity morphism $\mathrm{id}_{F(X)}$ in $\mathcal{D}$.
CategoryTheory.NatTrans.comp_app theorem
{F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X
Full source 
@[simp]
theorem comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
    (α ≫ β).app X = α.app X ≫ β.app X := rfl
Componentwise Composition of Natural Transformations
Informal description
For any functors $F, G, H \colon \mathcal{C} \to \mathcal{D}$ and natural transformations $\alpha \colon F \to G$, $\beta \colon G \to H$, the component of the composition $\alpha \circ \beta$ at any object $X$ in $\mathcal{C}$ is equal to the composition of the components $\alpha_X \circ \beta_X$ in $\mathcal{D}$. That is, $(\alpha \circ \beta)_X = \alpha_X \circ \beta_X$.
CategoryTheory.NatTrans.app_naturality theorem
{F G : C ⥤ D ⥤ E} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f
Full source 
@[reassoc]
theorem app_naturality {F G : C ⥤ D ⥤ E} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) :
    (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f :=
  (T.app X).naturality f
Naturality Condition for Components of a Natural Transformation Between Functor Categories
Informal description
For functors $F, G \colon \mathcal{C} \to (\mathcal{D} \to \mathcal{E})$ and a natural transformation $T \colon F \to G$, given an object $X$ in $\mathcal{C}$ and a morphism $f \colon Y \to Z$ in $\mathcal{D}$, the following diagram commutes: \[ (F(X))(f) \circ (T_X)_Z = (T_X)_Y \circ (G(X))(f) \] where $(T_X)_Y$ denotes the component of the natural transformation $T_X \colon F(X) \to G(X)$ at object $Y$ in $\mathcal{D}$.
CategoryTheory.NatTrans.naturality_app theorem
{F G : C ⥤ D ⥤ E} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) : (F.map f).app Z ≫ (T.app Y).app Z = (T.app X).app Z ≫ (G.map f).app Z
Full source 
@[reassoc]
theorem naturality_app {F G : C ⥤ D ⥤ E} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) :
    (F.map f).app Z ≫ (T.app Y).app Z = (T.app X).app Z ≫ (G.map f).app Z :=
  congr_fun (congr_arg app (T.naturality f)) Z
Naturality Condition for Components of a Natural Transformation
Informal description
For any natural transformation $T \colon F \Rightarrow G$ between functors $F, G \colon \mathcal{C} \to \mathcal{D} \to \mathcal{E}$, any object $Z$ in $\mathcal{D}$, and any morphism $f \colon X \to Y$ in $\mathcal{C}$, the following diagram commutes: \[ (F(f))_Z \circ T(Y)_Z = T(X)_Z \circ G(f)_Z \] where $(-)_Z$ denotes the component of the functor at $Z$, and $T(-)_Z$ denotes the component of the natural transformation at $Z$.
CategoryTheory.NatTrans.naturality_app_app theorem
{F G : C ⥤ D ⥤ E ⥤ E'} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) : ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃
Full source 
@[reassoc]
theorem naturality_app_app {F G : C ⥤ D ⥤ E ⥤ E'}
    (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) :
    ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ =
      ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃ :=
  congr_app (NatTrans.naturality_app α X₂ f) X₃
Naturality Condition for Components of a Natural Transformation Between Higher Functor Categories
Informal description
For functors $F, G \colon \mathcal{C} \to \mathcal{D} \to \mathcal{E} \to \mathcal{E}'$ and a natural transformation $\alpha \colon F \to G$, given objects $X_2 \in \mathcal{D}$ and $X_3 \in \mathcal{E}$, and a morphism $f \colon X_1 \to Y_1$ in $\mathcal{C}$, the following diagram commutes: \[ (F(f)_{X_2})_{X_3} \circ \alpha_{Y_1, X_2, X_3} = \alpha_{X_1, X_2, X_3} \circ (G(f)_{X_2})_{X_3} \] where $F(f)_{X_2}$ denotes the component of the functor $F(f)$ at $X_2$, and $\alpha_{X_1, X_2, X_3}$ denotes the component of the natural transformation $\alpha$ at $X_1, X_2, X_3$.
CategoryTheory.NatTrans.mono_of_mono_app theorem
(α : F ⟶ G) [∀ X : C, Mono (α.app X)] : Mono α
Full source 
/-- A natural transformation is a monomorphism if each component is. -/
theorem mono_of_mono_app (α : F ⟶ G) [∀ X : C, Mono (α.app X)] : Mono α :=
  ⟨fun g h eq => by
    ext X
    rw [← cancel_mono (α.app X), ← comp_app, eq, comp_app]⟩
Natural Transformation is Monic if All Components Are Monic
Informal description
A natural transformation $\alpha \colon F \Rightarrow G$ between functors $F, G \colon \mathcal{C} \to \mathcal{D}$ is a monomorphism in the functor category $\mathcal{C} \to \mathcal{D}$ if each component $\alpha_X \colon F(X) \to G(X)$ is a monomorphism in $\mathcal{D}$ for every object $X$ in $\mathcal{C}$.
CategoryTheory.NatTrans.epi_of_epi_app theorem
(α : F ⟶ G) [∀ X : C, Epi (α.app X)] : Epi α
Full source 
/-- A natural transformation is an epimorphism if each component is. -/
theorem epi_of_epi_app (α : F ⟶ G) [∀ X : C, Epi (α.app X)] : Epi α :=
  ⟨fun g h eq => by
    ext X
    rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]⟩
Componentwise Epimorphism Implies Natural Transformation Epimorphism
Informal description
A natural transformation $\alpha \colon F \to G$ between functors $F, G \colon \mathcal{C} \to \mathcal{D}$ is an epimorphism in the functor category if each component $\alpha_X \colon F(X) \to G(X)$ is an epimorphism in $\mathcal{D}$ for every object $X$ in $\mathcal{C}$.
CategoryTheory.NatTrans.id_comm theorem
(α β : (𝟭 C) ⟶ (𝟭 C)) : α ≫ β = β ≫ α
Full source 
/-- The monoid of natural transformations of the identity is commutative. -/
lemma id_comm (α β : (𝟭 C) ⟶ (𝟭 C)) : α ≫ β = β ≫ α := by
  ext X
  exact (α.naturality (β.app X)).symm
Commutativity of Natural Transformations of the Identity Functor
Informal description
For any two natural transformations $\alpha, \beta$ of the identity functor $\mathbf{1}_C$ on a category $C$, the composition $\alpha \circ \beta$ is equal to $\beta \circ \alpha$.
CategoryTheory.NatTrans.hcomp definition
{H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ H ⟶ G ⋙ I
Full source 
/-- `hcomp α β` is the horizontal composition of natural transformations. -/
@[simps]
def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ HF ⋙ H ⟶ G ⋙ I where
  app := fun X : C => β.app (F.obj X) ≫ I.map (α.app X)
  naturality X Y f := by
    rw [Functor.comp_map, Functor.comp_map, ← assoc, naturality, assoc, ← map_comp I, naturality,
      map_comp, assoc]
Horizontal composition of natural transformations
Informal description
Given natural transformations $\alpha \colon F \to G$ and $\beta \colon H \to I$ between functors $F, G \colon C \to D$ and $H, I \colon D \to E$ respectively, the horizontal composition $\alpha \square \beta$ is a natural transformation from $F \circ H$ to $G \circ I$ defined componentwise as follows: for each object $X$ in $C$, the component $(\alpha \square \beta)_X$ is given by the composition $\beta_{F(X)} \circ I(\alpha_X)$ in $E$.
CategoryTheory.NatTrans.term_◫_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Notation for horizontal composition of natural transformations. -/
infixl:80 " ◫ " => hcomp
Horizontal composition of natural transformations
Informal description
The notation `◫` represents horizontal composition of natural transformations between functors. Given natural transformations `α : F ⟶ G` and `β : H ⟶ I`, where `F, G : C ⥤ D` and `H, I : D ⥤ E` are functors between categories, the horizontal composition `α ◫ β` is a natural transformation from `F ⋙ H` to `G ⋙ I` (where `⋙` denotes functor composition).
CategoryTheory.NatTrans.hcomp_id_app theorem
{H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X)
Full source 
theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) := by
  simp
Horizontal composition with identity natural transformation: $(\alpha \square \text{id}_H)_X = H(\alpha_X)$
Informal description
For any natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to D$, and any functor $H \colon D \to E$, the horizontal composition $\alpha \square \text{id}_H$ satisfies that for every object $X$ in $C$, the component at $X$ is given by $(\alpha \square \text{id}_H)_X = H(\alpha_X)$.
CategoryTheory.NatTrans.id_hcomp_app theorem
{H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _
Full source 
theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙𝟙 H ◫ α).app X = α.app _ := by simp
Identity Horizontal Composition Property: $(\text{id}_H \square \alpha)_X = \alpha_{H(X)}$
Informal description
For any natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to D$, and any functor $H \colon E \to C$, the horizontal composition of the identity natural transformation $\text{id}_H$ with $\alpha$ satisfies $(\text{id}_H \square \alpha)_X = \alpha_{H(X)}$ for every object $X$ in $E$.
CategoryTheory.NatTrans.exchange theorem
{I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) : (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ
Full source 
theorem exchange {I J K : D ⥤ E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :
    (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ := by
  aesop_cat
Exchange Law for Horizontal and Vertical Composition of Natural Transformations
Informal description
Given natural transformations $\alpha \colon F \to G$, $\beta \colon G \to H$ between functors $F, G, H \colon C \to D$, and $\gamma \colon I \to J$, $\delta \colon J \to K$ between functors $I, J, K \colon D \to E$, the following diagram commutes: $$(\alpha \circ \beta) \square (\gamma \circ \delta) = (\alpha \square \gamma) \circ (\beta \square \delta)$$ where $\square$ denotes horizontal composition and $\circ$ denotes vertical composition of natural transformations.
CategoryTheory.Functor.flip definition
(F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E
Full source 
/-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/
@[simps]
protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
  obj k :=
    { obj := fun j => (F.obj j).obj k,
      map := fun f => (F.map f).app k, }
  map f := { app := fun j => (F.obj j).map f }
Flipped bifunctor
Informal description
Given a bifunctor \( F \colon \mathcal{C} \to (\mathcal{D} \to \mathcal{E}) \), the flipped bifunctor \( \text{flip } F \colon \mathcal{D} \to (\mathcal{C} \to \mathcal{E}) \) is defined by: - On objects: For each \( k \in \mathcal{D} \), \( (\text{flip } F).obj\, k \) is the functor sending \( j \in \mathcal{C} \) to \( (F.obj\, j).obj\, k \). - On morphisms: For each \( f \colon k \to k' \) in \( \mathcal{D} \), \( (\text{flip } F).map\, f \) is the natural transformation whose component at \( j \in \mathcal{C} \) is \( (F.obj\, j).map\, f \).
CategoryTheory.Functor.leftUnitor definition
(F : C ⥤ D) : 𝟭 C ⋙ F ≅ F
Full source 
/-- The left unitor, a natural isomorphism `((𝟭 _) ⋙ F) ≅ F`.
-/
@[simps]
def leftUnitor (F : C ⥤ D) :
    𝟭𝟭 C ⋙ F𝟭 C ⋙ F ≅ F where
  hom := { app := fun X => 𝟙 (F.obj X) }
  inv := { app := fun X => 𝟙 (F.obj X) }
Left unitor for functor composition
Informal description
For any functor \( F : \mathcal{C} \to \mathcal{D} \), the left unitor is a natural isomorphism between the composition of the identity functor \( \mathbf{1}_{\mathcal{C}} \) with \( F \) and \( F \) itself. Specifically, it consists of: - A natural transformation \( \alpha : \mathbf{1}_{\mathcal{C}} \circ F \Rightarrow F \) where each component \( \alpha_X \) is the identity morphism \( \text{id}_{F(X)} \) for every object \( X \) in \( \mathcal{C} \). - An inverse natural transformation \( \alpha^{-1} : F \Rightarrow \mathbf{1}_{\mathcal{C}} \circ F \) where each component \( \alpha^{-1}_X \) is also the identity morphism \( \text{id}_{F(X)} \). This isomorphism satisfies \( \alpha \circ \alpha^{-1} = \text{id}_F \) and \( \alpha^{-1} \circ \alpha = \text{id}_{\mathbf{1}_{\mathcal{C}} \circ F} \).
CategoryTheory.Functor.rightUnitor definition
(F : C ⥤ D) : F ⋙ 𝟭 D ≅ F
Full source 
/-- The right unitor, a natural isomorphism `(F ⋙ (𝟭 B)) ≅ F`.
-/
@[simps]
def rightUnitor (F : C ⥤ D) :
    F ⋙ 𝟭 DF ⋙ 𝟭 D ≅ F where
  hom := { app := fun X => 𝟙 (F.obj X) }
  inv := { app := fun X => 𝟙 (F.obj X) }
Right unitor for functor composition
Informal description
For any functor \( F : \mathcal{C} \to \mathcal{D} \), the right unitor is a natural isomorphism between the composition \( F \circ \text{id}_\mathcal{D} \) and \( F \) itself. The components of this isomorphism at each object \( X \) in \( \mathcal{C} \) are given by the identity morphism \( \text{id}_{F(X)} \) in \( \mathcal{D} \).
CategoryTheory.Functor.associator definition
(F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') : (F ⋙ G) ⋙ H ≅ F ⋙ G ⋙ H
Full source 
/-- The associator for functors, a natural isomorphism `((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H))`.

(In fact, `iso.refl _` will work here, but it tends to make Lean slow later,
and it's usually best to insert explicit associators.)
-/
@[simps]
def associator (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') :
    (F ⋙ G) ⋙ H(F ⋙ G) ⋙ H ≅ F ⋙ G ⋙ H where
  hom := { app := fun _ => 𝟙 _ }
  inv := { app := fun _ => 𝟙 _ }
Associator for functor composition
Informal description
For any functors \( F : \mathcal{C} \to \mathcal{D} \), \( G : \mathcal{D} \to \mathcal{E} \), and \( H : \mathcal{E} \to \mathcal{E}' \), the associator is a natural isomorphism between the functors \( (F \circ G) \circ H \) and \( F \circ (G \circ H) \), where \( \circ \) denotes functor composition. The components of this isomorphism are identity morphisms in the target category \( \mathcal{E}' \).
CategoryTheory.Functor.assoc theorem
(F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') : (F ⋙ G) ⋙ H = F ⋙ G ⋙ H
Full source 
protected theorem assoc (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') : (F ⋙ G) ⋙ H = F ⋙ G ⋙ H :=
  rfl
Associativity of Functor Composition: $(F \circ G) \circ H = F \circ (G \circ H)$
Informal description
For any functors $F \colon C \to D$, $G \colon D \to E$, and $H \colon E \to E'$, the composition of functors is associative, i.e., $(F \circ G) \circ H = F \circ (G \circ H)$.
CategoryTheory.flipFunctor definition
: (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E
Full source 
/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/
@[simps]
def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where
  obj F := F.flip
  map {F₁ F₂} φ :=
    { app := fun Y =>
        { app := fun X => (φ.app X).app Y
          naturality := fun X₁ X₂ f => by
            dsimp
            simp only [← NatTrans.comp_app, naturality] } }
Flip Functor for Bifunctors
Informal description
The functor $\text{flipFunctor} \colon (\mathcal{C} \to (\mathcal{D} \to \mathcal{E})) \to (\mathcal{D} \to (\mathcal{C} \to \mathcal{E}))$ transforms a bifunctor $F \colon \mathcal{C} \to (\mathcal{D} \to \mathcal{E})$ into its flipped version $\text{flip } F \colon \mathcal{D} \to (\mathcal{C} \to \mathcal{E})$. For any bifunctor $F$, the flipped functor $\text{flip } F$ is defined by: - On objects: For each $Y \in \mathcal{D}$, $(\text{flip } F)(Y)$ is the functor sending $X \in \mathcal{C}$ to $F(X)(Y)$. - On morphisms: For each natural transformation $\varphi \colon F_1 \to F_2$ between bifunctors, $\text{flipFunctor}(\varphi)$ is the natural transformation whose component at $Y \in \mathcal{D}$ is the natural transformation with components $\varphi(X)(Y)$ for each $X \in \mathcal{C}$.
CategoryTheory.Iso.map_hom_inv_id_app theorem
{X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) : (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _
Full source 
@[reassoc (attr := simp)]
theorem map_hom_inv_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
    (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _ := by
  simp [← NatTrans.comp_app, ← Functor.map_comp]
Functoriality of Isomorphism Components: Hom-Inverse Composition Yields Identity
Informal description
For any isomorphism $e \colon X \cong Y$ in category $\mathcal{C}$ and any functor $F \colon \mathcal{C} \to (\mathcal{D} \to \mathcal{E})$, the composition of the component morphisms $(F(e.hom)).app_Z$ and $(F(e.inv)).app_Z$ at any object $Z$ in $\mathcal{D}$ equals the identity morphism on $F(X)(Z)$. That is, $$(F(e.hom)).app_Z \circ (F(e.inv)).app_Z = id_{F(X)(Z)}.$$
CategoryTheory.Iso.map_inv_hom_id_app theorem
{X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) : (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _
Full source 
@[reassoc (attr := simp)]
theorem map_inv_hom_id_app {X Y : C} (e : X ≅ Y) (F : C ⥤ D ⥤ E) (Z : D) :
    (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _ := by
  simp [← NatTrans.comp_app, ← Functor.map_comp]
Functoriality of Isomorphism Components: Inverse-Hom Composition Yields Identity
Informal description
For any isomorphism $e \colon X \cong Y$ in a category $\mathcal{C}$ and any functor $F \colon \mathcal{C} \to (\mathcal{D} \to \mathcal{E})$, the composition of the component morphisms $(F(e.inv)).app_Z$ and $(F(e.hom)).app_Z$ at any object $Z$ in $\mathcal{D}$ equals the identity morphism on $F(Y)(Z)$. That is, $$(F(e.inv)).app_Z \circ (F(e.hom)).app_Z = id_{F(Y)(Z)}.$$