English
If e: C ≌ α is a categorical equivalence from a thin category C to a partial order α, then ThinSkeleton C is order-isomorphic to α.
Русский
Если e: C ≌ α — эквивалентность между тонкой категорией C и частичным порядком α, то ThinSkeleton C изоморфен по порядку α.
LaTeX
$$thinSkeletonOrderIso (e) : ThinSkeleton C ≃o α$$
Lean4
/-- An adjunction between thin categories gives an adjunction between their thin skeletons. -/
def lowerAdjunction (R : D ⥤ C) (L : C ⥤ D) (h : L ⊣ R) : ThinSkeleton.map L ⊣ ThinSkeleton.map R
where
unit :=
{
app := fun X => by
letI := isIsomorphicSetoid C
exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩ }
-- TODO: make quotient.rec_on_subsingleton' so the letI isn't needed
counit :=
{
app := fun X => by
letI := isIsomorphicSetoid D
exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩ }
