hasLimitsOfShape_discrete — Mathlib

English

If a category has finite coproducts, then it has limits of shape Discrete ι for any finite ι.

Русский

Если в категории существуют конечные копроизведения, то существуют пределы формы Discrete ι для любого конечного ι.

LaTeX

$$$[\text{HasFiniteCoproducts } C] \Rightarrow \operatorname{HasLimitsOfShape}(\mathrm{Discrete}\, \iota) C$ for finite ι$$

Lean4

instance hasLimitsOfShape_discrete [HasFiniteProducts C] (ι : Type w) [Finite ι] : HasLimitsOfShape (Discrete ι) C :=
  by
  rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
  haveI : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
  exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

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