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} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) :

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]

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

    @[simp]

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

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

    Notation for an isomorphism in a category.

    Equations
    Instances For
      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 = { hom := I.inv, inv := I.hom, hom_inv_id := , inv_hom_id := }
      Instances For
        @[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) :
        { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id }.symm = { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id }
        @[simp]
        theorem 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 α = β

        Identity isomorphism.

        Equations
        Instances For
          Equations
          @[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
          @[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
          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
          Instances For
            @[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 }

            Notation for composition of isomorphisms.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[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) :
              { 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 := CategoryTheory.CategoryStruct.comp hom hom', inv := CategoryTheory.CategoryStruct.comp inv' inv, hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }
              @[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]
              @[simp]
              @[simp]
              theorem CategoryTheory.Iso.symm_self_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) :
              @[simp]
              theorem CategoryTheory.Iso.self_symm_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) :
              @[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} :
              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} :
              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} :
              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} :
              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_eq_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (β : Y X) :
              α.hom = β.inv β.hom = α.inv
              @[simp]
              theorem CategoryTheory.Iso.homToEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} (f : Z X) :
              α.homToEquiv f = CategoryTheory.CategoryStruct.comp f α.hom
              @[simp]
              theorem CategoryTheory.Iso.homToEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} (g : Z Y) :
              α.homToEquiv.symm g = CategoryTheory.CategoryStruct.comp g α.inv
              def CategoryTheory.Iso.homToEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} :
              (Z X) (Z Y)

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

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Iso.homFromEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} (g : Y Z) :
                α.homFromEquiv.symm g = CategoryTheory.CategoryStruct.comp α.hom g
                @[simp]
                theorem CategoryTheory.Iso.homFromEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} (f : X Z) :
                α.homFromEquiv f = CategoryTheory.CategoryStruct.comp α.inv f
                def CategoryTheory.Iso.homFromEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {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
                  class CategoryTheory.IsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :

                  IsIso typeclass expressing that a morphism is invertible.

                  Instances
                    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
                    Instances For
                      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
                      Instances For
                        @[simp]
                        theorem CategoryTheory.asIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :
                        @[simp]
                        @[instance 100]
                        Equations
                        • =
                        @[instance 100]
                        Equations
                        • =
                        @[deprecated CategoryTheory.Iso.isIso_hom]
                        theorem CategoryTheory.IsIso.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (e : X Y) :

                        Alias of CategoryTheory.Iso.isIso_hom.

                        @[deprecated CategoryTheory.Iso.isIso_inv]

                        Alias of CategoryTheory.Iso.isIso_inv.

                        @[instance 900]
                        Equations
                        • =
                        @[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
                        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) :
                        @[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) :
                        @[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) :
                        @[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) :
                        @[simp]
                        theorem CategoryTheory.Iso.map_hom_inv_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {X : C} {Y : C} (e : X Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj X Z) :
                        @[simp]
                        theorem CategoryTheory.Iso.map_inv_hom_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {X : C} {Y : C} (e : X Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj Y Z) :
                        @[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.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.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.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
                          @[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