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 of
iso; note that
IsIso fis a
Prop, 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
asIso: convert from
of_iso: convert from
- standard operations on isomorphisms (composition, inverse etc)
category, category theory, isomorphism
An isomorphism (a.k.a. an invertible morphism) between two objects of a category. The inverse morphism is bundled.
CategoryTheory.Core for the category with the same objects and isomorphisms playing
the role of morphisms.
- hom : X ⟶ Y
The forward direction of an isomorphism.
- inv : Y ⟶ X
The backwards direction of an isomorphism.
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.
Composition of two isomorphisms
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.
All these cancellation lemmas can be solved by
simp [cancel_mono] (or
but with the current design
cancel_mono is not a good
because it generates a typeclass search.
When we can see syntactically that a morphism is a
mono or an
because it came from an isomorphism, it's fine to do the cancellation via
In the longer term, it might be worth exploring making
rather than typeclasses, with coercions back to
X ⟶ Y.
Presumably we could write
X ↪ Y and
X ↠ Y.
F : C ⥤ D sends isomorphisms
i : X ≅ Y to isomorphisms
F.obj X ≅ F.obj Y