English
If Φ is a localized equivalence, then the induced functor on localized categories Φ.localizedFunctor L1 L2 is an equivalence.
Русский
Если Φ — локализованная эквивалентность, то локализованный функтор Φ.localizedFunctor L1 L2 является эквивалентностью.
LaTeX
$$$(\Phi.\text{localizedFunctor} L_1 L_2) \text{ is an equivalence}$$$
Lean4
theorem functor_linear_iff (F : C ⥤ E) (G : D ⥤ E) [Lifting L W F G] : F.Linear R ↔ G.Linear R :=
by
constructor
· intro
have : (L ⋙ G).Linear R := Functor.linear_of_iso _ (Lifting.iso L W F G).symm
have := Localization.essSurj L W
rw [Functor.linear_iff]
intro X r
have e := L.objObjPreimageIso X
have : r • 𝟙 X = e.inv ≫ (r • 𝟙 _) ≫ e.hom := by simp
rw [this, G.map_comp, G.map_comp, ← L.map_id, ← L.map_smul, ← Functor.comp_map, (L ⋙ G).map_smul, Functor.map_id,
Linear.smul_comp, Linear.comp_smul]
dsimp
rw [Category.id_comp, ← G.map_comp, e.inv_hom_id, G.map_id]
· intro
exact Functor.linear_of_iso _ (Lifting.iso L W F G)
