English
The app at d for colimitPointwiseProductToProductColimit F equals a specified composition of evaluations and isomorphisms.
Русский
Приложение в d для colimitPointwiseProductToProductColimit F равно заданной композиции оценок и изоморфизмов.
LaTeX
$$colimitPointwiseProductToProductColimit_app (d) = (colimitObjIsoColimitCompEvaluation _ _).hom ≫ (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation F d)).hom ≫ colimitPointwiseProductToProductColimit _ ≫ (Pi.mapIso (fun _ => (colimitObjIsoColimitCompEvaluation _ _).symm)).hom ≫ (piObjIso _ _).inv$$
Lean4
/-- Evaluating the pointwise product `k ↦ ∏ᶜ fun (s : α) => (F s).obj (k s)` at `d` is the same as
taking the pointwise product `k ↦ ∏ᶜ fun (s : α) => ((F s).obj (k s)).obj d`. -/
@[simps!]
noncomputable def pointwiseProductCompEvaluation (d : D) :
pointwiseProduct F ⋙ (evaluation D C).obj d ≅ pointwiseProduct (fun s => F s ⋙ (evaluation _ _).obj d) :=
NatIso.ofComponents (fun k => piObjIso _ _) (fun f => Pi.hom_ext _ _ (by simp [← NatTrans.comp_app]))
