localization_app — Mathlib

English

For any X in C, the action of the localized CatCenter at L.obj X equals the image under L of the action of r at X: (r.localization L W).app (L.obj X) = L.map (r.app X).

Русский

Для любого X ∈ C локализация CatCenter по L.obj X равна изображению под L действия r в X: (r.localization L W).app (L.obj X) = L.map (r.app X).

LaTeX

$$$ (r.localization\; L\; W).app (L.obj X) = L.map (r.app X) $$$

Lean4

@[simp]
theorem localization_app (X : C) : (r.localization L W).app (L.obj X) = L.map (r.app X) :=
  by
  dsimp [localization]
  simp only [Localization.liftNatTrans_app, Functor.id_obj, Functor.whiskerRight_app, NatTrans.naturality,
    Functor.comp_map, Functor.id_map, Iso.hom_inv_id_app_assoc]

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