instHasLift

Mathlib.CategoryTheory.LiftingProperties.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CommSq.instHasLift

English

If a square has a lift, then the right adjoint square also has a lift.

Русский

Если у квадрата есть подъем, то у правой сопряженной квадрата тоже есть подъем.

LaTeX

$$$\text{HasLift }(\mathrm{sq}) \Rightarrow \text{HasLift }(\mathrm{sq.right\_adjoint})$$$

Lean4

instance [HasLift sq] : HasLift (sq.right_adjoint adj) :=
  by
  rw [right_adjoint_hasLift_iff]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru