English
Let W be a class of morphisms in a category C, and L1: C → D1, L2: C → D2 be localization functors with respect to W. For any morphism f: Y → X in C with hf ∈ W, the inverse of the isomorphism isoOfHom L1 W f hf in the localized category equals the inverse of isoOfHom L2 W f hf, when transported along the hom-equivalence between the two localizations.
Русский
Пусть W — класс морфизмов в категории C, а L1: C → D1 и L2: C → D2 — локализационные функторы по отношению к W. Для любого морфизма f: Y → X в C с hf ∈ W, обратный элемент изоморфизма isoOfHom L1 W f hf в локализованной категории совпадает с обратным элементом isoOfHom L2 W f hf при переносе через гом-эквивалентность между двумя локализациями.
LaTeX
$$$\operatorname{homEquiv}_{W,L_1,L_2}\big((\mathrm{isoOfHom}_{L_1}(W,f,hf))^{-1}\big) = (\mathrm{isoOfHom}_{L_2}(W,f,hf))^{-1}$$$
Lean4
theorem homEquiv_isoOfHom_inv (f : Y ⟶ X) (hf : W f) :
homEquiv W L₁ L₂ (isoOfHom L₁ W f hf).inv = (isoOfHom L₂ W f hf).inv := by
rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom, ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp,
isoOfHom_inv_hom_id, homEquiv_id]
