Commit 2025-06-02 13:05 47ea1827

View on Github →

feat(Algebra): The category of fin. gen. modules is essentially small (#25249)

Estimated changes

Modified Mathlib.lean

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

modified def FGModuleCat.carrier

added def FGModuleCat.fullyFaithfulULift

modified theorem FGModuleCat.hom_comp

modified theorem FGModuleCat.hom_ext

modified theorem FGModuleCat.hom_id

modified def FGModuleCat.isoToLinearEquiv

modified theorem FGModuleCat.obj_carrier

modified theorem FGModuleCat.of_carrier

added def FGModuleCat.ulift

modified def ModuleCat.isFG

modified theorem ModuleCat.isFG_iff

Created Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean

added def FGModuleRepr.embed

added def FGModuleRepr.repr

added structure FGModuleRepr

Modified Mathlib/Algebra/Category/FGModuleCat/Limits.lean

Modified Mathlib/CategoryTheory/EssentiallySmall.lean

added theorem CategoryTheory.essentiallySmall_of_fully_faithful

Modified Mathlib/CategoryTheory/Skeletal.lean

added theorem CategoryTheory.Functor.mapSkeleton_injective

Modified Mathlib/RepresentationTheory/FDRep.lean

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean

added theorem Module.Finite.exists_fin_quot_equiv