leftUnitor_naturality — Mathlib

English

The left unitor is compatible with tensoring by a morphism, reflecting naturality of the left unitor with respect to tensoring.

Русский

Левый унитор совместим с тензорингом по морфизму, естественность левому унитору сохраняется при тензорировании.

LaTeX

$$$$ tensorHom \ℬ (f) (𝟙) ≫ leftUnitor.hom = leftUnitor.hom ≫ f $$$$

Lean4

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

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