rightUnitor_naturality — Mathlib

English

TensorHom on chosen finite products respects composition componentwise; composing maps corresponds to composing their tensorHom images.

Русский

TensorHom на выбранных конечных произведениях сохраняет композицию компонент; композиция отображений соответствует композиции их тензорных изображений.

LaTeX

$$$$ tensorHom \ℬ f_1 f_2 ≫ tensorHom \ℬ g_1 g_2 = tensorHom \ℬ (f_1 ≫ g_1) (f_2 ≫ g_2) $$$$

Lean4

theorem rightUnitor_naturality (f : X₁ ⟶ X₂) :
    tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
      (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom ≫ f :=
  by simp [tensorHom]

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