English
Legitimacy of the ι-map with respect to the Day convolution’s corepresentable map structure.
Русский
Правомерность ι-карты относительно структуры отображения Day-конволюционного ядра-образа.
LaTeX
$$$ (ι C V D).map (f \otimes f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') $$$
Lean4
/-- With the data of chosen isomorphic objects to given day convolutions,
and provably equal unit maps through these isomorphisms,
we can transform a given family of Day convolutions to one with
convolutions definitionally equals to the given objects, and component of units
definitionally equal to the provided map family. -/
def convolutions (d d' : D) : DayConvolution ((ι C V D).obj d) ((ι C V D).obj d')
where
convolution := (ι C V D).obj (tensorObj C V d d')
unit :=
{ app x := convolutionUnitApp V d d' x.1 x.2
naturality := by
intros
simp only [convolutionUnitApp_eq, Category.assoc, NatTrans.naturality_assoc]
simp }
isPointwiseLeftKanExtensionUnit :=
Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso
(StructuredArrow.isoMk (tensorObjIsoConvolution C V d d').symm
(by
ext ⟨x, y⟩
simp [convolutionUnitApp_eq V d d' x y]))
(convolutions' d d' |>.isPointwiseLeftKanExtensionUnit)
