forget₂AddCommGroup_reflectsLimit

English

The forgetful functor forget₂ from ModuleCat to AddCommGrpCat reflects limits of shape J; i.e., a cone is a limit in ModuleCat iff its image is a limit in AddCommGrpCat.

Русский

Функтор забывания forget₂: ModuleCat → AddCommGrpCat отражает пределы формы J; то есть предельность конуса следует по образу в AddCommGrpCat.

LaTeX

$$$\\text{forget₂AddCommGroup_reflectsLimit}$$$

Lean4

instance forget₂AddCommGroup_reflectsLimit : ReflectsLimit F (forget₂ (ModuleCat.{w} R) AddCommGrpCat) where
  reflects {c}
    hc :=
    ⟨by
      have : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) := ⟨_, hc⟩
      have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
        simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using this
      have := reflectsLimit_of_reflectsIsomorphisms F (forget₂ (ModuleCat R) AddCommGrpCat)
      exact isLimitOfReflects _ hc⟩

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