isLocalization_isoModSerre_kernel_of_leftAdjoint

English

If adj is a left adjoint with F full and faithful, then G.kernel.isoModSerre equals LeftBousfield.W on range F.obj.

Русский

Если adj — левый сопряженный с F полным и точным отображением, то G.kernel.isoModSerre равен LeftBousfield.W на диапазоне F.obj.

LaTeX

$$G.kernel.isoModSerre = LeftBousfield.W (\,\cdot\in Set.range F.obj)$$

Lean4

theorem isLocalization_isoModSerre_kernel_of_leftAdjoint {F : C ⥤ D} (adj : G ⊣ F) [F.Full] [F.Faithful] :
    G.IsLocalization G.kernel.isoModSerre :=
  by
  rw [isoModSerre_kernel_eq_inverseImage_isomorphisms G]
  exact adj.isLocalization

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