instMonoLiftπ — Mathlib

English

If F has a limit and F.obj has products, then the canonical lift to the product is mono.

Русский

Если у F есть предел, и у F.obj есть произведения, то канонический переход в произведение монофункционален.

LaTeX

$$$\text{Mono} (\mathrm{Pi.lift} (\mathrm{limit.\pi} F))$$$

Lean4

instance [HasLimit F] [HasProduct F.obj] : Mono (Pi.lift (limit.π F)) where
  right_cancellation _ _
    h := by
    refine limit.hom_ext fun j => ?_
    simpa using h =≫ Pi.π _ j

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