The Yoneda embedding for preadditive categories preserves limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The Yoneda embedding for preadditive categories preserves limits.

Implementation notes #

This is in a separate file to avoid having to import the development of the abelian structure on Module in the main file about the preadditive Yoneda embedding.

source

@[protected, instance]

noncomputable def category_theory.preserves_limits_preadditive_yoneda_obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X : C) :

category_theory.limits.preserves_limits (category_theory.preadditive_yoneda_obj X)

Equations

category_theory.preserves_limits_preadditive_yoneda_obj X = have this : category_theory.limits.preserves_limits (category_theory.preadditive_yoneda_obj X ⋙ category_theory.forget (Module (category_theory.End X))), from infer_instance, category_theory.limits.preserves_limits_of_reflects_of_preserves (category_theory.preadditive_yoneda_obj X) (category_theory.forget (Module (category_theory.End X))) Module.forget_reflects_limits

source

@[protected, instance]

noncomputable def category_theory.preserves_limits_preadditive_coyoneda_obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X : Cᵒᵖ) :

category_theory.limits.preserves_limits (category_theory.preadditive_coyoneda_obj X)

Equations

category_theory.preserves_limits_preadditive_coyoneda_obj X = have this : category_theory.limits.preserves_limits (category_theory.preadditive_coyoneda_obj X ⋙ category_theory.forget (Module (category_theory.End X))), from infer_instance, category_theory.limits.preserves_limits_of_reflects_of_preserves (category_theory.preadditive_coyoneda_obj X) (category_theory.forget (Module (category_theory.End X))) Module.forget_reflects_limits

source

@[protected, instance]

noncomputable def category_theory.preserves_limits_preadditive_yoneda.obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X : C) :

category_theory.limits.preserves_limits (category_theory.preadditive_yoneda.obj X)

Equations

category_theory.preserves_limits_preadditive_yoneda.obj X = show category_theory.limits.preserves_limits (category_theory.preadditive_yoneda_obj X ⋙ category_theory.forget₂ (Module (category_theory.End X)) AddCommGroup), from infer_instance

source

@[protected, instance]

noncomputable def category_theory.preserves_limits_preadditive_coyoneda.obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (X : Cᵒᵖ) :

category_theory.limits.preserves_limits (category_theory.preadditive_coyoneda.obj X)

Equations

category_theory.preserves_limits_preadditive_coyoneda.obj X = show category_theory.limits.preserves_limits (category_theory.preadditive_coyoneda_obj X ⋙ category_theory.forget₂ (Module (category_theory.End X)) AddCommGroup), from infer_instance