map_epi — Mathlib

English

If each component map p_j is epi, then the indexwise product map Pi.map p is epi.

Русский

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

LaTeX

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

Lean4

instance map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Epi (p j)] :
    Epi (Pi.map p) :=
  by
  rw [show Pi.map p = (biproduct.isoProduct _).inv ≫ biproduct.map p ≫ (biproduct.isoProduct _).hom by aesop]
  infer_instance

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