English
Promotes a Lawful Day Convolution structure on D from an induced core structure using a fully faithful functor ι.
Русский
Устанавливает законную Day-конволюцию на D через индуцированную структуру ядра с помощью полноценно-фидельного функторa ι.
LaTeX
$$$ \text{induced.mkMonoidalCategoryStruct }(C,V,D) \Rightarrow \text{LawfulDayConvolutionMonoidalCategoryStruct } C V D $$$
Lean4
/-- Given a fully faithful functor `ι : C ⥤ V ⥤ D`,
a family of Day convolutions, candidate functions for `tensorObj` and `tensorHom`,
suitable isomorphisms
`ι.obj (tensorObj d d') ≅ ι.obj (tensorObj d) ⊛ ι.obj (tensorObj d')`
that behave in a lawful way with respect to the chosen Day convolutions, we can
construct a `MonoidalCategoryStruct` on `D`. -/
abbrev mkMonoidalCategoryStruct : MonoidalCategoryStruct D
where
tensorObj := tensorObj C V
tensorHom := tensorHom
tensorUnit := tensorUnit C V D
whiskerLeft x {_ _} f := tensorHom (𝟙 x) f
whiskerRight f x := tensorHom f (𝟙 x)
associator x y
z :=
-- To make this work we use the better instance `convolutions`
letI : DayConvolution (ι C V D |>.obj x) ((ι C V D |>.obj y) ⊛ (ι C V D |>.obj z)) := convolutions C V _ _
letI : DayConvolution ((ι C V D |>.obj x) ⊛ (ι C V D |>.obj y)) (ι C V D |>.obj z) := convolutions C V _ _
fullyFaithulι.preimageIso <| DayConvolution.associator (ι C V D |>.obj x) (ι C V D |>.obj y) (ι C V D |>.obj z)
leftUnitor
x :=
letI : DayConvolution (ι C V D |>.obj <| tensorUnit C V D) (ι C V D |>.obj x) := convolutions C V _ _
fullyFaithulι.preimageIso <| DayConvolutionUnit.leftUnitor (ι C V D |>.obj <| tensorUnit C V D) (ι C V D |>.obj x)
rightUnitor
x :=
letI : DayConvolution (ι C V D |>.obj x) (ι C V D |>.obj <| tensorUnit C V D) := convolutions C V _ _
fullyFaithulι.preimageIso <| DayConvolutionUnit.rightUnitor (ι C V D |>.obj <| tensorUnit C V D) (ι C V D |>.obj x)
