Commit 2024-10-26 23:35 608b89fc

View on Github →

chore: do not depend on CategoryTheory in Module.Injective (#17747) The category-theoretic results can be split between Mathlib/Algebra/Category/Grp/Injective.lean and Mathlib/Algebra/Category/ModuleCat/Injective.lean instead, with no changes to downstream proofs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/EnoughInjectives.lean

Modified Mathlib/Algebra/Category/Grp/Injective.lean

Created Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean

added theorem ModuleCat.enoughInjectives

Modified Mathlib/Algebra/Category/ModuleCat/Injective.lean

added theorem Module.injective_iff_injective_object

added theorem Module.injective_module_of_injective_object

added theorem Module.injective_object_of_injective_module

deleted theorem ModuleCat.enoughInjectives

Modified Mathlib/Algebra/Module/Injective.lean

deleted theorem Module.injective_iff_injective_object

deleted theorem Module.injective_module_of_injective_object

deleted theorem Module.injective_object_of_injective_module