feat(Algebra/Category/Grp/Ulift): some properties of the universe lift functor for groups.#19968

Open

smorel394 wants to merge 16 commits intomasterfrom SM.uliftPreservesLimits

+137

Commits on Dec 14, 2024

initial commit
morel
committed
initial commit
morel
committed
added doc strings
morel
committed
initial commit
morel
committed
remove superfluous imports
morel
committed
minimize more imports
morel
committed
initial commit
morel
committed
added line to mathlib.lean
morel
committed
added creation of small limits
morel
committed
forget the copyright...
morel
committed

Commits on Dec 16, 2024

remove lines
morel
committed
Merge remote-tracking branch 'origin/master' into SM.uliftPreservesLimits
morel
committed

Commits on Dec 25, 2024

Merge remote-tracking branch 'origin' into SM.uliftPreservesLimits
morel
committed
start with fully faithful
morel
committed
Update Mathlib/Algebra/Category/Grp/Ulift.lean

smorel394
and
joelriou
authored
two isLimitOfReflects uses
morel
committed