Commit 2022-07-19 01:02 fcaedc52

View on Github →

feat(algebra/module): add injective module and Baer's criterion (#12895) Baer's criterion for injective modules: if an $R$-module $M$ is such that every linear map from an ideal of $R$ to $M$ can be extended to $R\to M$, then $M$ is injective.

Estimated changes

Created src/algebra/module/injective.lean

added theorem module.Baer.chain_linear_pmap_of_chain_extension_of

added theorem module.Baer.extension_of.ext

added theorem module.Baer.extension_of.ext_iff

added theorem module.Baer.extension_of.le_max

added def module.Baer.extension_of.max

added structure module.Baer.extension_of

added def module.Baer.extension_of_max

added theorem module.Baer.extension_of_max_adjoin.eqn

added def module.Baer.extension_of_max_adjoin.extend_ideal_to

added theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_eq

added theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_is_extension

added theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_wd'

added theorem module.Baer.extension_of_max_adjoin.extend_ideal_to_wd

added def module.Baer.extension_of_max_adjoin.extension_to_fun

added theorem module.Baer.extension_of_max_adjoin.extension_to_fun_wd

added def module.Baer.extension_of_max_adjoin.fst

added def module.Baer.extension_of_max_adjoin.ideal

added def module.Baer.extension_of_max_adjoin.ideal_to

added def module.Baer.extension_of_max_adjoin.snd

added def module.Baer.extension_of_max_adjoin

added theorem module.Baer.extension_of_max_is_max

added theorem module.Baer.extension_of_max_le

added theorem module.Baer.extension_of_max_to_submodule_eq_top

added def module.Baer

added theorem module.injective_iff_injective_object

added theorem module.injective_module_of_injective_object

added theorem module.injective_object_of_injective_module

Modified src/linear_algebra/linear_pmap.lean

added theorem linear_pmap.ext_iff

Modified src/order/chain.lean

added theorem is_chain.exists3