doc-next-gen

Mathlib.CategoryTheory.NatIso

Module docstring

{"# Natural isomorphisms

For the most part, natural isomorphisms are just another sort of isomorphism.

We provide some special support for extracting components: * if α : F ≅ G, then a.app X : F.obj X ≅ G.obj X, and building natural isomorphisms from components: * NatIso.ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) : F ≅ G only needing to check naturality in one direction.

Implementation

Note that NatIso is a namespace without a corresponding definition; we put some declarations that are specifically about natural isomorphisms in the Iso namespace so that they are available using dot notation. ","Unfortunately we need a separate set of cancellation lemmas for components of natural isomorphisms, because the simp normal form is α.hom.app X, rather than α.app.hom X.

(With the latter, the morphism would be visibly part of an isomorphism, so general lemmas about isomorphisms would apply.)

In the future, we should consider a redesign that changes this simp norm form, but for now it breaks too many proofs. "}

CategoryTheory.Iso.app definition
{F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X
Full source 
/-- The application of a natural isomorphism to an object. We put this definition in a different
namespace, so that we can use `α.app` -/
@[simps]
def app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
    F.obj X ≅ G.obj X where
  hom := α.hom.app X
  inv := α.inv.app X
  hom_inv_id := by rw [← comp_app, Iso.hom_inv_id]; rfl
  inv_hom_id := by rw [← comp_app, Iso.inv_hom_id]; rfl
Component of a natural isomorphism
Informal description
Given a natural isomorphism $\alpha : F \cong G$ between functors $F, G : C \to D$ and an object $X$ in $C$, the component $\alpha.app\ X$ is an isomorphism $F(X) \cong G(X)$ in $D$, where the morphisms are given by $\alpha.hom.app\ X$ and $\alpha.inv.app\ X$, satisfying the isomorphism conditions.
CategoryTheory.Iso.hom_inv_id_app theorem
{F G : C ⥤ D} (α : F ≅ G) (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)
Full source 
@[reassoc (attr := simp)]
theorem hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
    α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
  congr_fun (congr_arg NatTrans.app α.hom_inv_id) X
Natural isomorphism components satisfy hom-inverse composition identity
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the composition of the component morphisms $\alpha.hom.app\ X \colon F(X) \to G(X)$ and $\alpha.inv.app\ X \colon G(X) \to F(X)$ equals the identity morphism on $F(X)$, i.e., $\alpha.hom.app\ X \circ \alpha.inv.app\ X = id_{F(X)}$.
CategoryTheory.Iso.inv_hom_id_app theorem
{F G : C ⥤ D} (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)
Full source 
@[reassoc (attr := simp)]
theorem inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
    α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
  congr_fun (congr_arg NatTrans.app α.inv_hom_id) X
Inverse-Hom Identity for Components of Natural Isomorphism
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the composition of the inverse component $\alpha^{-1}.app\ X$ followed by the forward component $\alpha.hom.app\ X$ is equal to the identity morphism on $G(X)$, i.e., $\alpha^{-1}.app\ X \circ \alpha.hom.app\ X = \mathrm{id}_{G(X)}$.
CategoryTheory.Iso.hom_inv_id_app_app theorem
{F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) : (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma hom_inv_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
    (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _ := by
  rw [← NatTrans.comp_app, Iso.hom_inv_id_app, NatTrans.id_app]
Component-wise Hom-Inverse Identity for Bifunctor Natural Isomorphism
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to (D \to E)$ and any objects $X_1$ in $C$ and $X_2$ in $D$, the composition of the component morphisms $(e.hom.app\ X_1).app\ X_2 \colon F(X_1)(X_2) \to G(X_1)(X_2)$ and $(e.inv.app\ X_1).app\ X_2 \colon G(X_1)(X_2) \to F(X_1)(X_2)$ equals the identity morphism on $F(X_1)(X_2)$, i.e., $(e.hom.app\ X_1).app\ X_2 \circ (e.inv.app\ X_1).app\ X_2 = id_{F(X_1)(X_2)}$.
CategoryTheory.Iso.inv_hom_id_app_app theorem
{F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) : (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma inv_hom_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
    (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _ := by
  rw [← NatTrans.comp_app, Iso.inv_hom_id_app, NatTrans.id_app]
Inverse-Hom Identity for Components of Bifunctor Natural Isomorphism
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to D \to E$ and any objects $X_1$ in $C$ and $X_2$ in $D$, the composition of the inverse component $(e^{-1}.app\ X_1).app\ X_2$ followed by the forward component $(e.hom.app\ X_1).app\ X_2$ is equal to the identity morphism on $G(X_1)(X_2)$, i.e., $(e^{-1}.app\ X_1).app\ X_2 \circ (e.hom.app\ X_1).app\ X_2 = \mathrm{id}_{G(X_1)(X_2)}$.
CategoryTheory.Iso.hom_inv_id_app_app_app theorem
{F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) : ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma hom_inv_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G)
    (X₁ : C) (X₂ : D) (X₃ : E) :
    ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 _ := by
  rw [← NatTrans.comp_app, ← NatTrans.comp_app, Iso.hom_inv_id_app,
    NatTrans.id_app, NatTrans.id_app]
Natural isomorphism components satisfy hom-inverse composition identity for triply-nested functors
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to D \to E \to E'$ and any objects $X_1 \in C$, $X_2 \in D$, $X_3 \in E$, the composition of the component morphisms $((e.hom.app\ X_1).app\ X_2).app\ X_3$ and $((e.inv.app\ X_1).app\ X_2).app\ X_3$ equals the identity morphism on $F(X_1)(X_2)(X_3)$, i.e., \[ ((e.hom.app\ X_1).app\ X_2).app\ X_3 \circ ((e.inv.app\ X_1).app\ X_2).app\ X_3 = id_{F(X_1)(X_2)(X_3)}. \]
CategoryTheory.Iso.inv_hom_id_app_app_app theorem
{F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) : ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma inv_hom_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G)
    (X₁ : C) (X₂ : D) (X₃ : E) :
    ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 _ := by
  rw [← NatTrans.comp_app, ← NatTrans.comp_app, Iso.inv_hom_id_app,
    NatTrans.id_app, NatTrans.id_app]
Inverse-Hom Identity for Triple-Component Natural Isomorphism
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to D \to E \to E'$ and objects $X_1 \in C$, $X_2 \in D$, $X_3 \in E$, the composition of the inverse component $((e^{-1}).app\ X_1).app\ X_2).app\ X_3$ followed by the forward component $((e.hom.app\ X_1).app\ X_2).app\ X_3$ is equal to the identity morphism on the object obtained by applying $G$ to $X_1$, $X_2$, and $X_3$, i.e., $$((e^{-1}).app\ X_1).app\ X_2).app\ X_3 \circ ((e.hom.app\ X_1).app\ X_2).app\ X_3 = \mathrm{id}_{G(X_1)(X_2)(X_3)}.$$
CategoryTheory.NatIso.trans_app theorem
{F G H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) (X : C) : (α ≪≫ β).app X = α.app X ≪≫ β.app X
Full source 
@[simp]
theorem trans_app {F G H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) (X : C) :
    (α ≪≫ β).app X = α.app X ≪≫ β.app X :=
  rfl
Component-wise Composition of Natural Isomorphisms
Informal description
For any natural isomorphisms $\alpha \colon F \cong G$ and $\beta \colon G \cong H$ between functors $F, G, H \colon C \to D$, and for any object $X$ in $C$, the component of the composition $\alpha \circ \beta$ at $X$ is equal to the composition of the components $\alpha.app\ X$ and $\beta.app\ X$, i.e., $$(\alpha \circ \beta).app\ X = \alpha.app\ X \circ \beta.app\ X.$$
CategoryTheory.NatIso.app_hom theorem
{F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.app X
Full source 
@[deprecated Iso.app_hom (since := "2025-03-11")]
theorem app_hom {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.app X :=
  rfl
Homomorphism Component of Natural Isomorphism Application
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the homomorphism component of the isomorphism $\alpha.app\ X \colon F(X) \cong G(X)$ is equal to the component $\alpha.hom.app\ X \colon F(X) \to G(X)$. In other words, $(\alpha.app\ X).hom = \alpha.hom.app\ X$.
CategoryTheory.NatIso.app_inv theorem
{F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.app X
Full source 
@[deprecated Iso.app_hom (since := "2025-03-11")]
theorem app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.app X :=
  rfl
Inverse of Natural Isomorphism Component Equals Component of Inverse
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the inverse of the component isomorphism $\alpha.app\ X$ is equal to the component of the inverse natural isomorphism $\alpha.inv.app\ X$.
CategoryTheory.NatIso.hom_app_isIso instance
(α : F ≅ G) (X : C) : IsIso (α.hom.app X)
Full source 
instance hom_app_isIso (α : F ≅ G) (X : C) : IsIso (α.hom.app X) :=
  ⟨⟨α.inv.app X,
    ⟨by rw [← comp_app, Iso.hom_inv_id, ← id_app], by rw [← comp_app, Iso.inv_hom_id, ← id_app]⟩⟩⟩
Components of Natural Isomorphisms are Isomorphisms
Informal description
For any natural isomorphism $\alpha : F \cong G$ between functors $F, G : C \to D$ and any object $X$ in $C$, the component $\alpha.hom.app X : F(X) \to G(X)$ is an isomorphism in $D$.
CategoryTheory.NatIso.inv_app_isIso instance
(α : F ≅ G) (X : C) : IsIso (α.inv.app X)
Full source 
instance inv_app_isIso (α : F ≅ G) (X : C) : IsIso (α.inv.app X) :=
  ⟨⟨α.hom.app X,
    ⟨by rw [← comp_app, Iso.inv_hom_id, ← id_app], by rw [← comp_app, Iso.hom_inv_id, ← id_app]⟩⟩⟩
Inverse Components of Natural Isomorphisms are Isomorphisms
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the component $\alpha^{-1}.app(X) \colon G(X) \to F(X)$ is an isomorphism.
CategoryTheory.NatIso.cancel_natIso_hom_left theorem
{X : C} {Z : D} (g g' : G.obj X ⟶ Z) : α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'
Full source 
@[simp]
theorem cancel_natIso_hom_left {X : C} {Z : D} (g g' : G.obj X ⟶ Z) :
    α.hom.app X ≫ gα.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g' := by simp only [cancel_epi, refl]
Left Cancellation Property for Components of Natural Isomorphisms
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$, any object $X$ in $C$, and any morphisms $g, g' \colon G(X) \to Z$ in $D$, we have $\alpha_{\mathrm{hom},X} \circ g = \alpha_{\mathrm{hom},X} \circ g'$ if and only if $g = g'$.
CategoryTheory.NatIso.cancel_natIso_inv_left theorem
{X : C} {Z : D} (g g' : F.obj X ⟶ Z) : α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'
Full source 
@[simp]
theorem cancel_natIso_inv_left {X : C} {Z : D} (g g' : F.obj X ⟶ Z) :
    α.inv.app X ≫ gα.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g' := by simp only [cancel_epi, refl]
Left Cancellation Property for Inverse Components of Natural Isomorphisms
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$, any object $X$ in $C$, and any morphisms $g, g' \colon F(X) \to Z$ in $D$, the compositions $\alpha^{-1}.app(X) \circ g$ and $\alpha^{-1}.app(X) \circ g'$ are equal if and only if $g = g'$.
CategoryTheory.NatIso.cancel_natIso_hom_right theorem
{X : D} {Y : C} (f f' : X ⟶ F.obj Y) : f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'
Full source 
@[simp]
theorem cancel_natIso_hom_right {X : D} {Y : C} (f f' : X ⟶ F.obj Y) :
    f ≫ α.hom.app Yf ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f' := by simp only [cancel_mono, refl]
Cancellation of morphisms through natural isomorphism components: $f \circ \alpha_Y = f' \circ \alpha_Y \leftrightarrow f = f'$
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$, any object $Y$ in $C$, and any morphisms $f, f' \colon X \to F(Y)$ in $D$, the equality $f \circ \alpha.hom_Y = f' \circ \alpha.hom_Y$ holds if and only if $f = f'$.
CategoryTheory.NatIso.cancel_natIso_inv_right theorem
{X : D} {Y : C} (f f' : X ⟶ G.obj Y) : f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f'
Full source 
@[simp]
theorem cancel_natIso_inv_right {X : D} {Y : C} (f f' : X ⟶ G.obj Y) :
    f ≫ α.inv.app Yf ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f' := by simp only [cancel_mono, refl]
Cancellation Property for Post-Composition with Inverse Components of Natural Isomorphisms
Informal description
For any natural isomorphism $\alpha \colon F \cong G$ between functors $F, G \colon C \to D$, objects $X$ in $D$ and $Y$ in $C$, and morphisms $f, f' \colon X \to G(Y)$, we have the equivalence: $$f \circ \alpha^{-1}.app(Y) = f' \circ \alpha^{-1}.app(Y) \quad \text{if and only if} \quad f = f'.$$
CategoryTheory.NatIso.cancel_natIso_hom_right_assoc theorem
{W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y) (f' : W ⟶ X') (g' : X' ⟶ F.obj Y) : f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'
Full source 
@[simp]
theorem cancel_natIso_hom_right_assoc {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y)
    (f' : W ⟶ X') (g' : X' ⟶ F.obj Y) :
    f ≫ g ≫ α.hom.app Yf ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono, refl]
Cancellation of Natural Isomorphism Components in Composition (Hom Version)
Informal description
Let $F, G : C \to D$ be functors with a natural isomorphism $\alpha : F \cong G$. For any objects $W, X, X'$ in $D$ and $Y$ in $C$, and morphisms $f : W \to X$, $g : X \to F(Y)$, $f' : W \to X'$, $g' : X' \to F(Y)$, the composition $f \circ g \circ \alpha.hom_Y$ equals $f' \circ g' \circ \alpha.hom_Y$ if and only if $f \circ g$ equals $f' \circ g'$.
CategoryTheory.NatIso.cancel_natIso_inv_right_assoc theorem
{W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ G.obj Y) (f' : W ⟶ X') (g' : X' ⟶ G.obj Y) : f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'
Full source 
@[simp]
theorem cancel_natIso_inv_right_assoc {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ G.obj Y)
    (f' : W ⟶ X') (g' : X' ⟶ G.obj Y) :
    f ≫ g ≫ α.inv.app Yf ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g' := by
  simp only [← Category.assoc, cancel_mono, refl]
Cancellation of Natural Isomorphism Inverse Components in Composition
Informal description
Let $F, G \colon C \to D$ be functors with a natural isomorphism $\alpha \colon F \cong G$. For any objects $W, X, X'$ in $D$ and $Y$ in $C$, and morphisms $f \colon W \to X$, $g \colon X \to G(Y)$, $f' \colon W \to X'$, $g' \colon X' \to G(Y)$, the following equivalence holds: \[ f \circ g \circ \alpha^{-1}.app(Y) = f' \circ g' \circ \alpha^{-1}.app(Y) \iff f \circ g = f' \circ g'. \]
CategoryTheory.NatIso.inv_inv_app theorem
{F G : C ⥤ D} (e : F ≅ G) (X : C) : inv (e.inv.app X) = e.hom.app X
Full source 
@[simp]
theorem inv_inv_app {F G : C ⥤ D} (e : F ≅ G) (X : C) : inv (e.inv.app X) = e.hom.app X := by
  aesop_cat
Double Inverse of Natural Isomorphism Component Equals Forward Component
Informal description
For any natural isomorphism $e \colon F \cong G$ between functors $F, G \colon C \to D$ and any object $X$ in $C$, the inverse of the inverse component $e^{-1}.app\ X$ is equal to the forward component $e.hom.app\ X$, i.e., $(e^{-1}.app\ X)^{-1} = e.hom.app\ X$.
CategoryTheory.NatIso.naturality_1 theorem
(α : F ≅ G) (f : X ⟶ Y) : α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f
Full source 
theorem naturality_1 (α : F ≅ G) (f : X ⟶ Y) : α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f := by
  simp
Naturality condition for components of a natural isomorphism (first variant)
Informal description
Let $F, G \colon C \to D$ be functors and $\alpha \colon F \cong G$ be a natural isomorphism. Then for any morphism $f \colon X \to Y$ in $C$, the following diagram commutes: \[ \alpha^{-1}_X \circ F(f) \circ \alpha_Y = G(f) \] where $\alpha_X \colon F(X) \cong G(X)$ denotes the component of $\alpha$ at $X$, and $\alpha^{-1}_X$ is its inverse.
CategoryTheory.NatIso.naturality_2 theorem
(α : F ≅ G) (f : X ⟶ Y) : α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f
Full source 
theorem naturality_2 (α : F ≅ G) (f : X ⟶ Y) : α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f := by
  simp
Naturality condition for inverse components of a natural isomorphism
Informal description
Let $F, G \colon C \to D$ be functors and $\alpha \colon F \cong G$ be a natural isomorphism. Then for any morphism $f \colon X \to Y$ in $C$, the following diagram commutes: \[ \alpha_{\text{hom},X} \circ G(f) \circ \alpha_{\text{inv},Y} = F(f), \] where $\alpha_{\text{hom},X} \colon F(X) \to G(X)$ is the component of the natural isomorphism at $X$, and $\alpha_{\text{inv},Y} \colon G(Y) \to F(Y)$ is its inverse at $Y$.
CategoryTheory.NatIso.naturality_1' theorem
(α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app X)} : inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f
Full source 
theorem naturality_1' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app X)} :
    invinv (α.app X) ≫ F.map f ≫ α.app Y = G.map f := by simp
Naturality condition for isomorphisms in natural transformations (first variant)
Informal description
Let $F, G \colon C \to D$ be functors and $\alpha \colon F \Rightarrow G$ be a natural transformation such that $\alpha_X \colon F(X) \to G(X)$ is an isomorphism for some object $X$ in $C$. Then for any morphism $f \colon X \to Y$ in $C$, the following diagram commutes: \[ (\alpha_X)^{-1} \circ F(f) \circ \alpha_Y = G(f) \] where $(\alpha_X)^{-1}$ denotes the inverse of the isomorphism $\alpha_X$.
CategoryTheory.NatIso.naturality_2' theorem
(α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app Y)} : α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f
Full source 
@[reassoc (attr := simp)]
theorem naturality_2' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app Y)} :
    α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f := by
  rw [← Category.assoc, ← naturality, Category.assoc, IsIso.hom_inv_id, Category.comp_id]
Naturality condition for isomorphisms of functors
Informal description
Let $F$ and $G$ be functors between categories, and let $\alpha : F \to G$ be a natural transformation such that for every object $Y$, the component $\alpha_Y$ is an isomorphism. Then for any morphism $f : X \to Y$, the following diagram commutes: \[ \alpha_X \circ G(f) \circ \alpha_Y^{-1} = F(f). \]
CategoryTheory.NatIso.isIso_app_of_isIso instance
(α : F ⟶ G) [IsIso α] (X) : IsIso (α.app X)
Full source 
/-- The components of a natural isomorphism are isomorphisms.
-/
instance isIso_app_of_isIso (α : F ⟶ G) [IsIso α] (X) : IsIso (α.app X) :=
  ⟨⟨(inv α).app X,
      ⟨congr_fun (congr_arg NatTrans.app (IsIso.hom_inv_id α)) X,
        congr_fun (congr_arg NatTrans.app (IsIso.inv_hom_id α)) X⟩⟩⟩
Components of Natural Isomorphisms are Isomorphisms
Informal description
For any natural isomorphism $\alpha : F \to G$ between functors $F$ and $G$ in a category, and for any object $X$ in the domain category, the component $\alpha.app X : F(X) \to G(X)$ is an isomorphism.
CategoryTheory.NatIso.isIso_inv_app theorem
(α : F ⟶ G) {_ : IsIso α} (X) : (inv α).app X = inv (α.app X)
Full source 
@[simp]
theorem isIso_inv_app (α : F ⟶ G) {_ : IsIso α} (X) : (inv α).app X = inv (α.app X) := by
  -- Porting note: the next lemma used to be in `ext`, but that is no longer allowed.
  -- We've added an aesop apply rule;
  -- it would be nice to have a hook to run those without aesop warning it didn't close the goal.
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← NatTrans.comp_app]
  simp
Inverse Components of Natural Isomorphisms are Component Inverses
Informal description
For any natural isomorphism $\alpha : F \to G$ between functors $F$ and $G$ in a category, and for any object $X$ in the domain category, the component of the inverse natural transformation $\alpha^{-1}$ at $X$ is equal to the inverse of the component $\alpha_X$, i.e., $(\alpha^{-1})_X = (\alpha_X)^{-1}$.
CategoryTheory.NatIso.inv_map_inv_app theorem
(F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) : inv ((F.map e.inv).app Z) = (F.map e.hom).app Z
Full source 
@[simp]
theorem inv_map_inv_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :
    inv ((F.map e.inv).app Z) = (F.map e.hom).app Z := by
  aesop_cat
Inverse of Functor-Applied Isomorphism Component Equals Forward Component
Informal description
Let $F : C \to D \to E$ be a functor between categories, and let $e : X \cong Y$ be an isomorphism in $C$. For any object $Z$ in $D$, the inverse of the component $(F(e^{-1})).app Z$ is equal to the component $(F(e)).app Z$.
CategoryTheory.NatIso.ofComponents.app theorem
(app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) : (ofComponents app' naturality).app X = app' X
Full source 
@[simp]
theorem ofComponents.app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
    (ofComponents app' naturality).app X = app' X := by aesop
Component Equality in Natural Isomorphism Construction
Informal description
Given a family of isomorphisms $\{ \alpha_X : F(X) \cong G(X) \}_{X \in C}$ between functors $F, G : C \to D$ and a naturality condition, the component at $X$ of the natural isomorphism constructed via `NatIso.ofComponents` equals $\alpha_X$.
CategoryTheory.NatIso.isIso_of_isIso_app theorem
(α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso α
Full source 
/-- A natural transformation is an isomorphism if all its components are isomorphisms.
-/
theorem isIso_of_isIso_app (α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso α :=
  (ofComponents (fun X => asIso (α.app X)) (by simp)).isIso_hom
Natural transformation is an isomorphism if all components are isomorphisms
Informal description
Let $F, G : C \to D$ be functors between categories, and let $\alpha : F \to G$ be a natural transformation. If for every object $X$ in $C$, the component $\alpha_X : F(X) \to G(X)$ is an isomorphism, then $\alpha$ itself is a natural isomorphism.
CategoryTheory.NatIso.hcomp definition
{F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I
Full source 
/-- Horizontal composition of natural isomorphisms. -/
@[simps]
def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ HF ⋙ H ≅ G ⋙ I := by
  refine ⟨α.hom ◫ β.hom, α.inv ◫ β.inv, ?_, ?_⟩
  · ext
    rw [← NatTrans.exchange]
    simp
  ext; rw [← NatTrans.exchange]; simp
Horizontal composition of natural isomorphisms
Informal description
Given categories $C$, $D$, and $E$, functors $F,G: C \rightrightarrows D$, and $H,I: D \rightrightarrows E$, and natural isomorphisms $\alpha: F \cong G$ and $\beta: H \cong I$, the horizontal composition $\alpha \square \beta$ is a natural isomorphism between the composed functors $F \circ H \cong G \circ I$.
CategoryTheory.NatIso.isIso_map_iff theorem
{F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) : IsIso (F₁.map f) ↔ IsIso (F₂.map f)
Full source 
theorem isIso_map_iff {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) :
    IsIsoIsIso (F₁.map f) ↔ IsIso (F₂.map f) := by
  revert F₁ F₂
  suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) by
    exact fun F₁ F₂ e => ⟨this e, this e.symm⟩
  intro F₁ F₂ e hf
  refine IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, ?_, ?_⟩
  · simp only [NatTrans.naturality_assoc, IsIso.hom_inv_id_assoc, Iso.inv_hom_id_app]
  · simp only [assoc, ← e.hom.naturality, IsIso.inv_hom_id_assoc, Iso.inv_hom_id_app]
Natural Isomorphism Preserves Isomorphism Property of Morphisms
Informal description
Given two functors $F_1, F_2 \colon C \to D$ and a natural isomorphism $e \colon F_1 \cong F_2$, for any morphism $f \colon X \to Y$ in $C$, the morphism $F_1(f)$ is an isomorphism if and only if $F_2(f)$ is an isomorphism.
CategoryTheory.NatTrans.isIso_iff_isIso_app theorem
{F G : C ⥤ D} (τ : F ⟶ G) : IsIso τ ↔ ∀ X, IsIso (τ.app X)
Full source 
lemma NatTrans.isIso_iff_isIso_app {F G : C ⥤ D} (τ : F ⟶ G) :
    IsIsoIsIso τ ↔ ∀ X, IsIso (τ.app X) :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ NatIso.isIso_of_isIso_app _⟩
Natural Transformation is Isomorphism if and only if All Components are Isomorphisms
Informal description
For any natural transformation $\tau \colon F \to G$ between functors $F, G \colon C \to D$, $\tau$ is a natural isomorphism if and only if for every object $X$ in $C$, the component $\tau_X \colon F(X) \to G(X)$ is an isomorphism.
CategoryTheory.Functor.copyObj definition
: C ⥤ D
Full source 
/-- Constructor for a functor that is isomorphic to a given functor `F : C ⥤ D`,
while being definitionally equal on objects to a given map `obj : C → D`
such that for all `X : C`, we have an isomorphism `F.obj X ≅ obj X`. -/
@[simps obj]
def copyObj : C ⥤ D where
  obj := obj
  map f := (e _).inv ≫ F.map f ≫ (e _).hom
Functor isomorphic copy with specified object map
Informal description
Given a functor \( F : C \to D \) and a map \( \text{obj} : C \to D \) such that for every object \( X \) in \( C \), there is an isomorphism \( F(X) \cong \text{obj}(X) \), this constructor produces a new functor that is isomorphic to \( F \) and has object map equal to \( \text{obj} \). The morphism map is defined by \( f \mapsto e(X)^{-1} \circ F(f) \circ e(Y) \) for any morphism \( f : X \to Y \), where \( e(X) : F(X) \cong \text{obj}(X) \) is the given isomorphism.
CategoryTheory.Functor.isoCopyObj definition
: F ≅ F.copyObj obj e
Full source 
/-- The functor constructed with `copyObj` is isomorphic to the given functor. -/
@[simps!]
def isoCopyObj : F ≅ F.copyObj obj e :=
  NatIso.ofComponents e (by simp [Functor.copyObj])
Natural isomorphism between a functor and its isomorphic copy
Informal description
Given a functor \( F : C \to D \), a map \( \text{obj} : C \to D \), and for each object \( X \) in \( C \) an isomorphism \( e(X) : F(X) \cong \text{obj}(X) \), the natural isomorphism \( F \cong F.\text{copyObj obj e} \) is constructed using the components \( e \) and satisfies the naturality condition \( F(f) \circ e(Y) = e(X) \circ (F.\text{copyObj obj e})(f) \) for any morphism \( f : X \to Y \).