coskAdj — Mathlib

English

There is an adjunction between the n-truncation and the n-coskeleton: truncation_n ⊣ Truncated.cosk n.

Русский

Существует адъюнкция между n‑усечением и n‑коскелетоном: truncation_n ⊣ Truncated.cosk n.

LaTeX

$$$\mathrm{truncation}_n \dashv \mathrm{Truncated.cosk}_n$$$

Lean4

/-- The adjunction between n-truncation and the n-coskeleton. -/
noncomputable def coskAdj (n : ℕ) : truncation.{u} n ⊣ Truncated.cosk n :=
  SimplicialObject.coskAdj n

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