isLocalization_rightAdjoint' — Mathlib

English

A dual statement to Left Localization', asserting that the right adjoint case yields localization with respect to the same inverted class.

Русский

Дуальное утверждение к левому случаю: правая версия локализации по тем же инвертируемым морфизмам.

LaTeX

$$$\mathrm{IsLocalization}(G, (\mathrm{isomorphisms}(C_2))^{-1}\!\text{-image } G)$$$

Lean4

theorem isLocalization_rightAdjoint' (adj : F ⊣ G) : G.IsLocalization ((isomorphisms C₂).inverseImage G) :=
  adj.isLocalization_rightAdjoint _ (fun _ _ _ h ↦ h) adj.functorCategory_inverseImage_isomorphisms_counit

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