3.4. Isomorphisms
An isomorphism between two objects X and Y in a category
C is a term e in the type Iso X Y, which is denoted X ≅ Y
(type ≅ as \cong). It involves a morphism e.hom : X ⟶ Y in
the forward direction, a morphism e.inv : Y ⟶ X in the backwards
direction and two axioms e.hom_inv_id : e.hom ≫ e.inv = 𝟙 X and
e.inv_hom_id : e.inv ≫ e.hom = 𝟙 Y (which Lean tries to auto-fill
by cat_disch). For example, the composition of two isomorphisms
is defined as follows:
variable {X Y Z : C} (e₁ : X ≅ Y) (e₂ : Y ≅ Z)
-- the definition in mathlib is `Iso.trans`,
-- and it is denoted `e₁ ≪≫ e₂`
@[simps]
def Iso.trans' : X ≅ Z where
hom := e₁.hom ≫ e₂.hom
inv := e₂.inv ≫ e₁.inv
In particular, if F and G are functors in C ⥤ D, we may say that
they are naturally isomorphic when we have e : F ≅ G:
variable {F G : C ⥤ D} (e : F ≅ G)
example (X : C) : F.obj X ≅ G.obj X := e.app X
Terms in the type of isomorphisms X ≅ Y contain data. We also
have a Prop-valued typeclass IsIso f which can be used to
express that a morphism f : X ⟶ Y is an isomorphism.
variable (f : X ⟶ Y) [IsIso f]
-- `inv f` is a choice of inverse to `f`
noncomputable example : Y ⟶ X := inv f
example : f ≫ inv f = 𝟙 X := C:Type u_1D:Type u_2inst✝²:Category.{v_1, u_1} Cinst✝¹:Category.{v_2, u_2} DX:CY:CZ:Ce₁:X ≅ Ye₂:Y ≅ ZF:C ⥤ DG:C ⥤ De:F ≅ Gf:X ⟶ Yinst✝:IsIso f⊢ f ≫ inv f = 𝟙 X All goals completed! 🐙
example : inv f ≫ f = 𝟙 Y := C:Type u_1D:Type u_2inst✝²:Category.{v_1, u_1} Cinst✝¹:Category.{v_2, u_2} DX:CY:CZ:Ce₁:X ≅ Ye₂:Y ≅ ZF:C ⥤ DG:C ⥤ De:F ≅ Gf:X ⟶ Yinst✝:IsIso f⊢ inv f ≫ f = 𝟙 Y All goals completed! 🐙
-- `asIso f` promotes a morphism `f : X ⟶ Y`
-- to an isomorphism `X ≅ Y` when `[IsIso f]` holds
noncomputable example : X ≅ Y := asIso f