English
A left-adjoint version of the commutative square lifting has a bijection with the right-adjoint version, respecting adjunction structure.
Русский
Левая версия подъема квадрата имеет биекцию с правой версией, сохраняющей структуру сопряжения.
LaTeX
$$$\mathrm{sq.left\_adjointLift} \cong (\mathrm{sq.right\_adjointLift})$$$
Lean4
/-- When we have an adjunction `G ⊣ F`, any commutative square where the left
map is of the form `i` and the right map is `F.map p` has an "adjoint" commutative
square whose left map is `G.map i` and whose right map is `p`. -/
theorem left_adjoint (sq : CommSq u i (F.map p) v) (adj : G ⊣ F) :
CommSq ((adj.homEquiv _ _).symm u) (G.map i) p ((adj.homEquiv _ _).symm v) :=
⟨by
simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
rw [G.map_comp, assoc, Adjunction.counit_naturality]⟩
