skeletonEquiv — Mathlib

English

Two categorically equivalent categories have skeletons that are equivalent as categories.

Русский

Две категориально эквивалентные категории имеют эквивалентные их скелеты как категории.

LaTeX

$$$\\mathrm{Skeleton}(C) \\simeq \\mathrm{Skeleton}(D)$ for any equivalence $C \\simeq D$$$

Lean4

/-- Two categories which are categorically equivalent have skeletons with equivalent objects.
-/
noncomputable def skeletonEquiv (e : C ≌ D) : Skeleton C ≃ Skeleton D :=
  let f := ((skeletonEquivalence C).trans e).trans (skeletonEquivalence D).symm
  { toFun := f.functor.obj
    invFun := f.inverse.obj
    left_inv := fun X => skeleton_skeletal C ⟨(f.unitIso.app X).symm⟩
    right_inv := fun Y => skeleton_skeletal D ⟨f.counitIso.app Y⟩ }

Похожие утверждения