Commit 2025-07-03 01:23 44ec04b3

View on Github →

feat(Algebra/Category): category of f.g. algebras is essentially small (#26634) Co-authored by: Andrew Yang the.erd.one@gmail.com

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

added def ULift.algEquiv

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

added def CategoryTheory.CommAlgCat.fullyFaithfulUliftFunctor

added def CategoryTheory.CommAlgCat.uliftFunctor

Created Mathlib/Algebra/Category/CommAlgCat/FiniteType.lean

added theorem Algebra.FiniteType.exists_fgAlgCatSkeleton

added def FGAlgCat.equivUnder

added def FGAlgCat.fullyFaithfulUliftFunctor

added def FGAlgCat.uliftFunctor

added structure FGAlgCatSkeleton

added theorem essentiallySmall_of_le

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added def CategoryTheory.MorphismProperty.Comma.changeProp

added def CategoryTheory.MorphismProperty.Comma.fullyFaithfulChangeProp