finiteSubproductsCone — Mathlib

English

A detailed proof that the finite-subproducts cone is a limit, via a comparison with the lifted limit cone and a cone-extensional argument.

Русский

Подробное доказательство того, что конус конечных подпроизведений действительно является пределом, через сравнение с поднимаемым пределом и аргумент о расширении конуса.

LaTeX

$$$$ \text{isLimitFiniteSubproductsCone}(f) \;=\; \text{IsLimit}(\mathrm{finiteSubproductsCone}\ f). $$$$

Lean4

/-- The converse of the construction in `liftToFinsetLimitCone`: we can form a cone on the
product of `f` whose legs are the products over the finite subsets of `α`. -/
@[simps!]
def finiteSubproductsCone (f : α → C) [HasProduct f] : Cone (liftToFinsetObj (Discrete.functor f))
    where
  pt := ∏ᶜ f
  π := { app S := Pi.lift fun s => Pi.π f _ }

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