isLeftAdjoint_of_iso — Mathlib

English

If F and G are naturally isomorphic functors C → D and F is a left adjoint, then G is also a left adjoint.

Русский

Если два функторы F и G: C ⥤ D естественно изоморфны и F является левой адъюнктной, то и G является левой адъюнктной.

LaTeX

$$$F \\cong G \\;\\wedge\\; F \\text{ is a left adjoint} \\Rightarrow G \\text{ is a left adjoint}$$$

Lean4

/-- Transport being a left adjoint along a natural isomorphism. -/
theorem isLeftAdjoint_of_iso {F G : C ⥤ D} (h : F ≅ G) [IsLeftAdjoint F] : IsLeftAdjoint G where
  exists_rightAdjoint := ⟨_, ⟨(Adjunction.ofIsLeftAdjoint F).ofNatIsoLeft h⟩⟩

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