Natural isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

nat_iso.of_components
  (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 nat_iso 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

@[simp]

theorem category_theory.iso.app_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

(α.app X).inv = α.inv.app X

source

def category_theory.iso.app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : 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' := _}

source

@[simp]

theorem category_theory.iso.app_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

(α.app X).hom = α.hom.app X

source

@[simp]

theorem category_theory.iso.hom_inv_id_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)

source

@[simp]

theorem category_theory.iso.hom_inv_id_app_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) {X' : D} (f' : F.obj X ⟶ X') :

α.hom.app X ≫ α.inv.app X ≫ f' = f'

source

@[simp]

theorem category_theory.iso.inv_hom_id_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)

source

@[simp]

theorem category_theory.iso.inv_hom_id_app_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) {X' : D} (f' : G.obj X ⟶ X') :

α.inv.app X ≫ α.hom.app X ≫ f' = f'

source

@[simp]

theorem category_theory.nat_iso.trans_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) (X : C) :

(α ≪≫ β).app X = α.app X ≪≫ β.app X

source

theorem category_theory.nat_iso.app_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

(α.app X).hom = α.hom.app X

source

theorem category_theory.nat_iso.app_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

(α.app X).inv = α.inv.app X

source

@[protected, instance]

def category_theory.nat_iso.hom_app_is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

category_theory.is_iso (α.hom.app X)

source

@[protected, instance]

def category_theory.nat_iso.inv_app_is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) (X : C) :

category_theory.is_iso (α.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 later, 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 category_theory.nat_iso.cancel_nat_iso_hom_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) {X : C} {Z : D} (g g' : G.obj X ⟶ Z) :

α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'

source

@[simp]

theorem category_theory.nat_iso.cancel_nat_iso_inv_left {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) {X : C} {Z : D} (g g' : F.obj X ⟶ Z) :

α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'

source

@[simp]

theorem category_theory.nat_iso.cancel_nat_iso_hom_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) {X : D} {Y : C} (f f' : X ⟶ F.obj Y) :

f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'

source

@[simp]

theorem category_theory.nat_iso.cancel_nat_iso_inv_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) {X : D} {Y : C} (f f' : X ⟶ G.obj Y) :

f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f'

source

@[simp]

theorem category_theory.nat_iso.cancel_nat_iso_hom_right_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : 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) :

f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'

source

@[simp]

theorem category_theory.nat_iso.cancel_nat_iso_inv_right_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : 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) :

f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'

source

@[simp]

theorem category_theory.nat_iso.inv_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (e : F ≅ G) (X : C) :

category_theory.inv (e.inv.app X) = e.hom.app X

source

theorem category_theory.nat_iso.naturality_1 {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) :

α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f

source

theorem category_theory.nat_iso.naturality_2 {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) :

α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f

source

theorem category_theory.nat_iso.naturality_1' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) [category_theory.is_iso (α.app X)] :

category_theory.inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f

source

@[simp]

theorem category_theory.nat_iso.naturality_2'_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) [category_theory.is_iso (α.app Y)] {X' : D} (f' : F.obj Y ⟶ X') :

α.app X ≫ G.map f ≫ category_theory.inv (α.app Y) ≫ f' = F.map f ≫ f'

source

@[simp]

theorem category_theory.nat_iso.naturality_2' {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) [category_theory.is_iso (α.app Y)] :

α.app X ≫ G.map f ≫ category_theory.inv (α.app Y) = F.map f

source

@[protected, instance]

def category_theory.nat_iso.is_iso_app_of_is_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) [category_theory.is_iso α] (X : C) :

category_theory.is_iso (α.app X)

The components of a natural isomorphism are isomorphisms.

source

@[simp]

theorem category_theory.nat_iso.is_iso_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) [category_theory.is_iso α] (X : C) :

(category_theory.inv α).app X = category_theory.inv (α.app X)

source

@[simp]

theorem category_theory.nat_iso.inv_map_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :

category_theory.inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

source

@[simp]

theorem category_theory.nat_iso.of_components_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (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) (X : C) :

(category_theory.nat_iso.of_components app naturality).inv.app X = (app X).inv

source

def category_theory.nat_iso.of_components {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (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

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

Equations

category_theory.nat_iso.of_components app naturality = {hom := {app := λ (X : C), (app X).hom, naturality' := naturality}, inv := {app := λ (X : C), (app X).inv, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.nat_iso.of_components_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (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) (X : C) :

(category_theory.nat_iso.of_components app naturality).hom.app X = (app X).hom

source

@[simp]

theorem category_theory.nat_iso.of_components.app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (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) (X : C) :

(category_theory.nat_iso.of_components app' naturality).app X = app' X

source

theorem category_theory.nat_iso.is_iso_of_is_iso_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) [∀ (X : C), category_theory.is_iso (α.app X)] :

category_theory.is_iso α

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

source

@[simp]

theorem category_theory.nat_iso.hcomp_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) :

(category_theory.nat_iso.hcomp α β).inv = α.inv ◫ β.inv

source

def category_theory.nat_iso.hcomp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) :

F ⋙ H ≅ G ⋙ I

Horizontal composition of natural isomorphisms.

Equations

category_theory.nat_iso.hcomp α β = {hom := α.hom ◫ β.hom, inv := α.inv ◫ β.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.nat_iso.hcomp_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) :

(category_theory.nat_iso.hcomp α β).hom = α.hom ◫ β.hom

source

theorem category_theory.nat_iso.is_iso_map_iff {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) :

category_theory.is_iso (F₁.map f) ↔ category_theory.is_iso (F₂.map f)