Commit 2024-07-19 02:26 819c2d46

View on Github →

feat(CategoryTheory): a sequential limit of surjections is surjective (#13507) We prove that in a concrete category whose forgetful functor preserves sequential limits, a sequential limit of surjections is surjective. Since this will be applied to LightProfinite, we provide the necessary instance to be able to apply this lemma as well.

Estimated changes

Modified Mathlib/CategoryTheory/Countable.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

modified theorem CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq

modified theorem CategoryTheory.Limits.Concrete.colimit_exists_rep

modified theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists

modified theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists

modified theorem CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit

modified theorem CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq

modified theorem CategoryTheory.Limits.Concrete.isColimit_exists_rep

modified theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists

modified theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists

modified theorem CategoryTheory.Limits.Concrete.isLimit_ext

modified theorem CategoryTheory.Limits.Concrete.limit_ext

modified theorem CategoryTheory.Limits.Concrete.small_sections_of_hasLimit

added theorem CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map

modified theorem CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit

Modified Mathlib/CategoryTheory/Limits/Types.lean

added theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map

added theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean