hasExactLimitsOfShape — Mathlib

English

If a category A has limits of shape J, has exact limits of shape J, and has finite colimits, then the condensed category Condensed(A) has exact limits of shape J.

Русский

Если у категории A существуют пределы формы J, пределы точны и у A есть конечные когломы, то Condensed(A) имеет точные пределы формы J.

LaTeX

$$$\\mathrm{HasExactLimitsOfShape}\\,J\\; (\\mathrm{Condensed}\\; A)$$$

Lean4

theorem hasExactLimitsOfShape [HasLimitsOfShape J A] [HasExactLimitsOfShape J A] [HasFiniteColimits A] :
    HasExactLimitsOfShape J (Condensed.{u} A) :=
  by
  let e : Condensed.{u} A ≌ Sheaf (extensiveTopology Stonean.{u}) A :=
    (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
  exact HasExactLimitsOfShape.domain_of_functor _ e.functor

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