Commit 2024-02-11 14:32 76c1f6e7

View on Github →

chore(CategoryTheory/Limits/Concrete): generalize universe assumptions (#10418) Generalizes universe assumptions for various statements on colimits in concrete categories. Also simplifies some proofs.

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Abelian.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

modified theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean