isLocalization

Mathlib.CategoryTheory.Localization.Bousfield

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.LeftBousfield.isLocalization

English

The localization of W with respect to Set.range F.obj yields a localization of G.

Русский

Локализация W по Set.range F.obj образует локализацию G.

LaTeX

$$$\\text{isLocalization: } G.IsLocalization (W (\\cdot \\in Set.range F.obj))$$$

Lean4

theorem isLocalization : G.IsLocalization (W (· ∈ Set.range F.obj)) :=
  by
  rw [W_eq_inverseImage_isomorphisms adj]
  exact adj.isLocalization

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

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

Разделы

Аффилиация

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