ofHasDayConvolutions — Mathlib

English

Extraction yielding a MonoidalCategoryStruct on D from Day convolution data and fully faithful ι.

Русский

Получение моноидальной структуры на D из данных Day конволюции и полностью верного ι.

LaTeX

$$$ \text{mkMonoidalCategoryStruct }(C,V,D) : \text{MonoidalCategoryStruct } D $$$

Lean4

/-- Given a fully faithful functor `ι : D ⥤ C ⥤ V` and mere existence of Day convolutions of
`ι.obj d` and `ι.obj d'` such that the convolution remains in the essential image of `ι`,
construct an `InducedLawfulDayConvolutionMonoidalCategoryStructCore` by letting all other
data be the generic ones from the `HasPointwiseLeftKanExtension` API. -/
noncomputable def ofHasDayConvolutions {D : Type u₃} [Category.{v₃} D] (ι : D ⥤ C ⥤ V) (ffι : ι.FullyFaithful)
    [hasDayConvolution : ∀ (d d' : D), (tensor C).HasPointwiseLeftKanExtension (ι.obj d ⊠ ι.obj d')]
    (essImageDayConvolution : ∀ (d d' : D), ι.essImage <| (tensor C).pointwiseLeftKanExtension (ι.obj d ⊠ ι.obj d'))
    [hasDayConvolutionUnit :
      (Functor.fromPUnit.{0} <| 𝟙_ C).HasPointwiseLeftKanExtension (Functor.fromPUnit.{0} <| 𝟙_ V)]
    (essImageDayConvolutionUnit :
      ι.essImage <| (Functor.fromPUnit.{0} <| 𝟙_ C).pointwiseLeftKanExtension (Functor.fromPUnit.{0} <| 𝟙_ V)) :
    InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
    where
  ι := ι
  fullyFaithulι := ffι
  tensorObj := fun d d' ↦ essImageDayConvolution d d' |>.witness
  convolutions' := fun d d' ↦
    { convolution := (tensor C).pointwiseLeftKanExtension (ι.obj d ⊠ ι.obj d')
      unit := (tensor C).pointwiseLeftKanExtensionUnit (ι.obj d ⊠ ι.obj d')
      isPointwiseLeftKanExtensionUnit :=
        (tensor C).pointwiseLeftKanExtensionIsPointwiseLeftKanExtension (ι.obj d ⊠ ι.obj d') }
  tensorObjIsoConvolution := fun d d' => Functor.essImage.getIso _
  tensorUnit := essImageDayConvolutionUnit.witness
  tensorUnitConvolutionUnit :=
    { can :=
        ((Functor.fromPUnit.{0} <| 𝟙_ C).pointwiseLeftKanExtensionUnit (Functor.fromPUnit.{0} <| 𝟙_ V)).app
            (.mk PUnit.unit) ≫
          (essImageDayConvolutionUnit.getIso.inv.app (𝟙_ C))
      isPointwiseLeftKanExtensionCan :=
        Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso
          (StructuredArrow.isoMk (essImageDayConvolutionUnit.getIso).symm)
          (Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension (Functor.fromPUnit.{0} <| 𝟙_ C)
            (Functor.fromPUnit.{0} <| 𝟙_ V)) }

Похожие утверждения