Documentation Verification Report

IsomorphismClasses

📁 Source: Mathlib/CategoryTheory/IsomorphismClasses.lean

Statistics

Metric	Count
Definitions `IsIsomorphic`, `isIsomorphicSetoid`, `isomorphismClasses`	3
Theorems `isIsomorphic_iff_nonempty_hom`	1
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
`IsIsomorphic` 📖	MathDef	1 math math: `Groupoid.isIsomorphic_iff_nonempty_hom`
`isIsomorphicSetoid` 📖	CompOp	23 math math: `ThinSkeleton.map_map`, `CommRing.Pic.mul_eq_tensor`, `ThinSkeleton.map_obj`, `ThinSkeleton.fromThinSkeleton_map`, `ThinSkeleton.fromThinSkeleton_obj`, `skeletonEquivalence_unitIso`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `CommRing.Pic.inv_eq_dual`, `CommRing.Pic.mk_eq_iff`, `CommRing.Pic.mk_eq_self`, `CommRing.Pic.mapAlgebra_apply`, `Subobject.inf_eq_map_pullback'`, `CommRing.Pic.ext_iff`, `CommRing.Pic.instFreeAsModuleOfNat`, `fromSkeleton_obj`, `fromSkeleton_map`, `Skeleton.comp_hom`, `toSkeletonFunctor_map_hom`, `ThinSkeleton.equiv_of_both_ways`, `Subobject.inf_eq_map_pullback`, `Skeleton.mul_eq`, `instInvertibleCarrierOutModuleCatValSkeleton`, `Skeleton.comp_hom_assoc`
`isomorphismClasses` 📖	CompOp	—

CategoryTheory.Groupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIsomorphic_iff_nonempty_hom` 📖	mathematical	—	`CategoryTheory.IsIsomorphic` `toCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`Equiv.nonempty_congr`

---

← Back to Index