Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 09:27 a574db13

View on Github →

refactor(algebra/category/*/limits): refactor concrete limits (#3463) We used to construct categorical limits for AddCommGroup and CommRing. Now we construct them for

(Add)(Comm)Mon
(Add)(Comm)Group
(Comm)(Semi)Ring
Module R
Algebra R Even better, we reuse structure along the way, and show that all the relevant forgetful functors preserve limits. We're still not at the point were this can either be done by
automation, or
noticing that everything is a model of a Lawvere theory but ... maybe one day.

Estimated changes

Created src/algebra/category/Algebra/limits.lean

added def Algebra.has_limits.limit

added def Algebra.has_limits.limit_is_limit

added def Algebra.limit_π_alg_hom

added def Algebra.sections_subalgebra

Modified src/algebra/category/CommRing/basic.lean

Modified src/algebra/category/CommRing/colimits.lean

Modified src/algebra/category/CommRing/limits.lean

deleted def CommRing.CommRing_has_limits.limit

deleted def CommRing.CommRing_has_limits.limit_is_limit

deleted def CommRing.limit_π_ring_hom

added def Ring.forget₂_AddCommGroup_preserves_limits_aux

added def SemiRing.forget₂_AddCommMon_preserves_limits_aux

added def SemiRing.forget₂_Mon_preserves_limits_aux

added def SemiRing.has_limits.limit

added def SemiRing.has_limits.limit_is_limit

added def SemiRing.limit_π_ring_hom

added def SemiRing.sections_subsemiring

Modified src/algebra/category/Group/limits.lean

deleted def AddCommGroup.AddCommGroup_has_limits.limit

deleted def AddCommGroup.AddCommGroup_has_limits.limit_is_limit

modified def AddCommGroup.kernel_iso_ker_over

deleted def AddCommGroup.limit_π_add_monoid_hom

added def CommGroup.forget₂_CommMon_preserves_limits_aux

added def Group.sections_subgroup

Modified src/algebra/category/Group/zero.lean

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

added def Module.has_limits.limit

added def Module.has_limits.limit_is_limit

added def Module.limit_π_linear_map

added def Module.sections_submodule

Modified src/algebra/category/Mon/basic.lean

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

added def Mon.has_limits.limit

added def Mon.has_limits.limit_is_limit

added def Mon.limit_π_monoid_hom

added def Mon.sections_submonoid

Modified src/algebra/module/basic.lean

added theorem linear_map.coe_inj

deleted theorem linear_map.coe_injective

Modified src/algebra/ring/pi.lean

added theorem pi.ring_hom_apply

Modified src/analysis/normed_space/operator_norm.lean

Modified src/category_theory/adjunction/limits.lean

Modified src/category_theory/concrete_category/bundled_hom.lean

Modified src/category_theory/limits/creates.lean

added def category_theory.creates_limit_of_fully_faithful_of_iso

added def category_theory.creates_limit_of_fully_faithful_of_lift

Modified src/category_theory/reflect_isomorphisms.lean

Modified src/ring_theory/algebra.lean

added theorem pi.algebra_map_apply

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.coe_inj

deleted theorem continuous_linear_map.coe_injective'