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 ofiso
; note thatIsIso f
is aProp
, 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 fromIsIso
toIso
(noncomputable);of_iso
: convert fromIso
toIsIso
;- standard operations on isomorphisms (composition, inverse etc)
Notations #
Tags #
category, category theory, isomorphism
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.
- hom : X ⟶ Y
The forward direction of an isomorphism.
- inv : Y ⟶ X
The backwards direction of an isomorphism.
- hom_inv_id : CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X
Composition of the two directions of an isomorphism is the identity on the source.
- inv_hom_id : CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y
Composition of the two directions of an isomorphism in reverse order is the identity on the target.
Instances For
Composition of the two directions of an isomorphism is the identity on the source.
Composition of the two directions of an isomorphism in reverse order is the identity on the target.
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
Inverse isomorphism.
Equations
- I.symm = { hom := I.inv, inv := I.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
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
Equations
- CategoryTheory.Iso.instInhabited = { default := CategoryTheory.Iso.refl X }
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
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
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
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
IsIso
typeclass expressing that a morphism is invertible.
- out : ∃ (inv : Y ⟶ X), CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y
The existence of an inverse morphism.
Instances
The existence of an inverse morphism.
The inverse of a morphism f
when we have [IsIso f]
.
Equations
Instances For
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Alias of CategoryTheory.Iso.isIso_hom
.
Alias of CategoryTheory.Iso.isIso_inv
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
.
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
Equations
- ⋯ = ⋯