instPiObj — Mathlib

English

If each c(b) is injective, then the product (Pi-object) ∏ c is injective; more generally, a finite product (HasProduct) of injectives is injective.

Русский

Если каждый c(b) инъективен, то произведение (Pi) ∏ c инъективно; в частности, конечное произведение инъективных остаётся инъективным.

LaTeX

$$$$\forall b,\ \text{Injective}(c(b)) \Rightarrow \text{Injective}(\prod_{b} c(b)).$$$$

Lean4

instance {β : Type v} (c : β → C) [HasProduct c] [∀ b, Injective (c b)] : Injective (∏ᶜ c) where
  factors g f
    mono := by
    refine ⟨Pi.lift fun b => factorThru (g ≫ Pi.π c _) f, ?_⟩
    ext b
    simp only [Category.assoc, limit.lift_π, Fan.mk_π_app, comp_factorThru]

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