Structures · Category theory
CategoryTheory.Functor.IsIso
A functor F : C ⥤ D is an isomorphism of categories if it is full, faithful and
bijective on objects. Such a functor has a strict inverse Functor.strictInv and assembles
into an IsoCat via Functor.asIsomorphism.
- Defined in
- Mathlib.CategoryTheory.IsoCat
- Shape
- One type argument · adds faithful, full, bijective_obj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CategoryTheory.Functor.IsIso is also a
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CategoryTheory.Functor.objEquiv
- CategoryTheory.Functor.IsIso.bijective_obj
- CategoryTheory.instIsIsoComp
- CategoryTheory.Functor.instIsEquivalence
- CategoryTheory.Functor.asIsomorphism
- CategoryTheory.Functor.objEquiv_apply_symm_apply
- CategoryTheory.Functor.strictInv
- CategoryTheory.Functor.objEquiv.congr_simp
- CategoryTheory.Functor.IsIso.faithful
- CategoryTheory.instIsIsoStrictInv
- CategoryTheory.Functor.objEquiv_symm_apply_apply
- CategoryTheory.Functor.IsIso.full