English
The homEquiv is computed via a composite of the localized functor and the natural isomorphisms; it evaluates on f as the usual conjugation by the isomorphism e.
Русский
ГомЭкв выражается через локализованный функтор и натуральные изоморфизмы; на f оно принимает вид конъюгации изоморфизмом e.
LaTeX
$$$ \\mathrm{homEquiv } W L_1 L_2 f = e.hom.app X \\circ G.map f \\circ e.inv.app Y $$$
Lean4
@[reassoc]
theorem homMap_apply (G : D₁ ⥤ D₂) (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G) (f : L₁.obj X ⟶ L₁.obj Y) :
Φ.homMap L₁ L₂ f = e.hom.app X ≫ G.map f ≫ e.inv.app Y :=
by
let G' := Φ.localizedFunctor L₁ L₂
let e' := CatCommSq.iso Φ.functor L₁ L₂ G'
change e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = _
letI : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := ⟨e.symm⟩
let α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor ⋙ L₂) _ _ e'.symm
have : e = e' ≪≫ Functor.isoWhiskerLeft _ α := by
ext X
dsimp [α]
rw [Localization.liftNatTrans_app]
erw [id_comp]
rw [Iso.hom_inv_id_app_assoc]
rfl
simp [this]
