localization_unit_app — Mathlib

English

The localization unit at L1 is given by a specified composite connecting the unit with isomorphisms and the forgetful functor.

Русский

Единица локализации на L1 задаётся конкретной композицией, соединяющей единицу с изоморфизмами и забывающим функтором.

LaTeX

$$$\\text{localization unit}$$$

Lean4

@[simp]
theorem localization_unit_app (X₁ : C₁) :
    (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) =
      L₁.map (adj.unit.app X₁) ≫
        (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) :=
  by apply Localization.ε_app

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