right_adjoint_hasLift_iff — Mathlib

English

The equivalence between liftings has inverse maps that respect the adjunction structure.

Русский

Эквивалентность подъема имеет обратные отображения, сохраняющие структуру сопряжения.

LaTeX

$$$\text{toFunLike} : (\mathrm{sq.LiftStruct} \rightleftarrows (\mathrm{sq.right\_adjoint}\;\mathrm{adj}).LiftStruct)$$$

Lean4

/-- A square has a lifting if and only if its (right) adjoint square has a lifting. -/
theorem right_adjoint_hasLift_iff : HasLift (sq.right_adjoint adj) ↔ HasLift sq :=
  by
  simp only [HasLift.iff]
  exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

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