symmetry — Mathlib

English

If Day convolution F ⊠ G and G ⊠ F exist, then the braiding on Day convolution is symmetric, i.e., the braiding maps compose to the identity: (braiding F G)^{hom} ∘ (braiding G F)^{hom} = id.

Русский

Если существуют Day конволюции F ⊠ G и G ⊠ F, то Braiding на Day конволюции симметричен: композиция двух braiding даёт тождество.

LaTeX

$$$ (\\mathrm{braiding}_{F,G})^{\\mathrm{hom}} \\circ (\\mathrm{braiding}_{G,F})^{\\mathrm{hom}} = \\mathrm{id} $$$

Lean4

theorem symmetry [DayConvolution F G] [DayConvolution G F] : (braiding F G).hom ≫ (braiding G F).hom = 𝟙 _ :=
  by
  apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G) (unit F G)
  ext ⟨x, y⟩
  simp [← Functor.map_comp]

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