English
Let G have a left adjoint F with G inverting a class W of morphisms in C1, and assume the adjunction unit interacts compatibly with W. Then G exhibits C2 as the localization of C1 with respect to W.
Русский
Пусть у парыFunctor G ⊣ F существует левая сопряжённость, и множество W морфизмов C1 разворачивается этой связью через G; предположим совместимость единицы адъюнкции с W. Тогда G представляет собой локализацию C1 по отношению к W.
LaTeX
$$$\mathrm{IsLocalization}(G,W)$$$
Lean4
theorem isLocalization_leftAdjoint (adj : G ⊣ F) (W : MorphismProperty C₁) (hW : W.IsInvertedBy G)
(hW' : (W.functorCategory C₁) adj.unit) : G.IsLocalization W :=
by
let Φ : W.Localization ⥤ C₂ := Localization.lift _ hW W.Q
let e : W.Q ⋙ Φ ≅ G := by apply Localization.fac
have : IsIso (Functor.whiskerRight adj.unit W.Q) :=
by
rw [NatTrans.isIso_iff_isIso_app]
intro X
exact Localization.inverts W.Q W _ (hW' X)
exact
Functor.IsLocalization.of_equivalence_target W.Q W _
(Equivalence.mk Φ (F ⋙ W.Q)
(Localization.liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
(W.Q.leftUnitor.symm ≪≫ asIso (Functor.whiskerRight adj.unit W.Q) ≪≫ Functor.associator _ _ _))
(Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e ≪≫ asIso adj.counit))
e
