preservesLimits — Mathlib

English

The forgetful functor from Stonean to TopCat preserves limits, since it is a right adjoint given by the Stone–Čech adjunction.

Русский

Функтор забывания из Stonean в TopCat сохраняет пределы, так как он является правым сопряжённым к adjunction Stone–Čech.

LaTeX

$$$\text{Limits.PreservesLimits}(\text{forget Stonean})$$$

Lean4

/-- The forgetful functor from Stonean spaces, being a right adjoint, preserves limits. -/
noncomputable instance preservesLimits : Limits.PreservesLimits (forget Stonean) :=
  rightAdjoint_preservesLimits stoneCechAdjunction

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