productConeIsLimit — Mathlib

English

There is an isomorphism between the categorical product cone and the ordinary product, realized by the universal property.

Русский

Существует изоморфизм между категориальным конусом произведения и обычным произведением, реализованный через универсальное свойство.

LaTeX

$$$ \text{There exists } \; \text{Iso}( \prod \text{Cone}, \text{of} ) $$$

Lean4

/-- The concrete product cone is limiting. -/
def productConeIsLimit : IsLimit (productCone Z)
    where
  lift s := ofHom (LinearMap.pi fun j => (s.π.app ⟨j⟩).hom : s.pt →ₗ[R] ∀ i : ι, Z i)
  uniq s m
    w := by
    ext x
    funext i
    exact DFunLike.congr_fun (congr_arg Hom.hom (w ⟨i⟩)) x

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