# 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)

## Notation #

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

## Tags #

category, category theory, isomorphism

source
structure CategoryTheory.Iso {C : Type u} [Category.{v, u} C] (X 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.

- hom : X ⟶ Y

  The forward direction of an isomorphism.

- inv : Y ⟶ X

  The backwards direction of an isomorphism.

- hom_inv_id : CategoryStruct.comp self.hom self.inv = CategoryStruct.id X

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

- inv_hom_id : CategoryStruct.comp self.inv self.hom = CategoryStruct.id Y

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

Instances For

source
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : X ⟶ Z) :
CategoryStruct.comp self.hom (CategoryStruct.comp self.inv h) = h
source
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : Y ⟶ Z) :
CategoryStruct.comp self.inv (CategoryStruct.comp self.hom h) = h
source
def CategoryTheory.«term_≅_» :
Lean.TrailingParserDescr

Notation for an isomorphism in a category.

Equations

- CategoryTheory.«term_≅_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_≅_» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ ") (Lean.ParserDescr.cat `term 10))

Instances For

source
theorem CategoryTheory.Iso.ext {C : Type u} [Category.{v, u} C] {X Y : C} ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) :
α = β
source
theorem CategoryTheory.Iso.ext_iff {C : Type u} [Category.{v, u} C] {X Y : C} {α β : X ≅ Y} :
α = β ↔ α.hom = β.hom
source
def CategoryTheory.Iso.symm {C : Type u} [Category.{v, u} 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 := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Iso.symm_hom {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
α.symm.hom = α.inv
source
@[simp]
theorem CategoryTheory.Iso.symm_inv {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
α.symm.inv = α.hom
source
@[simp]
theorem CategoryTheory.Iso.symm_mk {C : Type u} [Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryStruct.comp hom inv = CategoryStruct.id X) (inv_hom_id : CategoryStruct.comp inv hom = CategoryStruct.id 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 CategoryTheory.Iso.symm_symm_eq {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
α.symm.symm = α
source
theorem CategoryTheory.Iso.symm_bijective {C : Type u} [Category.{v, u} C] {X Y : C} :
Function.Bijective symm
source
@[simp]
theorem CategoryTheory.Iso.symm_eq_iff {C : Type u} [Category.{v, u} C] {X Y : C} {α β : X ≅ Y} :
α.symm = β.symm ↔ α = β
source
theorem CategoryTheory.Iso.nonempty_iso_symm {C : Type u} [Category.{v, u} C] (X Y : C) :
Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)
source
def CategoryTheory.Iso.refl {C : Type u} [Category.{v, u} C] (X : C) :
X ≅ X

Identity isomorphism.

Equations

- CategoryTheory.Iso.refl X = { hom := CategoryTheory.CategoryStruct.id X, inv := CategoryTheory.CategoryStruct.id X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Iso.refl_hom {C : Type u} [Category.{v, u} C] (X : C) :
(refl X).hom = CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.Iso.refl_inv {C : Type u} [Category.{v, u} C] (X : C) :
(refl X).inv = CategoryStruct.id X
source
instance CategoryTheory.Iso.instInhabited {C : Type u} [Category.{v, u} C] {X : C} :
Inhabited (X ≅ X)
Equations

- CategoryTheory.Iso.instInhabited = { default := CategoryTheory.Iso.refl X }

source
theorem CategoryTheory.Iso.nonempty_iso_refl {C : Type u} [Category.{v, u} C] (X : C) :
Nonempty (X ≅ X)
source
@[simp]
theorem CategoryTheory.Iso.refl_symm {C : Type u} [Category.{v, u} C] (X : C) :
(refl X).symm = refl X
source
def CategoryTheory.Iso.trans {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) :
X ≅ Z

Composition of two isomorphisms

Equations

- α ≪≫ β = { hom := CategoryTheory.CategoryStruct.comp α.hom β.hom, inv := CategoryTheory.CategoryStruct.comp β.inv α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Iso.trans_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) :
(α ≪≫ β).hom = CategoryStruct.comp α.hom β.hom
source
@[simp]
theorem CategoryTheory.Iso.trans_inv {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) :
(α ≪≫ β).inv = CategoryStruct.comp β.inv α.inv
source
instance CategoryTheory.Iso.instTransIso {C : Type u} [Category.{v, u} C] :
Trans (fun (x1 x2 : C) => x1 ≅ x2) (fun (x1 x2 : C) => x1 ≅ x2) fun (x1 x2 : C) => x1 ≅ x2
Equations

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

source
@[simp]
theorem CategoryTheory.Iso.trans_def {C : Type u} [Category.{v, u} C] {a✝ b✝ c✝ : C} (α : a✝ ≅ b✝) (β : b✝ ≅ c✝) :
Trans.trans α β = α ≪≫ β
source
def CategoryTheory.Iso.«term_≪≫_» :
Lean.TrailingParserDescr

Notation for composition of isomorphisms.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Iso.trans_mk {C : Type u} [Category.{v, u} C] {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryStruct.comp hom inv = CategoryStruct.id X) (inv_hom_id : CategoryStruct.comp inv hom = CategoryStruct.id Y) (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id' : CategoryStruct.comp hom' inv' = CategoryStruct.id Y) (inv_hom_id' : CategoryStruct.comp inv' hom' = CategoryStruct.id Z) (hom_inv_id'' : CategoryStruct.comp (CategoryStruct.comp hom hom') (CategoryStruct.comp inv' inv) = CategoryStruct.id X) (inv_hom_id'' : CategoryStruct.comp (CategoryStruct.comp inv' inv) (CategoryStruct.comp hom hom') = CategoryStruct.id 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 := CategoryStruct.comp hom hom', inv := CategoryStruct.comp inv' inv, hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }
source
@[simp]
theorem CategoryTheory.Iso.trans_symm {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) :
(α ≪≫ β).symm = β.symm ≪≫ α.symm
source
@[simp]
theorem CategoryTheory.Iso.trans_assoc {C : Type u} [Category.{v, u} C] {X Y Z Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') :
(α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
source
@[simp]
theorem CategoryTheory.Iso.refl_trans {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
refl X ≪≫ α = α
source
@[simp]
theorem CategoryTheory.Iso.trans_refl {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
α ≪≫ refl Y = α
source
@[simp]
theorem CategoryTheory.Iso.symm_self_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
α.symm ≪≫ α = refl Y
source
@[simp]
theorem CategoryTheory.Iso.self_symm_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) :
α ≪≫ α.symm = refl X
source
@[simp]
theorem CategoryTheory.Iso.symm_self_id_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z) :
α.symm ≪≫ α ≪≫ β = β
source
@[simp]
theorem CategoryTheory.Iso.self_symm_id_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : X ≅ Z) :
α ≪≫ α.symm ≪≫ β = β
source
theorem CategoryTheory.Iso.inv_comp_eq {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} :
CategoryStruct.comp α.inv f = g ↔ f = CategoryStruct.comp α.hom g
source
theorem CategoryTheory.Iso.eq_inv_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} :
g = CategoryStruct.comp α.inv f ↔ CategoryStruct.comp α.hom g = f
source
theorem CategoryTheory.Iso.comp_inv_eq {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} :
CategoryStruct.comp f α.inv = g ↔ f = CategoryStruct.comp g α.hom
source
theorem CategoryTheory.Iso.eq_comp_inv {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} :
g = CategoryStruct.comp f α.inv ↔ CategoryStruct.comp g α.hom = f
source
theorem CategoryTheory.Iso.inv_eq_inv {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ≅ Y) :
f.inv = g.inv ↔ f.hom = g.hom
source
theorem CategoryTheory.Iso.hom_comp_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X} :
CategoryStruct.comp α.hom f = CategoryStruct.id X ↔ f = α.inv
source
theorem CategoryTheory.Iso.comp_hom_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X} :
CategoryStruct.comp f α.hom = CategoryStruct.id Y ↔ f = α.inv
source
theorem CategoryTheory.Iso.inv_comp_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} :
CategoryStruct.comp α.inv f = CategoryStruct.id Y ↔ f = α.hom
source
theorem CategoryTheory.Iso.comp_inv_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} :
CategoryStruct.comp f α.inv = CategoryStruct.id X ↔ f = α.hom
source
theorem CategoryTheory.Iso.hom_eq_inv {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) (β : Y ≅ X) :
α.hom = β.inv ↔ β.hom = α.inv
source
def CategoryTheory.Iso.homToEquiv {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} :
(Z ⟶ X) ≃ (Z ⟶ Y)

The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`.

Equations

- α.homToEquiv = { toFun := fun (f : Z ⟶ X) => CategoryTheory.CategoryStruct.comp f α.hom, invFun := fun (g : Z ⟶ Y) => CategoryTheory.CategoryStruct.comp g α.inv, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Iso.homToEquiv_apply {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (f : Z ⟶ X) :
α.homToEquiv f = CategoryStruct.comp f α.hom
source
@[simp]
theorem CategoryTheory.Iso.homToEquiv_symm_apply {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (g : Z ⟶ Y) :
α.homToEquiv.symm g = CategoryStruct.comp g α.inv
source
def CategoryTheory.Iso.homFromEquiv {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} :
(X ⟶ Z) ≃ (Y ⟶ Z)

The bijection `(X ⟶ Z) ≃ (Y ⟶ Z)` induced by `α : X ≅ Y`.

Equations

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

Instances For

source
@[simp]
theorem CategoryTheory.Iso.homFromEquiv_symm_apply {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (g : Y ⟶ Z) :
α.homFromEquiv.symm g = CategoryStruct.comp α.hom g
source
@[simp]
theorem CategoryTheory.Iso.homFromEquiv_apply {C : Type u} [Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (f : X ⟶ Z) :
α.homFromEquiv f = CategoryStruct.comp α.inv f
source
class CategoryTheory.IsIso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) :
Prop

The `IsIso` typeclass expresses that a morphism is invertible.

Given a morphism `f` with `IsIso f`, one can view `f` as an isomorphism via `asIso f` and get the inverse using `inv f`.

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

  The existence of an inverse morphism.

Instances

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

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

Equations

- CategoryTheory.inv f = Classical.choose ⋯

Instances For

source
@[simp]
theorem CategoryTheory.IsIso.hom_inv_id {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : IsIso f] :
CategoryStruct.comp f (inv f) = CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.IsIso.inv_hom_id {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : IsIso f] :
CategoryStruct.comp (inv f) f = CategoryStruct.id Y
source
@[simp]
theorem CategoryTheory.IsIso.hom_inv_id_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : IsIso f] {Z : C} (g : X ⟶ Z) :
CategoryStruct.comp f (CategoryStruct.comp (inv f) g) = g
source
@[simp]
theorem CategoryTheory.IsIso.inv_hom_id_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : IsIso f] {Z : C} (g : Y ⟶ Z) :
CategoryStruct.comp (inv f) (CategoryStruct.comp f g) = g
source
instance CategoryTheory.Iso.isIso_hom {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) :
IsIso e.hom
source
instance CategoryTheory.Iso.isIso_inv {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) :
IsIso e.inv
source
noncomputable def CategoryTheory.asIso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
X ≅ Y

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

Equations

- CategoryTheory.asIso f = { hom := f, inv := CategoryTheory.inv f, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.asIso_hom {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
(asIso f).hom = f
source
@[simp]
theorem CategoryTheory.asIso_inv {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
(asIso f).inv = inv f
source
@[instance 100]
instance CategoryTheory.IsIso.epi_of_iso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
Epi f
source
@[instance 100]
instance CategoryTheory.IsIso.mono_of_iso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [IsIso f] :
Mono f
source
theorem CategoryTheory.IsIso.inv_eq_of_hom_inv_id {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryStruct.comp f g = CategoryStruct.id X) :
inv f = g
source
theorem CategoryTheory.IsIso.inv_eq_of_inv_hom_id {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : CategoryStruct.comp g f = CategoryStruct.id Y) :
inv f = g
source
theorem CategoryTheory.IsIso.eq_inv_of_hom_inv_id {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryStruct.comp f g = CategoryStruct.id X) :
g = inv f
source
theorem CategoryTheory.IsIso.eq_inv_of_inv_hom_id {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : CategoryStruct.comp g f = CategoryStruct.id Y) :
g = inv f
source
instance CategoryTheory.IsIso.id {C : Type u} [Category.{v, u} C] (X : C) :
IsIso (CategoryStruct.id X)
source
instance CategoryTheory.IsIso.inv_isIso {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [IsIso f] :
IsIso (inv f)
source
@[instance 900]
instance CategoryTheory.IsIso.comp_isIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [IsIso f] [IsIso h] :
IsIso (CategoryStruct.comp f h)
source
theorem CategoryTheory.IsIso.comp_isIso' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} :
IsIso f → IsIso h → IsIso (CategoryStruct.comp f h)

The composition of isomorphisms is an isomorphism. Here the arguments of type `IsIso` are explicit, to make this easier to use with the `refine` tactic, for instance.

source
@[simp]
theorem CategoryTheory.IsIso.inv_id {C : Type u} [Category.{v, u} C] {X : C} :
inv (CategoryStruct.id X) = CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.IsIso.inv_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [IsIso f] [IsIso h] :
inv (CategoryStruct.comp f h) = CategoryStruct.comp (inv h) (inv f)
source
theorem CategoryTheory.IsIso.inv_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} [IsIso f] [IsIso h] {Z✝ : C} (h✝ : X ⟶ Z✝) :
CategoryStruct.comp (inv (CategoryStruct.comp f h)) h✝ = CategoryStruct.comp (inv h) (CategoryStruct.comp (inv f) h✝)
source
@[simp]
theorem CategoryTheory.IsIso.inv_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [IsIso f] :
inv (inv f) = f
source
@[simp]
theorem CategoryTheory.IsIso.Iso.inv_inv {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ≅ Y) :
inv f.inv = f.hom
source
@[simp]
theorem CategoryTheory.IsIso.Iso.inv_hom {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ≅ Y) :
inv f.hom = f.inv
source
@[simp]
theorem CategoryTheory.IsIso.inv_comp_eq {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} :
CategoryStruct.comp (inv α) f = g ↔ f = CategoryStruct.comp α g
source
@[simp]
theorem CategoryTheory.IsIso.eq_inv_comp {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [IsIso α] {f : X ⟶ Z} {g : Y ⟶ Z} :
g = CategoryStruct.comp (inv α) f ↔ CategoryStruct.comp α g = f
source
@[simp]
theorem CategoryTheory.IsIso.comp_inv_eq {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [IsIso α] {f : Z ⟶ Y} {g : Z ⟶ X} :
CategoryStruct.comp f (inv α) = g ↔ f = CategoryStruct.comp g α
source
@[simp]
theorem CategoryTheory.IsIso.eq_comp_inv {C : Type u} [Category.{v, u} C] {X Y Z : C} (α : X ⟶ Y) [IsIso α] {f : Z ⟶ Y} {g : Z ⟶ X} :
g = CategoryStruct.comp f (inv α) ↔ CategoryStruct.comp g α = f
source
theorem CategoryTheory.IsIso.of_isIso_comp_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsIso (CategoryStruct.comp f g)] :
IsIso g
source
theorem CategoryTheory.IsIso.of_isIso_comp_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsIso (CategoryStruct.comp f g)] :
IsIso f
source
theorem CategoryTheory.IsIso.of_isIso_fac_left {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso f] [hh : IsIso h] (w : CategoryStruct.comp f g = h) :
IsIso g
source
theorem CategoryTheory.IsIso.of_isIso_fac_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso g] [hh : IsIso h] (w : CategoryStruct.comp f g = h) :
IsIso f
source
@[simp]
theorem CategoryTheory.isIso_comp_left_iff {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
IsIso (CategoryStruct.comp f g) ↔ IsIso g
source
@[simp]
theorem CategoryTheory.isIso_comp_right_iff {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] :
IsIso (CategoryStruct.comp f g) ↔ IsIso f
source
theorem CategoryTheory.eq_of_inv_eq_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [IsIso f] [IsIso g] (p : inv f = inv g) :
f = g
source
theorem CategoryTheory.IsIso.inv_eq_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} [IsIso f] [IsIso g] :
inv f = inv g ↔ f = g
source
theorem CategoryTheory.hom_comp_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} :
CategoryStruct.comp g f = CategoryStruct.id X ↔ f = inv g
source
theorem CategoryTheory.comp_hom_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} :
CategoryStruct.comp f g = CategoryStruct.id Y ↔ f = inv g
source
theorem CategoryTheory.inv_comp_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} :
CategoryStruct.comp (inv g) f = CategoryStruct.id Y ↔ f = g
source
theorem CategoryTheory.comp_inv_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [IsIso g] {f : X ⟶ Y} :
CategoryStruct.comp f (inv g) = CategoryStruct.id X ↔ f = g
source
theorem CategoryTheory.isIso_of_hom_comp_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : CategoryStruct.comp g f = CategoryStruct.id X) :
IsIso f
source
theorem CategoryTheory.isIso_of_comp_hom_eq_id {C : Type u} [Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : CategoryStruct.comp f g = CategoryStruct.id Y) :
IsIso f
source
theorem CategoryTheory.Iso.inv_ext {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryStruct.comp f.hom g = CategoryStruct.id X) :
f.inv = g
source
theorem CategoryTheory.Iso.inv_ext' {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryStruct.comp f.hom g = 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`.

source
@[simp]
theorem CategoryTheory.Iso.cancel_iso_hom_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ≅ Y) (g g' : Y ⟶ Z) :
CategoryStruct.comp f.hom g = CategoryStruct.comp f.hom g' ↔ g = g'
source
@[simp]
theorem CategoryTheory.Iso.cancel_iso_inv_left {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : Y ≅ X) (g g' : Y ⟶ Z) :
CategoryStruct.comp f.inv g = CategoryStruct.comp f.inv g' ↔ g = g'
source
@[simp]
theorem CategoryTheory.Iso.cancel_iso_hom_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z) :
CategoryStruct.comp f g.hom = CategoryStruct.comp f' g.hom ↔ f = f'
source
@[simp]
theorem CategoryTheory.Iso.cancel_iso_inv_right {C : Type u} [Category.{v, u} C] {X Y Z : C} (f f' : X ⟶ Y) (g : Z ≅ Y) :
CategoryStruct.comp f g.inv = CategoryStruct.comp f' g.inv ↔ f = f'
source
@[simp]
theorem CategoryTheory.Iso.cancel_iso_hom_right_assoc {C : Type u} [Category.{v, u} C] {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Y ≅ Z) :
CategoryStruct.comp f (CategoryStruct.comp g h.hom) = CategoryStruct.comp f' (CategoryStruct.comp g' h.hom) ↔ CategoryStruct.comp f g = CategoryStruct.comp f' g'
source
@[simp]
theorem CategoryTheory.Iso.cancel_iso_inv_right_assoc {C : Type u} [Category.{v, u} C] {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) (h : Z ≅ Y) :
CategoryStruct.comp f (CategoryStruct.comp g h.inv) = CategoryStruct.comp f' (CategoryStruct.comp g' h.inv) ↔ CategoryStruct.comp f g = CategoryStruct.comp f' g'
source
@[simp]
theorem CategoryTheory.Iso.map_hom_inv_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : Functor C D) :
CategoryStruct.comp (F.map e.hom) (F.map e.inv) = CategoryStruct.id (F.obj X)
source
@[simp]
theorem CategoryTheory.Iso.map_hom_inv_id_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : Functor C D) {Z : D} (h : F.obj X ⟶ Z) :
CategoryStruct.comp (F.map e.hom) (CategoryStruct.comp (F.map e.inv) h) = h
source
@[simp]
theorem CategoryTheory.Iso.map_inv_hom_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : Functor C D) :
CategoryStruct.comp (F.map e.inv) (F.map e.hom) = CategoryStruct.id (F.obj Y)
source
@[simp]
theorem CategoryTheory.Iso.map_inv_hom_id_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : Functor C D) {Z : D} (h : F.obj Y ⟶ Z) :
CategoryStruct.comp (F.map e.inv) (CategoryStruct.comp (F.map e.hom) h) = h
source
def CategoryTheory.Functor.mapIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor 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.mapIso i = { hom := F.map i.hom, inv := F.map i.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Functor.mapIso_hom {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (i : X ≅ Y) :
(F.mapIso i).hom = F.map i.hom
source
@[simp]
theorem CategoryTheory.Functor.mapIso_inv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (i : X ≅ Y) :
(F.mapIso i).inv = F.map i.inv
source
@[simp]
theorem CategoryTheory.Functor.mapIso_symm {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (i : X ≅ Y) :
F.mapIso i.symm = (F.mapIso i).symm
source
@[simp]
theorem CategoryTheory.Functor.mapIso_trans {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (i : X ≅ Y) (j : Y ≅ Z) :
F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j
source
@[simp]
theorem CategoryTheory.Functor.mapIso_refl {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
F.mapIso (Iso.refl X) = Iso.refl (F.obj X)
source
instance CategoryTheory.Functor.map_isIso {C : Type u} [Category.{v, u} C] {X Y : C} {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (f : X ⟶ Y) [IsIso f] :
IsIso (F.map f)
source
@[simp]
theorem CategoryTheory.Functor.map_inv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
F.map (inv f) = inv (F.map f)
source
theorem CategoryTheory.Functor.map_hom_inv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
CategoryStruct.comp (F.map f) (F.map (inv f)) = CategoryStruct.id (F.obj X)
source
theorem CategoryTheory.Functor.map_hom_inv_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [IsIso f] {Z : D} (h : F.obj X ⟶ Z) :
CategoryStruct.comp (F.map f) (CategoryStruct.comp (F.map (inv f)) h) = h
source
theorem CategoryTheory.Functor.map_inv_hom {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
CategoryStruct.comp (F.map (inv f)) (F.map f) = CategoryStruct.id (F.obj Y)
source
theorem CategoryTheory.Functor.map_inv_hom_assoc {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [IsIso f] {Z : D} (h : F.obj Y ⟶ Z) :
CategoryStruct.comp (F.map (inv f)) (CategoryStruct.comp (F.map f) h) = h