tensor_sum — Mathlib

English

Let P be fixed and consider a finite set s with g_j: P ⟶ Q_j and objects R,S. Then f ⊗ (∑ g_j) = ∑ (f ⊗ g_j).

Русский

Пусть фиксирован Морфизм f: P ⟶ Q и конечная сумма г_j: R_j ⟶ S_j, тогда f ⊗ (∑ g_j) = ∑ (f ⊗ g_j).

LaTeX

$$$ f \\otimes \\left(\\sum_{j\\in s} g_j\\right) = \\sum_{j\\in s} (f \\otimes g_j) $$$

Lean4

theorem tensor_sum {P Q R S : C} {J : Type*} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) :
    (f ⊗ₘ ∑ j ∈ s, g j) = ∑ j ∈ s, f ⊗ₘ g j := by simp only [tensorHom_def, whiskerLeft_sum, Preadditive.comp_sum]

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