isoCoskOfIsCoskeletal — Mathlib

English

If X is coskeletal, then X is isomorphic to its coskeleton (cosk n) applied to X.

Русский

Если X кососкелетно, то X изоморфно к (cosk n).obj X.

LaTeX

$$$[X.IsCoskeletal\ n] : X \cong (\cosk n).obj X$$$

Lean4

/-- The canonical isomorphism `X ≅ (cosk n).obj X` defined when `X` is coskeletal and the
`n`-coskeleton functor exists. -/
@[simps! hom]
noncomputable def isoCoskOfIsCoskeletal [X.IsCoskeletal n] : X ≅ (cosk n).obj X :=
  asIso ((coskAdj n).unit.app X)

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