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

source

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

Type v

hom : X ⟶ Y
inv : Y ⟶ X
hom_inv_id' : self.hom ≫ self.inv = 𝟙 X . "obviously"
inv_hom_id' : self.inv ≫ self.hom = 𝟙 Y . "obviously"

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.

Instances for category_theory.iso

category_theory.iso.has_sizeof_inst
category_theory.iso.inhabited
category_theory.subsingleton_iso
category_theory.limits.has_zero_object.category_theory.iso.subsingleton

source

@[simp]

theorem category_theory.iso.hom_inv_id {C : Type u} [category_theory.category C] {X Y : C} (self : X ≅ Y) :

self.hom ≫ self.inv = 𝟙 X

source

@[simp]

theorem category_theory.iso.inv_hom_id {C : Type u} [category_theory.category C] {X Y : C} (self : X ≅ Y) :

self.inv ≫ self.hom = 𝟙 Y

source

@[simp]

theorem category_theory.iso.hom_inv_id_assoc {C : Type u} [category_theory.category C] {X Y : C} (self : X ≅ Y) {X' : C} (f' : X ⟶ X') :

self.hom ≫ self.inv ≫ f' = f'

source

@[simp]

theorem category_theory.iso.inv_hom_id_assoc {C : Type u} [category_theory.category C] {X Y : C} (self : X ≅ Y) {X' : C} (f' : Y ⟶ X') :

self.inv ≫ self.hom ≫ f' = f'

source

@[ext]

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

α = β

source

@[symm]

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

Y ≅ X

Inverse isomorphism.

Equations

I.symm = {hom := I.inv, inv := I.hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.iso.symm_hom {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

α.symm.hom = α.inv

source

@[simp]

theorem category_theory.iso.symm_inv {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

α.symm.inv = α.hom

source

@[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}

source

@[simp]

theorem category_theory.iso.symm_symm_eq {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

α.symm.symm = α

source

@[simp]

theorem category_theory.iso.symm_eq_iff {C : Type u} [category_theory.category C] {X Y : C} {α β : X ≅ Y} :

α.symm = β.symm ↔ α = β

source

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

nonempty (X ≅ Y) ↔ nonempty (Y ≅ X)

source

@[refl]

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

X ≅ X

Identity isomorphism.

Equations

category_theory.iso.refl X = {hom := 𝟙 X, inv := 𝟙 X, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.iso.refl_hom {C : Type u} [category_theory.category C] (X : C) :

(category_theory.iso.refl X).hom = 𝟙 X

source

@[simp]

theorem category_theory.iso.refl_inv {C : Type u} [category_theory.category C] (X : C) :

(category_theory.iso.refl X).inv = 𝟙 X

source

@[protected, instance]

def category_theory.iso.inhabited {C : Type u} [category_theory.category C] {X : C} :

inhabited (X ≅ X)

Equations

category_theory.iso.inhabited = {default := category_theory.iso.refl X}

source

@[simp]

theorem category_theory.iso.refl_symm {C : Type u} [category_theory.category C] (X : C) :

(category_theory.iso.refl X).symm = category_theory.iso.refl X

source

@[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

source

@[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

source

@[trans]

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

α ≪≫ β = {hom := α.hom ≫ β.hom, inv := β.inv ≫ α.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[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''}

source

@[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

source

@[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') :

(α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

source

@[simp]

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

category_theory.iso.refl X ≪≫ α = α

source

@[simp]

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

α ≪≫ category_theory.iso.refl Y = α

source

@[simp]

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

α.symm ≪≫ α = category_theory.iso.refl Y

source

@[simp]

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

α ≪≫ α.symm = category_theory.iso.refl X

source

@[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 ≪≫ α ≪≫ β = β

source

@[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 ≪≫ β = β

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem category_theory.iso.inv_comp_eq_id {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} :

α.inv ≫ f = 𝟙 Y ↔ f = α.hom

source

theorem category_theory.iso.comp_inv_eq_id {C : Type u} [category_theory.category C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} :

f ≫ α.inv = 𝟙 X ↔ f = α.hom

source

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

source

@[class]

structure category_theory.is_iso {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

Prop

out : ∃ (inv : Y ⟶ X), f ≫ inv = 𝟙 X ∧ inv ≫ f = 𝟙 Y

is_iso typeclass expressing that a morphism is invertible.

Instances of this typeclass

source

@[protected]

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

category_theory.inv f = classical.some category_theory.is_iso.out

Instances for category_theory.inv

category_theory.is_iso.inv_is_iso

source

@[simp]

theorem category_theory.is_iso.hom_inv_id {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [I : category_theory.is_iso f] :

f ≫ category_theory.inv f = 𝟙 X

source

@[simp]

theorem category_theory.is_iso.hom_inv_id_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [I : category_theory.is_iso f] {X' : C} (f' : X ⟶ X') :

f ≫ category_theory.inv f ≫ f' = f'

source

@[simp]

theorem category_theory.is_iso.inv_hom_id {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [I : category_theory.is_iso f] :

category_theory.inv f ≫ f = 𝟙 Y

source

@[simp]

theorem category_theory.is_iso.inv_hom_id_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [I : category_theory.is_iso f] {X' : C} (f' : Y ⟶ X') :

category_theory.inv f ≫ f ≫ f' = f'

source

noncomputable 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

category_theory.as_iso f = {hom := f, inv := category_theory.inv f h, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.as_iso_hom {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :

(category_theory.as_iso f).hom = f

source

@[simp]

theorem category_theory.as_iso_inv {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :

(category_theory.as_iso f).inv = category_theory.inv f

source

@[protected, instance]

def category_theory.is_iso.epi_of_iso {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.epi f

source

@[protected, instance]

def category_theory.is_iso.mono_of_iso {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.mono f

source

@[ext]

theorem category_theory.is_iso.inv_eq_of_hom_inv_id {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.is_iso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :

category_theory.inv f = g

source

theorem category_theory.is_iso.inv_eq_of_inv_hom_id {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.is_iso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) :

category_theory.inv f = g

source

@[ext]

theorem category_theory.is_iso.eq_inv_of_hom_inv_id {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.is_iso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :

g = category_theory.inv f

source

theorem category_theory.is_iso.eq_inv_of_inv_hom_id {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.is_iso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) :

g = category_theory.inv f

source

@[protected, instance]

def category_theory.is_iso.id {C : Type u} [category_theory.category C] (X : C) :

category_theory.is_iso (𝟙 X)

source

@[protected, instance]

def category_theory.is_iso.of_iso {C : Type u} [category_theory.category C] {X Y : C} (f : X ≅ Y) :

category_theory.is_iso f.hom

source

@[protected, instance]

def category_theory.is_iso.of_iso_inv {C : Type u} [category_theory.category C] {X Y : C} (f : X ≅ Y) :

category_theory.is_iso f.inv

source

@[protected, instance]

def category_theory.is_iso.inv_is_iso {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.is_iso f] :

category_theory.is_iso (category_theory.inv f)

source

@[protected, instance]

def category_theory.is_iso.comp_is_iso {C : Type u} [category_theory.category C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [category_theory.is_iso f] [category_theory.is_iso h] :

category_theory.is_iso (f ≫ h)

source

@[simp]

theorem category_theory.is_iso.inv_id {C : Type u} [category_theory.category C] {X : C} :

category_theory.inv (𝟙 X) = 𝟙 X

source

@[simp]

theorem category_theory.is_iso.inv_comp {C : Type u} [category_theory.category C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [category_theory.is_iso f] [category_theory.is_iso h] :

category_theory.inv (f ≫ h) = category_theory.inv h ≫ category_theory.inv f

source

@[simp]

theorem category_theory.is_iso.inv_inv {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.is_iso f] :

category_theory.inv (category_theory.inv f) = f

source

@[simp]

theorem category_theory.is_iso.iso.inv_inv {C : Type u} [category_theory.category C] {X Y : C} (f : X ≅ Y) :

category_theory.inv f.inv = f.hom

source

@[simp]

theorem category_theory.is_iso.iso.inv_hom {C : Type u} [category_theory.category C] {X Y : C} (f : X ≅ Y) :

category_theory.inv f.hom = f.inv

source

@[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} :

category_theory.inv α ≫ f = g ↔ f = α ≫ g

source

@[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} :

g = category_theory.inv α ≫ f ↔ α ≫ g = f

source

@[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} :

f ≫ category_theory.inv α = g ↔ f = g ≫ α

source

@[simp]

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

g = f ≫ category_theory.inv α ↔ g ≫ α = f

source

theorem category_theory.is_iso.of_is_iso_comp_left {C : Type u} [category_theory.category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso f] [category_theory.is_iso (f ≫ g)] :

category_theory.is_iso g

source

theorem category_theory.is_iso.of_is_iso_comp_right {C : Type u} [category_theory.category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso g] [category_theory.is_iso (f ≫ g)] :

category_theory.is_iso f

source

theorem category_theory.is_iso.of_is_iso_fac_left {C : Type u} [category_theory.category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [category_theory.is_iso f] [hh : category_theory.is_iso h] (w : f ≫ g = h) :

category_theory.is_iso g

source

theorem category_theory.is_iso.of_is_iso_fac_right {C : Type u} [category_theory.category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [category_theory.is_iso g] [hh : category_theory.is_iso h] (w : f ≫ g = h) :

category_theory.is_iso f

source

theorem category_theory.eq_of_inv_eq_inv {C : Type u} [category_theory.category C] {X Y : C} {f g : X ⟶ Y} [category_theory.is_iso f] [category_theory.is_iso g] (p : category_theory.inv f = category_theory.inv g) :

f = g

source

theorem category_theory.is_iso.inv_eq_inv {C : Type u} [category_theory.category C] {X Y : C} {f g : X ⟶ Y} [category_theory.is_iso f] [category_theory.is_iso g] :

category_theory.inv f = category_theory.inv g ↔ f = g

source

theorem category_theory.hom_comp_eq_id {C : Type u} [category_theory.category C] {X Y : C} (g : X ⟶ Y) [category_theory.is_iso g] {f : Y ⟶ X} :

g ≫ f = 𝟙 X ↔ f = category_theory.inv g

source

theorem category_theory.comp_hom_eq_id {C : Type u} [category_theory.category C] {X Y : C} (g : X ⟶ Y) [category_theory.is_iso g] {f : Y ⟶ X} :

f ≫ g = 𝟙 Y ↔ f = category_theory.inv g

source

theorem category_theory.inv_comp_eq_id {C : Type u} [category_theory.category C] {X Y : C} (g : X ⟶ Y) [category_theory.is_iso g] {f : X ⟶ Y} :

category_theory.inv g ≫ f = 𝟙 Y ↔ f = g

source

theorem category_theory.comp_inv_eq_id {C : Type u} [category_theory.category C] {X Y : C} (g : X ⟶ Y) [category_theory.is_iso g] {f : X ⟶ Y} :

f ≫ category_theory.inv g = 𝟙 X ↔ f = g

source

theorem category_theory.is_iso_of_hom_comp_eq_id {C : Type u} [category_theory.category C] {X Y : C} (g : X ⟶ Y) [category_theory.is_iso g] {f : Y ⟶ X} (h : g ≫ f = 𝟙 X) :

category_theory.is_iso f

source

theorem category_theory.is_iso_of_comp_hom_eq_id {C : Type u} [category_theory.category C] {X Y : C} (g : X ⟶ Y) [category_theory.is_iso g] {f : Y ⟶ X} (h : f ≫ g = 𝟙 Y) :

category_theory.is_iso f

source

@[ext]

theorem category_theory.iso.inv_ext {C : Type u} [category_theory.category C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) :

f.inv = g

source

@[ext]

theorem category_theory.iso.inv_ext' {C : Type u} [category_theory.category C] {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.

source

@[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'

source

@[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'

source

@[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'

source

@[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'

source

@[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'

source

@[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'

source

@[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

source

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} (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

F.map_iso i = {hom := F.map i.hom, inv := F.map i.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[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

source

@[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) :

F.map_iso i.symm = (F.map_iso i).symm

source

@[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) :

F.map_iso (i ≪≫ j) = F.map_iso i ≪≫ F.map_iso j

source

@[simp]

theorem category_theory.functor.map_iso_refl {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X : C) :

F.map_iso (category_theory.iso.refl X) = category_theory.iso.refl (F.obj X)

source

@[protected, instance]

def category_theory.functor.map_is_iso {C : Type u} [category_theory.category C] {X Y : C} {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.is_iso (F.map f)

source

@[simp]

theorem category_theory.functor.map_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] :

F.map (category_theory.inv f) = category_theory.inv (F.map f)

source

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] :

F.map f ≫ F.map (category_theory.inv f) = 𝟙 (F.obj X)

source

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] :

F.map (category_theory.inv f) ≫ F.map f = 𝟙 (F.obj Y)