English
Let adj be an adjunction G ⊣ F with F full and faithful. Then G induces a localization of the domain category with respect to the image under G of isomorphisms in the codomain.
Русский
Пусть имеется сопряжение G ⊣ F с F полным и сохраняющим изоморфизмы. Тогда G индуцирует локализацию исходной категории по образу под G изоморфизм в кодомаршруте.
LaTeX
$$$G \\IsLocalization ((\\mathrm{MorphismProperty.isomorphisms}\\ C_2).inverseImage G)$$$
Lean4
theorem isLocalization [F.Full] [F.Faithful] : G.IsLocalization ((MorphismProperty.isomorphisms C₂).inverseImage G) :=
by
let W := ((MorphismProperty.isomorphisms C₂).inverseImage G)
have hG : W.IsInvertedBy G := fun _ _ _ hf => hf
have : ∀ (X : C₁), IsIso ((whiskerRight adj.unit W.Q).app X) := fun X =>
Localization.inverts W.Q W _
(by
change IsIso _
infer_instance)
have : IsIso (whiskerRight adj.unit W.Q) := NatIso.isIso_of_isIso_app _
let e : W.Localization ≌ C₂ :=
Equivalence.mk (Localization.lift G hG W.Q) (F ⋙ W.Q)
(liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _ (W.Q.leftUnitor.symm ≪≫ asIso (whiskerRight adj.unit W.Q)))
(Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Localization.fac G hG W.Q) ≪≫ asIso adj.counit)
apply Functor.IsLocalization.of_equivalence_target W.Q W G e (Localization.fac G hG W.Q)
