isIso_unit_iff_isIso_counit — Mathlib

English

For an adjoint triple F ⊣ G ⊣ H, the left adjoint’s unit is an isomorphism if and only if the right adjoint’s counit is an isomorphism.

Русский

Для троек смежностей F ⊣ G ⊣ H выполняется: единица левого смежного пары тождественна тождественному изоморосу тогда и только тогда, когда каунит правого смежного пара изоморос.

LaTeX

$$$\operatorname{IsIso}(t.adj_1.unit) \iff \operatorname{IsIso}(t.adj_2.counit).$$$

Lean4

theorem isIso_unit_iff_isIso_counit : IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit :=
  by
  let adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
  constructor
  · intro h
    let idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
    exact t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)
  · intro h
    let adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso t.adj₂.counit)
    exact t.adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

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