Mathlib Map

Structures · Category theory

CategoryTheory.IsIso

The IsIso typeclass expresses that a morphism is invertible. Given a morphism f with IsIso f, one can view f as an isomorphism via asIso f and get the inverse using inv f.

Defined in
Mathlib.CategoryTheory.Iso
Shape
One type argument · adds out
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Every CategoryTheory.IsIso is also a

Provided automatically by

Concrete types that are instances50

  • Quiver.Hom
  • CategoryTheory.Functor
  • CategoryTheory.Over
  • CategoryTheory.Discrete
  • ModuleCat
  • CategoryTheory.Grp
  • HomologicalComplex
  • Action
  • CategoryTheory.Mon
  • AlgebraicGeometry.Scheme
  • TopCat
  • CategoryTheory.MonoidalOpposite
  • SheafOfModules
  • CategoryTheory.Ind
  • CategoryTheory.Comma
  • CategoryTheory.WithTerminal
  • CategoryTheory.WithInitial
  • CommRingCat
  • AlgebraicGeometry.SheafedSpace
  • AlgebraicGeometry.LocallyRingedSpace
  • CategoryTheory.Sheaf
  • DerivedCategory
  • AlgebraicGeometry.Scheme.Modules
  • ContinuousGeneratedByCat
  • CategoryTheory.GradedObject
  • AlgebraicGeometry.PresheafedSpace
  • TopCat.Presheaf
  • ProfiniteGrp
  • CategoryTheory.Center
  • CategoryTheory.Limits.Cocone
  • CategoryTheory.Limits.Cone
  • CategoryTheory.Bundled.α
  • CategoryTheory.MorphismProperty.Comma
  • CategoryTheory.Limits.CatCospanTransform
  • CategoryTheory.MorphismProperty.LeftFraction.Localization
  • SSet
  • FGModuleCat
  • CategoryTheory.Cat
  • CochainComplex
  • Profinite
  • GeneratedByTopCat
  • CategoryTheory.SimplicialObject
  • LightCondSet
  • HomotopicalAlgebra.BifibrantObject.HoCat
  • CondensedSet
  • CategoryTheory.ComposableArrows
  • Ab
  • CategoryTheory.Limits.Fan
  • CategoryTheory.Abelian.Preradical
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by839

Ancestors17