English
If L and L' are two localization functors for the same class of morphisms, there is a canonical equivalence between the structured arrows from X in the target with respect to L and L'.
Русский
Пусть L и L' — два локализационных функторов для одного и того же класса морфизмов; существует каноническое эквивалентное соответствие между структурированными стрелками из X относительно L и L'.
LaTeX
$$$\text{StructuredArrow}(L(X),L) \simeq \text{StructuredArrow}(L'(X),L')$$$
Lean4
/-- The bijection `StructuredArrow (L.obj X) L ≃ StructuredArrow (L'.obj X) L'`
when `L` and `L'` are two localization functors for the same class of morphisms. -/
@[simps]
noncomputable def structuredArrowEquiv : StructuredArrow (L.obj X) L ≃ StructuredArrow (L'.obj X) L'
where
toFun f := StructuredArrow.mk (homEquiv W L L' f.hom)
invFun f := StructuredArrow.mk (homEquiv W L' L f.hom)
left_inv
f := by
obtain ⟨Y, f, rfl⟩ := f.mk_surjective
dsimp
rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]
right_inv
f := by
obtain ⟨Y, f, rfl⟩ := f.mk_surjective
dsimp
rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]
