Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-01 07:48 4a758765

View on Github →

feat(category_theory/limits/concrete_category): Some lemmas about limits in concrete categories (#8130) Generalizes some lemmas from LTE. See zulip discussion here.

Estimated changes

Modified src/category_theory/limits/concrete_category.lean

added theorem category_theory.limits.concrete.colimit_exists_rep

added theorem category_theory.limits.concrete.from_union_surjective_of_is_colimit

added theorem category_theory.limits.concrete.is_colimit_exists_rep

added theorem category_theory.limits.concrete.is_limit_ext

added theorem category_theory.limits.concrete.limit_ext

added theorem category_theory.limits.concrete.to_product_injective_of_is_limit

added theorem category_theory.limits.concrete.wide_pullback_ext'

added theorem category_theory.limits.concrete.wide_pullback_ext

added theorem category_theory.limits.concrete.wide_pushout_exists_rep'

added theorem category_theory.limits.concrete.wide_pushout_exists_rep

Modified src/topology/category/Profinite/default.lean