map_desc — Mathlib

English

The composition of a projection with a suitable map equals the corresponding component after applying the map.

Русский

Слоение проекции с подходящим отображением даёт соответствующую компоненту после применения отображения.

LaTeX

$$$\forall J\, {f g : J \to C} [HasBiproduct f] [HasBiproduct g] (p : \forall j, f j \to g j) {P : C} (k : \forall j, g j \to P) :\n biproduct.map p \; \gg \; biproduct.desc k = biproduct.desc (\lambda j, p j \circ k j)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_desc {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) {P : C} (k : ∀ j, g j ⟶ P) :
    biproduct.map p ≫ biproduct.desc k = biproduct.desc fun j => p j ≫ k j := by ext; simp

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