forgetToScheme_preservesLimits — Mathlib

English

The forgetful functor forgetToScheme preserves limits.

Русский

Функтор forgetToScheme сохраняет пределы.

LaTeX

$$$$ \text{PreservesLimits}(\text{forgetToScheme}). $$$$

Lean4

noncomputable instance forgetToScheme_preservesLimits : PreservesLimits forgetToScheme :=
  by
  apply (config := { allowSynthFailures := true })
    @preservesLimits_of_natIso _ _ _ _ _ _ (Functor.isoWhiskerRight equivCommRingCat.unitIso forgetToScheme).symm
  change PreservesLimits (equivCommRingCat.functor ⋙ Scheme.Spec)
  infer_instance

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