Documentation

Mathlib.CategoryTheory.NatIso

Natural isomorphisms #

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

We provide some special support for extracting 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.

source
def CategoryTheory.Iso.app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
F.obj X ≅ G.obj X

The application of a natural isomorphism to an object. We put this definition in a different namespace, so that we can use α.app

Equations
  • α.app X = { hom := α.hom.app X, inv := α.inv.app X, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
    source
    @[simp]
    theorem CategoryTheory.Iso.app_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    (α.app X).inv = α.inv.app X
    source
    @[simp]
    theorem CategoryTheory.Iso.app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    (α.app X).hom = α.hom.app X
    source
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    CategoryStruct.comp (α.hom.app X) (α.inv.app X) = CategoryStruct.id (F.obj X)
    source
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) {Z : D} (h : F.obj X ⟶ Z) :
    CategoryStruct.comp (α.hom.app X) (CategoryStruct.comp (α.inv.app X) h) = h
    source
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    CategoryStruct.comp (α.inv.app X) (α.hom.app X) = CategoryStruct.id (G.obj X)
    source
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) {Z : D} (h : G.obj X ⟶ Z) :
    CategoryStruct.comp (α.inv.app X) (CategoryStruct.comp (α.hom.app X) h) = h
    source
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) :
    CategoryStruct.comp ((e.hom.app X₁).app X₂) ((e.inv.app X₁).app X₂) = CategoryStruct.id ((F.obj X₁).obj X₂)
    source
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_app_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) {Z : E} (h : (F.obj X₁).obj X₂ ⟶ Z) :
    CategoryStruct.comp ((e.hom.app X₁).app X₂) (CategoryStruct.comp ((e.inv.app X₁).app X₂) h) = h
    source
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) :
    CategoryStruct.comp ((e.inv.app X₁).app X₂) ((e.hom.app X₁).app X₂) = CategoryStruct.id ((G.obj X₁).obj X₂)
    source
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_app_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) {Z : E} (h : (G.obj X₁).obj X₂ ⟶ Z) :
    CategoryStruct.comp ((e.inv.app X₁).app X₂) (CategoryStruct.comp ((e.hom.app X₁).app X₂) h) = h
    source
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_app_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {F G : Functor C (Functor D (Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) :
    CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) (((e.inv.app X₁).app X₂).app X₃) = CategoryStruct.id (((F.obj X₁).obj X₂).obj X₃)
    source
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_app_app_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {F G : Functor C (Functor D (Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) {Z : E'} (h : ((F.obj X₁).obj X₂).obj X₃ ⟶ Z) :
    CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) (CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) h) = h
    source
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_app_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {F G : Functor C (Functor D (Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) :
    CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) (((e.hom.app X₁).app X₂).app X₃) = CategoryStruct.id (((G.obj X₁).obj X₂).obj X₃)
    source
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_app_app_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {F G : Functor C (Functor D (Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj X₁).obj X₂).obj X₃ ⟶ Z) :
    CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) (CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) h) = h
    source
    @[simp]
    theorem CategoryTheory.NatIso.trans_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ≅ G) (β : G ≅ H) (X : C) :
    (α ≪≫ β).app X = α.app X ≪≫ β.app X
    source
    @[deprecated CategoryTheory.Iso.app_hom (since := "2025-03-11")]
    theorem CategoryTheory.NatIso.app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    (α.app X).hom = α.hom.app X
    source
    @[deprecated CategoryTheory.Iso.app_hom (since := "2025-03-11")]
    theorem CategoryTheory.NatIso.app_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    (α.app X).inv = α.inv.app X
    source
    instance CategoryTheory.NatIso.hom_app_isIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    IsIso (α.hom.app X)
    source
    instance CategoryTheory.NatIso.inv_app_isIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) (X : C) :
    IsIso (α.inv.app X)

    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.

    source
    @[simp]
    theorem CategoryTheory.NatIso.cancel_natIso_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) {X : C} {Z : D} (g g' : G.obj X ⟶ Z) :
    CategoryStruct.comp (α.hom.app X) g = CategoryStruct.comp (α.hom.app X) g' ↔ g = g'
    source
    @[simp]
    theorem CategoryTheory.NatIso.cancel_natIso_inv_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) {X : C} {Z : D} (g g' : F.obj X ⟶ Z) :
    CategoryStruct.comp (α.inv.app X) g = CategoryStruct.comp (α.inv.app X) g' ↔ g = g'
    source
    @[simp]
    theorem CategoryTheory.NatIso.cancel_natIso_hom_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) {X : D} {Y : C} (f f' : X ⟶ F.obj Y) :
    CategoryStruct.comp f (α.hom.app Y) = CategoryStruct.comp f' (α.hom.app Y) ↔ f = f'
    source
    @[simp]
    theorem CategoryTheory.NatIso.cancel_natIso_inv_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) {X : D} {Y : C} (f f' : X ⟶ G.obj Y) :
    CategoryStruct.comp f (α.inv.app Y) = CategoryStruct.comp f' (α.inv.app Y) ↔ f = f'
    source
    @[simp]
    theorem CategoryTheory.NatIso.cancel_natIso_hom_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ F.obj Y) (f' : W ⟶ X') (g' : X' ⟶ F.obj Y) :
    CategoryStruct.comp f (CategoryStruct.comp g (α.hom.app Y)) = CategoryStruct.comp f' (CategoryStruct.comp g' (α.hom.app Y)) ↔ CategoryStruct.comp f g = CategoryStruct.comp f' g'
    source
    @[simp]
    theorem CategoryTheory.NatIso.cancel_natIso_inv_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ≅ G) {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ G.obj Y) (f' : W ⟶ X') (g' : X' ⟶ G.obj Y) :
    CategoryStruct.comp f (CategoryStruct.comp g (α.inv.app Y)) = CategoryStruct.comp f' (CategoryStruct.comp g' (α.inv.app Y)) ↔ CategoryStruct.comp f g = CategoryStruct.comp f' g'
    source
    @[simp]
    theorem CategoryTheory.NatIso.inv_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) (X : C) :
    inv (e.inv.app X) = e.hom.app X
    source
    theorem CategoryTheory.NatIso.naturality_1 {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) :
    CategoryStruct.comp (α.inv.app X) (CategoryStruct.comp (F.map f) (α.hom.app Y)) = G.map f
    source
    theorem CategoryTheory.NatIso.naturality_2 {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) :
    CategoryStruct.comp (α.hom.app X) (CategoryStruct.comp (G.map f) (α.inv.app Y)) = F.map f
    source
    theorem CategoryTheory.NatIso.naturality_1' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x✝ : IsIso (α.app X)} :
    CategoryStruct.comp (inv (α.app X)) (CategoryStruct.comp (F.map f) (α.app Y)) = G.map f
    source
    @[simp]
    theorem CategoryTheory.NatIso.naturality_2' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x✝ : IsIso (α.app Y)} :
    CategoryStruct.comp (α.app X) (CategoryStruct.comp (G.map f) (inv (α.app Y))) = F.map f
    source
    @[simp]
    theorem CategoryTheory.NatIso.naturality_2'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x✝ : IsIso (α.app Y)} {Z : D} (h : F.obj Y ⟶ Z) :
    CategoryStruct.comp (α.app X) (CategoryStruct.comp (G.map f) (CategoryStruct.comp (inv (α.app Y)) h)) = CategoryStruct.comp (F.map f) h
    source
    instance CategoryTheory.NatIso.isIso_app_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) [IsIso α] (X : C) :
    IsIso (α.app X)

    The components of a natural isomorphism are isomorphisms.

    source
    @[simp]
    theorem CategoryTheory.NatIso.isIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) {x✝ : IsIso α} (X : C) :
    (inv α).app X = inv (α.app X)
    source
    @[simp]
    theorem CategoryTheory.NatIso.inv_map_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) {X Y : C} (e : X ≅ Y) (Z : D) :
    inv ((F.map e.inv).app Z) = (F.map e.hom).app Z
    source
    def CategoryTheory.NatIso.ofComponents {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (app Y).hom = CategoryStruct.comp (app X).hom (G.map f) := by cat_disch) :
    F ≅ G

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.NatIso.ofComponents_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (app Y).hom = CategoryStruct.comp (app X).hom (G.map f) := by cat_disch) (X : C) :
      (ofComponents app naturality).hom.app X = (app X).hom
      source
      @[simp]
      theorem CategoryTheory.NatIso.ofComponents_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (app Y).hom = CategoryStruct.comp (app X).hom (G.map f) := by cat_disch) (X : C) :
      (ofComponents app naturality).inv.app X = (app X).inv
      source
      @[simp]
      theorem CategoryTheory.NatIso.ofComponents.app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (app' : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (app' Y).hom = CategoryStruct.comp (app' X).hom (G.map f)) (X : C) :
      (ofComponents app' naturality).app X = app' X
      source
      theorem CategoryTheory.NatIso.isIso_of_isIso_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) [∀ (X : C), IsIso (α.app X)] :
      IsIso α

      A natural transformation is an isomorphism if all its components are isomorphisms.

      source
      def CategoryTheory.NatIso.hcomp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H I : Functor D E} (α : F ≅ G) (β : H ≅ I) :
      F.comp H ≅ G.comp I

      Horizontal composition of natural isomorphisms.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.NatIso.hcomp_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H I : Functor D E} (α : F ≅ G) (β : H ≅ I) :
        (hcomp α β).inv = α.inv ◫ β.inv
        source
        @[simp]
        theorem CategoryTheory.NatIso.hcomp_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H I : Functor D E} (α : F ≅ G) (β : H ≅ I) :
        (hcomp α β).hom = α.hom ◫ β.hom
        source
        theorem CategoryTheory.NatIso.isIso_map_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F₁ F₂ : Functor C D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) :
        IsIso (F₁.map f) ↔ IsIso (F₂.map f)
        source
        theorem CategoryTheory.NatTrans.isIso_iff_isIso_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (τ : F ⟶ G) :
        IsIso τ ↔ ∀ (X : C), IsIso (τ.app X)
        source
        def CategoryTheory.Functor.copyObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) :
        Functor C D

        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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.copyObj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (a✝ : C) :
          (F.copyObj obj e).obj a✝ = obj a✝
          source
          def CategoryTheory.Functor.isoCopyObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) :
          F ≅ F.copyObj obj e

          The functor constructed with copyObj is isomorphic to the given functor.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Functor.isoCopyObj_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (X : C) :
            (F.isoCopyObj obj e).hom.app X = (e X).hom
            source
            @[simp]
            theorem CategoryTheory.Functor.isoCopyObj_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (X : C) :
            (F.isoCopyObj obj e).inv.app X = (e X).inv