isLocalization_leftAdjoint' — Mathlib

English

If adjunction G ⊣ F with F full and faithful is given, then G is a localization for the inverse-image of isomorphisms, by a standard universal construction.

Русский

Если дана адъюнкция G ⊣ F с полной и верной F, то G является локализацией относительно образа изоморфизмов, достигаемым стандартной универсальной конструкцией.

LaTeX

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

Lean4

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

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