sigmaConstAdj — Mathlib

English

There is an adjunction between the coproduct functor indexed by a discrete index and the coyoneda functor at X.

Русский

Существуют сопряженные пары между суммирующей (ко-)построением функцией по дискретному индексу иCoyoneda-функтором на X.

LaTeX

$$$\sigma\text{Const}_X \dashv \mathrm{coyoneda}_{\mathrm{op}X}$$$

Lean4

/-- `n ↦ ∐ₙ X` is left adjoint to `Hom(X, -)`. -/
def sigmaConstAdj [Limits.HasCoproducts.{v} C] (X : C) : sigmaConst.obj X ⊣ coyoneda.obj (Opposite.op X)
    where
  unit := { app n i := Limits.Sigma.ι (fun _ : n ↦ X) i }
  counit := { app Y := Limits.Sigma.desc id }

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