map_π — Mathlib

English

If p_j are epimorphisms componentwise, then the product map is an epimorphism.

Русский

Если каждый компонент p_j является эпиморфизмом, то отображение на произведение является эпиморфизмом.

LaTeX

$$$\forall J\, C [HasBiproduct f] [HasBiproduct g] (p : \forall j, f j \to g j) [\forall j, Epi (p j)] : Epi (biproduct.map p)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_π {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) (j : J) :
    biproduct.map p ≫ biproduct.π g j = biproduct.π f j ≫ p j :=
  Limits.IsLimit.map_π _ _ _ (Discrete.mk j)

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