Commit 2024-02-28 22:21 eaf18cb1

feat : rework enough-injectiveness proof of groups using character module (#8559) For $R$-modules $M$ and $D$ where $D$ is injective, we can consider the dual module $M^\star := \mathrm{Hom}_R(M, D)$. $(\cdot^\star)$ can define a contravariant functor $R$-mod to $R$-mod by $L \mapsto L^\star$ where $L^\star f = f \circ L$ where $L \in \mathrm{Hom}_R(M, N)$ and $f \in N^\star$. This functor sends monomorphisms to epimorphisms. For an abelian group $A$, it is useful to consider its character module in the unit rational circle. This construction appears in proof of enough-injectiveness of groups and it can be shown that a module is flat if and only if its character module is injective, reference. Hence we use Baer to relate ideals. Also refactored enough-injectiveness of abelian groups. The refactor is not a separated PR because construction of character module needs some result from GroupCat/Injective.lean file.