English
The constant functor on the opposite category taking every object to op X is naturally isomorphic to the opposite of the constant functor sending every object to X.
Русский
Постоянный функтор из противоположной категории, отправляющий каждый объект в op X, естественно изоморфен противоположному функтору, отправляющему каждый объект в X.
LaTeX
$$$ (\text{const } J^{\mathrm{op}})^{\mathrm{obj}}(\mathrm{op} X) \cong ((\text{const } J)^{\mathrm{obj}} X)^{\mathrm{op}}$$$
Lean4
/-- The constant functor `Jᵒᵖ ⥤ Cᵒᵖ` sending everything to `op X`
is (naturally isomorphic to) the opposite of the constant functor `J ⥤ C` sending everything to `X`.
-/
@[simps]
def opObjOp (X : C) : (const Jᵒᵖ).obj (op X) ≅ ((const J).obj X).op
where
hom := { app := fun _ => 𝟙 _ }
inv := { app := fun _ => 𝟙 _ }
