instPreservesLimitsOfShapeOppositeNatForget

English

The forgetful functor forget LightProfinite preserves limits of shape ℕᵒᵖ, i.e., inverse limits indexed by natural numbers, up to opposite.

Русский

Функтор forget LightProfinite сохраняет пределы формы ℕᵒᵖ (обратные пределы по натуральным числам).

LaTeX

$$$\text{PreservesLimitsOfShape } \mathbb{N}^{\mathrm{op}}(\text{forget LightProfinite})$$$

Lean4

instance : PreservesLimitsOfShape ℕᵒᵖ (forget LightProfinite.{u}) :=
  have : PreservesLimitsOfSize.{0, 0} (forget Profinite.{u}) := preservesLimitsOfSize_shrink _
  inferInstanceAs (PreservesLimitsOfShape ℕᵒᵖ (lightToProfinite ⋙ forget Profinite))

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