instFiniteCarrierColimitModuleCatCompForget₂

English

The carrier of the colimit in FGModuleCat obtained via forget₂ is finite-dimensional when each Z j is finite-dimensional.

Русский

Носитель полученного предела FGModuleCat через забывание ограничен конечной размерностью, если каждый Z j конечномер.

LaTeX

$$Module.Finite k (CategoryTheory.Limits.colimit (F.comp (forget₂ (FGModuleCat k) (ModuleCat k)))).carrier$$

Lean4

/-- Finite colimits of finite modules are finite, because we can realise them as quotients
of a finite coproduct. -/
instance (F : J ⥤ FGModuleCat k) :
    Module.Finite k (colimit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k)) : ModuleCat.{v} k) :=
  have (j : J) : Module.Finite k ((F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k)).obj j) := by
    change Module.Finite k (F.obj j); infer_instance
  Module.Finite.of_surjective (colimitQuotientCoproduct (F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k))).hom
    ((ModuleCat.epi_iff_surjective _).1 inferInstance)

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