Documentation

Mathlib.CategoryTheory.Iso

Isomorphisms #

This file defines isomorphisms between objects of a category.

Main definitions #

Notations #

Tags #

category, category theory, isomorphism

structure CategoryTheory.Iso {C : Type u} [inst : CategoryTheory.Category C] (X : C) (Y : C) :
  • The forward direction of an isomorphism.

    hom : X Y
  • The backwards direction of an isomorphism.

    inv : Y X
  • Composition of the two directions of an isomorphism is the identity on the source.

    hom_inv_id : autoParam (hom inv = 𝟙 X) _auto✝
  • Composition of the two directions of an isomorphism in reverse order is the identity on the target.

    inv_hom_id : autoParam (inv hom = 𝟙 Y) _auto✝

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 https://stacks.math.columbia.edu/tag/0017.

Instances For
    @[simp]
    theorem CategoryTheory.Iso.inv_hom_id_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (self : X Y) {Z : C} (h : Y Z) :
    self.inv self.hom h = h
    @[simp]
    theorem CategoryTheory.Iso.hom_inv_id_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (self : X Y) {Z : C} (h : X Z) :
    self.hom self.inv h = h

    Notation for an isomorphism in a category.

    Equations
    theorem CategoryTheory.Iso.ext {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} ⦃α : X Y ⦃β : X Y (w : α.hom = β.hom) :
    α = β
    def CategoryTheory.Iso.symm {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (I : X Y) :
    Y X

    Inverse isomorphism.

    Equations
    @[simp]
    theorem CategoryTheory.Iso.symm_hom {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) :
    (CategoryTheory.Iso.symm α).hom = α.inv
    @[simp]
    theorem CategoryTheory.Iso.symm_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) :
    (CategoryTheory.Iso.symm α).inv = α.hom
    @[simp]
    theorem CategoryTheory.Iso.symm_mk {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (hom : X Y) (inv : Y X) (hom_inv_id : hom inv = 𝟙 X) (inv_hom_id : inv hom = 𝟙 Y) :
    @[simp]
    theorem CategoryTheory.Iso.symm_eq_iff {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {α : X Y} {β : X Y} :
    def CategoryTheory.Iso.refl {C : Type u} [inst : CategoryTheory.Category C] (X : C) :
    X X

    Identity isomorphism.

    Equations
    Equations
    @[simp]
    theorem CategoryTheory.Iso.trans_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) (β : Y Z) :
    (α ≪≫ β).inv = β.inv α.inv
    @[simp]
    theorem CategoryTheory.Iso.trans_hom {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) (β : Y Z) :
    (α ≪≫ β).hom = α.hom β.hom
    def CategoryTheory.Iso.trans {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) (β : Y Z) :
    X Z

    Composition of two isomorphisms

    Equations
    @[simp]
    theorem CategoryTheory.Iso.instTransIso_trans {C : Type u} [inst : CategoryTheory.Category C] :
    ∀ {a b c : C} (α : a b) (β : b c), Trans.trans α β = α ≪≫ β
    instance CategoryTheory.Iso.instTransIso {C : Type u} [inst : CategoryTheory.Category C] :
    Trans (fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
    Equations
    • CategoryTheory.Iso.instTransIso = { trans := fun {a b c} => CategoryTheory.Iso.trans }

    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} [inst : CategoryTheory.Category C] {X : C} {Y : C} {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) :
    @[simp]
    theorem CategoryTheory.Iso.trans_symm {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) (β : Y Z) :
    @[simp]
    theorem CategoryTheory.Iso.trans_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {Z' : C} (α : X Y) (β : Y Z) (γ : Z Z') :
    (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ
    @[simp]
    theorem CategoryTheory.Iso.refl_trans {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) :
    @[simp]
    theorem CategoryTheory.Iso.trans_refl {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) :
    @[simp]
    theorem CategoryTheory.Iso.symm_self_id_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) (β : Y Z) :
    @[simp]
    theorem CategoryTheory.Iso.self_symm_id_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) (β : X Z) :
    theorem CategoryTheory.Iso.inv_comp_eq {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) {f : X Z} {g : Y Z} :
    α.inv f = g f = α.hom g
    theorem CategoryTheory.Iso.eq_inv_comp {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) {f : X Z} {g : Y Z} :
    g = α.inv f α.hom g = f
    theorem CategoryTheory.Iso.comp_inv_eq {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) {f : Z Y} {g : Z X} :
    f α.inv = g f = g α.hom
    theorem CategoryTheory.Iso.eq_comp_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) {f : Z Y} {g : Z X} :
    g = f α.inv g α.hom = f
    theorem CategoryTheory.Iso.inv_eq_inv {C : Type u} [inst : CategoryTheory.Category 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} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) {f : Y X} :
    α.hom f = 𝟙 X f = α.inv
    theorem CategoryTheory.Iso.comp_hom_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) {f : Y X} :
    f α.hom = 𝟙 Y f = α.inv
    theorem CategoryTheory.Iso.inv_comp_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) {f : X Y} :
    α.inv f = 𝟙 Y f = α.hom
    theorem CategoryTheory.Iso.comp_inv_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) {f : X Y} :
    f α.inv = 𝟙 X f = α.hom
    theorem CategoryTheory.Iso.hom_eq_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (α : X Y) (β : Y X) :
    α.hom = β.inv β.hom = α.inv
    class CategoryTheory.IsIso {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) :

    IsIso typeclass expressing that a morphism is invertible.

    Instances
      noncomputable def CategoryTheory.inv {C : Type u} [inst : CategoryTheory.Category 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
      @[simp]
      theorem CategoryTheory.IsIso.hom_inv_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [I : CategoryTheory.IsIso f] :
      @[simp]
      theorem CategoryTheory.IsIso.inv_hom_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [I : CategoryTheory.IsIso f] :
      @[simp]
      theorem CategoryTheory.IsIso.hom_inv_id_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [I : CategoryTheory.IsIso f] {Z : C} (g : X Z) :
      @[simp]
      theorem CategoryTheory.IsIso.inv_hom_id_assoc {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [I : CategoryTheory.IsIso f] {Z : C} (g : Y Z) :
      noncomputable def CategoryTheory.asIso {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso f] :
      X Y

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

      Equations
      @[simp]
      theorem CategoryTheory.asIso_hom {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso f] :
      @[simp]
      theorem CategoryTheory.asIso_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso f] :
      theorem CategoryTheory.IsIso.inv_eq_of_hom_inv_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} [inst : CategoryTheory.IsIso f] {g : Y X} (hom_inv_id : f g = 𝟙 X) :
      theorem CategoryTheory.IsIso.inv_eq_of_inv_hom_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} [inst : CategoryTheory.IsIso f] {g : Y X} (inv_hom_id : g f = 𝟙 Y) :
      theorem CategoryTheory.IsIso.eq_inv_of_hom_inv_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} [inst : CategoryTheory.IsIso f] {g : Y X} (hom_inv_id : f g = 𝟙 X) :
      theorem CategoryTheory.IsIso.eq_inv_of_inv_hom_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} [inst : CategoryTheory.IsIso f] {g : Y X} (inv_hom_id : g f = 𝟙 Y) :
      @[simp]
      theorem CategoryTheory.IsIso.inv_comp {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {f : X Y} {h : Y Z} [inst : CategoryTheory.IsIso f] [inst : CategoryTheory.IsIso h] :
      @[simp]
      theorem CategoryTheory.IsIso.inv_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} [inst : CategoryTheory.IsIso f] :
      @[simp]
      theorem CategoryTheory.IsIso.Iso.inv_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) :
      CategoryTheory.inv f.inv = f.hom
      @[simp]
      theorem CategoryTheory.IsIso.Iso.inv_hom {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) :
      CategoryTheory.inv f.hom = f.inv
      @[simp]
      theorem CategoryTheory.IsIso.inv_comp_eq {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) [inst : CategoryTheory.IsIso α] {f : X Z} {g : Y Z} :
      @[simp]
      theorem CategoryTheory.IsIso.eq_inv_comp {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) [inst : CategoryTheory.IsIso α] {f : X Z} {g : Y Z} :
      @[simp]
      theorem CategoryTheory.IsIso.comp_inv_eq {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) [inst : CategoryTheory.IsIso α] {f : Z Y} {g : Z X} :
      @[simp]
      theorem CategoryTheory.IsIso.eq_comp_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (α : X Y) [inst : CategoryTheory.IsIso α] {f : Z Y} {g : Z X} :
      theorem CategoryTheory.IsIso.of_isIso_comp_left {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) [inst : CategoryTheory.IsIso f] [inst : CategoryTheory.IsIso (f g)] :
      theorem CategoryTheory.IsIso.of_isIso_comp_right {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) [inst : CategoryTheory.IsIso g] [inst : CategoryTheory.IsIso (f g)] :
      theorem CategoryTheory.IsIso.of_isIso_fac_left {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} {h : X Z} [inst : CategoryTheory.IsIso f] [hh : CategoryTheory.IsIso h] (w : f g = h) :
      theorem CategoryTheory.IsIso.of_isIso_fac_right {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} {h : X Z} [inst : CategoryTheory.IsIso g] [hh : CategoryTheory.IsIso h] (w : f g = h) :
      theorem CategoryTheory.eq_of_inv_eq_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} {g : X Y} [inst : CategoryTheory.IsIso f] [inst : CategoryTheory.IsIso g] (p : CategoryTheory.inv f = CategoryTheory.inv g) :
      f = g
      theorem CategoryTheory.IsIso.inv_eq_inv {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} {g : X Y} [inst : CategoryTheory.IsIso f] [inst : CategoryTheory.IsIso g] :
      theorem CategoryTheory.hom_comp_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (g : X Y) [inst : CategoryTheory.IsIso g] {f : Y X} :
      theorem CategoryTheory.comp_hom_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (g : X Y) [inst : CategoryTheory.IsIso g] {f : Y X} :
      theorem CategoryTheory.inv_comp_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (g : X Y) [inst : CategoryTheory.IsIso g] {f : X Y} :
      theorem CategoryTheory.comp_inv_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (g : X Y) [inst : CategoryTheory.IsIso g] {f : X Y} :
      theorem CategoryTheory.isIso_of_hom_comp_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (g : X Y) [inst : CategoryTheory.IsIso g] {f : Y X} (h : g f = 𝟙 X) :
      theorem CategoryTheory.isIso_of_comp_hom_eq_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (g : X Y) [inst : CategoryTheory.IsIso g] {f : Y X} (h : f g = 𝟙 Y) :
      theorem CategoryTheory.Iso.inv_ext {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X Y} {g : Y X} (hom_inv_id : f.hom g = 𝟙 X) :
      f.inv = g
      theorem CategoryTheory.Iso.inv_ext' {C : Type u} [inst : CategoryTheory.Category C] {X : C} {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⟶ Y. Presumably we could write X ↪ Y↪ Y and X ↠ Y↠ Y.

      @[simp]
      theorem CategoryTheory.Iso.cancel_iso_hom_left {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (g' : Y Z) :
      f.hom g = f.hom g' g = g'
      @[simp]
      theorem CategoryTheory.Iso.cancel_iso_inv_left {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : Y X) (g : Y Z) (g' : Y Z) :
      f.inv g = f.inv g' g = g'
      @[simp]
      theorem CategoryTheory.Iso.cancel_iso_hom_right {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X Y) (f' : X Y) (g : Y Z) :
      f g.hom = f' g.hom f = f'
      @[simp]
      theorem CategoryTheory.Iso.cancel_iso_inv_right {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X Y) (f' : X Y) (g : Z Y) :
      f g.inv = f' g.inv f = f'
      @[simp]
      theorem CategoryTheory.Iso.cancel_iso_hom_right_assoc {C : Type u} [inst : CategoryTheory.Category 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) :
      f g h.hom = f' g' h.hom f g = f' g'
      @[simp]
      theorem CategoryTheory.Iso.cancel_iso_inv_right_assoc {C : Type u} [inst : CategoryTheory.Category 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) :
      f g h.inv = f' g' h.inv f g = f' g'
      @[simp]
      theorem CategoryTheory.Functor.mapIso_inv {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (i : X Y) :
      (CategoryTheory.Functor.mapIso F i).inv = F.map i.inv
      @[simp]
      theorem CategoryTheory.Functor.mapIso_hom {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (i : X Y) :
      (CategoryTheory.Functor.mapIso F i).hom = F.map i.hom
      def CategoryTheory.Functor.mapIso {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (i : X Y) :
      F.obj X F.obj Y

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

      Equations
      @[simp]
      theorem CategoryTheory.Functor.mapIso_trans {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} {Z : C} (i : X Y) (j : Y Z) :
      @[simp]
      theorem CategoryTheory.Functor.map_inv {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso f] :
      theorem CategoryTheory.Functor.map_hom_inv {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso f] :
      F.map f F.map (CategoryTheory.inv f) = 𝟙 (F.obj X)
      theorem CategoryTheory.Functor.map_inv_hom {C : Type u} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso f] :
      F.map (CategoryTheory.inv f) F.map f = 𝟙 (F.obj Y)