tensorHom_def' — Mathlib

English

The tensor product of morphisms f: X₁ → Y₁ and g: X₂ → Y₂ is defined by f ⊗ₘ g = X₁ ◁ g ≫ f ▷ Y₂.

Русский

Тензорное произведение морфизмов f: X₁ → Y₁ и g: X₂ → Y₂ определяется как f ⊗ₘ g = X₁ ◁ g ≫ f ▷ Y₂.

LaTeX

$$$ f \\otimes_{\\mathrm{⊗}} g = X_1 \\triangleleft g \\;\\;\\; \\; \\; ≫ f \\triangleright Y_2 $$$

Lean4

@[reassoc]
theorem tensorHom_def' {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : f ⊗ₘ g = X₁ ◁ g ≫ f ▷ Y₂ :=
  whisker_exchange f g ▸ tensorHom_def f g

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