instIsRightAdjointPushforward — Mathlib

English

The pushforward functor is right adjoint to some left adjoint when defined by a top object.

Русский

Функтор pushforward является правым сопряжённым к левому при заданной верхней структуре.

LaTeX

$$$(\\text{pushforward} \\varphi) \\text{IsRightAdjoint}$$$

Lean4

instance : (pushforward.{u} φ).IsRightAdjoint :=
  Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top (pullbackObjIsDefined_eq_top φ)

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