braiding_naturality_right — Mathlib

English

Corepresenting map for the inverse braiding of DayConvolution; defines a natural transformation from external product to tensor after applying the inverse braiding.

Русский

Ко-образующая карта для обратного braiding DayConvolution; задаёт естественную трансформацию из внешнего произведения в тензор после применения обратного braiding.

LaTeX

$$$\text{braidingInvCorepresenting} : G \odot F \to \mathrm{tensor}(C) \circ (F \odot G)$$$

Lean4

@[reassoc (attr := simp)]
theorem braiding_naturality_right (H : C ⥤ V) (η : F ⟶ G) [DayConvolution F H] [DayConvolution H F] [DayConvolution G H]
    [DayConvolution H G] :
    DayConvolution.map (𝟙 H) η ≫ (braiding H G).hom = (braiding H F).hom ≫ DayConvolution.map η (𝟙 H) :=
  by
  apply Functor.hom_ext_of_isLeftKanExtension (H ⊛ F) (unit H F)
  ext ⟨_, _⟩
  simp

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