instPreservesLimitsProfiniteForget₂

English

The forget₂ functor forget₂ ProfiniteGrp Profinite preserves limits: limits in ProfiniteGrp are sent to corresponding limits in Profinite.

Русский

Функтор забывания forget₂ ProfiniteGrp Profinite сохраняет пределы: пределы в ProfiniteGrp отображаются в соответствующие пределы в Profinite.

LaTeX

$$$\text{forget₂ preserves limits}$$$

Lean4

instance : Limits.PreservesLimits (forget₂ ProfiniteGrp Profinite) where
  preservesLimitsOfShape :=
    {
      preservesLimit := fun {F} ↦
        CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone (limitConeIsLimit F)
          (Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))) }

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