forget₂ (FinVect K) (Module K) creates all finite limits. #
And hence FinVect K has all finite limits.
Future work #
After generalising FinVect to allow the ring and the module to live in different universes,
generalize this construction so we can take limits over smaller diagrams,
as is done for the other algebraic categories.
@[protected, instance]
def
FinVect.category_theory.limits.pi_obj.finite_dimensional
{k : Type v}
[field k]
{J : Type v}
[fintype J]
(Z : J → Module k)
[∀ (j : J), finite_dimensional k ↥(Z j)] :
finite_dimensional k (↥∏ λ (j : J), Z j)
@[protected, instance]
def
FinVect.category_theory.limits.limit.finite_dimensional
{J : Type v}
[category_theory.small_category J]
[category_theory.fin_category J]
{k : Type v}
[field k]
(F : J ⥤ FinVect k) :
finite_dimensional k ↥(category_theory.limits.limit (F ⋙ category_theory.forget₂ (FinVect k) (Module k)))
Finite limits of finite finite dimensional vectors spaces are finite dimensional, because we can realise them as subobjects of a finite product.
noncomputable
def
FinVect.forget₂_creates_limit
{J : Type v}
[category_theory.small_category J]
[category_theory.fin_category J]
{k : Type v}
[field k]
(F : J ⥤ FinVect k) :
The forgetful functor from FinVect k to Module k creates all finite limits.
Equations
- FinVect.forget₂_creates_limit F = category_theory.creates_limit_of_fully_faithful_of_iso ⟨category_theory.limits.limit (F ⋙ category_theory.forget₂ (FinVect k) (Module k)) _, _⟩ (category_theory.iso.refl ((category_theory.forget₂ (FinVect k) (Module k)).obj ⟨category_theory.limits.limit (F ⋙ category_theory.forget₂ (FinVect k) (Module k)) _, _⟩))
@[protected, instance]
noncomputable
def
FinVect.category_theory.forget₂.category_theory.creates_limits_of_shape
{J : Type v}
[category_theory.small_category J]
[category_theory.fin_category J]
{k : Type v}
[field k] :
Equations
@[protected, instance]
@[protected, instance]
noncomputable
def
FinVect.category_theory.forget₂.category_theory.limits.preserves_finite_limits
{k : Type v}
[field k] :
Equations
- FinVect.category_theory.forget₂.category_theory.limits.preserves_finite_limits = {preserves_finite_limits := λ (J : Type v) (_x : category_theory.small_category J) (_x_1 : category_theory.fin_category J), infer_instance}