localization_counit_app — Mathlib

English

The additive structure transfers to the localization isomorphically: the Q'-localization is additive.

Русский

Аддитивная структура переносится в локализации без искажений: локализация Q' является аддитивной.

LaTeX

$$$\\text{instAdditiveLocalization'Q'} : W.Q'.Additive$$$

Lean4

@[simp]
theorem localization_counit_app (X₂ : C₂) :
    (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) =
      G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
        (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂) :=
  by apply Localization.η_app

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