tensorProductAdjunction — Mathlib

English

There is an adjunction between the functors tensorLeft X and coyoneda.obj (Opposite.op X) for any type X.

Русский

Для любого типа X существует адъюнкция между функторами tensorLeft X и coyoneda.obj (Opposite.op X).

LaTeX

$$$ \text{tensorLeft}(X) \dashv \mathrm{coyoneda}(\mathrm{Opposite}(X)) $$$

Lean4

/-- The adjunction `tensorLeft.obj X ⊣ coyoneda.obj (Opposite.op X)`
for any `X : Type v₁`. -/
def tensorProductAdjunction (X : Type v₁) : tensorLeft X ⊣ coyoneda.obj (Opposite.op X)
    where
  unit := { app := fun Z (z : Z) x => ⟨x, z⟩ }
  counit := { app := fun _ xf => xf.2 xf.1 }

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