English
Applying homEquiv twice is the same as a single homEquiv for the composed target functors; this uses homMap_homMap.
Русский
Применение homEquiv дважды эквивалентно однократному homEquiv для композиции целевых функторов; используется homMap_homMap.
LaTeX
$$$ homEquiv W L_2 L_3 (homEquiv W L_1 L_2 f) = homEquiv W L_1 L_3 f $$$
Lean4
@[simp]
theorem homMap_homMap (f : L₁.obj X ⟶ L₁.obj Y) : Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f :=
by
let G := Φ.localizedFunctor L₁ L₂
let G' := Ψ.localizedFunctor L₂ L₃
let e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso _ _ _ _
let e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso _ _ _ _
rw [Φ.homMap_apply L₁ L₂ G e, Ψ.homMap_apply L₂ L₃ G' e',
(Φ.comp Ψ).homMap_apply L₁ L₃ (G ⋙ G')
(Functor.associator _ _ _ ≪≫
Functor.isoWhiskerLeft _ e' ≪≫
(Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight e _ ≪≫ Functor.associator _ _ _)]
dsimp
simp only [Functor.map_comp, assoc, comp_id, id_comp]
