English
There is a natural isomorphism between the cocones in the setting of an adjunction, as described above.
Русский
Существуют естественные изоморфизмы коконов в рамках adjunction.
LaTeX
$$$$\\mathrm{Iso}\\Big((\\mathrm{cocones}\\ J\\ D)(\\operatorname{op}(K\\circ F)), G\\circ(\\mathrm{cocones}\\ J\\ C)(\\operatorname{op}K)\\Big).$$$$
Lean4
/-- When `F ⊣ G`,
the functor associating to each `Y` the cocones over `K ⋙ F` with cone point `Y`
is naturally isomorphic to
the functor associating to each `Y` the cocones over `K` with cone point `G.obj Y`.
-/
def coconesIso {J : Type u} [Category.{v} J] {K : J ⥤ C} :
(cocones J D).obj (op (K ⋙ F)) ≅ G ⋙ (cocones J C).obj (op K) :=
NatIso.ofComponents fun Y =>
{ hom := coconesIsoComponentHom adj Y
inv := coconesIsoComponentInv adj Y }
-- Note: this is natural in K, but we do not yet have the tools to formulate that.
