ι_map_tensorHom_eq — Mathlib

English

Maps under ι commute with Day convolution's tensor-hom structure, in a corepresentable setting.

Русский

Отображения ι коммутируют с тензор-гом структурой Day-конволюции в рамках представления ядра.

LaTeX

$$$ (ι C V D).map (d \otimes d') = DayConvolution.map ((ι C V D).map d) ((ι C V D).map d') $$$

Lean4

theorem ι_map_tensorHom_eq {d₁ d₁' d₂ d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') :
    letI := mkMonoidalCategoryStruct C V D
    (ι C V D).map (f ⊗ₘ f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') :=
  by
  dsimp [mkMonoidalCategoryStruct]
  rw [tensorHom_eq]
  apply (convolutions C V d₁ d₁').corepresentableBy.homEquiv.injective
  dsimp
  ext ⟨u₁, u₂⟩
  dsimp
  simp only [DayConvolution.unit_app_map_app, Functor.comp_obj, tensor_obj]
  simp [convolutions, convolutionUnitApp_eq]

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