forget₂CreatesLimit — Mathlib

English

The forgetful functor from FGModuleCat(k) to ModuleCat(k) creates limits of shape J.

Русский

Забывающая функция из FGModuleCat(k) в ModuleCat(k) создает пределы формы J.

LaTeX

$$$\operatorname{forget}_2\text{ CreatesLimit } F$$$

Lean4

/-- The forgetful functor from `FGModuleCat k` to `ModuleCat k` creates all finite limits. -/
def forget₂CreatesLimit (F : J ⥤ FGModuleCat k) : CreatesLimit F (forget₂ (FGModuleCat k) (ModuleCat.{v} k)) :=
  createsLimitOfFullyFaithfulOfIso
    ⟨(limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k)) : ModuleCat.{v} k), by rw [ModuleCat.isFG_iff];
      infer_instance⟩
    (Iso.refl _)

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