sum_whiskerRight — Mathlib

English

For Q,R and a finite index set J with g_j: Q ⟶ R, the right whiskering with P distributes over finite sums: (∑ g_j) ▷ P = ∑ (g_j ▷ P).

Русский

Для Q,R и конечного индекса J с morphisms g_j: Q ⟶ R, правая штриховка на P распределяется по сумме: (∑ g_j) ▷ P = ∑ (g_j ▷ P).

LaTeX

$$$ \\left(\\sum_{j\\in s} g_j\\right) \\;\\triangleright\\; P = \\sum_{j\\in s} (g_j \\;\\triangleright\\; P) $$$

Lean4

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

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