right_adjoint — Mathlib

English

A square has a lift if and only if its right adjoint square has a lift.

Русский

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

LaTeX

$$$\text{HasLift }(\mathrm{sq.right\_adjoint}\;\mathrm{adj}) \iff \text{HasLift }\mathrm{sq}$$$

Lean4

/-- When we have an adjunction `G ⊣ F`, any commutative square where the left
map is of the form `G.map i` and the right map is `p` has an "adjoint" commutative
square whose left map is `i` and whose right map is `F.map p`. -/
theorem right_adjoint (sq : CommSq u (G.map i) p v) (adj : G ⊣ F) :
    CommSq (adj.homEquiv _ _ u) i (F.map p) (adj.homEquiv _ _ v) :=
  ⟨by
    simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
    rw [F.map_comp, Adjunction.unit_naturality_assoc]⟩

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