English
Given a functor G and a natural isomorphism e, the localized map of Φ.smallHomMap f equals the composite e.hom.app X ⋯ G.map (equiv_{W1,L1} f) ⋯ e.inv.app Y.
Русский
Для данного G и натуралного изоморфизма e отображение SmallHom через Φ.smallHomMap согласуется с композициями через e.hom.app, G.map и e.inv.app.
LaTeX
$$$ (SmallHom.equiv W_2 L_2) (\Phi.smallHomMap f) = e.hom.app X \circ G.map (SmallHom.equiv W_1 L_1 f) \circ e.inv.app Y $$$
Lean4
theorem equiv_smallHomMap (G : D₁ ⥤ D₂) (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G) (f : SmallHom.{w} W₁ X Y) :
(SmallHom.equiv W₂ L₂) (Φ.smallHomMap f) = e.hom.app X ≫ G.map (SmallHom.equiv W₁ L₁ f) ≫ e.inv.app Y :=
by
obtain ⟨g, rfl⟩ := (SmallHom.equiv W₁ W₁.Q).symm.surjective f
simp only [smallHomMap, Equiv.apply_symm_apply]
let G' := Φ.localizedFunctor W₁.Q W₂.Q
let β := CatCommSq.iso Φ.functor W₁.Q W₂.Q G'
let E₁ := (uniq W₁.Q L₁ W₁).functor
let α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
let E₂ := (uniq W₂.Q L₂ W₂).functor
let α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
rw [SmallHom.equiv_equiv_symm W₁ W₁.Q L₁ E₁ α₁, SmallHom.equiv_equiv_symm W₂ W₂.Q L₂ E₂ α₂]
change α₂.inv.app _ ≫ E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ _ = _
let γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) _ _
((Functor.associator _ _ _).symm ≪≫
Functor.isoWhiskerRight β.symm E₂ ≪≫
Functor.associator _ _ _ ≪≫
Functor.isoWhiskerLeft _ α₂ ≪≫ e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ Functor.associator _ _ _)
have hγ :
∀ (X : C₁),
γ.hom.app (W₁.Q.obj X) =
E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X) :=
fun X ↦ by simp [γ, id_comp, comp_id]
simp only [Functor.map_comp, assoc]
erw [← NatIso.naturality_1 γ]
simp only [Functor.comp_map, ← cancel_epi (e.inv.app X), ← cancel_epi (G.map (α₁.hom.app X)),
← cancel_epi (γ.hom.app (W₁.Q.obj X)), assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc,
Iso.hom_inv_id_app, Functor.map_id, id_comp, Iso.hom_inv_id_app_assoc]
simp only [hγ, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id, id_comp, Iso.hom_inv_id_app_assoc,
Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]
