instHasProductsOfShapeOfHasCountableProductsOfCountable

English

In a concrete category, two elements of a wide pullback are equal if all their base and projections agree.

Русский

В конкретной категории два элемента широкого предела равны, если совпадают их базовые части и все проекции.

LaTeX

$$$$ x=y \\Rightarrow base f x = base f y \\land \\forall j, \\pi f j x = \\pi f j y $$ and conversely, equality follows from these data. $$$$

Lean4

instance [HasCountableProducts C] (J : Type*) [Countable J] : HasProductsOfShape J C :=
  have : Countable (Shrink.{0} J) := Countable.of_equiv _ (equivShrink.{0} J)
  have : HasLimitsOfShape (Discrete (Shrink.{0} J)) C := HasCountableProducts.out _
  hasLimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{0} J)).symm

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