equivalence — Mathlib

English

There is an equivalence between ThinSkeleton C and C; the construction is described by skeleton equivalence.

Русский

Существует эквивалентность между ThinSkeleton C и C; конструирование задано эквивалентностью скелета.

LaTeX

$$equivalence : ThinSkeleton C ≌ C$$

Lean4

/-- The equivalence between the thin skeleton and the category itself. -/
noncomputable def equivalence : ThinSkeleton C ≌ C
    where
  functor := fromThinSkeleton C
  inverse := toThinSkeleton C
  counitIso := NatIso.ofComponents fun X => Nonempty.some (Quotient.mk_out X)
  unitIso :=
    NatIso.ofComponents fun x =>
      Quotient.recOnSubsingleton x fun X => eqToIso (Quotient.sound ⟨(Nonempty.some (Quotient.mk_out X)).symm⟩)

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