localization_one

Mathlib.CategoryTheory.Center.Localization

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatCenter.localization_one

English

The localization of the unit 1 in CatCenter C is 1 in CatCenter D.

Русский

Локализация единицы в CatCenter C равна единице в CatCenter D.

LaTeX

$$$1_{\!\text{CatCenter C}}.localization\;L\;W = 1_{\!\text{CatCenter D}}$$$

Lean4

theorem localization_one : (1 : CatCenter C).localization L W = 1 :=
  ext_of_localization L W _ _ (fun X => by simp)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru