Commit 2026-05-28 22:31 9a568f0b

View on Github →

feat(Algebra/Category): filtered colimits in AlgCat (#39145) From Proetale.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/AlgCat/Basic.lean

added theorem AlgCat.forget₂_ringCat_map

added theorem AlgCat.forget₂_ringCat_obj

modified def CategoryTheory.Iso.toAlgEquiv

modified def algEquivIsoAlgebraIso

Created Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean

deleted theorem CategoryTheory.reflectsIsomorphisms_forget₂

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

added theorem CategoryTheory.Limits.Concrete.exists_hom_ι_eq_of_isColimit