Isomorphisms

This file defines isomorphisms between objects of a category.

Main definitions

• structure Iso : a bundled isomorphism between two objects of a category;
• class IsIso : an unbundled version of iso; note that IsIso 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 [IsIso f]
• asIso : convert from IsIso to Iso (noncomputable);
• of_iso : convert from Iso to IsIso;
• 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 CategoryTheory.Iso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) : Type v

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

See also CategoryTheory.Core for the category with the same objects and isomorphisms playing the role of morphisms.

See .

• hom : X ⟶ Y

  The forward direction of an isomorphism.

• inv : Y ⟶ X

  The backwards direction of an isomorphism.

• hom_inv_id : CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X

  Composition of the two directions of an isomorphism is the identity on the source.

• inv_hom_id : CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y

  Composition of the two directions of an isomorphism in reverse order is the identity on the target.

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (self : X ≅ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.inv (CategoryTheory.CategoryStruct.comp self.hom h) = h

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (self : X ≅ Y) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp self.inv h) = h

def CategoryTheory.«term_≅_» : Lean.TrailingParserDescr

Notation for an isomorphism in a category.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Iso.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} ⦃α : X ≅ Y⦄ ⦃β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β

def CategoryTheory.Iso.symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (I : X ≅ Y) : Y ≅ X

Inverse isomorphism.

Equations

• I.symm = CategoryTheory.Iso.mk I.inv I.hom

@[simp]

theorem CategoryTheory.Iso.symm_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α.symm.hom = α.inv

@[simp]

theorem CategoryTheory.Iso.symm_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α.symm.inv = α.hom

@[simp]

theorem CategoryTheory.Iso.symm_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) : (CategoryTheory.Iso.mk hom inv).symm = CategoryTheory.Iso.mk inv hom

@[simp]

theorem CategoryTheory.Iso.symm_symm_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α.symm.symm = α

@[simp]

theorem CategoryTheory.Iso.symm_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {α : X ≅ Y} {β : X ≅ Y} : α.symm = β.symm ↔ α = β

theorem CategoryTheory.Iso.nonempty_iso_symm {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) : Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)

@[simp]

theorem CategoryTheory.Iso.refl_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Iso.refl X).inv = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Iso.refl_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Iso.refl X).hom = CategoryTheory.CategoryStruct.id X

def CategoryTheory.Iso.refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : X ≅ X

Identity isomorphism.

Equations

• CategoryTheory.Iso.refl X = CategoryTheory.Iso.mk (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)

instance CategoryTheory.Iso.instInhabitedIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : Inhabited (X ≅ X)

Equations

• CategoryTheory.Iso.instInhabitedIso = { default := CategoryTheory.Iso.refl X }

theorem CategoryTheory.Iso.nonempty_iso_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Nonempty (X ≅ X)

@[simp]

theorem CategoryTheory.Iso.refl_symm {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Iso.refl X).symm = CategoryTheory.Iso.refl X

@[simp]

theorem CategoryTheory.Iso.trans_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = CategoryTheory.CategoryStruct.comp β.inv α.inv

@[simp]

theorem CategoryTheory.Iso.trans_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom

def CategoryTheory.Iso.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z

Composition of two isomorphisms

Equations

• α ≪≫ β = CategoryTheory.Iso.mk (CategoryTheory.CategoryStruct.comp α.hom β.hom) (CategoryTheory.CategoryStruct.comp β.inv α.inv)

@[simp]

theorem CategoryTheory.Iso.instTransIso_trans {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {a b c : C} (α : a ≅ b) (β : b ≅ c), Trans.trans α β = α ≪≫ β

instance CategoryTheory.Iso.instTransIso {C : Type u} [CategoryTheory.Category.{v, u} C] : Trans (fun (x x_1 : C) => x ≅ x_1) (fun (x x_1 : C) => x ≅ x_1) fun (x x_1 : C) => x ≅ x_1

Equations

• CategoryTheory.Iso.instTransIso = { trans := fun {a b c : C} => CategoryTheory.Iso.trans }

def CategoryTheory.Iso.«term_≪≫_» : Lean.TrailingParserDescr

Notation for composition of isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Iso.trans_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id' : CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id Y) (inv_hom_id' : CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Z) (hom_inv_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp hom hom') (CategoryTheory.CategoryStruct.comp inv' inv) = CategoryTheory.CategoryStruct.id X) (inv_hom_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp inv' inv) (CategoryTheory.CategoryStruct.comp hom hom') = CategoryTheory.CategoryStruct.id Z) : CategoryTheory.Iso.mk hom inv ≪≫ CategoryTheory.Iso.mk hom' inv' = CategoryTheory.Iso.mk (CategoryTheory.CategoryStruct.comp hom hom') (CategoryTheory.CategoryStruct.comp inv' inv)

@[simp]

theorem CategoryTheory.Iso.trans_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).symm = β.symm ≪≫ α.symm

@[simp]

theorem CategoryTheory.Iso.trans_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') : (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

@[simp]

theorem CategoryTheory.Iso.refl_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : CategoryTheory.Iso.refl X ≪≫ α = α

@[simp]

theorem CategoryTheory.Iso.trans_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α ≪≫ CategoryTheory.Iso.refl Y = α

@[simp]

theorem CategoryTheory.Iso.symm_self_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α.symm ≪≫ α = CategoryTheory.Iso.refl Y

@[simp]

theorem CategoryTheory.Iso.self_symm_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) : α ≪≫ α.symm = CategoryTheory.Iso.refl X

@[simp]

theorem CategoryTheory.Iso.symm_self_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) (β : Y ≅ Z) : α.symm ≪≫ α ≪≫ β = β

@[simp]

theorem CategoryTheory.Iso.self_symm_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) (β : X ≅ Z) : α ≪≫ α.symm ≪≫ β = β

theorem CategoryTheory.Iso.inv_comp_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp α.inv f = g ↔ f = CategoryTheory.CategoryStruct.comp α.hom g

theorem CategoryTheory.Iso.eq_inv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : g = CategoryTheory.CategoryStruct.comp α.inv f ↔ CategoryTheory.CategoryStruct.comp α.hom g = f

theorem CategoryTheory.Iso.comp_inv_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : CategoryTheory.CategoryStruct.comp f α.inv = g ↔ f = CategoryTheory.CategoryStruct.comp g α.hom

theorem CategoryTheory.Iso.eq_comp_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : g = CategoryTheory.CategoryStruct.comp f α.inv ↔ CategoryTheory.CategoryStruct.comp g α.hom = f

theorem CategoryTheory.Iso.inv_eq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ≅ Y) (g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom

theorem CategoryTheory.Iso.hom_comp_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp α.hom f = CategoryTheory.CategoryStruct.id X ↔ f = α.inv

theorem CategoryTheory.Iso.comp_hom_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp f α.hom = CategoryTheory.CategoryStruct.id Y ↔ f = α.inv

theorem CategoryTheory.Iso.inv_comp_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp α.inv f = CategoryTheory.CategoryStruct.id Y ↔ f = α.hom

theorem CategoryTheory.Iso.comp_inv_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp f α.inv = CategoryTheory.CategoryStruct.id X ↔ f = α.hom

theorem CategoryTheory.Iso.hom_eq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom = α.inv

class CategoryTheory.IsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : Prop

IsIso typeclass expressing that a morphism is invertible.

• out : ∃ (inv : Y ⟶ X), CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y

  The existence of an inverse morphism.

noncomputable def CategoryTheory.inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : Y ⟶ X

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.IsIso.hom_inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.IsIso.inv_hom_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) f = CategoryTheory.CategoryStruct.id Y

@[simp]

theorem CategoryTheory.IsIso.hom_inv_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C} (g : X ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g) = g

@[simp]

theorem CategoryTheory.IsIso.inv_hom_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C} (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp f g) = g

noncomputable def CategoryTheory.asIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : X ≅ Y

Reinterpret a morphism f with an IsIso f instance as an Iso.

Equations

• CategoryTheory.asIso f = CategoryTheory.Iso.mk f (CategoryTheory.inv f)

@[simp]

theorem CategoryTheory.asIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : ∀ {x : CategoryTheory.IsIso f}, (CategoryTheory.asIso f).hom = f

@[simp]

theorem CategoryTheory.asIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : ∀ {x : CategoryTheory.IsIso f}, (CategoryTheory.asIso f).inv = CategoryTheory.inv f

instance CategoryTheory.IsIso.epi_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.Epi f

Equations

• (_ : CategoryTheory.Epi f) = (_ : CategoryTheory.Epi f)

instance CategoryTheory.IsIso.mono_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.Mono f

Equations

• (_ : CategoryTheory.Mono f) = (_ : CategoryTheory.Mono f)

theorem CategoryTheory.IsIso.inv_eq_of_hom_inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : CategoryTheory.inv f = g

theorem CategoryTheory.IsIso.inv_eq_of_inv_hom_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (inv_hom_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y) : CategoryTheory.inv f = g

theorem CategoryTheory.IsIso.eq_inv_of_hom_inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : g = CategoryTheory.inv f

theorem CategoryTheory.IsIso.eq_inv_of_inv_hom_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (inv_hom_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id Y) : g = CategoryTheory.inv f

instance CategoryTheory.IsIso.id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X)) = (_ : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X))

instance CategoryTheory.IsIso.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ≅ Y) : CategoryTheory.IsIso f.hom

Equations

• (_ : CategoryTheory.IsIso f.hom) = (_ : CategoryTheory.IsIso f.hom)

instance CategoryTheory.IsIso.of_iso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ≅ Y) : CategoryTheory.IsIso f.inv

Equations

• (_ : CategoryTheory.IsIso f.inv) = (_ : CategoryTheory.IsIso f.symm.hom)

instance CategoryTheory.IsIso.inv_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] : CategoryTheory.IsIso (CategoryTheory.inv f)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.inv f)) = (_ : CategoryTheory.IsIso (CategoryTheory.asIso f).inv)

instance CategoryTheory.IsIso.comp_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [CategoryTheory.IsIso f] [CategoryTheory.IsIso h] : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f h)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f h)) = (_ : CategoryTheory.IsIso (CategoryTheory.asIso f ≪≫ CategoryTheory.asIso h).hom)

@[simp]

theorem CategoryTheory.IsIso.inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.inv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.IsIso.inv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [CategoryTheory.IsIso f] [CategoryTheory.IsIso h] : CategoryTheory.inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) (CategoryTheory.inv f)

@[simp]

theorem CategoryTheory.IsIso.inv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] : CategoryTheory.inv (CategoryTheory.inv f) = f

@[simp]

theorem CategoryTheory.IsIso.Iso.inv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ≅ Y) : CategoryTheory.inv f.inv = f.hom

@[simp]

theorem CategoryTheory.IsIso.Iso.inv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ≅ Y) : CategoryTheory.inv f.hom = f.inv

@[simp]

theorem CategoryTheory.IsIso.inv_comp_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ⟶ Y) [CategoryTheory.IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f = g ↔ f = CategoryTheory.CategoryStruct.comp α g

@[simp]

theorem CategoryTheory.IsIso.eq_inv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ⟶ Y) [CategoryTheory.IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} : g = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv α) f ↔ CategoryTheory.CategoryStruct.comp α g = f

@[simp]

theorem CategoryTheory.IsIso.comp_inv_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ⟶ Y) [CategoryTheory.IsIso α] {f : Z ⟶ Y} {g : Z ⟶ X} : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) = g ↔ f = CategoryTheory.CategoryStruct.comp g α

@[simp]

theorem CategoryTheory.IsIso.eq_comp_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (α : X ⟶ Y) [CategoryTheory.IsIso α] {f : Z ⟶ Y} {g : Z ⟶ X} : g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv α) ↔ CategoryTheory.CategoryStruct.comp g α = f

theorem CategoryTheory.IsIso.of_isIso_comp_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.IsIso g

theorem CategoryTheory.IsIso.of_isIso_comp_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.IsIso f

theorem CategoryTheory.IsIso.of_isIso_fac_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [CategoryTheory.IsIso f] [hh : CategoryTheory.IsIso h] (w : CategoryTheory.CategoryStruct.comp f g = h) : CategoryTheory.IsIso g

theorem CategoryTheory.IsIso.of_isIso_fac_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [CategoryTheory.IsIso g] [hh : CategoryTheory.IsIso h] (w : CategoryTheory.CategoryStruct.comp f g = h) : CategoryTheory.IsIso f

theorem CategoryTheory.eq_of_inv_eq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] (p : CategoryTheory.inv f = CategoryTheory.inv g) : f = g

theorem CategoryTheory.IsIso.inv_eq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} [CategoryTheory.IsIso f] [CategoryTheory.IsIso g] : CategoryTheory.inv f = CategoryTheory.inv g ↔ f = g

theorem CategoryTheory.hom_comp_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g

theorem CategoryTheory.comp_hom_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id Y ↔ f = CategoryTheory.inv g

theorem CategoryTheory.inv_comp_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f = CategoryTheory.CategoryStruct.id Y ↔ f = g

theorem CategoryTheory.comp_inv_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g) = CategoryTheory.CategoryStruct.id X ↔ f = g

theorem CategoryTheory.isIso_of_hom_comp_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} (h : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : CategoryTheory.IsIso f

theorem CategoryTheory.isIso_of_comp_hom_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} (h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id Y) : CategoryTheory.IsIso f

theorem CategoryTheory.Iso.inv_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X) : f.inv = g

theorem CategoryTheory.Iso.inv_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id 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 CategoryTheory.Iso.cancel_iso_hom_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ≅ Y) (g : Y ⟶ Z) (g' : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.comp f.hom g' ↔ g = g'

@[simp]

theorem CategoryTheory.Iso.cancel_iso_inv_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : Y ≅ X) (g : Y ⟶ Z) (g' : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f.inv g = CategoryTheory.CategoryStruct.comp f.inv g' ↔ g = g'

@[simp]

theorem CategoryTheory.Iso.cancel_iso_hom_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (f' : X ⟶ Y) (g : Y ≅ Z) : CategoryTheory.CategoryStruct.comp f g.hom = CategoryTheory.CategoryStruct.comp f' g.hom ↔ f = f'

@[simp]

theorem CategoryTheory.Iso.cancel_iso_inv_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (f' : X ⟶ Y) (g : Z ≅ Y) : CategoryTheory.CategoryStruct.comp f g.inv = CategoryTheory.CategoryStruct.comp f' g.inv ↔ f = f'

@[simp]

theorem CategoryTheory.Iso.cancel_iso_hom_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {X' : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Y ≅ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.hom) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.hom) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

@[simp]

theorem CategoryTheory.Iso.cancel_iso_inv_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {X' : C} {Y : C} {Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Z ≅ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.inv) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.inv) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

@[simp]

theorem CategoryTheory.Functor.mapIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (i : X ≅ Y) : (F.mapIso i).inv = F.toPrefunctor.map i.inv

@[simp]

theorem CategoryTheory.Functor.mapIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (i : X ≅ Y) : (F.mapIso i).hom = F.toPrefunctor.map i.hom

def CategoryTheory.Functor.mapIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (i : X ≅ Y) : F.toPrefunctor.obj X ≅ F.toPrefunctor.obj Y

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

Equations

• F.mapIso i = CategoryTheory.Iso.mk (F.toPrefunctor.map i.hom) (F.toPrefunctor.map i.inv)

@[simp]

theorem CategoryTheory.Functor.mapIso_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (i : X ≅ Y) : F.mapIso i.symm = (F.mapIso i).symm

@[simp]

theorem CategoryTheory.Functor.mapIso_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (i : X ≅ Y) (j : Y ≅ Z) : F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

@[simp]

theorem CategoryTheory.Functor.mapIso_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.mapIso (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl (F.toPrefunctor.obj X)

instance CategoryTheory.Functor.map_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (F.toPrefunctor.map f)

Equations

• (_ : CategoryTheory.IsIso (F.toPrefunctor.map f)) = (_ : CategoryTheory.IsIso (F.mapIso (CategoryTheory.asIso f)).hom)

@[simp]

theorem CategoryTheory.Functor.map_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : F.toPrefunctor.map (CategoryTheory.inv f) = CategoryTheory.inv (F.toPrefunctor.map f)

theorem CategoryTheory.Functor.map_hom_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (F.toPrefunctor.map (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)

theorem CategoryTheory.Functor.map_inv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.inv f)) (F.toPrefunctor.map f) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj Y)