commShiftIso_inv_app_counit_app — Mathlib

English

A parallel explicit formula for the inverse of the iso adj a is given by a sequence of shifted unit, G-maps, and counit compositions.

Русский

Альтернативное явное выражение обратной стороны изоморфизма adj a через цепочку сдвигов единицы, отображений G, и кавитации.

LaTeX

$$$ (\mathrm{iso}(\mathrm{adj}, a)).\mathrm{inv}.\mathrm{app} Y = \text{long composite similar to the previous item}$$$

Lean4

@[reassoc (attr := simp)]
theorem commShiftIso_inv_app_counit_app [adj.CommShift A] (a : A) (Y : D) :
    ((G ⋙ F).commShiftIso a).inv.app Y ≫ adj.counit.app (Y⟦a⟧) = (adj.counit.app Y)⟦a⟧' := by
  simp [← cancel_epi (((G ⋙ F).commShiftIso _).hom.app _)]

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