biproductComparison_π — Mathlib

English

The map biproductComparison correlates the universal biproduct projections with the componentwise projections after applying a functor.

Русский

Отображение biproductComparison соотносит универсальные проекции би-произведения с компонентными проекциями после применения функторa.

LaTeX

$$$\biproductComparison F f \;\; \text{and} \;\biproduct.\pi (F.obj f) j = F(\biproduct.\pi f j)$$$

Lean4

@[reassoc (attr := simp)]
theorem biproductComparison_π (j : J) : biproductComparison F f ≫ biproduct.π _ j = F.map (biproduct.π f j) :=
  biproduct.lift_π _ _

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