mkLawfulDayConvolutionMonoidalCategoryStruct

English

Acompatibility between the associator under ι and the DayConvolution associator’s hom component.

Русский

Совместимость ассоциатора под ι и гом-части ассоциатора DayConvolution.

LaTeX

$$$ (ι C V D).map (α_ d d' d'').hom = (DayConvolution.associator (ι d) (ι d') (ι d'')).hom $$$

Lean4

/-- The monoidal category struct constructed in `DayConvolution.mkMonoidalCategoryStruct` extends
to a `LawfulDayConvolutionMonoidalCategoryStruct`. -/
def mkLawfulDayConvolutionMonoidalCategoryStruct :
    letI : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
    LawfulDayConvolutionMonoidalCategoryStruct C V D :=
  letI : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
  { ι := ι C V D
    faithful_ι := fullyFaithulι.faithful
    convolutionExtensionUnit d d' := (convolutions C V d d').unit
    isPointwiseLeftKanExtensionConvolutionExtensionUnit d d' := (convolutions C V d d').isPointwiseLeftKanExtensionUnit
    unitUnit := tensorUnitConvolutionUnit.can
    isPointwiseLeftKanExtensionUnitUnit := tensorUnitConvolutionUnit.isPointwiseLeftKanExtensionCan
    convolutionExtensionUnit_comp_ι_map_tensorHom_app :=
      by
      intros d₁ d₁' d₂ d₂' f f' x y
      simp [ι_map_tensorHom_eq C V D f f']
    convolutionExtensionUnit_comp_ι_map_whiskerLeft_app :=
      by
      intros d₁ d₂ d₂' f x y
      simp [← id_tensorHom, ι_map_tensorHom_eq C V D]
    convolutionExtensionUnit_comp_ι_map_whiskerRight_app :=
      by
      intros
      simp [← tensorHom_id, ι_map_tensorHom_eq C V D]
    associator_hom_unit_unit d₁ d₂ d₃ x₁ x₂
      x₃ :=
      by
      simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj, associator,
        Functor.FullyFaithful.preimageIso_hom, Functor.FullyFaithful.map_preimage]
      letI : DayConvolution (ι C V D |>.obj d₁) ((ι C V D |>.obj d₂) ⊛ (ι C V D |>.obj d₃)) := convolutions C V _ _
      letI : DayConvolution ((ι C V D |>.obj d₁) ⊛ (ι C V D |>.obj d₂)) (ι C V D |>.obj d₃) := convolutions C V _ _
      apply DayConvolution.associator_hom_unit_unit
    leftUnitor_hom_unit_app _
      _ :=
      by
      simp only [Functor.comp_obj, tensor_obj, leftUnitor, Functor.FullyFaithful.preimageIso_hom,
        Functor.FullyFaithful.map_preimage]
      apply DayConvolutionUnit.leftUnitor_hom_unit_app
    rightUnitor_hom_unit_app _
      _ :=
      by
      simp only [Functor.comp_obj, tensor_obj, rightUnitor, Functor.FullyFaithful.preimageIso_hom,
        Functor.FullyFaithful.map_preimage]
      apply DayConvolutionUnit.rightUnitor_hom_unit_app }

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