English
The symmetric of homEquiv sends the pair (W) to the reverse localization; it maps g to the corresponding symmetry partner.
Русский
Симметрия homEquiv переводит пару (W) в обратную локализацию; отображает g на соответствующую симметрическую пару.
LaTeX
$$$ (homEquiv W L_1 L_2).symm g = homEquiv W L_2 L_1 g $$$
Lean4
/-- Bijection between types of morphisms in two localized categories
for the same class of morphisms `W`. -/
@[simps -isSimp apply]
noncomputable def homEquiv : (L₁.obj X ⟶ L₁.obj Y) ≃ (L₂.obj X ⟶ L₂.obj Y)
where
toFun := (LocalizerMorphism.id W).homMap L₁ L₂
invFun := (LocalizerMorphism.id W).homMap L₂ L₁
left_inv
f := by
rw [LocalizerMorphism.homMap_homMap]
apply LocalizerMorphism.id_homMap
right_inv
g := by
rw [LocalizerMorphism.homMap_homMap]
apply LocalizerMorphism.id_homMap
