instProd — Mathlib

English

The product of injective objects is injective: if P and Q are injective, then P × Q is injective.

Русский

Произведение инъективных объектов инъективно: если P и Q инъективны, то P × Q инъективно.

LaTeX

$$$$\text{Injective}(P) \land \text{Injective}(Q) \Rightarrow \text{Injective}(P \times Q).$$$$

Lean4

instance {P Q : C} [HasBinaryProduct P Q] [Injective P] [Injective Q] : Injective (P ⨯ Q) where
  factors g f
    mono := by
    use Limits.prod.lift (factorThru (g ≫ Limits.prod.fst) f) (factorThru (g ≫ Limits.prod.snd) f)
    simp only [prod.comp_lift, comp_factorThru]
    ext
    · simp only [prod.lift_fst]
    · simp only [prod.lift_snd]

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