forget₂Group_preservesLimit — Mathlib

English

The forgetful functor Forget₂ from CommGrpCat to GrpCat preserves limits of any shape F.

Русский

Забывающий функтор Forget₂ из CommGrpCat в GrpCat сохраняет пределы любой формы F.

LaTeX

$$$ \mathrm{PreservesLimit}(F, \mathrm{forget₂ CommGrpCat GrpCat}) $$$

Lean4

@[to_additive]
instance forget₂Group_preservesLimit : PreservesLimit F (forget₂ CommGrpCat.{u} GrpCat.{u}) where
  preserves {c}
    hc :=
    ⟨by
      have : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat) :=
        by
        rw [GrpCat.hasLimit_iff_small_sections]
        change Small.{u} (F ⋙ forget CommGrpCat).sections
        rw [← CommGrpCat.hasLimit_iff_small_sections]
        exact ⟨_, hc⟩
      exact isLimitOfPreserves _ hc⟩

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