Lean4
/-- If we have a map `G ⟶ G'` and a `DayConvolutionInternalHom F G' H'`, then
there is a unique map `H ⟶ H'` induced by functoriality of ends and functoriality
of `internalHomDiagramFunctor F`. -/
def map (ℌ : DayConvolutionInternalHom F G H) {G' : C ⥤ V} {H' : C ⥤ V} (f : G ⟶ G')
(ℌ' : DayConvolutionInternalHom F G' H') : H ⟶ H'
where
app
c :=
Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
(fun j ↦ (ℌ.π c j) ≫ (dayConvolutionInternalHomDiagramFunctor F |>.map f |>.app c |>.app (op j) |>.app j))
(fun ⦃j j'⦄ φ ↦
by
have :=
congrArg (fun t ↦ t.app j') <| dayConvolutionInternalHomDiagramFunctor F |>.map f |>.app c |>.naturality φ.op
dsimp at this ⊢
rw [Category.assoc, ← (ihom (F.obj j)).map_comp, ← f.naturality, Functor.map_comp, reassoc_of% ℌ.hπ]
simp)
naturality {c c'}
f := by
apply Wedge.IsLimit.hom_ext (ℌ'.isLimitWedge c')
intro j
dsimp
simp only [Category.assoc, map_comp_π]
rw [←
Wedge.mk_ι (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c') (H'.obj c') (ℌ'.π c') (ℌ'.hπ c'), ←
Wedge.mk_ι (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c) (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c'), Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)]
simp [← Functor.map_comp]
