isRightAdjoint_of_iso — Mathlib

English

If F and G are functors with an isomorphism F ≅ G and F is a right adjoint, then G is also a right adjoint.

Русский

Если F и G — эндофункторы с изоморфизмом F ≅ G и F есть правый сопряжённый, то G тоже является правым сопряжённым.

LaTeX

$$$F \cong G \quad\&\&\quad F \text{ is a right adjoint }\Rightarrow G \text{ is a right adjoint}$$$

Lean4

/-- Transport being a right adjoint along a natural isomorphism. -/
theorem isRightAdjoint_of_iso {F G : C ⥤ D} (h : F ≅ G) [F.IsRightAdjoint] : IsRightAdjoint G where
  exists_leftAdjoint := ⟨_, ⟨(Adjunction.ofIsRightAdjoint F).ofNatIsoRight h⟩⟩

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