limitSubobjectProduct — Mathlib

English

Given the equalizer and product data that yield a limit, the lifted maps satisfy the universal property.

Русский

Для данных равноселителя и произведений, образующий предел удовлетворяет общему свойству универсальности.

LaTeX

$$$IsLimit\,buildLimit\,s\,t\,hs\,ht$$$

Lean4

/-- A limit can be realised as a subobject of a product. -/
noncomputable def limitSubobjectProduct [HasLimitsOfSize.{w, w} C] (F : J ⥤ C) : limit F ⟶ ∏ᶜ fun j => F.obj j :=
  have := hasFiniteLimits_of_hasLimitsOfSize C
  (limit.isoLimitCone (limitConeOfEqualizerAndProduct F)).hom ≫ equalizer.ι _ _

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