Isomorphisms
This file defines isomorphisms between objects of a category.
Main definitions
structure iso: a bundled isomorphism between two objects of a category;class is_iso: an unbundled version ofiso; note thatis_iso fis usually not aProp, because it holds the inverse morphism;as_iso: convert fromis_isotoiso;of_iso: convert fromisotois_iso;- standard operations on isomorphisms (composition, inverse etc)
Notations
X ≅ Y: same asiso X Y;α ≪≫ β: composition of two isomorphisms; it is callediso.trans
Tags
category, category theory, isomorphism
- hom : X ⟶ Y
- inv : Y ⟶ X
- hom_inv_id' : c.hom ≫ c.inv = 𝟙 X . "obviously"
- inv_hom_id' : c.inv ≫ c.hom = 𝟙 Y . "obviously"
An isomorphism (a.k.a. an invertible morphism) between two objects of a category. The inverse morphism is bundled.
See also category_theory.core for the category with the same objects and isomorphisms playing
the role of morphisms.
@[ext]
theorem
category_theory.iso.ext
{C : Type u}
[category_theory.category C]
{X Y : C}
⦃α β : X ≅ Y⦄ :
Inverse isomorphism.
Equations
- I.symm = {hom := I.inv, inv := I.hom, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.iso.symm_hom
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
@[simp]
theorem
category_theory.iso.symm_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
@[simp]
theorem
category_theory.iso.symm_mk
{C : Type u}
[category_theory.category C]
{X Y : C}
(hom : X ⟶ Y)
(inv : Y ⟶ X)
(hom_inv_id : hom ≫ inv = 𝟙 X)
(inv_hom_id : inv ≫ hom = 𝟙 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
category_theory.iso.symm_symm_eq
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
@[simp]
theorem
category_theory.iso.symm_eq_iff
{C : Type u}
[category_theory.category C]
{X Y : C}
{α β : X ≅ Y} :
@[simp]
theorem
category_theory.iso.refl_hom
{C : Type u}
[category_theory.category C]
(X : C) :
(category_theory.iso.refl X).hom = 𝟙 X
@[simp]
theorem
category_theory.iso.refl_inv
{C : Type u}
[category_theory.category C]
(X : C) :
(category_theory.iso.refl X).inv = 𝟙 X
Identity isomorphism.
Equations
- category_theory.iso.refl X = {hom := 𝟙 X, inv := 𝟙 X, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
Equations
@[simp]
Composition of two isomorphisms
@[simp]
theorem
category_theory.iso.trans_mk
{C : Type u}
[category_theory.category C]
{X Y 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) :
{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 := hom ≫ hom', inv := inv' ≫ inv, hom_inv_id' := hom_inv_id'', inv_hom_id' := inv_hom_id''}
@[simp]
theorem
category_theory.iso.refl_trans
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
category_theory.iso.refl X ≪≫ α = α
@[simp]
theorem
category_theory.iso.trans_refl
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
α ≪≫ category_theory.iso.refl Y = α
@[simp]
theorem
category_theory.iso.symm_self_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
α.symm ≪≫ α = category_theory.iso.refl Y
@[simp]
theorem
category_theory.iso.self_symm_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(α : X ≅ Y) :
α ≪≫ α.symm = category_theory.iso.refl X
@[simp]
theorem
category_theory.iso.symm_self_id_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(α : X ≅ Y)
(β : Y ≅ Z) :
@[simp]
theorem
category_theory.iso.self_symm_id_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(α : X ≅ Y)
(β : X ≅ Z) :
@[class]
structure
category_theory.is_iso
{C : Type u}
[category_theory.category C]
{X Y : C} :
(X ⟶ Y) → Type v
- inv : Y ⟶ X
- hom_inv_id' : f ≫ category_theory.is_iso.inv f = 𝟙 X . "obviously"
- inv_hom_id' : category_theory.is_iso.inv f ≫ f = 𝟙 Y . "obviously"
is_iso typeclass expressing that a morphism is invertible.
This contains the data of the inverse, but is a subsingleton type.
Instances
- category_theory.is_iso.of_groupoid
- category_theory.is_iso.category_theory.is_iso
- category_theory.is_iso.of_iso
- category_theory.is_iso.of_iso_inverse
- category_theory.is_iso.inv_is_iso
- category_theory.is_iso.comp_is_iso
- category_theory.functor.map_is_iso
- category_theory.nat_iso.hom_app_is_iso
- category_theory.nat_iso.inv_app_is_iso
- category_theory.nat_iso.is_iso_of_is_iso_app'
- category_theory.is_iso_whisker_left
- category_theory.is_iso_whisker_right
- category_theory.limits.equalizer.ι_of_self
- category_theory.limits.coequalizer.π_of_self
- category_theory.limits.category_theory.is_iso
- category_theory.limits.kernel.ι_zero_is_iso
- category_theory.limits.cokernel.π_zero_is_iso
- category_theory.limits.kernel.of_cokernel_of_epi
- category_theory.limits.cokernel.of_kernel_of_mono
- category_theory.non_preadditive_abelian.is_iso_factor_thru_image
- category_theory.non_preadditive_abelian.is_iso_factor_thru_coimage
- category_theory.non_preadditive_abelian.is_iso_r
- category_theory.abelian.images.is_iso_factor_thru_image
- category_theory.abelian.coimages.is_iso_factor_thru_coimage
- category_theory.monoidal_category.tensor_is_iso
- category_theory.unit_is_iso_of_L_fully_faithful
- category_theory.counit_is_iso_of_R_fully_faithful
- category_theory.limits.prod_comparison_iso_of_preserves_binary_prods
- category_theory.strict_initial
- category_theory.μ_iso_of_reflective
- category_theory.reflective.category_theory.is_iso
def
category_theory.as_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[h : category_theory.is_iso f] :
X ≅ Y
Reinterpret a morphism f with an is_iso f instance as an iso.
Equations
- category_theory.as_iso f = {hom := f, inv := category_theory.is_iso.inv f h, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.as_iso_hom
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
(category_theory.as_iso f).hom = f
@[simp]
theorem
category_theory.as_iso_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.is_iso.hom_inv_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
f ≫ category_theory.is_iso.inv f = 𝟙 X
@[simp]
theorem
category_theory.is_iso.inv_hom_id
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
category_theory.is_iso.inv f ≫ f = 𝟙 Y
@[simp]
theorem
category_theory.is_iso.hom_inv_id_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
[category_theory.is_iso f]
(g : X ⟶ Z) :
f ≫ category_theory.is_iso.inv f ≫ g = g
@[simp]
theorem
category_theory.is_iso.inv_hom_id_assoc
{C : Type u}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
[category_theory.is_iso f]
(g : Y ⟶ Z) :
category_theory.is_iso.inv f ≫ f ≫ g = g
@[instance]
def
category_theory.is_iso.category_theory.is_iso
{C : Type u}
[category_theory.category C]
(X : C) :
Equations
- category_theory.is_iso.category_theory.is_iso X = {inv := 𝟙 X, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
def
category_theory.is_iso.of_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ≅ Y) :
Equations
- category_theory.is_iso.of_iso f = {inv := f.inv, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
def
category_theory.is_iso.of_iso_inverse
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ≅ Y) :
@[instance]
def
category_theory.is_iso.inv_is_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_iso f] :
@[instance]
def
category_theory.is_iso.comp_is_iso
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
[category_theory.is_iso f]
[category_theory.is_iso h] :
category_theory.is_iso (f ≫ h)
@[simp]
theorem
category_theory.is_iso.inv_id
{C : Type u}
[category_theory.category C]
{X : C} :
category_theory.is_iso.inv (𝟙 X) = 𝟙 X
@[simp]
theorem
category_theory.is_iso.inv_comp
{C : Type u}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
[category_theory.is_iso f]
[category_theory.is_iso h] :
@[simp]
theorem
category_theory.is_iso.inv_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.is_iso f] :
@[simp]
theorem
category_theory.is_iso.iso.inv_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ≅ Y) :
@[simp]
theorem
category_theory.is_iso.iso.inv_hom
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ≅ Y) :
@[instance]
def
category_theory.is_iso.epi_of_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
Equations
- _ = _
@[instance]
def
category_theory.is_iso.mono_of_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
Equations
- _ = _
theorem
category_theory.eq_of_inv_eq_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
{f g : X ⟶ Y}
[category_theory.is_iso f]
[category_theory.is_iso g] :
@[instance]
Equations
- _ = _
theorem
category_theory.is_iso.inv_eq_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
{f g : X ⟶ Y}
[category_theory.is_iso f]
[category_theory.is_iso g] :
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.
def
category_theory.functor.map_iso
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C} :
A functor F : C ⥤ D sends isomorphisms i : X ≅ Y to isomorphisms F.obj X ≅ F.obj Y
@[simp]
theorem
category_theory.functor.map_iso_hom
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(i : X ≅ Y) :
@[simp]
theorem
category_theory.functor.map_iso_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(i : X ≅ Y) :
@[simp]
theorem
category_theory.functor.map_iso_symm
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(i : X ≅ Y) :
@[simp]
theorem
category_theory.functor.map_iso_trans
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
(i : X ≅ Y)
(j : Y ≅ Z) :
@[simp]
theorem
category_theory.functor.map_iso_refl
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
F.map_iso (category_theory.iso.refl X) = category_theory.iso.refl (F.obj X)
@[instance]
def
category_theory.functor.map_is_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(f : X ⟶ Y)
[category_theory.is_iso f] :
category_theory.is_iso (F.map f)
Equations
@[simp]
theorem
category_theory.functor.map_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
F.map (category_theory.is_iso.inv f) = category_theory.is_iso.inv (F.map f)
theorem
category_theory.functor.map_hom_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
theorem
category_theory.functor.map_inv_hom
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso f] :