English
Lift structures of a square are in bijection with lift structures of its right adjoint square via a canonical equivalence.
Русский
Структуры подъема квадрата эквивалентны структурам подъема правой пары через каноническое биекцию.
LaTeX
$$$\mathrm{sq.LiftStruct} \cong (\mathrm{sq.right\_adjoint}\;\mathrm{adj}).\mathrm{LiftStruct}$$$
Lean4
/-- The liftings of a commutative are in bijection with the liftings of its (right)
adjoint square. -/
def rightAdjointLiftStructEquiv : sq.LiftStruct ≃ (sq.right_adjoint adj).LiftStruct
where
toFun
l :=
{ l := adj.homEquiv _ _ l.l
fac_left := by rw [← adj.homEquiv_naturality_left, l.fac_left]
fac_right := by rw [← Adjunction.homEquiv_naturality_right, l.fac_right] }
invFun
l :=
{ l := (adj.homEquiv _ _).symm l.l
fac_left := by
rw [← Adjunction.homEquiv_naturality_left_symm, l.fac_left]
apply (adj.homEquiv _ _).left_inv
fac_right := by
rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]
apply (adj.homEquiv _ _).left_inv }
left_inv := by cat_disch
right_inv := by cat_disch
