forget_preservesLimits — Mathlib

English

The forgetful functor from Profinite to Top preserves limits: limits computed in Profinite agree with the corresponding limits in Top under forgetting the profinite structure.

Русский

Функтор забывания из Profinite в Top сохраняет пределы: пределы в Profinite совпадают с соответствующими пределами в Top после стирания профинидной структуры.

LaTeX

$$$\\mathrm{PreservesLimits}(\\mathrm{forget}_{\\mathrm{Profinite}}).$$$

Lean4

instance forget_preservesLimits : Limits.PreservesLimits (forget Profinite) := by
  apply Limits.comp_preservesLimits Profinite.toTopCat (forget TopCat)

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