Commit 2023-02-22 19:47 72ff023f

View on Github →

feat: port CategoryTheory.Skeletal (#2432)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Skeletal.lean

added theorem CategoryTheory.Functor.eq_of_iso

added structure CategoryTheory.IsSkeletonOf

added def CategoryTheory.Skeletal

added def CategoryTheory.Skeleton

added theorem CategoryTheory.ThinSkeleton.comp_toThinSkeleton

added theorem CategoryTheory.ThinSkeleton.equiv_of_both_ways

added def CategoryTheory.ThinSkeleton.lowerAdjunction

added def CategoryTheory.ThinSkeleton.map

added def CategoryTheory.ThinSkeleton.mapNatTrans

added theorem CategoryTheory.ThinSkeleton.map_comp_eq

added theorem CategoryTheory.ThinSkeleton.map_id_eq

added theorem CategoryTheory.ThinSkeleton.map_iso_eq

added def CategoryTheory.ThinSkeleton.map₂

added def CategoryTheory.ThinSkeleton.map₂Functor

added def CategoryTheory.ThinSkeleton.map₂NatTrans

added def CategoryTheory.ThinSkeleton.map₂ObjMap

added theorem CategoryTheory.ThinSkeleton.skeletal

added def CategoryTheory.ThinSkeleton

added theorem CategoryTheory.functor_skeletal

added theorem CategoryTheory.skeleton_skeletal

added def CategoryTheory.toThinSkeleton