biproduct_ι_comp_leftDistributor_hom

English

Let P ∈ C, s a Finset of J, and g_j: Q_j → R. Then P whiskers the finite sum equals the sum of whiskers: P ◁ ∑_{j∈s} g_j = ∑_{j∈s} (P ◁ g_j).

Русский

Пусть P ∈ C, s — конечный множитель, 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

@[reassoc (attr := simp)]
theorem biproduct_ι_comp_leftDistributor_hom {J : Type} [Finite J] (X : C) (f : J → C) (j : J) :
    (X ◁ biproduct.ι _ j) ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j := by
  classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.comp_sum, ← whiskerLeft_comp_assoc, biproduct.ι_π, whiskerLeft_dite, dite_comp]

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