instPreservesFiniteProductsOppositeCompHausVal

English

A condensed object X preserves finite products: the functor associated to X preserves finite products in the sense of category theory.

Русский

У конденсированного объекта X сохраняются конечные произведения: сопряжённый к нему функтор сохраняет конечные произведения в смысле теории категорий.

LaTeX

$$$$\mathrm{PreservesFiniteProducts}(X).$$$$

Lean4

/-- A condensed object preserves finite products. -/
noncomputable instance (X : Condensed A) : PreservesFiniteProducts X.val :=
  isSheaf_iff_preservesFiniteProducts_and_equalizerCondition X.val |>.mp X.cond |>.1

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