equivalence_counitIso_app — Mathlib

English

In the localization equivalence setup, the counit component at L₂.obj X is described via a specified isomorphism and the β component.

Русский

В рамках локализационной эквивалентности компонент counit при L₂.obj X описывается через заданный изоморфизм и компонент β.

LaTeX

$$$\big(\text{equivalence } L_1 W_1 L_2 W_2 G G' F F' \alpha \beta\big).\mathrm counitIso.app (L_2.obj X) = (\text{Lifting.iso } L_2 W_2 (F \circ G') (F' \circ G')).app X \;\;\Rightarrow\; \beta.app X$$$

Lean4

@[simp]
theorem equivalence_counitIso_app (X : C₂) :
    (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
      (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X :=
  by
  ext
  dsimp [equivalence, Equivalence.mk]
  rw [liftNatTrans_app]
  dsimp [Lifting.iso]
  rw [comp_id]

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