mathlib documentation

category_theory.isomorphism

Isomorphisms

This file defines isomorphisms between objects of a category.

Main definitions

Notations

Tags

category, category theory, isomorphism

structure category_theory.iso {C : Type u} [category_theory.category C] :
C → C → Type v

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.

See https://stacks.math.columbia.edu/tag/0017.

@[ext]
theorem category_theory.iso.ext {C : Type u} [category_theory.category C] {X Y : C} ⦃α β : X Y⦄ :
α.hom = β.homα = β

def category_theory.iso.symm {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)(Y X)

Inverse isomorphism.

Equations
@[simp]
theorem category_theory.iso.symm_hom {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) :
α.symm.hom = α.inv

@[simp]
theorem category_theory.iso.symm_inv {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) :
α.symm.inv = α.hom

@[simp]
theorem category_theory.iso.symm_mk {C : Type u} [category_theory.category C] {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} [category_theory.category C] {X Y : C} (α : X Y) :
α.symm.symm = α

@[simp]
theorem category_theory.iso.symm_eq_iff {C : Type u} [category_theory.category C] {X Y : C} {α β : X Y} :
α.symm = β.symm α = β

def category_theory.iso.refl {C : Type u} [category_theory.category C] (X : C) :
X X

Identity isomorphism.

Equations
@[simp]
theorem category_theory.iso.trans_inv {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) (β : Y Z) :
≪≫ β).inv = β.inv α.inv

@[simp]
theorem category_theory.iso.trans_hom {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) (β : Y Z) :
≪≫ β).hom = α.hom β.hom

def category_theory.iso.trans {C : Type u} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {X Y Z : C} (α : X Y) (β : Y Z) :
≪≫ β).symm = β.symm ≪≫ α.symm

@[simp]
theorem category_theory.iso.trans_assoc {C : Type u} [category_theory.category C] {X Y Z Z' : C} (α : X Y) (β : Y Z) (γ : Z Z') :
≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

@[simp]
theorem category_theory.iso.refl_trans {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) :

@[simp]
theorem category_theory.iso.trans_refl {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) :

@[simp]
theorem category_theory.iso.symm_self_id {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) :

@[simp]
theorem category_theory.iso.self_symm_id {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) :

@[simp]
theorem category_theory.iso.symm_self_id_assoc {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) (β : Y Z) :
α.symm ≪≫ α ≪≫ β = β

@[simp]
theorem category_theory.iso.self_symm_id_assoc {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) (β : X Z) :
α ≪≫ α.symm ≪≫ β = β

theorem category_theory.iso.inv_comp_eq {C : Type u} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {X Y : C} (α : X Y) {f : Y X} :
α.hom f = 𝟙 X f = α.inv

theorem category_theory.iso.comp_hom_eq_id {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) {f : Y X} :
f α.hom = 𝟙 Y f = α.inv

theorem category_theory.iso.hom_eq_inv {C : Type u} [category_theory.category C] {X Y : C} (α : X Y) (β : Y X) :
α.hom = β.inv β.hom = α.inv

@[class]
structure category_theory.is_iso {C : Type u} [category_theory.category C] {X Y : C} :
(X Y)Type v

is_iso typeclass expressing that a morphism is invertible. This contains the data of the inverse, but is a subsingleton type.

Instances
def category_theory.as_iso {C : Type u} [category_theory.category C] {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]

@[simp]

@[simp]

@[instance]

Equations
@[simp]

@[simp]

@[simp]
theorem category_theory.is_iso.inv_comp_eq {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) [category_theory.is_iso α] {f : X Z} {g : Y Z} :

@[simp]
theorem category_theory.is_iso.eq_inv_comp {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) [category_theory.is_iso α] {f : X Z} {g : Y Z} :

@[simp]
theorem category_theory.is_iso.comp_inv_eq {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) [category_theory.is_iso α] {f : Z Y} {g : Z X} :

@[simp]
theorem category_theory.is_iso.comp_is_iso_eq {C : Type u} [category_theory.category C] {X Y Z : C} (α : X Y) [category_theory.is_iso α] {f : Z Y} {g : Z X} :

@[instance]

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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {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'

def category_theory.functor.map_iso {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} :
(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} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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_inv {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (i : X Y) :
(F.map_iso i).inv = F.map i.inv

@[simp]
theorem category_theory.functor.map_iso_symm {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (i : X Y) :

@[simp]
theorem category_theory.functor.map_iso_trans {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y Z : C} (i : X Y) (j : Y Z) :

@[simp]

theorem category_theory.functor.map_hom_inv {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (f : X Y) [category_theory.is_iso f] :

theorem category_theory.functor.map_inv_hom {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (f : X Y) [category_theory.is_iso f] :