English
Let sq be a commutative square together with a left adjoint adj to a pair of functors G ⊣ F. Then the liftings of sq are in bijection with the liftings of its left-adjoint square (with respect to adj).
Русский
Пусть sq — коммутативный квадрат вместе с левой сопряжённой парой adj к парамFunctor G ⊣ F. Тогда подъёмы квадрата соответствуют друг другу; множество подъёмов sq гомогенны с множеством подъёмов его левого сопряженного квадрата.
LaTeX
$$$$ sq.LiftStruct \\cong (sq.left\\_adjoint adj).LiftStruct $$$$
Lean4
/-- The liftings of a commutative are in bijection with the liftings of its (left)
adjoint square. -/
def leftAdjointLiftStructEquiv : sq.LiftStruct ≃ (sq.left_adjoint adj).LiftStruct
where
toFun
l :=
{ l := (adj.homEquiv _ _).symm l.l
fac_left := by rw [← adj.homEquiv_naturality_left_symm, l.fac_left]
fac_right := by rw [← adj.homEquiv_naturality_right_symm, l.fac_right] }
invFun
l :=
{ l := (adj.homEquiv _ _) l.l
fac_left := by
rw [← adj.homEquiv_naturality_left, l.fac_left]
apply (adj.homEquiv _ _).right_inv
fac_right := by
rw [← adj.homEquiv_naturality_right, l.fac_right]
apply (adj.homEquiv _ _).right_inv }
left_inv := by cat_disch
right_inv := by cat_disch
