whiskerLeft_sum — Mathlib

English

For any P in C, any finite index set J, and any family g: J → (Q ⟶ R), left whiskering distributes over finite sums: P ◁ ∑_{j∈s} g_j = ∑_{j∈s} P ◁ g_j.

Русский

Для произвольного P ∈ C и любого конечного индекса J, где g_j: Q_j → R, левая штриховка распределяется по конечной сумме: P ◁ ∑ g_j = ∑ (P ◁ g_j).

LaTeX

$$$ P \\;\\triangleleft\\; \\sum_{j\\in s} g_j = \\sum_{j\\in s} (P \\;\\triangleleft\\; g_j) $$$

Lean4

theorem whiskerLeft_sum (P : C) {Q R : C} {J : Type*} (s : Finset J) (g : J → (Q ⟶ R)) :
    P ◁ ∑ j ∈ s, g j = ∑ j ∈ s, P ◁ g j :=
  map_sum ((tensoringLeft C).obj P).mapAddHom g s

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