Commit 2021-09-22 15:37 dc5a3db9

View on Github →

feat(algebra/category): Forgetful functors preserve filtered colimits (#9101) Shows that forgetful functors of various algebraic categories preserve filtered colimits.

Estimated changes

Created src/algebra/category/CommRing/filtered_colimits.lean

added def CommRing.filtered_colimits.R

added def CommRing.filtered_colimits.colimit

added def CommRing.filtered_colimits.colimit_cocone

added def CommRing.filtered_colimits.colimit_cocone_is_colimit

added def CommSemiRing.filtered_colimits.R

added def CommSemiRing.filtered_colimits.colimit

added def CommSemiRing.filtered_colimits.colimit_cocone

added def CommSemiRing.filtered_colimits.colimit_cocone_is_colimit

added def Ring.filtered_colimits.R

added def Ring.filtered_colimits.colimit

added def Ring.filtered_colimits.colimit_cocone

added def Ring.filtered_colimits.colimit_cocone_is_colimit

added def SemiRing.filtered_colimits.R

added def SemiRing.filtered_colimits.colimit

added def SemiRing.filtered_colimits.colimit_cocone

added def SemiRing.filtered_colimits.colimit_cocone_is_colimit

Created src/algebra/category/Group/filtered_colimits.lean

added def CommGroup.filtered_colimits.G

added def CommGroup.filtered_colimits.colimit

added def CommGroup.filtered_colimits.colimit_cocone

added def CommGroup.filtered_colimits.colimit_cocone_is_colimit

added def Group.filtered_colimits.G.mk

added theorem Group.filtered_colimits.G.mk_eq

added def Group.filtered_colimits.G

added def Group.filtered_colimits.colimit

added def Group.filtered_colimits.colimit_cocone

added def Group.filtered_colimits.colimit_cocone_is_colimit

added def Group.filtered_colimits.colimit_inv_aux

added theorem Group.filtered_colimits.colimit_inv_aux_eq_of_rel

added theorem Group.filtered_colimits.colimit_inv_mk_eq

Created src/algebra/category/Module/filtered_colimits.lean

added def Module.filtered_colimits.M.mk

added theorem Module.filtered_colimits.M.mk_eq

added def Module.filtered_colimits.M

added def Module.filtered_colimits.cocone_morphism

added def Module.filtered_colimits.colimit

added def Module.filtered_colimits.colimit_cocone

added def Module.filtered_colimits.colimit_cocone_is_colimit

added def Module.filtered_colimits.colimit_desc

added def Module.filtered_colimits.colimit_smul_aux

added theorem Module.filtered_colimits.colimit_smul_aux_eq_of_rel

added theorem Module.filtered_colimits.colimit_smul_mk_eq

Created src/algebra/category/Mon/filtered_colimits.lean

added def CommMon.filtered_colimits.M

added def CommMon.filtered_colimits.colimit

added def CommMon.filtered_colimits.colimit_cocone

added def CommMon.filtered_colimits.colimit_cocone_is_colimit

added def Mon.filtered_colimits.M.mk

added theorem Mon.filtered_colimits.M.mk_eq

added def Mon.filtered_colimits.M

added def Mon.filtered_colimits.cocone_morphism

added theorem Mon.filtered_colimits.cocone_naturality

added def Mon.filtered_colimits.colimit

added def Mon.filtered_colimits.colimit_cocone

added def Mon.filtered_colimits.colimit_cocone_is_colimit

added def Mon.filtered_colimits.colimit_desc

added def Mon.filtered_colimits.colimit_mul_aux

added theorem Mon.filtered_colimits.colimit_mul_aux_eq_of_rel_left

added theorem Mon.filtered_colimits.colimit_mul_aux_eq_of_rel_right

added theorem Mon.filtered_colimits.colimit_mul_mk_eq

added theorem Mon.filtered_colimits.colimit_one_eq

Modified src/category_theory/filtered.lean

Created src/category_theory/limits/preserves/filtered.lean