# mathlib3documentation

category_theory.isomorphism

# Isomorphisms #

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

This file defines isomorphisms between objects of a category.

## Main definitions #

• structure iso : a bundled isomorphism between two objects of a category;
• class is_iso : an unbundled version of iso; note that is_iso f is a Prop, and only asserts the existence of an inverse. Of course, this inverse is unique, so it doesn't cost us much to use choice to retrieve it.
• inv f, for the inverse of a morphism with [is_iso f]
• as_iso : convert from is_iso to iso (noncomputable);
• of_iso : convert from iso to is_iso;
• standard operations on isomorphisms (composition, inverse etc)

## Notations #

• X ≅ Y : same as iso X Y;
• α ≪≫ β : composition of two isomorphisms; it is called iso.trans

## Tags #

category, category theory, isomorphism

structure category_theory.iso {C : Type u} (X Y : C) :

An isomorphism (a.k.a. an invertible morphism) between two objects of a category. The inverse morphism is bundled.

See also category_theory.core for the category with the same objects and isomorphisms playing the role of morphisms.

Instances for category_theory.iso
@[simp]
theorem category_theory.iso.hom_inv_id {C : Type u} {X Y : C} (self : X Y) :
self.hom self.inv = 𝟙 X
@[simp]
theorem category_theory.iso.inv_hom_id {C : Type u} {X Y : C} (self : X Y) :
self.inv self.hom = 𝟙 Y
@[simp]
theorem category_theory.iso.hom_inv_id_assoc {C : Type u} {X Y : C} (self : X Y) {X' : C} (f' : X X') :
self.hom self.inv f' = f'
@[simp]
theorem category_theory.iso.inv_hom_id_assoc {C : Type u} {X Y : C} (self : X Y) {X' : C} (f' : Y X') :
self.inv self.hom f' = f'
@[ext]
theorem category_theory.iso.ext {C : Type u} {X Y : C} ⦃α β : X Y⦄ (w : α.hom = β.hom) :
α = β
@[symm]
def category_theory.iso.symm {C : Type u} {X Y : C} (I : X Y) :
Y X

Inverse isomorphism.

Equations
@[simp]
theorem category_theory.iso.symm_hom {C : Type u} {X Y : C} (α : X Y) :
α.symm.hom = α.inv
@[simp]
theorem category_theory.iso.symm_inv {C : Type u} {X Y : C} (α : X Y) :
α.symm.inv = α.hom
@[simp]
theorem category_theory.iso.symm_mk {C : Type u} {X Y : C} (hom : X Y) (inv : Y X) (hom_inv_id : hom inv = 𝟙 X) (inv_hom_id : inv hom = 𝟙 Y) :
{hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id}.symm = {hom := inv, inv := hom, hom_inv_id' := inv_hom_id, inv_hom_id' := hom_inv_id}
@[simp]
theorem category_theory.iso.symm_symm_eq {C : Type u} {X Y : C} (α : X Y) :
α.symm.symm = α
@[simp]
theorem category_theory.iso.symm_eq_iff {C : Type u} {X Y : C} {α β : X Y} :
α.symm = β.symm α = β
theorem category_theory.iso.nonempty_iso_symm {C : Type u} (X Y : C) :
@[refl]
def category_theory.iso.refl {C : Type u} (X : C) :
X X

Identity isomorphism.

Equations
@[simp]
theorem category_theory.iso.refl_hom {C : Type u} (X : C) :
@[simp]
theorem category_theory.iso.refl_inv {C : Type u} (X : C) :
@[protected, instance]
def category_theory.iso.inhabited {C : Type u} {X : C} :
Equations
@[simp]
theorem category_theory.iso.refl_symm {C : Type u} (X : C) :
@[simp]
theorem category_theory.iso.trans_inv {C : Type u} {X Y Z : C} (α : X Y) (β : Y Z) :
≪≫ β).inv = β.inv α.inv
@[simp]
theorem category_theory.iso.trans_hom {C : Type u} {X Y Z : C} (α : X Y) (β : Y Z) :
≪≫ β).hom = α.hom β.hom
@[trans]
def category_theory.iso.trans {C : Type u} {X Y Z : C} (α : X Y) (β : Y Z) :
X Z

Composition of two isomorphisms

Equations
@[simp]
theorem category_theory.iso.trans_mk {C : Type u} {X Y Z : C} (hom : X Y) (inv : Y X) (hom_inv_id : hom inv = 𝟙 X) (inv_hom_id : inv hom = 𝟙 Y) (hom' : Y Z) (inv' : Z Y) (hom_inv_id' : hom' inv' = 𝟙 Y) (inv_hom_id' : inv' hom' = 𝟙 Z) (hom_inv_id'' : (hom hom') inv' inv = 𝟙 X) (inv_hom_id'' : (inv' inv) hom hom' = 𝟙 Z) :
{hom := hom, inv := inv, hom_inv_id' := hom_inv_id, inv_hom_id' := inv_hom_id} ≪≫ {hom := hom', inv := inv', hom_inv_id' := hom_inv_id', inv_hom_id' := inv_hom_id'} = {hom := hom hom', inv := inv' inv, hom_inv_id' := hom_inv_id'', inv_hom_id' := inv_hom_id''}
@[simp]
theorem category_theory.iso.trans_symm {C : Type u} {X Y Z : C} (α : X Y) (β : Y Z) :
≪≫ β).symm = β.symm ≪≫ α.symm
@[simp]
theorem category_theory.iso.trans_assoc {C : Type u} {X Y Z Z' : C} (α : X Y) (β : Y Z) (γ : Z Z') :
≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
@[simp]
theorem category_theory.iso.refl_trans {C : Type u} {X Y : C} (α : X Y) :
@[simp]
theorem category_theory.iso.trans_refl {C : Type u} {X Y : C} (α : X Y) :
@[simp]
theorem category_theory.iso.symm_self_id {C : Type u} {X Y : C} (α : X Y) :
@[simp]
theorem category_theory.iso.self_symm_id {C : Type u} {X Y : C} (α : X Y) :
@[simp]
theorem category_theory.iso.symm_self_id_assoc {C : Type u} {X Y Z : C} (α : X Y) (β : Y Z) :
α.symm ≪≫ α ≪≫ β = β
@[simp]
theorem category_theory.iso.self_symm_id_assoc {C : Type u} {X Y Z : C} (α : X Y) (β : X Z) :
α ≪≫ α.symm ≪≫ β = β
theorem category_theory.iso.inv_comp_eq {C : Type u} {X Y Z : C} (α : X Y) {f : X Z} {g : Y Z} :
α.inv f = g f = α.hom g
theorem category_theory.iso.eq_inv_comp {C : Type u} {X Y Z : C} (α : X Y) {f : X Z} {g : Y Z} :
g = α.inv f α.hom g = f
theorem category_theory.iso.comp_inv_eq {C : Type u} {X Y Z : C} (α : X Y) {f : Z Y} {g : Z X} :
f α.inv = g f = g α.hom
theorem category_theory.iso.eq_comp_inv {C : Type u} {X Y Z : C} (α : X Y) {f : Z Y} {g : Z X} :
g = f α.inv g α.hom = f
theorem category_theory.iso.inv_eq_inv {C : Type u} {X Y : C} (f g : X Y) :
f.inv = g.inv f.hom = g.hom
theorem category_theory.iso.hom_comp_eq_id {C : Type u} {X Y : C} (α : X Y) {f : Y X} :
α.hom f = 𝟙 X f = α.inv
theorem category_theory.iso.comp_hom_eq_id {C : Type u} {X Y : C} (α : X Y) {f : Y X} :
f α.hom = 𝟙 Y f = α.inv
theorem category_theory.iso.inv_comp_eq_id {C : Type u} {X Y : C} (α : X Y) {f : X Y} :
α.inv f = 𝟙 Y f = α.hom
theorem category_theory.iso.comp_inv_eq_id {C : Type u} {X Y : C} (α : X Y) {f : X Y} :
f α.inv = 𝟙 X f = α.hom
theorem category_theory.iso.hom_eq_inv {C : Type u} {X Y : C} (α : X Y) (β : Y X) :
α.hom = β.inv β.hom = α.inv
@[class]
structure category_theory.is_iso {C : Type u} {X Y : C} (f : X Y) :
Prop

is_iso typeclass expressing that a morphism is invertible.

Instances of this typeclass
@[protected]
noncomputable def category_theory.inv {C : Type u} {X Y : C} (f : X Y) [I : category_theory.is_iso f] :
Y X

The inverse of a morphism f when we have [is_iso f].

Equations
Instances for category_theory.inv
@[simp]
theorem category_theory.is_iso.hom_inv_id {C : Type u} {X Y : C} (f : X Y) [I : category_theory.is_iso f] :
= 𝟙 X
@[simp]
theorem category_theory.is_iso.hom_inv_id_assoc {C : Type u} {X Y : C} (f : X Y) [I : category_theory.is_iso f] {X' : C} (f' : X X') :
f = f'
@[simp]
theorem category_theory.is_iso.inv_hom_id {C : Type u} {X Y : C} (f : X Y) [I : category_theory.is_iso f] :
= 𝟙 Y
@[simp]
theorem category_theory.is_iso.inv_hom_id_assoc {C : Type u} {X Y : C} (f : X Y) [I : category_theory.is_iso f] {X' : C} (f' : Y X') :
f f' = f'
noncomputable def category_theory.as_iso {C : Type u} {X Y : C} (f : X Y) [h : category_theory.is_iso f] :
X Y

Reinterpret a morphism f with an is_iso f instance as an iso.

Equations
@[simp]
theorem category_theory.as_iso_hom {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.as_iso_inv {C : Type u} {X Y : C} (f : X Y)  :
@[protected, instance]
def category_theory.is_iso.epi_of_iso {C : Type u} {X Y : C} (f : X Y)  :
@[protected, instance]
def category_theory.is_iso.mono_of_iso {C : Type u} {X Y : C} (f : X Y)  :
@[ext]
theorem category_theory.is_iso.inv_eq_of_hom_inv_id {C : Type u} {X Y : C} {f : X Y} {g : Y X} (hom_inv_id : f g = 𝟙 X) :
theorem category_theory.is_iso.inv_eq_of_inv_hom_id {C : Type u} {X Y : C} {f : X Y} {g : Y X} (inv_hom_id : g f = 𝟙 Y) :
@[ext]
theorem category_theory.is_iso.eq_inv_of_hom_inv_id {C : Type u} {X Y : C} {f : X Y} {g : Y X} (hom_inv_id : f g = 𝟙 X) :
theorem category_theory.is_iso.eq_inv_of_inv_hom_id {C : Type u} {X Y : C} {f : X Y} {g : Y X} (inv_hom_id : g f = 𝟙 Y) :
@[protected, instance]
def category_theory.is_iso.id {C : Type u} (X : C) :
@[protected, instance]
def category_theory.is_iso.of_iso {C : Type u} {X Y : C} (f : X Y) :
@[protected, instance]
def category_theory.is_iso.of_iso_inv {C : Type u} {X Y : C} (f : X Y) :
@[protected, instance]
def category_theory.is_iso.inv_is_iso {C : Type u} {X Y : C} {f : X Y}  :
@[protected, instance]
def category_theory.is_iso.comp_is_iso {C : Type u} {X Y Z : C} {f : X Y} {h : Y Z}  :
@[simp]
theorem category_theory.is_iso.inv_id {C : Type u} {X : C} :
= 𝟙 X
@[simp]
theorem category_theory.is_iso.inv_comp {C : Type u} {X Y Z : C} {f : X Y} {h : Y Z}  :
@[simp]
theorem category_theory.is_iso.inv_inv {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.is_iso.iso.inv_inv {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.is_iso.iso.inv_hom {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.is_iso.inv_comp_eq {C : Type u} {X Y Z : C} (α : X Y) {f : X Z} {g : Y Z} :
= g f = α g
@[simp]
theorem category_theory.is_iso.eq_inv_comp {C : Type u} {X Y Z : C} (α : X Y) {f : X Z} {g : Y Z} :
g = α g = f
@[simp]
theorem category_theory.is_iso.comp_inv_eq {C : Type u} {X Y Z : C} (α : X Y) {f : Z Y} {g : Z X} :
= g f = g α
@[simp]
theorem category_theory.is_iso.eq_comp_inv {C : Type u} {X Y Z : C} (α : X Y) {f : Z Y} {g : Z X} :
g = g α = f
theorem category_theory.is_iso.of_is_iso_comp_left {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) [category_theory.is_iso (f g)] :
theorem category_theory.is_iso.of_is_iso_comp_right {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z) [category_theory.is_iso (f g)] :
theorem category_theory.is_iso.of_is_iso_fac_left {C : Type u} {X Y Z : C} {f : X Y} {g : Y Z} {h : X Z} [hh : category_theory.is_iso h] (w : f g = h) :
theorem category_theory.is_iso.of_is_iso_fac_right {C : Type u} {X Y Z : C} {f : X Y} {g : Y Z} {h : X Z} [hh : category_theory.is_iso h] (w : f g = h) :
theorem category_theory.eq_of_inv_eq_inv {C : Type u} {X Y : C} {f g : X Y}  :
f = g
theorem category_theory.is_iso.inv_eq_inv {C : Type u} {X Y : C} {f g : X Y}  :
theorem category_theory.hom_comp_eq_id {C : Type u} {X Y : C} (g : X Y) {f : Y X} :
g f = 𝟙 X
theorem category_theory.comp_hom_eq_id {C : Type u} {X Y : C} (g : X Y) {f : Y X} :
f g = 𝟙 Y
theorem category_theory.inv_comp_eq_id {C : Type u} {X Y : C} (g : X Y) {f : X Y} :
= 𝟙 Y f = g
theorem category_theory.comp_inv_eq_id {C : Type u} {X Y : C} (g : X Y) {f : X Y} :
= 𝟙 X f = g
theorem category_theory.is_iso_of_hom_comp_eq_id {C : Type u} {X Y : C} (g : X Y) {f : Y X} (h : g f = 𝟙 X) :
theorem category_theory.is_iso_of_comp_hom_eq_id {C : Type u} {X Y : C} (g : X Y) {f : Y X} (h : f g = 𝟙 Y) :
@[ext]
theorem category_theory.iso.inv_ext {C : Type u} {X Y : C} {f : X Y} {g : Y X} (hom_inv_id : f.hom g = 𝟙 X) :
f.inv = g
@[ext]
theorem category_theory.iso.inv_ext' {C : Type u} {X Y : C} {f : X Y} {g : Y X} (hom_inv_id : f.hom g = 𝟙 X) :
g = f.inv

All these cancellation lemmas can be solved by simp [cancel_mono] (or simp [cancel_epi]), but with the current design cancel_mono is not a good simp lemma, because it generates a typeclass search.

When we can see syntactically that a morphism is a mono or an epi because it came from an isomorphism, it's fine to do the cancellation via simp.

In the longer term, it might be worth exploring making mono and epi structures, rather than typeclasses, with coercions back to X ⟶ Y. Presumably we could write X ↪ Y and X ↠ Y.

@[simp]
theorem category_theory.iso.cancel_iso_hom_left {C : Type u} {X Y Z : C} (f : X Y) (g g' : Y Z) :
f.hom g = f.hom g' g = g'
@[simp]
theorem category_theory.iso.cancel_iso_inv_left {C : Type u} {X Y Z : C} (f : Y X) (g g' : Y Z) :
f.inv g = f.inv g' g = g'
@[simp]
theorem category_theory.iso.cancel_iso_hom_right {C : Type u} {X Y Z : C} (f f' : X Y) (g : Y Z) :
f g.hom = f' g.hom f = f'
@[simp]
theorem category_theory.iso.cancel_iso_inv_right {C : Type u} {X Y Z : C} (f f' : X Y) (g : Z Y) :
f g.inv = f' g.inv f = f'
@[simp]
theorem category_theory.iso.cancel_iso_hom_right_assoc {C : Type u} {W X X' Y Z : C} (f : W X) (g : X Y) (f' : W X') (g' : X' Y) (h : Y Z) :
f g h.hom = f' g' h.hom f g = f' g'
@[simp]
theorem category_theory.iso.cancel_iso_inv_right_assoc {C : Type u} {W X X' Y Z : C} (f : W X) (g : X Y) (f' : W X') (g' : X' Y) (h : Z Y) :
f g h.inv = f' g' h.inv f g = f' g'
@[simp]
theorem category_theory.functor.map_iso_inv {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (i : X Y) :
(F.map_iso i).inv = F.map i.inv
def category_theory.functor.map_iso {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (i : X Y) :
F.obj X F.obj Y

A functor F : C ⥤ D sends isomorphisms i : X ≅ Y to isomorphisms F.obj X ≅ F.obj Y

Equations
@[simp]
theorem category_theory.functor.map_iso_hom {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (i : X Y) :
(F.map_iso i).hom = F.map i.hom
@[simp]
theorem category_theory.functor.map_iso_symm {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (i : X Y) :
@[simp]
theorem category_theory.functor.map_iso_trans {C : Type u} {D : Type u₂} (F : C D) {X Y Z : C} (i : X Y) (j : Y Z) :
@[simp]
theorem category_theory.functor.map_iso_refl {C : Type u} {D : Type u₂} (F : C D) (X : C) :
@[protected, instance]
def category_theory.functor.map_is_iso {C : Type u} {X Y : C} {D : Type u₂} (F : C D) (f : X Y)  :
@[simp]
theorem category_theory.functor.map_inv {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (f : X Y)  :
theorem category_theory.functor.map_hom_inv {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (f : X Y)  :
F.map f F.map = 𝟙 (F.obj X)
theorem category_theory.functor.map_inv_hom {C : Type u} {D : Type u₂} (F : C D) {X Y : C} (f : X Y)  :
F.map F.map f = 𝟙 (F.obj Y)