English
For two localization functors L1,L2 and left fractions, the map compatibility condition holds: the derived maps coincide with a canonical comparison built from L1,L2 and the intermediate LeftFraction.
Русский
Для двух локализационных функторов L1,L2 и левых дробей выполняется совместимость отображений: полученные отображения совпадают с каноническим сравнением, построенным из L1,L2 и промежуточной LeftFraction.
LaTeX
$$$\forall {C D E} [\text{Category } C] [\text{Category } D] [\text{Category } E] {W} {X Y} (\phi : W.LeftFraction X Y) (L_1 : C \to D) (L_2 : C \to E) [L_1.IsLocalization W] [L_2.IsLocalization W],
(Localization.uniq L_1 L_2 W).functor.map (\phi.map L_1 (Localization.inverts L_1 W)) =
(Localization.compUniqFunctor L_1 L_2 W).hom.app X \circ\n \phi.map L_2 (Localization.inverts L_2 W) \circ (Localization.compUniqFunctor L_1 L_2 W).inv.app Y$$$
Lean4
theorem map_compatibility {W} {X Y : C} (φ : W.LeftFraction X Y) {E : Type*} [Category E] (L₁ : C ⥤ D) (L₂ : C ⥤ E)
[L₁.IsLocalization W] [L₂.IsLocalization W] :
(Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ (Localization.inverts L₁ W)) =
(Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫
φ.map L₂ (Localization.inverts L₂ W) ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app Y :=
by
let e := Localization.compUniqFunctor L₁ L₂ W
have := Localization.inverts L₂ W φ.s φ.hs
rw [← cancel_mono (e.hom.app Y), assoc, assoc, e.inv_hom_id_app, comp_id, ← cancel_mono (L₂.map φ.s), assoc, assoc,
map_comp_map_s, ← e.hom.naturality]
simpa [← Functor.map_comp_assoc, map_comp_map_s] using e.hom.naturality φ.f
