Preservation of filtered colimits and cofiltered limits. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Typically forgetful functors from algebraic categories preserve filtered colimits (although not general colimits). See e.g.
algebra/category/Mon/filtered_colimits
.
Future work #
This could be generalised to allow diagrams in lower universes.
@[class]
structure
category_theory.limits.preserves_filtered_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ u₂ (v+1))
- preserves_filtered_colimits : Π (J : Type ?) [_inst_5 : category_theory.small_category J] [_inst_6 : category_theory.is_filtered J], category_theory.limits.preserves_colimits_of_shape J F
A functor is said to preserve filtered colimits, if it preserves all colimits of shape J
, where
J
is a filtered category.
Instances of this typeclass
- category_theory.limits.preserves_colimits.preserves_filtered_colimits
- category_theory.limits.comp_preserves_filtered_colimits
- Mon.filtered_colimits.forget_preserves_filtered_colimits
- AddMon.filtered_colimits.forget_preserves_filtered_colimits
- CommMon.filtered_colimits.forget₂_Mon_preserves_filtered_colimits
- AddCommMon.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits
- CommMon.filtered_colimits.forget_preserves_filtered_colimits
- AddCommMon.filtered_colimits.forget_preserves_filtered_colimits
- Group.filtered_colimits.forget₂_Mon_preserves_filtered_colimits
- AddGroup.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits
- Group.filtered_colimits.forget_preserves_filtered_colimits
- AddGroup.filtered_colimits.forget_preserves_filtered_colimits
- CommGroup.filtered_colimits.forget₂_Group_preserves_filtered_colimits
- AddCommGroup.filtered_colimits.forget₂_AddGroup_preserves_filtered_colimits
- CommGroup.filtered_colimits.forget_preserves_filtered_colimits
- AddCommGroup.filtered_colimits.forget_preserves_filtered_colimits
- SemiRing.filtered_colimits.forget₂_Mon_preserves_filtered_colimits
- SemiRing.filtered_colimits.forget_preserves_filtered_colimits
- CommSemiRing.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits
- CommSemiRing.filtered_colimits.forget_preserves_filtered_colimits
- Ring.filtered_colimits.forget₂_SemiRing_preserves_filtered_colimits
- Ring.filtered_colimits.forget_preserves_filtered_colimits
- CommRing.filtered_colimits.forget₂_Ring_preserves_filtered_colimits
- CommRing.filtered_colimits.forget_preserves_filtered_colimits
- Module.filtered_colimits.forget₂_AddCommGroup_preserves_filtered_colimits
- Module.filtered_colimits.forget_preserves_filtered_colimits
Instances of other typeclasses for category_theory.limits.preserves_filtered_colimits
- category_theory.limits.preserves_filtered_colimits.has_sizeof_inst
@[protected, instance]
def
category_theory.limits.preserves_colimits.preserves_filtered_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.preserves_colimits F] :
Equations
- category_theory.limits.preserves_colimits.preserves_filtered_colimits F = {preserves_filtered_colimits := infer_instance (λ (J : Type v) [_inst_5_1 : category_theory.small_category J] [_inst_6 : category_theory.is_filtered J], category_theory.limits.preserves_colimits_of_size.preserves_colimits_of_shape)}
@[protected, instance]
def
category_theory.limits.comp_preserves_filtered_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_filtered_colimits F]
[category_theory.limits.preserves_filtered_colimits G] :
Equations
- category_theory.limits.comp_preserves_filtered_colimits F G = {preserves_filtered_colimits := λ (J : Type v) (_x : category_theory.small_category J) (_x_1 : category_theory.is_filtered J), infer_instance}
@[class]
structure
category_theory.limits.preserves_cofiltered_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ u₂ (v+1))
- preserves_cofiltered_limits : Π (J : Type ?) [_inst_5 : category_theory.small_category J] [_inst_6 : category_theory.is_cofiltered J], category_theory.limits.preserves_limits_of_shape J F
A functor is said to preserve cofiltered limits, if it preserves all limits of shape J
, where
J
is a cofiltered category.
Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_cofiltered_limits
- category_theory.limits.preserves_cofiltered_limits.has_sizeof_inst
@[protected, instance]
def
category_theory.limits.preserves_limits.preserves_cofiltered_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.preserves_limits F] :
Equations
- category_theory.limits.preserves_limits.preserves_cofiltered_limits F = {preserves_cofiltered_limits := infer_instance (λ (J : Type v) [_inst_5_1 : category_theory.small_category J] [_inst_6 : category_theory.is_cofiltered J], category_theory.limits.preserves_limits_of_size.preserves_limits_of_shape)}
@[protected, instance]
def
category_theory.limits.comp_preserves_cofiltered_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_cofiltered_limits F]
[category_theory.limits.preserves_cofiltered_limits G] :
Equations
- category_theory.limits.comp_preserves_cofiltered_limits F G = {preserves_cofiltered_limits := λ (J : Type v) (_x : category_theory.small_category J) (_x_1 : category_theory.is_cofiltered J), infer_instance}